Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <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>
    singulars
    1. This table or related slice is empty.
    1. POWhy this code returns Unsat (formula using ForAll & Implies)?
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USTaylor
    1. USTaylor
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POWhy this code returns Unsat (formula using ForAll & Implies)?
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTAcceptedByOriginator
    1. COThanks a lot, Taylor! I have few concerns: (1) Your first encode doesnt seem right to me, because if Z3 happens to give another value of `a`, the next part (trying to add opposite condition) would not work. (2) Why in the second encode you had `Implies(t==b, g)`, but not `Implies(g, t==b)`? (3) In more generalized problems, is there any way for us to know which variables (like `c` in this case) should not be universally qualified? I mean how to decide this with computation? Thanks a lot!
      singulars
      1. PO
      1. USuser311703
    2. CO(1) Adding the negation was just done to illustrate the code did what you wanted (assigned the right value to `a`). Of course, if you change the assertions, then a different value might be assigned, and this would fail. You can remove this without changing anything. (2) The way I wrote it is the correct way to encode your textual description that `t == b` holds. (3) As far as an algorithmic way, I'm not sure. I'd first try `solve`, then reason about which variables are assigned arbitrarily. There is probably some relationship to boolean 'don't cares' that someone else might comment on.
      singulars
      1. PO
      1. USTaylor
    3. COTaylor, on (2) above: actually both `g` and `t==b` hold, so IMHO it is possible to have `Implies(g, t==b)` as well. However, when I replaced `Implies(t==b, g)` with `Implies(g, t==b)`, the returned value of `a` is **0**, not **-4** anymore. This is pretty confused to me. Any idea why this happens? Thanks!
      singulars
      1. PO
      1. USuser311703
 

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