3

Solver.model()一見不必要な で代入を返すことがありますが、Var()私は (おそらく単純に)Solver.model()各変数に対して常に具体的な値を返すことを期待していました。例えば：

#!/usr/bin/python
import z3

x, y = z3.Ints('x y')
a = z3.Array('a', z3.IntSort(), z3.IntSort())
e = z3.Not(z3.Exists([x], z3.And(x != y, a[x] == a[y])))

solver = z3.Solver()
solver.add(e)
print solver.check()
print solver.model()

生産する

sat
[k!1 = 0,
 a = [else -> k!5!7(k!6(Var(0)))],
 y = 1,
 k!5 = [else -> k!5!7(k!6(Var(0)))],
 k!5!7 = [1 -> 3, else -> 2],
 k!6 = [1 -> 1, else -> 0]]

何が起きてる？Var(0)inaの「else」は、配列の 0 番目の引数を参照していますaかa[i] = k!5!7[k!6[i]]? のような具体的な満足のいく割り当てをaZ3から取得することは可能a = [1 -> 1, else -> 0]ですか?

4

1 に答える 1

3

これは意図した出力です。関数と配列の解釈は、関数の定義と見なす必要があります。という主張を心に留めておいてください

z3.Not(z3.Exists([x], z3.And(x != y, a[x] == a[y])))

は本質的に全称量指定子です。数量詞のない問題の場合、Z3 は投稿で提案されている「具体的な割り当て」を生成します。しかし、この種の表現は十分に表現力がありません。メッセージの最後に、「具体的な割り当て」を使用してエンコードできない例を添付しました。次の投稿には、Z3 でのモデルのエンコード方法に関する追加情報があります。

Z3 で使用されるエンコーディングの詳細については、http://rise4fun.com/Z3/tutorial/guideを参照してください。

「具体的な」割り当てを使用してエンコードできないモデルを生成する例を次に示します ( http://rise4fun.com/Z3Py/egghでオンラインで入手可能)。

a = Array('a', IntSort(), IntSort())
i, j = Ints('i j')
solver = Solver()
x, y = Ints('x y')
solver.add(ForAll([x, y], Implies(x <= y, a[x] <= a[y])))
solver.add(a[i] != a[j])
print solver.check()
print solver.model()
于 2012-12-07T22:13:39.943 に答える