空模型在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