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のオブジェクトであり、フロート/ BOOLオブジェクトをPYTHONありません。

は私がis_true/is_falseを使用してブール値をチェックすることができますことを、私はエレガントに（例えば、文字列を通過すると、この余分な?シンボルを離れて切断することなく）int型/実数/ ...背中使用可能な値に変換することができます方法を知っています。

Answer 1

ブール値の場合、関数is_trueとis_falseを使用できます。数値は整数、有理数または代数式にすることができます。 is_int_value,is_rational_value、is_algebraic_valueの各機能を使用して各ケースをテストすることができます。整数の場合が最も簡単ですが、メソッドas_long()を使用して、Z3整数値をPython longに変換することができます。有理数の場合、分子と分母を表すZ3の整数を得るには、numerator()とdenominator()のメソッドを使用できます。 numerator_as_long()とdenominator_as_long()は、self.numerator().as_long()とself.denominator().as_long()のショートカットです。最後に、代数的数は非合理的な数を表すために使用されます。 AlgebraicNumRefクラスにはapprox(self, precision)というメソッドがあります。これは、精度が1/10^precisionの代数的数を近似するZ3有理数を返します。次に、このメソッドの使用方法の例を示します。 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())