c++ - Z3 SMT Solver - 如何在 FPA 中提取 float 的值？

Question

我在 Linux 机器上使用 Z3-4.6.0 C/C++ API。

我陷入了一个非常愚蠢的问题。我有一个 QF_FP 逻辑求解器，该求解器能够针对输入问题返回 SAT。

当我这样做的时候

  z3::model model = z3_solver_.get_model();

我明白了

(define-fun var_1 () (_ FloatingPoint 11 53)
(fp #b0 #b10000000001 #x3333333333333))

然后调用eval

z3::expr r = model.eval(z3::expr(var_expr), true);

我明白了

(fp #b0 #b10000000001 #x3333333333333)

当我通过 IEEE-754 转换器在线检查时，我知道答案是正确的。

但我似乎无法弄清楚/找到任何可以将此值返回给我的函数。是否有像 Z3_get_numeral_uint64 (...) 这样的内置函数返回实数，或者即使它分别返回分子和分母，也可以工作。

谢谢。

Answer 1

(fp #...) 是 SMT 浮点理论定义的值/数字。它是精确的，并且避免了舍入和/或截断实数表达式带来的任何问题。例如。将此值转换为 double 需要至少一次舍入，并且将具有大指数的 float 转换为十进制实数表示可能会很大。

您可以使用 Z3_fpa_get_numeral_* 函数将单独的符号、有效数和指数值提取为位 vector 、字符串或 int64，但这取决于应用程序来组合和/或近似他们。

此外，还有一个名为 pp.fp_real_literals 的参数，用于启用模型值的实数/十进制编号表示形式，Z3_get_numeral_string 应该遵守该表示形式。它们也分为有效数和指数，但它们可以简化调试。