浏览Z3的源代码，我碰到了一堆指QF_FPA，这似乎代表免费量词，浮点运算的文件。 不过，我似乎并没有能够找到有关其状态的任何文件，或如何它可以通过各种前端使用（尤其是SMT-LIB2）。 这是IEEE-754 FP的编码？ 如果是这样，其精度/操作的支持？ 任何文件将是最有帮助..
Answer 1:
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.
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)
Answer 2:
浮点逻辑被命名为QF_FP和QF_FPBV在v4.4.2。 该理论在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)
文章来源: QF_FPA? Does Z3 support IEEE-754 arithmetic?
