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/を使用してブール値を確認できることは知っていますが、int / reals / ...を使用可能な値にエレガントに変換するにはどうすればよいですか（たとえば、is_false文字列を調べたり、この余分な記号を切り取ったりする必要はありません）。?
ブール値の場合、関数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()ショートカットです。最後に、代数的数は無理数を表すために使用されます。クラスには。というメソッドがあります。代数的数を正確に近似するZ3有理数を返しますself.numerator().as_long()self.denominator().as_long()AlgebraicNumRefapprox(self, precision)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())