The param.transc file

The user can tune the parameters of the roundoff error bound certification algorithm, by editing the real2float/param.transc file, whose content looks like: 
******* Real2Float Parameters *******

* Input file with program definitions
   ineqs_file = real2float.ineq

...

******* General User Parameters *******

* Branch and Bound Parameters  
   bb = true

* SOS relaxation order: degree of the SOS used to approximate nonnegative polynomials
   relax_order = 1

...

****** Verbosity Parameters ********

* Displays problem related data: input box, input constraints, objective function of optimization problem, lower/upper bounds, total execution time
   problem_verb = true
...
Each line starting with a star * is a comment.
The parameters are typed. For instance, the type of the parameter bb is bool, so the user can edit the file by writing either bb = true or bb = false. The type of the relaxation order relax_order is int, thus the user may write relax_order = 2 to find sums of squares decompositions (SOS) at second relaxation order (allowed when the maximal degree of the polynomials involved in the program is less than 4).

Real2Float Parameters

  • ineqs_file (string): Input file with program definitions. Default is real2float.ineq.
  • bits (int): Floating-Point Precision. Default is 53, which corresponds to double-precision.
  • real2float_ratpol (bool): For programs implementing rational functions, computes separetely rounding bounds of numerator and denominator. Default is false.
  • real2float_coarse (bool): Computes coarser bounds using interval arithmetics on additional error variables. Default is true.

General Parameters

  • bb (bool): when bb = true, domain subdivision is performed until the inequality is successfully certified. Default is true.
  • relax_order (int): SOS relaxation order: degree of the SOS used to approximate nonnegative polynomials. Default is 1.
  • coq (bool): Check the correctness of Sums of Squares (SOS) certificates inside Coq. Default is false.
  • pure_ia (bool): Trying to prove the inequality with interval arithmetics (ia) only. Default is false.
  • coeff_type (sting): The type of polynomial coefficients for verification, either float (double precision floating-points of the standard OCaml library, complying with IEEE 745) or zarith (arbitrary-size rationals, available in the ZArith OCaml library. Default is float.
  • samp_iters (int): Maximal number of iterations when using Semi-Algebraic Max-Plus (samp) approximation: lower/upper approximations for special univariate functions such as exp, sine, cos, etc. Default is 1.

Verbosity Parameters

  • problem_verb (bool): Displays problem related data: input box, input constraints, objective function of optimization problem, lower/upper bounds, total execution time. Default is true.
  • real2float_verb (bool): When using the Real2Float module, the absolute roundoff error r is decomposed as r = l + h, with l being affine w.r.t. the roundoff error variables (h is a remainder, nonlinear w.r.t. the error terms). The real2float_verb option allows to print data related to bounds obtained for l (using SOS approximations) and for h (using interval arithmetic). Default is false.
  • parab_verb (bool): Displays information (e.g. equations) of lower/upper approximations for special univariate functions such as exp, sine, cos, etc. Default is false.
  • coq_verb (bool): Prints data related to formal verification of SOS certificates inside Coq: execution time of the checker, location of the Coq data file containing the certificate (vernacular file with .v extension). Default is false.