z3py:解析小实数时出错

Question

我正在尝试将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中存在某种精度限制。如果是这样，是否有让第一个断言通过的选项？

谢谢。

Answer 1

在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应用编程接口Z3_mk_numeral来实现这一点。Z3发行版中包含的z3.py文件中提供了此代码。Z3_mk_numeral接口需要一个以十进制格式(例如，'1.3')或分数格式(例如，'1/3')对有理数进行编码的字符串。请注意，不支持科学记数法。为了方便python用户使用RealVal(a)，我们在调用Z3_mk_numeral之前使用str(a)方法将a转换为字符串。因此，用户还可以编写RealVal(1)、RealVal(1.2)等。

第二点信息是，语句solver.add(x <= 1e-4)本质上是solver.add(x <= RealVal(1e-4))的缩写。

现在，我们可以问，为什么这个例子适用于1e-4，而不适用于1e-6。问题在于str在Python中的实现。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中的科学记数法的支持。