2

Z3 python で 2 つの式 'f' と 'g' の同等性を証明したい。以下のコードでは、基本的に「g」は「f」にランダムなコードが追加されています。Exists 修飾子を使用して 'g' のすべてのランダム コードを無視したので、'f' と 'g' は実際には同等です。

MI = BitVecSort(32)
MV = BitVecSort(8)
Mem = Array('Mem', MI, MV)

def equivalence(F, G):
    s = Solver()
    s.add(Not(F == G))
    if s.check() == unsat:
        print "Equivalence"
    else:
        print "Inequivalence"

def Select2(M, I): 
    return Concat(Select(M, I+1), Select(M, I))

x, y = BitVecs('x y', 32)

g = True
t = BitVec('t', 32)
g = And(g, t == y)
t2 = BitVec('t2', 16)
g = And(g, t2 == Select2(Mem, t))
t3 = BitVec('t3', 32)
g = And(g, t3 == (t + 2))
y1 = BitVec('y1', 32)
g = And(g, y1 == t)
x1 = BitVec('x1', 32)
g = And(g, x1 == 0)

f = True
x1 = BitVec('x1', 32)
f = And(f, x1 == 0)

equivalence(Exists([t3, t2, t, y, y1, x], g), f)

しかし、このスクリプトは、期待される「同等」ではなく「不同等」を返します。実際、詳しく見ると、同等の s.check() は「不明」を返します。

Z3 ならこの些細な問題を簡単に解決できると思っていたのですが、Z3 はここで何か間違ったことをしているようです。何か案が？

どうもありがとう。

4

1 に答える 1

2

あなたunknownは数量詞のために得ます。量指定子の消去を適用することで、期待される答えを得ることができます。とソルバーを使用するソルバーを作成できqeますsmt。交換するしかない

   s = Solver()

と

   s = Then('qe', 'smt').solver()

Thenはコンビネータであり、適用する戦術を構築しqe(量指定子の除去)、汎用の SMT ソルバーを呼び出しますsmt。このメソッド.solver()は、戦術をソルバーに変換します。

ここでテストできます。

于 2013-04-11T16:35:23.693 に答える