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,但是如何优雅地将ints/reals/...转换回可用值(例如,不通过字符串并删除这个额外的?符号).

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