MiniZinc / libminizinc

The MiniZinc compiler
http://www.minizinc.org
Other
519 stars 81 forks source link

Fake floating numbers using integers when the backend does not support them #847

Open tobiasBora opened 2 months ago

tobiasBora commented 2 months ago

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;
----------

It would be great to support this, ideally by specifying the wanted precision via some annotations next to the number like:

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

NB: I also reported it here https://github.com/google/or-tools/issues/4375 in case it is easier to support this directly on OR-tools side… but I guess this would be less generic (maybe other backends would also benefit from a generic translation) Google does not plan to support this on their side, so it means that only MiniZinc can do something here.