为什么 Z3 将小实数“四舍五入”为 1.0/0.0？

Question

我正在使用 Z3 的 python API 来做一些线性实数运算。我遇到过非常接近零的实数以某种方式转换为 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 浮点数来让它工作？

Answer 1

我无法复制这个。当我运行你的程序时，我得到：

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

sat
[b = 50000, a = 0]

其中没有您所说的 (/ 1.0 0) 术语。

您使用的是哪个版本的 z3？也许您的旧版本有一个已修复的错误？我在 4.8.13（来自 GitHub master），不过您也可以使用 4.8.12 的最新官方版本。

NB话虽如此，我认为您使用Q(1, 100000) 的“解决方法”实际上是相当可取的，因为它可以避免各种浮点精度问题。除非你正在解决浮点逻辑问题，否则你真的不应该以这种方式使用浮点转换，因为会有关于表示问题的陷阱。

Answer 2

事实证明，Z3 并没有按原样获取浮点数，而是将其转换为字符串，然后尝试解析该字符串。对于小数字，Python 的 str() 默认为科学记数法，Z3 显然无法正确解析。使用"{:.20f}".format(my_small_float) 或类似的显式转换解决了我的问题。