z3 中的空模型 [英] Empty model in z3

问题描述

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 是否表示任何整数值都是有效模型?

Any value of x would do but z3 returns empty model. Does a missing free variable x in the model indicates that any integer value is a valid model?

推荐答案

是的，在 Z3 中，如果一个常量(比如 x)没有出现在模型中，那么它就是一个don不在乎".也就是说，x 的任何值都将满足公式.在评估常量的值时，我们可以启用模型完成".也就是说，Z3 将对无关"符号使用任意解释.这是一个示例 http://rise4fun.com/Z3Py/bvVO

Yes, in Z3, if a constant (such as x) does not appear in the model, then it is a "don't care". That is, any value of x will satisfy the formula. When evaluating the value of a constant, we can enable "model completion". That is, Z3 will use an arbitrary interpretation for "don't care" symbols. Here is an example 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

这篇关于z3 中的空模型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！