2

Z3Py スニペット:

x = Int('x')
fun = Function('fun', IntSort(), IntSort(), IntSort())
phi = ForAll(x, (fun(x, x) != x)) 
print phi
solve(phi)

パーマリンク: http://rise4fun.com/Z3Py/KZbR

出力:

∀x : fun(x, x) ≠ x
[elem!0 = 0,
 fun!6 = [(1, 1) → 2, else → 1],
 fun = [else → fun!6(ζ5(ν0), ζ5(ν1))],
 ζ5 = [1 → 1, else → 0]]

質問: Z3 によって生成されたモデルを理解しようとしています。以下の疑問があります。

  1. z3 で生成されたモデルでは、その部分funのみが含まれています。elseしたがって、一見すると、引数に関係なく単一の値があるように見えます。しかしよく見ると、v0とv1が の正式なパラメータのようですfun。これにはいくつかの規則がありますか？
  2. どの変数がelem!0参照していますか?

ありがとう。

4

1 に答える 1

2

Z3 によって作成されたモデルは、純粋な関数型プログラムと見なす必要があります。これは、Z3 にモデルを SMT 2.0 形式で表示するように依頼すると明らかになります。メソッドを使用してそれを実現できsexpr()ます。この方法を使用した例を次に示します ( http://rise4fun.com/Z3Py/4Pw ):

x = Int('x')
fun = Function('fun', IntSort(), IntSort(), IntSort())
phi = ForAll(x, (fun(x, x) != x)) 
print phi
s = Solver()
s.add(phi)
print s.check()
print s.model().sexpr()

の解釈には、fun自由変数が含まれています。次のように読む必要があります fun(v0, v1) = fun!6(k5(v0), k5(v1))。これは、モデルが SMT 2.0 形式で表示されている場合に明示的です。私が Python プリティ プリンターを作成したとき、量指定子のない問題に焦点を当てようとしました。「関数型プログラムとしてのモデル」の考え方は、量指定子のない問題には関係ありません。今後、Python モデルのプリティ プリンターの改善に努めます。定数elem!0は、解決プロセス中に Z3 によって作成される補助定数です。最終的に（モデルが単純化された後）、実際には必要ありません。この不要な情報を取り除くために、モデルの「デッド コード」の削除手順を改善します。ただし、モデルは正しいです。それは量指定子を満たします。Z3 で使用されるエンコーディングの詳細については、http://rise4fun を参照してください。、および補助機能は、この記事k!5で説明されている「投影」機能です。

于 2012-10-15T16:34:18.947 に答える