Z3 Python：For All 导致我的代码挂起，或者返回 Unsat，为什么？

Question

我仍在努力解决查找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”。关于如何解决这个问题的任何想法？

非常感谢。

Answer 1

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

您建议的版本使用辅助变量 a1、tmp、tmp1 和您 对这些变量使用通用量化。这不对应 到你想要的公式。