18

How can I get real python values from a Z3 model?

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]

prints 

-1.4142135623?
False

but those are Z3 objects and not python float/bool objects.

I know that I can check boolean values using is_true/is_false, but how can I elegantly convert ints/reals/... back to usable values (without going through strings and cutting away this extra ? symbol, for example).

Assem
  • 11,574
  • 5
  • 59
  • 97
sqx
  • 183
  • 1
  • 1
  • 5
  • Have you tried `bool(s.model()[x])` and `float(s.model()[p])`? – Andy Hayden Sep 26 '12 at 09:26
  • Yes, but that doesn't work (correctly): `bool(s.model()[p])` gives `True`, when it should be `False` and `float(s.model()[x])` throws an exception `AttributeError: AlgebraicNumRef instance has no attribute '__float__'` – sqx Sep 26 '12 at 09:27

1 Answers1

30

For Boolean values, you can use the functions is_true and is_false. Numerical values can be integer, rational or algebraic. We can use the functions is_int_value, is_rational_value and is_algebraic_value to test each case. The integer case is the simplest, we can use the method as_long() to convert the Z3 integer value into a Python long. For rational values, we can use the methods numerator() and denominator() to obtain the Z3 integers representing the numerator and denominator. The methods numerator_as_long() and denominator_as_long() are shortcuts for self.numerator().as_long() and self.denominator().as_long(). Finally, algebraic numbers are used to represent irrational numbers. The AlgebraicNumRef class has a method called approx(self, precision). It returns a Z3 rational number that approximates the algebraic number with precision 1/10^precision. Here is an example on how to use this methods. It is also available online at: 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())
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Thanks, Leonardo. I thought there would be an easier way, especially for Reals, but given the fact that Z3 values may be larger/more precise than what's possible in python, this makes sense. Nevertheless, some convenience methods returning python floats or perhaps `Fraction` instances for rational numbers would be nice for people who do not care about precision that much. – sqx Sep 26 '12 at 11:17
  • It would be really nice if comparing a z3 Bool to a Python bool would do this conversion for you, too. – Sushisource Mar 29 '13 at 21:00