MiniZinc/FlatZinc: Fake floating numbers using integers automatically

[tobiasBora]

What language and solver does this apply to?
FlatZinc with cp_sat backend

Describe the problem you are trying to solve.
MiniZinc is a great tool to describe a generic problem in a solver-agnostic way, and solve it using any solver later. It is this way possible to specify floating points since some solver supports them. Unfortunately, OR-tools would just crash if floating points are used:

╰─❯ cat model.mzn                                                                                                                                                                                              ─╯
var 1.0..3.0: x;
var 1.0..3.0: y;
constraint x+y > 3.1;
solve satisfy;

╰─❯ minizinc model.mzn                                                                                                                                                                                         ─╯
x = 2.10000000000001;
y = 1.0;
----------

╰─❯ minizinc --solver com.google.or-tools model.mzn                                                                                                                                                            ─╯
F0917 12:07:14.109151 441098 cp_model_fz_solver.cc:1161] Check failed: !fz_var->domain.is_float CP-SAT does not support float variables
*** Check failure stack trace: ***
=====ERROR=====

However, one can quite simply fake floating points by multiplying them with a constant based on the wanted precision (of course, this would still fail to find solutions that need more precision, but that's quite unavoidable here):

╰─❯ cat model.mzn                                                                                                                                                                                              ─╯
var 10..30: x;
var 10..30: y;
constraint x+y > 31;
solve satisfy;

╰─❯ minizinc --solver com.google.or-tools model.mzn                                                                                                                                                            ─╯
x = 10;
y = 22;
----------

Describe the solution you'd like

It would be great to support this automatically, so that the same minizinc file can be used for different backends. I guess one could use the existing annotation system to specify the precision with something like:

var 1.0..3.0: x :: precision=0.10

Describe alternatives you've considered

Re-write all the file by manually multiplying float numbers to make them integers. Really tedious, error-prone, and harder to maintain if we want to support other backends.

Additional context

Since I'm not sure if this must be solved here or directly in MiniZinc by compiling it differently for backends that do not support floating points, I also reported it here MiniZinc/libminizinc#847

[lperron]

won't fix.

[tobiasBora]

Too bad. Hopefully MiniZinc can do it directly.

[CervEdin]

If I'm not mistaken, work on something like is being explored in shackle