Z3/Python從模型獲取python值

Question

如何從Z3模型獲取真正的python值？

E.g.

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的對象和不蟒浮子/布爾對象。

我知道我可以使用is_true/is_false查布爾值，但我怎麼能轉換成優雅整數/實數/ ...回到可用值（不通過串去，去掉這額外的?符號，例如） 。

Answer 1

對於布爾值，可以使用函數is_true和is_false。數值可以是整數，有理數或代數。我們可以使用函數is_int_value,is_rational_value和is_algebraic_value來測試每個案例。整數情況是最簡單的，我們可以使用方法as_long()將Z3整數值轉換爲Python長整型。對於有理數值，我們可以使用方法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())