Z3 SMT求解器 - 如何在FPA中提取浮点数的值

Z3 SMT Solver - How can I extract the value of a floating point number in FPA?

本文关键字：FPA 提取 浮点数 SMT Z3      更新时间：2023-10-16

我在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(...(返回真实值，或者即使它分别返回分子和分母也可以工作。

谢谢。

(fp #...) 是 由SMT浮点理论定义的值/数字。这是精确的，避免了圆形和/或截断的实现表达式带来的任何问题。例如。将此值转换为double将需要至少一个圆形，并以较大的指数转换为十进制代表的浮子可能很大。

您可以使用Z3_fpa_get_numeral_*函数将单独的符号，显着和指数值作为位矢量，字符串或INT64S提取，但要取决于将它们组合和/或近似的应用。

此外，有一个称为pp.fp_real_literals的参数可以启用模型值的真实/小数编号表示，Z3_get_numeral_string应尊重。这些也被分为显着和指数，但它们可能会减轻调试。

相关文章：