Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>You can represent programs as a set of Horn clauses. For your program you can represent it as follows:</p> <pre><code> (set-logic HORN) (set-option :fixedpoint.engine bmc) (declare-fun L0 (Bool Bool) Bool) (declare-fun L1 (Bool Bool) Bool) (declare-fun L2 (Bool Bool) Bool) (declare-fun L3 (Bool Bool) Bool) (assert (forall ((x Bool) (y Bool)) (L0 x y))) ; all values of x,y are possible at L0 (assert (forall ((x Bool) (y Bool)) (=&gt; (L0 x y) (L1 x y)))) ; from L0 move to L1 without changing x, y (assert (forall ((x Bool) (y Bool) (x1 Bool) (y1 Bool)) (=&gt; (and (not x) (L1 x y) (= x1 (or x y)) (= y1 (and x1 y))) (L1 x1 y1)))); assignment in while loop (assert (forall ((x Bool) (y Bool)) (=&gt; (and x (L1 x y)) (L2 x y)))) ; exit while loop (assert (forall ((x Bool) (y Bool)) (=&gt; (L2 x y) (L3 x (or x y))))) ; assignment after while loop (assert (forall ((x Bool) (y Bool)) (=&gt; (L3 true true) false))) ; say x = true, y = true is unreachable. (check-sat) </code></pre> <p>I have added a last assertion to make a reachability statement. I have also instructed Z3 to use a BMC engine to unfold the Horn clauses using bounded model checking. Other engines are available as well, for the example the PDR/IC3 engine (set-option :fixedpoint.engine pdr), does not unfold transition relations.</p> <p>Now the meaning of reachability vs. satisfiability is going to be different for Horn clauses, as compared to a conjunction of the unfolded transition relation: the above clauses are UNSAT. This does in fact correspond to a feasible path from L0 to (L3 true true). If you change the last statement to (L3 true false), you get the answer "sat" (The BMC problem is UNSAT). While BMC itself would not terminate on with such a loop, it turns out that the last transition and loop exit condition are enough to prune out the possibility of (L3 true false) so Z3 solves this problem by pre-processing the horn clauses.</p> <p>You can of course also write down the transition relation for the program statements you have and unfold this directly yourself into a logical formula that you check satisfiability of.</p>
    singulars
    1. This table or related slice is empty.
    1. POProgram satisfiability using Z3
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USNikolaj Bjorner
    1. USNikolaj Bjorner
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COHey Nikolaj, thanks a lot for the reply! How can I check the satisfiability of this program for a given set of values of the Boolean variables x, y?
      singulars
      1. PO
      1. USJoyel
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload