0

我仍在努力解决寻找a价值的问题，以便a * b == b所有价值都达到b. 预期的结果是a == 1。我有以下两种解决方案。

（A）我ForAll在下面的代码中用量词实现了这个（如果有解决方案而不使用任何量词，请纠正我）。这个想法是证明f和g是等价的。

from z3 import *

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

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

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

s = Solver()
s.add(ForAll([b, tmp1, a1], f == g))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

但是，这个简单的代码会永远运行而不会返回结果。我认为这是因为ForAll. 关于如何解决问题的任何想法？

(B) 我用另一个版本再次尝试。这次我不证明两个公式是等价的，而是把它们都放在一个公式f中。从逻辑上讲，我认为这是真的，但如果我在这里错了，请纠正我：

from z3 import *

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

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

s = Solver()
s.add(ForAll([b, a1], f))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

这次代码没有挂起，而是立即返回“Unsat”。关于如何解决这个问题的任何想法？

非常感谢。

4

1 回答 1

1

您的问题的直接表述提供了您所期望的答案：http ://rise4fun.com/Z3Py/N07sW

您建议的版本使用辅助变量 a1、tmp、tmp1，并且您对这些变量使用通用量化。这不符合您想要的公式。

于 2013-06-19T07:04:46.860 回答