在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