Z3/Python 从模型中获取 python 值 [英] Z3/Python getting python values from model

问题描述

如何从 Z3 模型中获取真正的 Python 值?

How can I get real python values from a Z3 model?

例如

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 对象.

but those are Z3 objects and not python float/bool objects.

我知道我可以使用 is_true/is_false 检查布尔值，但是我如何优雅地将整数/实数/...例如，通过字符串并删除这个额外的 ? 符号).

I know that I can check boolean values using is_true/is_false, but how can I elegantly convert ints/reals/... back to usable values (without going through strings and cutting away this extra ? symbol, for example).

推荐答案

对于布尔值，您可以使用函数 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() 是 self.numerator().as_long() 和 self.denominator().as_long().最后，代数数用于表示无理数.AlgebraicNumRef 类有一个名为 approx(self, precision) 的方法.它返回一个 Z3 有理数，它以 1/10^precision 的精度逼近代数数.这是有关如何使用此方法的示例.它也可以在网上获得:http://rise4fun.com/Z3Py/Mkw

For Boolean values, you can use the functions is_true and is_false. Numerical values can be integer, rational or algebraic. We can use the functions is_int_value, is_rational_value and is_algebraic_value to test each case. The integer case is the simplest, we can use the method as_long() to convert the Z3 integer value into a Python long. For rational values, we can use the methods numerator() and denominator() to obtain the Z3 integers representing the numerator and denominator. The methods numerator_as_long() and denominator_as_long() are shortcuts for self.numerator().as_long() and self.denominator().as_long(). Finally, algebraic numbers are used to represent irrational numbers. The AlgebraicNumRef class has a method called approx(self, precision). It returns a Z3 rational number that approximates the algebraic number with precision 1/10^precision. Here is an example on how to use this methods. It is also available online at: 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())

这篇关于Z3/Python 从模型中获取 python 值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！