Z3/Python 从模型获取 python 值

Question

如何从 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

检查布尔值，但是如何优雅地将整数/实数/...转换回可用值（无需遍历字符串并删除这个额外的

?

符号，例如）。

Answer 1

对于布尔值，您可以使用函数

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

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())

Answer 2

z3 中应该有一个函数可以将任何原始 z3 值转换为 Python 值！