Array constrained to constants but declared as unbound not solvable with CBC

[elKei24]

This probably is related to #404 and chuffed/chuffed#72, but I think not really a duplicate, because in this case even if the declaration domain is unbounded the "real" domain is not.

The following model can be solved with Gecode, but fails with CBC:

enum options = { A, B };
var options: choice;

array[options] of var int: values;
constraint values[A] = 1;
constraint values[B] = 2;

var int: value = values[choice];

Stacktrace

MiniZinc: evaluation error: 
  /home/…/minerror.mzn:8:
  in variable declaration for 'value'
  in array access
  /home/…/miniZinc-2.5.5/share/minizinc/std/stdlib/stdlib_internal.mzn:218:
  in if-then-else expression
  in let expression
  /home/…/miniZinc-2.5.5/share/minizinc/std/stdlib/stdlib_internal.mzn:220:
  in call 'element_t'
  /home/…/miniZinc-2.5.5/share/minizinc/std/stdlib/stdlib_internal.mzn:184:
  in let expression
  /home/…/miniZinc-2.5.5/share/minizinc/std/stdlib/stdlib_internal.mzn:187:
  in call 'array_var_int_element_nonshifted'
  /home/…/miniZinc-2.5.5/share/minizinc/linear/redefinitions-2.0.2.mzn:23:
  in call 'array_var_int_element'
  /home/…/miniZinc-2.5.5/share/minizinc/linear/redefinitions.mzn:405:
  in let expression
  /home/…/miniZinc-2.5.5/share/minizinc/linear/redefinitions.mzn:409:
  in let expression
  /home/…/miniZinc-2.5.5/share/minizinc/linear/redefinitions.mzn:413:
  in if-then-else expression
  /home/…/miniZinc-2.5.5/share/minizinc/linear/redefinitions.mzn:416:
  in binary '/\' operator expression
  in binary '>=' operator expression
  arithmetic operation on infinite value

The problem seems to be that the type of the array entries is the unbounded int, even if all the values are fixed to constants.

I understand that it would be better to not even use a decision array for values but to initialize it directly. However, the real model is a lot bigger and this notation makes it a lot easier to for example change the order of the enum entries.

[Dekker1]

The problem here is mostly still the same as #404. When the element constraint is evaluated the values of the values array are not yet known and cause an operation on infinity since the bounds are required for the decomposition. This is not caused by the initial infinite bound of the variables, but from the actual value when the element constraint is evaluated.

The misconception is that the MiniZinc model is processed in the order in which it is given, but this is not true. The MiniZinc compiler actually re-orders the model. This is mostly to ensure topological order so values are "declared" (and a domain is known) before they are used. In this case it causes the element in the value declaration to be processed before the constraints. This is illustrated by introducing trace statements:

enum options = { A, B };
var options: choice;

array[options] of var int: values;
constraint values[A] = trace("% process A\n", 1);
constraint values[B] = trace("% process B\n", 2);

var int: value = trace("% process element\n", values[choice]);

This model has the following output when using Gecode

% process element
% process A
% process B
choice = A;
values = array1d(options, [1, 2]);
----------

and it will only output % process element when using the linear library.

Ideally, all (functionally) defined variables should be assigned in their declaration, but we know that this is not always feasible. In the future it might be interesting to see if we can pick a better processing order in this scenario. In the meantime, you can manually influence the order by assigning all values in constraint items

enum options = { A, B };
var options: choice;

array[options] of var int: values;
var int: value;
constraint values[A] = trace("% process A\n", 1);
constraint values[B] = trace("% process B\n", 2);

constraint value = trace("% process element\n", values[choice]);

[elKei24]

@Dekker1 Great, thank you for the explanation and the workaround!