如何从Z3模型获取真正的
python值？
例如.
p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5,x > 10),Or(p,x**2 == 2),Not(p))
s.check()
print s.model()[x]
print s.model()[p]
版画
-1.4142135623? False
但是那些是Z3对象,而不是python float / bool对象.
我知道我可以使用is_true / is_false来检查布尔值,但是如何优雅地将int / reals / …转换回可用的值(例如,不经过字符串和切除这个额外的符号).
解决方法
对于布尔值,可以使用函数is_true和is_false.数值可以是整数,合理或代数.我们可以使用函数is_int_value,is_rational_value和is_algebraic_value来测试每种情况.整数情况是最简单的,我们可以使用方法as_long()将Z3整数值转换为Python long.对于有理值,我们可以使用方法numerator()和分母()来获取表示分子和分母的Z3整数.方法numerator_as_long()和denominator_as_long()是self.numerator().as_long()和self.denominator().as_long()的快捷方式.最后,代数数字用于表示非理性数字. AlgebraicNumRef类有一个称为约(self,precision)的方法.它返回一个Z3有理数,它以精度为1/10 ^的精度逼近代数.这是一个关于如何使用这个方法的例子.也可在线获得：
http://rise4fun.com/Z3Py/Mkw
p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5,Not(p))
s.check()
m = s.model()
print m[p],m[x]
print "is_true(m[p]):",is_true(m[p])
print "is_false(m[p]):",is_false(m[p])
print "is_int_value(m[x]):",is_int_value(m[x])
print "is_rational_value(m[x]):",is_rational_value(m[x])
print "is_algebraic_value(m[x]):",is_algebraic_value(m[x])
r = m[x].approx(20) # r is an approximation of m[x] with precision 1/10^20
print "is_rational_value(r):",is_rational_value(r)
print r.numerator_as_long()
print r.denominator_as_long()
print float(r.numerator_as_long())/float(r.denominator_as_long())