z3 - いくつかの条件下で 2 つの式が等しいことを証明しますか?

Question

a1 == a + bの場合、 との 2 つの式a1 == bは等価ですa == 0。a == 0この必須条件( )をZ3 pythonで見つけたい。以下のコードを書きました。

from z3 import *

def equivalence(F, G):
    s = Solver()
    s.add(Not(F == G))
    r = s.check()
    if r == unsat:
        print 'Equ'
        print s.model()
    else:
        print 'Not Equ'

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

g = True
tmp = BitVec('tmp', 32)
g = And(g, tmp == a)
tmp1 = BitVec('tmp1', 32)
g = And(g, tmp1 == b)
tmp2 = BitVec('tmp2', 32)
g = And(g, tmp2 == (tmp1 + tmp))
a1 = BitVec('a1', 32) 
g = And(g, a1 == tmp2)

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

equivalence(Exists([a], g), f)

ただし、上記のコードは常に"Not Equ"出力として返されます。それから明らかに、モデル ( a === 0) を条件として取得することも、同等にする"f"こともできません。"g"

コードのどこが間違っているのか、それを修正する方法について何か考えはありますか? 本当にありがとう！

Answer 1

投稿のコードは、尋ねられた質問に対応していません。同様の質問が smt-lib メーリング リストで尋ねられ、回答されました。