QF_FPA? Does Z3 support IEEE-754 arithmetic?

问题:

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

回答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)

回答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)