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

【问题标题】：QF_FPA? Does Z3 support IEEE-754 arithmetic?QF_FPA？ Z3 是否支持 IEEE-754 算法？
【发布时间】：2013-02-17 08:09:44
【问题描述】：

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

【问题讨论】：

标签： z3

【解决方案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)

【讨论】：

z3 最新的稳定版本 4.3.2 是否已将这种对浮点运算的支持纳入？此外，浮点理论支持是否与其他理论相结合，例如线性整数算术，无论是稳定版本还是不稳定版本？
4.3.2只有部分支持，当前版本是4.4.0，全面支持，包括理论组合。请注意，从浮点数到实数/有理数的转换引入了非线性约束，因此与线性算术的组合也变得非线性。
感谢您提供有关转换和理论组合的知识。我在 github 上查看：4 月底的 z3 版本具有更广泛的支持是个好消息。很快就会尝试。
在 4.4.2 中运行示例代码 sn-p 产生 WARNING: unknown logic, ignoring set-logic command (error "line 3 column 20: unknown sort 'FP'") (error "line 4 column 20: unknown sort 'FP'") (error "line 5 column 20: unknown sort 'FP'") (error "line 8 column 7: unknown constant x")
自我的示例以来，SMT FP 标准发生了变化，请参阅下面 Daniel 的回答。

【解决方案2】：

浮点逻辑在 v4.4.2 中被命名为 QF_FP 和 QF_FPBV。 RELEASE_NOTES 中理论描述的链接已断开。正确的页面是http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml。上面建议的例子应该是

(set-logic QF_FP)

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

(assert (and 
    (= x (fp #b0 #b00000000010 #b0000000000000000000000000000000000000000000000000010))
    (= y (fp #b0 #b00000000010 #b0000000000000000000000000000000000000000000000000010))
    (= r (fp.add roundTowardZero x y))
))

(check-sat)

【讨论】：

感谢 Daniel 更新示例！自那以后，SMT FP 标准已经更新，这确实是新的语法。我们已从 Z3 中删除了所有旧符号，并且仅支持最终标准。