6

でバインドされた変数がどのようにインデックス付けされるかを理解しようとしていますz3。ここにスニペットz3pyと対応する出力があります。( http://rise4fun.com/Z3Py/plVw1 )

x, y = Ints('x y')
f1 = ForAll(x, And(x == 0, Exists(y, x == y)))
f2 = ForAll(x, Exists(y, And(x == 0, x == y)))
print f1.body()
print f2.body()

出力：

ν0 = 0 ∧ (∃y : ν1 = y)
y : ν1 = 0 ∧ ν1 = y

でf1、同じバインド変数のxインデックスが異なるのはなぜですか (0および1)。を変更しf1て を取り出すとExists、x同じ index( 0) になります。

インデックス作成メカニズムを理解したい理由:

に送信したい scala の DSL で表される FOL 式がありますz3。およびを引数として受け取るバインドされた変数を作成するためScalaZ3のmkBoundAPI が追加されました。引数にどの値を渡せばよいかわかりません。そこで、次のことを知りたいです。indexsortindex

2 つの式がphi1あり、変数インデックスが最大でとphi2がバインドされている場合、 inのインデックスはどうなるでしょうかn1n2xForAll(x, And(phi1, phi2))

また、インデックス形式ですべての変数を表示する方法はありますか? ではなく、インデックス付きの形式でf1.body()私を示しているだけです。（理由は、まだバインドされているためだと思います）xyyf1.body()

4

1 に答える 1

7

Z3は、deBruijnインデックスを使用して束縛変数をエンコードします。次のウィキペディアの記事では、de Bruijnインデックスについて詳しく説明しています。http： //en.wikipedia.org/wiki/De_Bruijn_index 備考：上記の記事では、インデックスは1から始まり、Z3では0から始まります。

2番目の質問に関しては、Z3プリティプリンターを変更できます。Z3ディストリビューションには、PythonAPIのソースコードが含まれています。きれいなプリンターはファイルに実装されていますpython\z3printer.py。メソッドを置き換える必要があります。

def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    sz  = len(xs)
    if idx >= sz:
        return seq1('Var', (to_format(idx),))
    else:
        return to_format(xs[sz - idx - 1])

と

def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    return seq1('Var', (to_format(idx),))

HTMLプリティプリンターを再定義する場合は、置き換える必要があります。

def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    sz  = len(xs)
    if idx >= sz:
        # 957 is the greek letter nu
        return to_format('&#957;<sub>%s</sub>' % idx, 1)
    else:
        return to_format(xs[sz - idx - 1])

と

def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    return to_format('&#957;<sub>%s</sub>' % idx, 1)
于 2012-08-05T15:21:42.987 に答える