Кастинг Z3 Real в поплавок - PullRequest
Новая
       37

Кастинг Z3 Real в поплавок

1 голос
/ 23 марта 2020

Есть ли способ привести значение Real в число с плавающей точкой, чтобы python мог играть со значениями после завершения z3? 

x = RealVal("1/3")
print(x.sort())
print(float(x))

1 Ответ

2 голосов
/ 23 марта 2020

Обратите внимание, что вы не можете разыграть реальное значение z3 в число с плавающей точкой. Действительное значение z3 - это бесконечно точное действительное число, и его нельзя точно представить как значение с плавающей запятой, которое имеет ограничения точности.

Вместо этого вы хотите преобразовать его в Python дробь: https://www.tutorialspoint.com/fraction-module-in-python, который может представлять все действительные значения z3, если они не являются иррациональными корнями полиномов. (Вы можете игнорировать этот последний комментарий, если вы не работаете с полными алгебраическими c -реалами в z3.)

Для этого используйте метод as_fraction: 

from z3 import *

x = RealVal("1/3")
x2 = x.as_fraction()
print type(x2)
print x2

Это печатает : 

<class 'fractions.Fraction'>
1/3

Если вы действительно хотите, вы можете превратить это в число с плавающей точкой: 

x_float = float(x2.numerator) / float(x2.denominator)
print type(x_float)
print x_float

Это напечатает: 

<type 'float'>
0.333333333333

, но, очевидно, вы теперь потерял точность.

...