Z3 SMT求解器--如何提取平安险中浮点数的值？

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))

然后打电话给伊娃

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

我得到了

(fp #b0 #b10000000001 #x3333333333333)

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

但我似乎找不出任何函数来将这个值返回给我。是否有像Z3_get_numeral_uint64 (.)这样的内建函数返回一个实际值，或者即使它分别返回分子和分母，它也能工作。

谢谢。

Answer 1

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

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

此外，还有一个名为pp.fp_real_literals的参数，用于为模型值启用实数/十进制编号表示，这是Z3_get_numeral_string应该遵守的。这些也被分为意义和指数，但它们可以方便调试。