z3 - QF_FPA？ Z3 是否支持 IEEE-754 算法？

Question

浏览 Z3 源代码，我遇到了一堆引用 QF_FPA 的文件，它似乎代表无量词、浮点运算。但是，我似乎无法找到有关其状态的任何文档，或者如何通过各种前端(特别是 SMT-Lib2)使用它。这是 IEEE-754 FP 的编码吗？如果是，支持哪些精度/操作？任何文档都将是最有帮助的..

Answer 1

是的，Z3 支持 Ruemmer 和 Wahl 在最近的 SMT 研讨会中提出的浮点运算paper .现阶段还没有官方的FPA理论，Z3的支持也很基础(只是有点吹牛)。我们还没有积极宣传这一点，但它可以完全按照 Ruemmer/Wahl 论文中的建议使用(设置逻辑 QF_FPA 和 QF_FPABV)。目前，我们正在为 FPA 制定新的决策程序，但需要一段时间才能实现。

以下是 FPA SMT2 公式的简要示例:

(set-logic QF_FPA)    

(declare-const x (_ FP 11 53))
(declare-const y (_ FP 11 53))
(declare-const r (_ FP 11 53))

(assert (and 
    (= x ((_ asFloat 11 53) roundTowardZero 0.5 0))
    (= y ((_ asFloat 11 53) roundTowardZero 0.5 0))
    (= r (+ roundTowardZero x y))
))

(check-sat)