0

我发布了一个相关的问题，但后来我认为它不是很清楚。我想改写这样的问题：

如果 ，则两个公式a1 == a + b(1) 和a1 == b(2) 等价a == 0。给定这些公式 (1) 和 (2)，我如何使用 Z3 python 找出这个所需的条件 ( a == 0)，以便上述公式变得等价？

我想a1,a并且b都是BitVecs(32).

编辑：我想出了这样的代码：

from z3 import *

a, b = BitVecs('a b', 32)
a1 = BitVec('a1', 32)
s = Solver()
s.add(ForAll(b, a + b == b))
if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Not Equ'

输出是：a = 0，正如预期的那样。

但是，当我稍微修改代码以使用两个公式时，它不再起作用：

from z3 import *

a, b = BitVecs('a b', 32)
a1 = BitVec('a1', 32)

f = True
f = And(f, a1 == a * b)

g = True
g = And(g, a1 == b)

s = Solver()
s.add(ForAll(b, f == g))
if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Not Equ'

现在的输出不同了：a = 1314914305

所以问题是：

（1）为什么第二个代码会产生不同（错误）的结果？

(2) 有没有办法在不使用 ForAll （或量词）的情况下做到这一点？

谢谢

4

1 回答 1

0

这两个代码产生相同的正确答案 a = 0。你有一个错字：你正在写 a1 = a*b 并且它必须是 a1 = a + b 。你同意吗？

不使用 ForAll 的可能代码：

a, b = BitVecs('a b', 32)
a1 = BitVec('a1', 32)
s = Solver()
s.add(a + b == b)
if s.check() == sat:
print 'a =', s.model()[a]
else:
print 'Not Equ'
s1 = Solver()
s1.add(a==0, Not(a + b == b))
print s1.check()

输出：

a = 0
unsat
于 2013-06-15T13:27:13.560 回答