sosy-lab
IEEE Floating-point to Bitvector Conversion Not Supported in All Solvers
IEEE Floating-point to Bitvector conversion is not supported in Bitwuzla and CVC5, possibly others. The standard says two things about this conversion:
:note
"There is no function for converting from (_ FloatingPoint eb sb) to the
corresponding IEEE 754-2008 binary format, as a bit vector (_ BitVec m) with
m = eb + sb, because (_ NaN eb sb) has multiple, well-defined representations.
Instead, an encoding of the kind below is recommended, where f is a term
of sort (_ FloatingPoint eb sb):
(declare-fun b () (_ BitVec m))
(assert (= ((_ to_fp eb sb) b) f))
"
So it is nice that some solvers give us this method, but in general we can not expect them to add it (for Bitwuzla we asked and got told that it will not be added).
And there is an implementation that we can follow, but it has 2 problems:
- A constraint is created and needs to be added to provers that use this variable (and as far as i can see ONLY those). So we would need to add a constraint without the users knowledge.
- A new BV variable is created that the user also does not know about.
We could of course add a method that returns this info and the constraint as well as the BV variable.
This came up in CPAchecker here.
Also, we already have an implementation in Bitwuzla.
In my opinion, this looks like something a user should add instead of us, but i am completely open to suggestions/ideas.
In my opinion, this looks like something a user should add instead of us, but i am completely open to suggestions/ideas.
Well, then it means that every user has to implement it themselves, and in the first place they have to come up with the solution (which is not obvious).
And there is an implementation that we can follow, but it has 2 problems:
- A constraint is created and needs to be added to provers that use this variable (and as far as i can see ONLY those). So we would need to add a constraint without the users knowledge.
This is something that I would strongly recommend to not consider. It is too much magic and probably breaks a lot of things (push/pop, copying formulas to other solvers).
- A new BV variable is created that the user also does not know about.
This is something that could be acceptable if the documentation of the method explains that it may happen, and the variable name is little likely to collide. Thinking more, maybe it is actually too difficult for JavaSMT to decide on a name, because it doesn't know what other formulas the user will create (consider the case that after starting to create formulas, they load a formula from a file that might also have such variables in it). But JavaSMT could let the user provide the name.
We could of course add a method that returns this info and the constraint as well as the BV variable.
Yes, or accept a Consumer<? super BitvectorFormula> as parameter.
Something like
public BitvectorFormula toIeeeBitvector(FloatingPointFormula f, Consumer<? super BitvectorFormula>)
(potentially with a way to specify the name, or with a record return value)
Then the old method could be documented as "Works only if solver supports it. If you want cross-solver support and can handle additional constraints that need to be conjuncted to the formula, call this other method". The new method would use the solver's one if it works and otherwise the fallback.
That hurts nobody and makes it easier for users of JavaSMT.
On the other hand, I am still of the opinion that solver developers should implement this, and I found a new argument: It will be bad for users who want to copy formulas from one solver to the other if the second one does not support this function natively. E.g., if in CPAchecker I want to use one solver as the primary one, but then use another for interpolation, or even just as a fallback if solving with the first fails. Maybe this can convince more solver developers?
In my opinion, this looks like something a user should add instead of us, but i am completely open to suggestions/ideas.
Agreed, and I think the current work-around for Bitwuzla should be removed in favor of something like 299 on the user side
The problem with toIeeeBitvector is that it is not a function as there are many possible representation for NaN. Solvers that still support it (i.e. Z3 and MathSat) fix the issue by returning a "canonical" representation. However, this representation is not standardized, and it doesn't fix the issue that the exact bit pattern is lost when converting from/to NaN. In CPAchecker we will therefore always have to introduce a new variable and some constraints to make that all bit patterns are possible and that the analysis remains sound.
Note that this is not something that can easily be done in JavaSMT, and that even with the current work-around for Bitwuzla we still return a canonical representation for NaN. We could remove this special case, but then the function would no longer be side-effect free and simple substitutions in the terms become impossible. All of this can more easily be handled on a higher level by the user, but It don't see a good way to do it directly in JavaSMT
Thank you both for your input!
I actually like both of your ideas in conjunction! Offer a call like Philipp suggests, and allow the user to specifiy how to handle special values (optionally).
Btw, this opens the question what the other solvers return for special values, and we should add tests and documentation for it.
Btw, this opens the question what the other solvers return for special values, and we should add tests and documentation for it.
MathSat seems to always return 0xFF800001 for single-precision floats. In Z3 it's usually 7F800001, but the value isn't necessarily fixed. The solver seems to use a UF to map from floats to bitvectors, and the definition can be found in the model: fp.to_ieee_bv(01111111111111111111111111111111): 2139278022. The value on the right may be any bit pattern that maps to NaN
I think it would be easiest to just mention in the documentation of toIeeeBitvector that the return value is unspecified if the argument is NaN?
But it is not unspecified, there are just multiple definitions ;D
The safest way for us would be to provide a method that forces the user to think about it by a need to specify the returned bitvector for special FPs, but this is at the same time not convenient for the user.
I'll read into this and the possible definitions more and add it to this discussion and the documentation of the new method(s).
Thank you for taking a look!