[Eva] Subdivision: slightly changes the strategy to cut a float interval in half.
If an interval contains positive and negative floating-point values, cuts the interval at 0. Otherwise, uses the same strategy as before: cuts the interval at the mathematical average of its bounds. This strategy always reaches the maximal precision in one split on e*e squares, which is the most common pattern for subdivisions. In the tests, it decreases the precision on computations of e-e, where a split at 0 is useless. However, this is not a common pattern in real codes.
Showing
- src/kernel_services/abstract_interp/float_interval.ml 15 additions, 13 deletionssrc/kernel_services/abstract_interp/float_interval.ml
- tests/float/oracle/nonlin.1.res.oracle 17 additions, 17 deletionstests/float/oracle/nonlin.1.res.oracle
- tests/float/oracle/nonlin.2.res.oracle 14 additions, 14 deletionstests/float/oracle/nonlin.2.res.oracle
- tests/float/oracle/nonlin.4.res.oracle 18 additions, 18 deletionstests/float/oracle/nonlin.4.res.oracle
- tests/float/oracle/nonlin.5.res.oracle 15 additions, 15 deletionstests/float/oracle/nonlin.5.res.oracle
- tests/misc/oracle/widen_hints_float.res.oracle 1 addition, 1 deletiontests/misc/oracle/widen_hints_float.res.oracle
Loading
Please register or sign in to comment