How to obtain an exact infinite-precision representation of rational numbers via a non-standard FlatZinc extension?

Question

By default mzn2fzn automatically computes the result of a floating point division within a MiniZinc model, and stores it as a constant float value in the resulting FlatZinc model.

Example:

The file test.mzn

var float: x;
constraint      1.0 / 1000000000000000000000000000000000.0 <= x;
constraint x <= 2.0 / 1000000000000000000000000000000000.0;
solve satisfy;

translated with

mzn2fzn test.mzn

becomes equal to

var 1e-33..2e-33: x;
solve satisfy;

---

What we would like to obtain***, instead, is a FlatZinc file along the following lines:

var float: x;
var float: lb;
var float: ub;
constraint float_div(1.0, 1000000000000000000000000000000000.0, lb);
constraint float_div(2.0, 1000000000000000000000000000000000.0, ub);
solve satisfy;

where float_div() is a newly introduced, non-standard, FlatZinc constraint.

Is it possible to generate such an encoding of the original problem by using a variant of the std directory of constraints, or does this encoding require a more significant change of the source code of the mzn2fzn tool? In the latter case, could we have some guidance?

---

***: we have some formulas for which the finite-precision floating-point representation is unsuitable, because it changes a SAT result into UNSAT.

Answer 1

Currently there is no way of generating FlatZinc with infinite precision. Although the idea has been discussed a few times, it would require much of MiniZinc to be rewritten or appended using a library that could provide these infinite precise types. Libraries like these, such as the Boost interval library, seem to be lacking in options and do currently not compile for all machine targets on which MiniZinc is distributed. There seem to be various interesting cases for infinite precise types, but within the implementation of the MiniZinc compiler we are still looking for finding a decent way of implementing them.

Although infinite precision is not on the table. The MiniZinc compiler does intend to be correct according to the floating point standards. Feel free to report any problems that might occur to the MiniZinc Issue Tracker.