What are these `float_div` and `float_times` constraints in the FlatZinc file?

Question

I just tried to run mzn2fzn over the following MiniZinc file:

var float: x1;
var float: y1;
var float: x2;
var float: y2;
constraint (x1 / y1) = 6.0;
constraint x2 * y2 <= 5.0;
solve satisfy;

This is the resulting FlatZinc file:

var -1.7976931348623157e+308..5.0: FLOAT____00001 :: is_defined_var :: var_is_introduced;
var float: x1;
var float: x2;
var float: y1;
var float: y2;
constraint float_div(x1, y1, 6.0);
constraint float_times(x2, y2, FLOAT____00001) :: defines_var(FLOAT____00001);
solve satisfy;

The version of mzn2fzn is as follows:

~$ mzn2fzn --version
G12 MiniZinc to FlatZinc converter, version 1.6.0
Copyright (C) 2006-2012 The University of Melbourne and NICTA

I have the following questions:

• what is the float_div constraint, which does not seem to be mentioned by the FlatZinc 1.6 Standard?
• what is the float_times constraint, which does not seem to be mentioned by the FlatZinc 1.6 Standard?

Does any FlatZinc solver actually support them?

---

N.B. I actually found trace of these functions in the docs for FlatZinc 2.2.0, however, I don't understand why these are generated by the version 1.6 of mzn2fzn when its documentation does not seem to mention either of them.

Answer 1

It seems to be oversight in the documentation of FlatZinc 1.6 that the constraints float_div and float_times are not documented. These constraints are necessary parts of the FlatZinc built-ins to be understood by solvers with support for floating point variables. They cannot be rewritten into other constraints that are among the FlatZinc builtins and that's why the compiler will use them. I would note that int_div and int_times are documented within the documentation of the old version of FlatZinc and the meaning of the constraints can be extrapolated from these constraints. (I'm also under the impression that their meaning has not changed in the conversion to FlatZinc 2.2.0)

Gecode, the CP solver shipped with MiniZinc, has support for these constraints.