为什么此代码返回 Unsat(使用 ForAll & Implies 的公式)? [英] Why this code returns Unsat (formula using ForAll & Implies)?
问题描述
给定2个方程c == a + 4和t == c + b，如果a == -4，则<代码>t == b.我正在尝试做相反的事情，这意味着 给定以上 2 个等式和 t == b，我尝试找到 a 的值.
Given 2 equations c == a + 4 and t == c + b, if a == -4, then t == b. I am trying to do the opposite, meaning given the above 2 equations, and t == b, I try to find value of a.
我有以下代码可以使用 ForAll 和 Implies:
I have below code to do this with ForAll and Implies:
from z3 import *
a, b, c, t = BitVecs('a b c t', 32)
g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))
s = Solver()
s.add(ForAll([c, t, b], Implies(g, t == b)))
if s.check() == sat:
print s.model()[a]
else:
print 'Unsat'
但是，运行上述代码会返回Unsat.我希望这会返回 -4(或 0xfffffffc)，所以很困惑.
However, running the above code returns Unsat. I expect this returns -4 (or 0xfffffffc), so pretty confused.
知道我哪里错了吗?
谢谢！
推荐答案
您编写的公式与问题的文字描述不符.特别是，您使用的含义并不能确保 t == b 必须为真才能满足公式.
The formulas you wrote don't correspond to the textual description of your problem. In particular, the implication you used does not ensure t == b must be true for the formulas to be satisfiable.
根据您的问题的文字描述，如果 t == b 为真，那么这意味着 t == c + b 为真的唯一方法是如果c == 0.由于c == 0，那么c == a + 4 为真的唯一方法是如果a == -4 符合要求.t 和 b 的赋值是任意的.
Based on the textual description of your problem, if t == b is true, then this means the only way t == c + b is true is if c == 0. Since c == 0, then the only way c == a + 4 is true is if a == -4 as desired. The assignments to t and b are arbitrary.
这里有两种编码方式.在第一种情况下，z3 将 0 分配给 t 和 b，因为它们都是隐式存在量化的.在第二种情况下，我在 b 和 t 上使用了全称量词来强调分配是任意的.根据刚才所述的讨论(因为 c == 0 必须为真)，对于 c 的任意选择，公式不能满足，所以 c> 不应被普遍量化.以下说明了这一点(http://rise4fun.com/Z3Py/uGEV):
Here are two ways to encode this. In the first case, z3 assigns 0 to t and b both as they are implicitly existentially quantified. In the second case, I've used a universal quantifier over b and t to highlight that the assignment is arbitrary. The formulas cannot be satisfiable for an arbitrary choice of c based on the discussion just stated (since c == 0 must be true), so c should not be universally quantified. The following illustrates this (http://rise4fun.com/Z3Py/uGEV ):
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]
更新根据下面的评论，我希望这个例子能帮助你理解为什么你需要 Implies(t == b, g) 而不是 Implies(g, t == b)代码>(带有 z3py 链接:http://rise4fun.com/Z3Py/pl80I):
Update
Based on the comments, below, I hope this example will help to see why you need Implies(t == b, g) instead of Implies(g, t == b) (with z3py link: http://rise4fun.com/Z3Py/pl80I ):
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
这篇关于为什么此代码返回 Unsat(使用 ForAll & Implies 的公式)?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
