QF_FPA?Z3 是否支持 IEEE-754 算法? [英] QF_FPA? Does Z3 support IEEE-754 arithmetic?

问题描述

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

Browsing Z3 source code, I came across a bunch of files referring to QF_FPA, which seems to stand for quantifier-free, floating-point-arithmetic. However, I don't seem to be able to locate any documentation regarding its state, or how it can be used via various front-ends (in particular SMT-Lib2). Is this an encoding of IEEE-754 FP? If so, which precisions/operations are supported? Any documentation would be most helpful..

推荐答案

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

Yes, Z3 supports floating point arithmetic as proposed by Ruemmer and Wahl in a recent SMT-workshop paper. At the current stage, there is no official FPA theory, and Z3's support is very basic (only a bit-blaster). We're not actively advertising this yet, but it can be used exactly as proposed in the paper by Ruemmer/Wahl (setting logics QF_FPA and QF_FPABV). At the moment, we are working on a new decision procedure for FPA, but it will be some time until that is available.

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

Here's a brief example of what an FPA SMT2 formula could look like:

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

这篇关于QF_FPA?Z3 是否支持 IEEE-754 算法?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！