Z3 SMT Solver - 如何在 FPA 中提取浮点数的值？

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 至少需要四舍五入，而将具有大指数的浮点数转换为十进制实数表示可能会非常庞大​​。

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

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