文章/答案/技术大牛

发布

问将Z3实铸成浮子
EN

Stack Overflow用户

提问于 2020-03-23 17:54:07

回答 1查看 974关注 0票数 1

有没有一种方法可以将Real值强制转换为浮点数，以便z3完成后python可以处理这些值？

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

回答已采纳

发布于 2020-03-23 18:17:04

请注意，不能将z3实值强制转换为浮点数。z3实值是一个无限精确的实数，不能忠实地表示为具有固有精度限制的浮点值。

相反，您希望将其转换为Python分数：https://www.tutorialspoint.com/fraction-module-in-python，它可以表示所有z3实数，只要它们不是多项式的非理性根。(除非您在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

但很明显你现在已经失去了精确性。

票数 3

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/60819028

复制

相似问题

问将Z3实铸成浮子EN