python - z3 の空のモデル

Question

z3py スニペット:

x = Int('x')

s = Solver()
s.add(x <= x)
print s.check()
print s.model()
print s.model().sexpr()

http://rise4fun.com/Z3Py/mfPU

出力：

sat
[]

の値は何でもx構いませんが、z3空のモデルを返します。モデルに自由変数xがないことは、任意の整数値が有効なモデルであることを示していますか?

Answer 1

はい、Z3では、定数（などx）がモデルに表示されない場合、それは「ドントケア」です。つまり、の任意の値がx式を満たします。定数の値を評価するときに、「モデルの完成」を有効にすることができます。つまり、Z3は「ドントケア」シンボルに対して任意の解釈を使用します。これが例ですhttp://rise4fun.com/Z3Py/bvVO

x = Int('x')
s = Solver()
s.add(x <= x)
print s.check()
m = s.model()
print m.evaluate(x)
print m.evaluate(x, model_completion=True)
print m