0

给定 2 个方程c == a + 4和t == c + b，如果a == -4，则t == b。我试图做相反的事情，这意味着给定上述 2 个等式，并且t == b，我试图找到 的值a。

我有以下代码可以使用ForAll和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），所以很困惑。

知道我哪里错了吗？

谢谢！

4

1 回答 1

3

您编写的公式与问题的文字描述不符。特别是，您使用的含义并不能确保t == b公式必须为真才能满足。

根据您的问题的文字描述，如果t == b是真的，那么这意味着唯一的方法t == c + b是如果是真的c == 0。既然c == 0，那么唯一的方法c == a + 4是如果a == -4需要的话。分配给t和b是任意的。

这里有两种编码方式。在第一种情况下，z3 分配0给t和b两者，因为它们是隐式存在量化的。在第二种情况下，我使用了一个通用量词b来t强调分配是任意的。这些公式不能满足c基于刚刚陈述的讨论的任意选择（因为c == 0必须是真的），所以c不应该被普遍量化。以下说明了这一点（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 ）：

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
于 2013-06-25T13:44:45.210 回答