QF_FPA？Z3是否支持IEEE-754算术？

Question

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

Answer 1

是的,Z3支持Ruemmer和Wahl在最近的SMT研讨会论文中提出的浮点运算.在目前阶段,没有官方的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)