StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>The formulas you wrote don't correspond to the textual description of your problem. In particular, the implication you used does not ensure <code>t == b</code> must be true for the formulas to be satisfiable.</p> <p>Based on the textual description of your problem, if <code>t == b</code> is true, then this means the only way <code>t == c + b</code> is true is if <code>c == 0</code>. Since <code>c == 0</code>, then the only way <code>c == a + 4</code> is true is if <code>a == -4</code> as desired. The assignments to <code>t</code> and <code>b</code> are arbitrary.</p> <p>Here are two ways to encode this. In the first case, z3 assigns <code>0</code> to <code>t</code> and <code>b</code> both as they are implicitly existentially quantified. In the second case, I've used a universal quantifier over <code>b</code> and <code>t</code> to highlight that the assignment is arbitrary. The formulas cannot be satisfiable for an arbitrary choice of <code>c</code> based on the discussion just stated (since <code>c == 0</code> must be true), so <code>c</code> should not be universally quantified. The following illustrates this (<a href="http://rise4fun.com/Z3Py/uGEV" rel="nofollow">http://rise4fun.com/Z3Py/uGEV</a> ):</p> <pre><code>a, b, c, t = BitVecs('a b c t', 32) g = True g = And(g, c == (a + 4)) g = And(g, t == (c + b)) g = And(g, t == b) s = Solver() s.add(g) s.check() print s.model() ma = s.model()[a] s = Solver() s.add(Not(ma == 0xfffffffc)) print s.check() # unsat, proves ma is -4 solve(g) # alternatively, just solve the equations # illustrate that the assignments to t and b are arbitrary s = Solver() g = True g = And(g, c == (a + 4)) g = And(g, t == (c + b)) g = ForAll([t, b], Implies(t == b, g)) s.add(g) s.check() print s.model() ma = s.model()[a] </code></pre> <p><strong>Update</strong> Based on the comments, below, I hope this example will help to see why you need <code>Implies(t == b, g)</code> instead of <code>Implies(g, t == b)</code> (with z3py link: <a href="http://rise4fun.com/Z3Py/pl80I" rel="nofollow">http://rise4fun.com/Z3Py/pl80I</a> ):</p> <pre><code>p1, p2 = BitVecs('p1 p2', 4) solve(Implies(p1 == 1, p2 == 2)) # gives p1 = 14, p2 = 13 solve(And(p1 == 0, Implies(p1 == 1, p2 == 2))) # gives p1 = 0, p2 unassigned solve(And(p1 == 0, p1 == 1)) # no solution to illustrate that p1 can only be 0 or 1 in previous, but would be unsat is trying to assign both solve(ForAll([p1], Implies(p1 == 1, p2 == 2))) # gives p2 == 2 solve(ForAll([p1], Implies(p2 == 2, p1 == 1))) # gives p2 = 0 and does not ensure p1 == 1 is true since the formula is satisfiable by picking p2 != 2 </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

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