MiniZinc 2.7.0: length of dynamically created array does not work

[matsc-at-sics-se]

A colleague found the following. This model is unsat, but IMHO it should not be:

array[1..4] of var 0..1: xs;

var 0..4: n = length([x | x in xs where x=1]);

constraint n = 2;

[guidotack]

This is explained in the documentation under “hidden option types”: https://www.minizinc.org/doc-latest/en/optiontypes.html#hidden-option-types

[matsc-at-sics-se]

Right. Nevertheless, convincing a beginner that the following makes sense is a bit of a challenge:

array[1..4] of bool: xa :: add_to_output = [true, true, false, false];
int: xlen :: add_to_output = length([x | x in xa where x]);

array[1..4] of var bool: ya :: add_to_output;
int: ylen :: add_to_output = length([y | y in ya where y]);

solve :: bool_search(ya[1..2], input_order, indomain_max)
  satisfy;

bash-3.2$ minizinc foo.mzn
xa = [true, true, false, false];
xlen = 2;
ya = [true, true, false, false];
ylen = 4;

[PerMildner]

Perhaps a better reference to why this unexpected behavior is as designed is the specification of what array comprehensions mean. The specification of Simple Array Comprehensions says:

Array comprehensions are allowed over a variable set with finite type, the result is an array of optional type, with length equal to the cardinality of the upper bound of the variable set.