我正在使用Z3的pythonAPI进行一些线性实数运算。我遇到过一种情况，非常接近于零的雷亚尔以某种方式转换为1.0/0.0。这进而导致Z3的C++部分内部出现浮点异常。

例如，我有以下的Python程序：

from z3 import *
s = Solver()
s.add(0.00001 * Real("a") + 0.00001 * Real("b") > 0.0)
print(s.to_smt2())
result = s.check()
print(result)
print(s.model())

这将产生以下输出：

; benchmark generated from python API
(set-info :status unknown)
(declare-fun b () Real)
(declare-fun a () Real)
(assert
 (let ((?x10 (+ (* (/ 1.0 0.0) a) (* (/ 1.0 0.0) b))))
 (> ?x10 0.0)))
(check-sat)

Floating point exception (core dumped)

如果我将第3行替换为

#s.add(Q(1,100000) * Real("a") + Q(1, 100000) * Real("b") > 0.0)

我得到了预期的输出。

有没有人能解释一下，有没有办法让我用普通的Python浮动让它工作？

推荐答案

结果是，Z3不接受浮点数，而是将其转换为字符串，然后尝试解析该字符串。对于较小的数字，Pythons str()默认使用科学记数法，显然Z3无法正确解析。使用"{:.20f}".format(my_small_float)或类似的显式转换解决了我的问题。