Input Settings

Real2Float supports conditional code without procedure calls nor loops.
The user defines the program prog implementing a nonlinear function together with input box constraints, input polynomial constraints, input uncertainties in the file real2float/real2float.ineq. Programs are encoded in an ML-like language:

let box_prog    x1 ... xn = [(a1, b1); ... ;(an, bn)];;
let obj_prog    x1 ... xn = [(f, eps)];;
let cstr_prog   x1 ... xn = [g1; ... ;gk];;
let uncert_prog x1 ... xn = [u1; ... ;un];;

Here, the first line encodes interval constraints for input variables, namely x := (x1, ..., xn) in the interval products of [a1, b1], ..., [an, bn]. The second line provides the function f(x) as well as the total rounding error bound epsilon. Then, one encodes polynomial nonnegativity constraints over the input variables, namely g1(x) ≥ 0, ... , gk(x) ≥ 0. Finally, the last line allows the user to specify a numerical constant ui to associate a given uncertainty to the variable xi, for each i= 1, ..., n. Note that it is mandatory to separate each definition with a double semicolon ;; (either for a box or an objective function).

Let us give a concrete example for the program keplerdouble. We want to bound the absolute rounding error of the program implementing the following function in double precision floating-point (default precision): f(x) = x2 x5 + x3 x6 - x2 x3 - x5 x6 + x1 ( - x1 + x2 + x3 - x4 + x5 + x6), for all x in [4.00, 6.36]^6. To show that this bound is less than epsilon = 8.76e-14, we write keplerdouble in real2float/real2float.ineq as follows:

let box_keplerdouble x1 x2 x3 x4 x5 x6 = [(4, 6.36); (4, 6.36); (4, 6.36); (4, 6.36); (4, 6.36); (4, 6.36)];;
let obj_keplerdouble x1 x2 x3 x4 x5 x6 = [(x2 * x5 + x3 * x6 - x2 * x3 - x5 * x6 + x1 * ( - x1 + x2 + x3 - x4 + x5 + x6), 8.76e-14)];;

Execution

Given a program identified with prog, the following command line allows to execute the main program:

% ./real2float prog

For instance, one performs the analysis of program keplerdouble with Real2Float as follows:

% ./real2float keplerdouble
...
1 problem solved, 0 cuts done
End of nonlinear optimization algorithm
Absolute rounding error bound = 8.75197e-14 <= 8.76e-14
Program keplerdouble verified
Total time: 0.429502 seconds

The analysis output indicates 0 cuts, meaning that no subdvision of the domain [4.00, 6.36]^6 was required to prove that 8.76e-14 is a valid upper bound of the rounding error. The execution time corresponds to an analysis performed on an Intel Core i5 CPU (2.40 GHz).

One can analyse the program keplersingle implementing the same function in single precision:

let box_keplersingle x1 x2 x3 x4 x5 x6 = [(4, 6.36); (4, 6.36); (4, 6.36); (4, 6.36); (4, 6.36); (4, 6.36)];;
let obj_keplersingle x1 x2 x3 x4 x5 x6 = [(x2 * x5 + x3 * x6 - x2 * x3 - x5 * x6 + x1 * ( - x1 + x2 + x3 - x4 + x5 + x6), 4.70e-5)];;

using the option -bits 24 in the command line:

% ./real2float keplersingle -bits 24
...
1 problem solved, 0 cuts done
End of nonlinear optimization algorithm
Absolute rounding error bound = 4.69868e-05 <= 4.7e-05
Program keplersingle verified

The Real2Float software relies on certified optimization techniques employing semidefinite programming and sums of squares polynomials. In a nutshell, one approximates nonnegative polynomials with sums of squares of fixed degree. This degree is called the relaxation order and can be modified using the option -relax_order d. Increasing the relaxation order might yield tighter bounds for the rounding error. The default value is equal to half of the maximal degree among all the polynomials involved in the program. We illustrate the potential advantage of increasing the relaxation order by two different analyses of the rigidbody1 program:

let box_rigidbody1 x1 x2 x3 = [(-15, 15); (-15, 15); (-15, 15)];;
let obj_rigidbody1 x1 x2 x3 = [(-x1*x2 - 2 * x2 * x3 - x1 - x3, 3.80e-13)];;

With the default value of relax_order (1 in this case), we obtain:

% ./real2float rigidbody1
...
38 problems solved, 37 cuts done
End of nonlinear optimization algorithm
Absolute rounding error bound = 3.79879e-13 <= 3.8e-13
Program rigidbody1 verified
Total time: 10.0224 seconds

Here, one needs to subdvide the input box [-15, 15]^3 in 38 parts to be able to certify the given bound.

At the second relaxation order, we obtain a much more efficient analysis:

1 problem solved, 0 cuts done
End of nonlinear optimization algorithm
Absolute rounding error bound = 3.79697e-13 <= 3.8e-13
Program rigidbody1 verified
Total time: 0.334389 seconds

Here, no subdivision is required and the bound is proved correct in less than one second.

Learn more about the parameter settings.