Minizinc 2.8.1 compatibility issues

[IgnaceBleukx]

Dear,

I'm using Choco v 4.10.14 through the MiniZinc interface on MiniZinc v.2.8.1 and I am encountering an error when trying to compile a model with an element constraint.

Below is a minimal working example:

include "globals.mzn";

var bool: x;
var 1..5: idx;
array[1..5] of var bool: arr;

constraint element(idx, arr, x);
% constraint x == arr[idx]; % same result

Output:

[flatzinc_builtins:436.78-107](err:/snap/minizinc/896/share/minizinc/std/flatzinc_builtins.mzn?line=436&column=78):
MiniZinc: type error: Type array[int,int] of var float is not allowed in as a FlatZinc builtin argument, arrays must be one dimensional
[flatzinc_builtins:442.76-110](err:/snap/minizinc/896/share/minizinc/std/flatzinc_builtins.mzn?line=442&column=76):
MiniZinc: type error: Type array[int,int] of var set of int is not allowed in as a FlatZinc builtin argument, arrays must be one dimensional
Process finished with non-zero exit code 1.

The problem remains when trying to change the type of the array or x-variable to int.

Kind regards, Ignace

[cprudhom]

Hello

Can you compile your model with choco and show it here?

[IgnaceBleukx]

Hi, The model doesn't actually compile. I get the error while MiniZinc is compiling to FlatZinc. For any other solver I have installed (gecode, chuffed and OR-tools) compiles fine.

After testing some more I discovered it is actually not the Element constraint that causes the error but just compiling any model for Choco on v.2.8.1 of MiniZinc.

For version 2.8.0 it does work fine. So maybe this is a MiniZinc bug and not a bug in the Mzn->Choco interface?

Kind regards, Ignace

[cprudhom]

Thank you for the investigation. I have the version tagged 2.8.0 installed on my computer, that explains why I didn't reproduce the bug. Did you create an issue on the MiniZinc issue tracker?

[IgnaceBleukx]

Hi, I opened the issue on their tracker as well.

Kind regards, Ignce

[Dekker1]

This issue stems from a new check in the MiniZinc compiler that ensures that all predicates that are "solver builtins" (i.e., calls no longer being rewritten), are valid FlatZinc.

Although there are no invalid declarations that are declared in the Choco library itself. It currently does not have any definitions for the following declarations.

predicate array_var_float_element2d_nonshifted(var int: idx1, var int: idx2, array[int,int] of var float: x, var float: c);

predicate array_var_set_element2d_nonshifted(var int: idx1, var int: idx2, array[int,int] of var set of int: x, var set of int: c);

These definitions would be expected in redefinitions-2.5.2.mzn.

Likely it was the intention to have the same definitions as the MiniZinc standard library:

predicate array_var_float_element2d_nonshifted(var int: idx1, var int: idx2, array[int,int] of var float: x, var float: c) =
  let {
    int: dim = card(index_set_2of2(x));
    int: min_flat = min(index_set_1of2(x))*dim+min(index_set_2of2(x))-1;
  } in array_var_float_element_nonshifted((idx1*dim+idx2-min_flat)::domain, array1d(x), c);

predicate array_var_set_element2d_nonshifted(var int: idx1, var int: idx2, array[int,int] of var set of int: x, var set of int: c) =
  let {
    int: dim = card(index_set_2of2(x));
    int: min_flat = min(index_set_1of2(x))*dim+min(index_set_2of2(x))-1;
  } in array_var_set_element_nonshifted((idx1*dim+idx2-min_flat)::domain, array1d(x), c);

Note that it is expected that solvers override all predicates in redefition-*.mzn files.

[cprudhom]

Thank you @Dekker1 for the details. It's always a question for me, when a new version of MiniZinc arrives, to know what I can and should implement. Are there guidelines I can follow?

[Dekker1]

Yes, I'm sorry that this hasn't always been very clear. We've done our best to keep the changes for solvers as minimal as possible, but there have been a lot of (unspoken) assumptions about MiniZinc solver libraries and FlatZinc that we've been trying to make more explicit.

Apart from the forced simple types (float, int, bool, string) that the compiler will now enforce automatically. The idea is still that a solver library can override files in the MiniZinc standard library. A few versions ago we've made the main part (the globals) a lot simpler to override. Solver implementations are now only supposed to override fzn_<global>.mzn files, which makes sure that the reification redefinition is always available, and these file only contains a simple override.

The redefitinon*.mzn don't follow the same rules (yet), so when you override these files, you have to be sure that all definitions in the original file are in the overriden solver library file.

There are still new globals being added to the standard library, these are mentioned in the changelog, and new fzn_<global>.mzn files will be available from that release to override. For MiniZinc 2.x we are not considering any current changes to the “FlatZinc built-ins” system, so it is unlikely that more redefinition*.mzn. In future MiniZinc 3.x versions, my hope is that we can make the built ins work the same way as the globals w.r.t. solver redefitniions.