5

私はまだ Z3 を使い始めたばかりで、質問があります。Z3 を使用して同等性チェックを行うことは可能ですか?

可能であれば、2 つの数式の等価性をチェックする例を 1 つ挙げていただけますか?

ありがとう。

4

1 に答える 1

15

はい、可能です。Z3を使用してそれを達成するための多くのものがあります。最も単純なものは、proveZ3PythonAPIの手順を使用します。たとえば、式x >= 1 and x == 2*yとx - 2*y == 0, x >= 2が同等であることを示したいとします。次のPythonプログラムを使用してこれを行うことができます（rise4funでオンラインで試すことができます）。

x, y = Ints('x y')
F = And(x >= 1, x == 2*y)
G = And(2*y - x == 0, x >= 2)
prove(F == G)

また、2つの式がいくつかのサイドコンディションを法として等価であることを示すこともできます。たとえば、ビットベクトル（つまり、マシン整数）の場合、if （オンラインで も利用可能）x / 2と同等です。x >> 1x >= 0

x = BitVec('x', 32)
prove(Implies(x >= 0, x / 2 == x >> 1))

x / 2は、と同等ではないことに注意してくださいx >> 1。Z3は、それを証明しようとすると反例を生み出します。

x = BitVec('x', 32)
prove(x / 2 == x >> 1)
>> counterexample
>> [x = 4294967295]

Z3 Pythonチュートリアルには、より複雑な例が含まれています。これは、が2の累乗である場合にのみ真であることを示していますx != 0 and x & (x - 1) == 0。x

一般に、充足可能性チェッカーは、2つの式が同等であることを示すために使用できます。2つの式がZ3を使用FしGて同等であることを示すために、それが満足できないことを示します（つまり、と異なるF != G割り当て/解釈はありません）。これが、コマンドがZ3PythonAPIで実装される方法です。ソルバーAPIに基づくスクリプトは次のとおりです。FGprove

s = Solver()
s.add(Not(F == G))
r = s.check()
if r == unsat:
    print("proved")
else:
    print("counterexample")
    print(s.model())
于 2012-12-18T15:11:31.047 に答える