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..
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)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With