z3 - Z3Python: ForAll が原因でコードがハングアップしたり、Unsat が返されたりするのはなぜですか?

Question

私はまだa値を見つける問題に苦労しているのでa * b == b、b. 期待される結果はa == 1です。以下に2つの解決策があります。

(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) 別のバージョンで再試行しました。今回は、2 つの式が等しいことを証明しませんが、すべてを 1 つの式にまとめます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」を返します。これを修正する方法について何か考えはありますか?

どうもありがとう。