CODEWITHSUNDEEP
z3
alias
alias

Reputation: 30418

Floating point literals

I've two questions regarding writing IEEE floating-point constants, as accepted by Z3's FPA logics:

First, in this question, Christoph used the example:

 ((_ asFloat 11 53) roundTowardZero 0.5 0))

I'm wondering what the final 0 signifies? I've tried:

 ((_ asFloat 11 53) roundTowardZero 0.5))

And that seems to work as well. Rummer's paper doesn't seem to require the final 0 either; so I'm curious what role it plays.

Second, when I get a model from Z3, it prints floating-point literals like so:

 (as +1.0000000000000002220446049250313080847263336181640625p1 (_ FP 11 53))

How do I interpret the p1 suffix? What other suffixes are possible?

Thanks..

Upvotes: 2

Views: 791

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

Thanks for pointing these issues out. Both of them are because there is no agreed upon standard for floating-point literals in the input or output yet.

The final 0 in the example represents the (binary) exponent, i.e., (... 0.5 1) == 1.0. We added this simply because numbers sometimes would require a lot of space if the exponent cannot be specified separately. This way, we can often specify them quite succinctly.

The p1 suffix in the output represents the binary exponent, i.e., where e8 means 10^8, the suffix p8 would mean 2^8. Z3 currently uses only binary exponents, so there would always be a p-suffix here, but this may change in the future. The rest of the number is given enough decimal digits to represent a precise result.

Note that the output format is not agreed upon yet by the SMT community. This may change in the future. For instance, there are discussions about whether this should be done in IEEE bit-vector format or an intermediate format that lies somewhere between reals and non-IEEE bit-vectors.

Upvotes: 3

Related Questions