QF_FPA? Does the Z3 support IEEE-754 arithmetic?

Question

Looking through the source code of Z3, I came across a bunch of files related to QF_FPA, which seems to be without quantifiers, floating point arithmetic. However, it seems that I cannot find any documentation regarding its status or how it can be used using various interfaces (in particular, SMT-Lib2). Is this the encoding of IEEE-754 FP? If so, what fixes / operations are supported? Any documentation would be most helpful.

Answer 1

Yes, Z3 supports floating point arithmetic proposed by Ruemmer and Wahl in a recent SMT seminar publication . There is no official FPA theory at this stage, and Z3 support is very simple (only a bit blaster). We are not actively advertising this yet, but it can be used exactly as suggested in the Ruemmer / Wahl article (setting the QF_FPA and QF_FPABV logics). We are currently working on a new decision-making procedure for FPA, but it will be a while until it is available.

Here is a brief example of what the FPA SMT2 formula looks 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 xy)) )) (check-sat) 

Answer 2

Floating point logic is called QF_FP and QF_FPBV in version 4.4.4. 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 above example 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 xy)) )) (check-sat)