为什么Z3&Quot；舍入&Real小到1.0/0.0？ [英] Why is Z3 "rounding" small reals to 1.0/0.0?

问题描述

我正在使用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)或类似的显式转换解决了我的问题。

这篇关于为什么Z3&Quot；舍入&Real小到1.0/0.0？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！