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

我正在尝试在 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，但不确定如何修复它)

请您参考如下方法:

你怎么看这个:

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