8

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

4

2 回答 2

8

是的，Z3 支持 Ruemmer 和 Wahl 在最近的 SMT-workshop论文中提出的浮点运算。现阶段，没有官方的 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)
于 2013-03-04T11:11:45.050 回答
3

浮点逻辑在 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)
于 2015-10-30T15:46:57.343 回答