Z3/Python obteniendo valores de python del modelo

Question

¿Cómo puedo obtener valores de python reales de un modelo Z3?

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] 

impresiones

-1.4142135623? 
False 

pero esos son objetos Z3 y no objetos de flotación/bool pitón.

sé que puedo comprobar los valores booleanos utilizando is_true/is_false, pero ¿cómo puedo convertir elegantemente enteros/reales/... volver a los valores utilizables (sin pasar por las cuerdas y cortando este ? símbolo adicional, por ejemplo) .

Answer 1

Para valores booleanos, puede usar las funciones is_true y is_false. Los valores numéricos pueden ser enteros, racionales o algebraicos. Podemos usar las funciones is_int_value, is_rational_value y is_algebraic_value para probar cada caso. El caso entero es el más simple, podemos usar el método as_long() para convertir el valor entero Z3 en un Python largo. Para valores racionales, podemos usar los métodos numerator() y denominator() para obtener los enteros Z3 que representan el numerador y el denominador. Los métodos numerator_as_long() y denominator_as_long() son atajos para self.numerator().as_long() y self.denominator().as_long(). Finalmente, los números algebraicos se usan para representar números irracionales. La clase AlgebraicNumRef tiene un método llamado approx(self, precision). Devuelve un número racional Z3 que se aproxima al número algebraico con precisión 1/10^precision. Aquí hay un ejemplo sobre cómo usar este método. También está disponible en línea en: 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())