Alexey Solovyev

Hexadecimal floating-point numerals

1

Use hexadecimal floating-point numerals for external optimization tools. Use `"%h"` in OCaml `printf` functions. OCaml >= 4.03 is required.

Add a custom error function for expressions in the form `expr +/- const`.

Add fixed precision rounding modes and fixed-precision variables.

Add custom floating-point rounding modes. At least add arbitrary precision floating-point rounding modes which behave as IEEE 754 modes.

Correctly handle subnormal constants in `binary_float.ml` and `taylor_form.ml`.

The improved rounding model can be rewritten as ``` rnd_b(x) = p_2(x, b) * eps(b) ``` where `p_2(x, b) = p_2(x)` if `|x| = 0` or `|x|` is in the...

This PR updates Formal_ineqs to the latest version. The only HOL Light file which is changed (besides files which belong to Formal_ineqs) is `bignum_zarith.ml`: I added the `Big_int` module (which...

Inverse trigonometric functions

11

I would like to be able to use inverse trigonometric functions in .dop files. The following functions are requested: arcsin arccos arctan Alternative names for these functions should also be...

NaN result in a simple test

5

Test code: ``` var: [7.84, 8] x1; cost: sqrt(x1) * 1; ``` Result: ``` bin/dop_gelpia benchmarks/tests/sqrt.dop [[2.82842712474619,NaN], {'x1' : [7.839999999999999, 8],}] ```

Named constants (pi)

21

Common mathematical constants should be supported in .dop files. The most important constant is pi. Internally, the best possible interval approximation should be used.