python - 代码使用 ForAll 产生错误结果，为什么？

Question

我正在尝试在 b 上使用 ForAll 量词，因此公式 a * b == b 与每个 b 会给我 a == 1 作为结果。我在下面的代码中实现了这个(Z3 python):

from z3 import *

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

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

s = Solver()
s.add(ForAll(b, f))

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

我希望 Z3 在输出中给我 a = 1，但我得到的是 Unsat。知道问题出在哪里吗？

(我怀疑我没有正确使用 ForAll，但不确定如何修复它)

Answer 1

你怎么看这个:

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

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

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

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

输出:

a = 1

其他形式:

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

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

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

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

输出:

a = 1