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

输出：

^{pr2}$

任何值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