QF_FPA? Does Z3 support IEEE-754 arithmetic?

Question

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..

Sultry

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)

Fauteuil

Has this support for floating-point arithmetic been incorporated into z3's latest stable version 4.3.2? Also, has the floating-point theory support been combined with other theories, e.g., with linear integer arithmetic, in either stable or unstable version? – Bagley

4.3.2 had only partial support, the current release is 4.4.0, which has full support, including theory combination. Note that the conversion from floating-point number to real/rational number introduces non-linear constraints, so the combination with linear arithmetic becomes non-linear too. – Fauteuil

Thanks for the piece of knowledge about conversion and theory combination. I checked on github: the April-end z3 release with broader support is great news. Will try soon. – Bagley

Running the example code snippet in 4.4.2 yields 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") – Succumb

The SMT FP standard has changed since my example, see Daniel's answer below. – Fauteuil

Answer 2

The floating point logics are named QF_FP and QF_FPBV in v4.4.2. The link to the description of the theory in RELEASE_NOTES is broken. The correct page is http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml. The proposed example above should be

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

Succumb

Thanks Daniel for updating the example! The SMT FP standard has been updated since and this is indeed the new syntax. We have removed all old symbols from Z3 and we support only the final standard. – Fauteuil