Out-of-bounds error in "then" branch goes undetected

[informarte]

int: M = 2;
int: N = 3;
array[1..M] of var 1..N: length; % We consider M tours of maximum length N
array[1..M, 1..N] of var int: places; % Only places[i, j] with j <= length[i] are valid

% In the valid part of places[i], adjacent places must be different
constraint
forall(i in 1..M, j in 1..N-1) (
if j < length[i] then places[i, j] != places[i, j + 1] else true endif
);

% Same constraint as above except for undetected out-of-bounds error ("j - 1" instead of "j + 1")
constraint
forall(i in 1..M, j in 1..N-1) (
if j < length[i] then places[i, j] != places[i, j - 1] else true endif
);

% Now without if/then/endif: Out-of-bounds error is detected properly
constraint
forall(i in 1..M, j in 1..N-1) (
places[i, j] != places[i, j - 1]
);

solve satisfy;

[informarte]

I noticed the above problem in both MiniZinc 2.0.2 and 2.0.6.

The same bug might lurk in the implementation of else but I did not check.

For those j that should cause an out-of-bounds error, flattening will not produce a reified constraint for the then branch, only for the condition.

[guidotack]

This may be an artefact of MiniZinc's relational semantics (I'll have to look at the code more closely). You are using a variable in the condition of the if, which can be rewritten as

constraint forall(i in 1..M, j in 1..N-1) (
  j < length[i] -> places[i, j] != places[i, j - 1]
);

In a Boolean expression like this, array accesses that are out of bounds simple become "false" in the closest Boolean context. That's expected MiniZinc behaviour.

[informarte]

Section 10.3 (Partial Array Access) of the MiniZinc 2.0 spec distinguishes two cases for array indices: fixed and unfixed values. Your statement pertains to unfixed array values. For fixed array values a run-time error is required.

[guidotack]

We will need to update the spec. The current behaviour is consistent with MiniZinc implementations back to version 1.6 (at least), e.g. the following code always compiled without warnings or errors:

array[1..3] of var 1..10: x;
var bool: b;
constraint forall (i in 1..10) (x[i]=1 -> b);
solve satisfy;

We have argued (internally) about whether these should be compile time errors or not but there are arguments for and against that. The current plan is to turn them into warnings and let the user switch those warnings off individually by annotating the corresponding array accesses.

[informarte]

Could you also add a compiler switch to turn these warnings into normal out-of-bound errors? Knowing that stupid programming errors will be detected by the compiler would make me feel much better ...

[guidotack]

You can use the -Werror compiler switch to turn warnings into errors.