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 APIZ3_mk_numeral来实现这一点。此代码z3.py在 Z3 发行版中包含的文件中可用。APIZ3_mk_numeral需要一个字符串，它以十进制格式（例如，'1.3'）或小数格式（例如，'1/3'）对有理数进行编码。请注意，不支持科学记数法。为了使RealVal(a)对Python用户方便，我们使用的方法str(a)来转换a成字符串调用之前Z3_mk_numeral。因此，用户也可以写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)返回"0.0001"Z3 支持的十进制表示形式的字符串Z3_mk_numeral，但str(1e-6)返回."1e-6"不支持的科学计数形式的字符串Z3_mk_numeral。

print str(1e-4)
print str(1e-6)

这是上面示例的链接：http : //rise4fun.com/Z3Py/C02q

为避免此问题，我们在创建 Z3 表达式时应避免使用科学记数法中的数字。我会看看我是否有时间在Z3_mk_numeralZ3 的下一个版本中添加对科学记数法的支持。