如何从 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 浮点/布尔对象。
我知道我可以使用is_true/检查布尔值is_false，但是如何优雅地将 ints/reals/... 转换回可用值（?例如，无需通过字符串并删除这个额外的符号）。
对于布尔值，您可以使用函数is_true和is_false。数值可以是整数、有理数或代数。我们可以使用函数is_int_value,is_rational_value和is_algebraic_value来测试每个案例。整数情况是最简单的，我们可以使用方法as_long()将 Z3 整数值转换为 Python long。对于有理值，我们可以使用 和 方法numerator()获得denominator()代表分子和分母的 Z3 整数。方法numerator_as_long()和是和denominator_as_long()的快捷方式。最后，代数数用于表示无理数。该类有一个名为. 它返回一个 Z3 有理数，它精确地逼近代数数self.numerator().as_long()self.denominator().as_long()AlgebraicNumRefapprox(self, precision)1/10^precision. 这是有关如何使用此方法的示例。它也可以在线获得：http ://rise4fun.com/Z3Py/Mkw
p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), 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())