QF_FPA Push and Pop

Jan 16, 2015 at 9:09 PM
Does QF_FPA support the push and pop commands yet? When I run z3 on the following smtlib 2 file, it reports unsat as expected.
(set-logic QF_FPA)
(define-sort dbl () (_ FP 11 53))
(declare-fun x0 () dbl)
(declare-fun x1 () dbl)
(declare-fun x2 () dbl)
(define-fun rm () RoundingMode roundTowardZero)
(define-fun zero () dbl ((_ asFloat 11 53) rm 0.0))
(define-fun nan () dbl (as NaN (_ FP 11 53)))

(define-fun type-Positive ((x dbl)) Bool (or (> x zero) (= x nan)))
(define-fun type-Negative ((x dbl)) Bool (or (< x zero) (= x nan)))
(define-fun type-Nonpositive ((x dbl)) Bool (or (<= x zero) (= x nan)))
(define-fun type-Nonnegative ((x dbl)) Bool (or (<= x zero) (= x nan)))
(define-fun type-Zero ((x dbl)) Bool (or (== x zero) (= x nan)))
(define-fun type-Nan ((x dbl)) Bool (or (== x zero) (= x nan)))
(define-fun type-All ((x dbl)) Bool true)

(define-fun fl+ () dbl (+ rm x0 x1))
(define-fun fl+-Positive-Positive-Positive () Bool (=> (and (type-Positive x0) (type-Positive x1)) (type-Positive (+ rm x0 x1))))

(assert (not fl+-Positive-Positive-Positive))
(get-value (fl+ x0 x1))
However, when I uncomment push and pop, it reports SAT, with the following model:
((fl+ (+ roundTowardZero FP!val!0 FP!val!3))
 (x0 FP!val!0)
 (x1 FP!val!3))
The same thing happens when a call to reset occurs in the file.

Reading Z3's source code, it appears that push and pop are not supported yet for QF_FPA. Are there any plans to implement them?
Jan 16, 2015 at 9:37 PM
The master and unstable branches don't support any of the more advanced features, they basically translate everything into SAT and then run a SAT solver that has no support for incrementality, etc. The reason you get a SAT result when you add push/pop commands is that the main underlying solver doesn't know what floats are and thus it interprets all of that as uninterpreted functions (and it makes up new FP!val!n's for the model).

However, earlier today I pretty much finished the theory integration implementation and testing, which implicitly also enables push/pop. The plan is to integrate that into the unstable branch next week. For a preview, you can get the branch called fpa-api which contains all of those features. I didn't run many tests with push/pop yet, so I'd be happy to get someone to beta-test it anyways.

Minor snag: the logic name and many of the operators have been assigned new names in the final SMT theory definition of the FloatingPoint theory. We decided to remove support for all previous operator and logic names to keep it consistent.
Apr 21, 2015 at 9:58 PM
I've been using the fpa-api branch for the past few months. There were a few simple type errors in the implementation that I had to fix in order to get Z3 building with g++. I haven't noticed any other problems. I noticed that Z3 has moved to github, but it's unclear what has happened to the fpa-api functionality. The floating point theory in the main branch is called QF_FPA, and it seems that some other things have changed as well.
Apr 21, 2015 at 10:27 PM
Thanks for the interest in this! The fpa-api branch has been removed a couple of months ago, after it had been integrated into the unstable branch, so full FP support is now available in unstable, which in turn will be integrated into master in the next few weeks. Note that we decided to remove some function aliases, we now support exactly those functions/operators defined in the SMT FP standard, but not any of the overloaded functions names we had supported before (like + instead of fp.add). The official logic designation ended up being FP, so the respective logics are now called QF_FP, QF_FPBV, etc.

With our move to github, we're also retiring this discussion forum, but feel free to open a new discussion/issue over at github!