1

Z3py の Exists 関数を別の変数と数式で呼び出すと、まったく同じ結果が得られます。それはある種のPythonの問題ですか、それともZ3がここで壊れていますか? 直し方？次の最小限の例は、問題を示しています。

from z3 import *
a, a0, a1, b, b0, b1 = Ints('a a0 a1 b b0 b1')
x, y = Bools('x y')
s = Solver()
formula = Implies(x, And(a>0,b1<0))
substitution1 = substitute(formula,(a1,a0),(b1,b0))
substitution2 = substitute(formula,(a1,a0),(b1,b0),(a,a1),(b,b1))
print substitution1
print substitution2
exist1 = Exists([a,b],substitution1)
exist2 = Exists([a1,b1],substitution2)
print exist1
print exist2

出力：

Implies(x, And(a > 0, b0 < 0))
Implies(x, And(a1 > 0, b0 < 0))
Exists([a, b], Implies(x, And(a > 0, b0 < 0)))
Exists([a, b], Implies(x, And(a > 0, b0 < 0)))
4

1 に答える 1

0

ご報告いただきありがとうございます。実際、Z3 はこれについて正しいのですが、出力がわかりにくいです。内部的には、Z3 は deBrujin インデックスを使用し、バインドされた変数の名前は重要ではありません。同じ本体 (およびパターン、no_patterns など) を持つ量指定子が作成されると、前と同じ量化された制約を解決する必要がないように、前に見たのとまったく同じ式が使用されます。これにより、バインドされた変数の名前が突然変更されたように見えるため、混乱する状況が生じます。

ここに示した例では、両方の量指定子の本体はまったく同一であり、変数の名前は重要ではありません。Z3 はこれらの変数に任意の名前を使用できますが、量指定子が最初に作成されたときに使用された名前を使用することを選択します。たとえば、追加することにより、それを無効にすることができます

compare_arrays(to_quantifier(n1)->get_decl_names(),
               to_quantifier(n2)->get_decl_names(),
               to_quantifier(n1)->get_num_decls()) &&

src/ast/ast.cpp:470 にあります。ただし、これは一部のベンチマークで Z3 のパフォーマンスに悪影響を及ぼす可能性があるため、この変更は行いません。使用したい場合は、もちろん Z3 のローカル コピーに追加できます。

于 2014-05-29T13:43:17.883 に答える