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

Question

我正在尝试在 上使用ForAll量词，因此每个b公式都会给我结果。我在下面的代码（Z3 python）中实现了这个：a * b == bba == 1

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'

我希望 Z3a = 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

Answer 2

您要求 Z3 （除其他外）为 b 的所有值找到一个等于b的单个a1。这是不可能的。您的问题不在于 Z3，而在于基本逻辑。

Answer 3

你怎么看待这件事：

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

a1 = a*b
a2 = b


s = Solver()
s.add(ForAll(b, a1 == a2))

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

输出：

a = 1

另一种方式：

a, b = BitVecs('a b', 32)
a1 = a*b
a2 = b
f = True
f = And(f, a1 == a2)


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

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

输出：

a = 1

Answer 4

如果你只是想验证a * b == b所有可能的公式b。您可以使用以下代码。

from z3 import *

a, b = BitVecs('a b', 32)
s = Solver()
s.add(ForAll(b, a * b == b))

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

此代码在眨眼间运行，但您的代码使求解器过载并且需要相对较长的时间才能完成。