ForAll代码产生错误结果，为什么？

Question

我正在尝试在ForAll上使用b量词，因此将公式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

Answer 2

您对此有何看法：

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 3

您正在让Z3（除其他事项外）找到一个a1，它对于b的所有值都等于b。这是不可能的。您的问题不是Z3，而是基本逻辑。

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'

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