MacOS 上 python z3-solver 的结果不正确

Posted 2023-03-16

【中文标题】MacOS 上 python z3-solver 的结果不正确

【英文标题】：Incorrect result from python z3-solver on MacOS

【发布时间】：2022-01-09 10:17:13

【问题描述】：

我是 z3 的新手。我正在尝试使用 z3 运行以下 python 示例。

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(And(x+y>1,x==0.00001,y==0.1))
print(s.check())

返回的结果是sat，我认为是不正确的，因为x+y=0.10001

[And(x + y > 1, x == 1/0, y == 1/10)]

我注意到术语 x==1/0 的分母为 0。我正在使用在 macOS 10.14.6 Mojave 上运行的 Python 3.9.8、z3-solver 4.8.12.0。

我还在装有 Ubuntu 20.04、python3.8 和 z3-solver 4.8.10.0 的机器上尝试了完全相同的示例。返回结果为unsat，并且在打印求解器时分母中没有0。

有谁知道我在这里做错了什么？非常感谢您。

【参考方案1】：

我无法用 z3 4.8.14 复制它；它在哪里打印unsat，就像您在 4.8.10 中找到的那样。您应该简单地升级您的 z3 版本。

之前有关于此的问题，并且在某些化身中出现了像0.00001 这样的小数字没有被正确翻译。我怀疑你正在遭受同样的痛苦。见这里：Why is Z3 "rounding" small reals to 1.0/0.0?

升级是最好的；如果您无法尝试那里的建议：不要使用0.00001，而是尝试Q(1, 100000)。

【讨论】：

您好，别名，非常感谢您的帮助。我可以通过更新我的 z3 版本来解决这个问题。