Z3/Python получает значения python из модели

Как я могу получить реальные значения python из модели Z3?

например.

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/is_false, но как я могу элегантно преобразовать ints/reals/... обратно к полезным значениям (без прохождения строк и отсечения этого дополнительного ? символ, например).

Ответы

Ответ 1

Для булевых значений вы можете использовать функции is_true и is_false. Численные значения могут быть целыми, рациональными или алгебраическими. Мы можем использовать функции is_int_value, is_rational_value и is_algebraic_value для проверки каждого случая. Integer случай является самым простым, мы можем использовать метод 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())