Unexpected exceptions with FP values

[Gbury]

When verifying models, there appears to be some operations on floating point values that raise unexpected exceptions. Consider the following example:

(set-logic QF_FPLRA)
(assert (let (
  (a (_ +zero 2 4))
  (b (_ -zero 2 4))
  ) (= (fp.min a b) a)))
(check-sat)

Trying to evaluate the formula e.g. using an empty model such as sat (), should yield an error because the fp.min function is not defined on +0/-0, however, it appears that before that can happen, the Farith library raises an assertion failure when trying to make the value for (_ +zero 2 4):

Error Uncaught exception:
      File "extracted/GenericFloat.ml", line 335, characters 16-22: Assertion failed
Raised at Farith__GenericFloat.GenericFloat.zero.(fun) in file "extracted/GenericFloat.ml", line 335, characters 16-24
Called from Farith.F.zero in file "farith.ml" (inlined), line 104, characters 23-57
Called from Dolmen_model__Fp.builtins in file "src/model/fp.ml", line 129, characters 16-47
Called from Dolmen_model__Eval.builtins.aux in file "src/model/eval.ml", line 31, characters 18-31
Called from Dolmen_model__Eval.eval_cst in file "src/model/eval.ml", line 68, characters 16-44
Called from Dolmen_model__Eval.eval_binder.(fun) in file "src/model/eval.ml", line 92, characters 43-56
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Dolmen_model__Eval.eval_binder in file "src/model/eval.ml", line 92, characters 13-59
Called from Dolmen_model__Loop.Make.eval in file "src/model/loop.ml", line 241, characters 6-24
Called from Dolmen_model__Loop.Make.eval_term in file "src/model/loop.ml", line 456, characters 16-45
Called from Dolmen_model__Loop.Make.eval_hyp in file "src/model/loop.ml", line 473, characters 14-47
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Dolmen_model__Loop.Make.check_solve.(fun) in file "src/model/loop.ml", line 558, characters 23-66
Called from Dolmen_model__Loop.Make.by_mode in file "src/model/loop.ml", line 438, characters 20-31
Called from Dolmen_model__Loop.Make.check_solve in file "src/model/loop.ml", line 539, characters 6-1023
Called from Dolmen_model__Loop.Make.check in file "src/model/loop.ml", line 588, characters 12-39
Called from Dolmen_loop__Pipeline.Make.eval_op in file "src/loop/pipeline.ml", line 87, characters 8-17

I don't know much about floating point numbers, so I can't assess whether (_ +zero 2 4) has a well-defined semantics, however:

• this exact example occurs in the documentation (cf https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml )
• the documentation does not seem to restrict the range of the length of the exponent and significand components of floating point numbers

Taking these two above points into account, I think that we should be able to correctly evaluate such expressions in dolmen. Therefore, this looks like it would need a fix in Farith, cc @bobot . Until the fix is released, it could be interesting to know whether there are other similar cases where Farith crashes unexpectedly / what are the conditions on lenght of exponent/signifcand for Farith to work, so that a more friendly error message can be displayed.

[bobot]

A nice error would be better. Farith doesn't accept when the exponent is too small compared to the size of the mantissa, it is derived from an hypothesis of the IEEE definition of Flocq. I don't remember why it is important.

So there is no quick fix.

[Gbury]

A nice error would be better. Farith doesn't accept when the exponent is too small compared to the size of the mantissa

Is there a way to have the exact condition that Farith requires of the exponent/mantissa sizes ?

[bobot]

GenericFloat.check_param

[Gbury]

Thanks, i'll use that for now.

@bobot : note however that the GenericFloat module is not exposed by Farith, and the only way I have managed to use it is to use the module alias generated by dune Farith__GenericFloat, which is not really meant to be used directly. Maybe the module (or at least some of its functions) could be exposed officially in the Farith top-level module. Separately, it would be nice if Farith could be made to throw a specific exception in such cases, instead of raising an internal assertion failure (which is not reasonably catchable).

[Gbury]

This was fixed as part of #151 : Dolmen now raises a proper error. We'll see later if we want/need to handle such exotic fp numbers.