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