我正在尝试将z3py集成到我的应用程序中。有些断言涉及小实数,例如
solver.add(x <= 1e-6)
然后我收到以下错误:
File "~/src/solver/z3.py", line 2001, in __le__
a, b = _coerce_exprs(self, other)
File "~/src/solver/z3.py", line 846, in _coerce_exprs
b = s.cast(b)
File "~/src/solver/z3.py", line 1742, in cast
return RealVal(val, self.ctx)
File "~/src/solver/z3.py", line 2526, in RealVal
return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
File "~/src/solver/z3core.py", line 1774, in Z3_mk_numeral
raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
src.solver.z3types.Z3Exception: 'parser error'
虽然断言
solver.add(x <= 1e-4)
似乎很好。
因此,我猜测 z3 中存在某种精度限制。如果是这样,是否有让第一个断言通过的选项?
谢谢。
Z3 中没有精度限制。它可以表示任意精度的有理数和代数数。下面是一个示例:
print RealVal('1/10000000000000000000000000000')
print simplify((RealVal('1/10') ** RealVal('10')) ** RealVal('10'))
您可以在以下位置在线试用: http://rise4fun.com/Z3Py/ahJQ
该函数RealVal(a)
将 Python 值转换为 Z3 实数值。它使用 Z3 C API Z3_mk_numeral
来实现这一点。此代码在 Z3 分发中包含的z3.py
文件中可用。API Z3_mk_numeral
需要一个字符串,该字符串以十进制格式(例如,"1.3"(或分数格式(例如,"1/3"(对有理数进行编码。请注意,不支持科学记数法。为了方便 python 用户RealVal(a)
,我们使用方法 str(a)
在调用 Z3_mk_numeral
之前将a
转换为字符串。因此,用户还可以编写RealVal(1)
、RealVal(1.2)
等。
第二点信息是语句solver.add(x <= 1e-4)
本质上是solver.add(x <= RealVal(1e-4))
的简写。
现在,我们可以问,为什么该示例适用于1e-4
但不适用于1e-6
。问题在于 Python 中 str
的实现。 str(1e-4)
返回 Z3 Z3_mk_numeral
支持的十进制表示法的字符串"0.0001"
,但str(1e-6)
返回Z3_mk_numeral
不支持的科学记数法"1e-6"
字符串。
print str(1e-4)
print str(1e-6)
这是上面示例的链接:http://rise4fun.com/Z3Py/C02q
为了避免这个问题,我们在创建 Z3 表达式时应该避免使用科学记数法中的数字。我将看看我是否有时间在下一个版本的 Z3 Z3_mk_numeral
中添加对科学记数法的支持。