Invalid internally rewritten comprehension

I found that in the following model

int: nshapes = 2;
set of int: SHAPE = 1..nshapes;
set of int: SHAPE0 = 0..nshapes;
array[SHAPE] of set of int: shape = [{1,2},{3,4}];
set of int: SHIP = 1..3;
array[SHIP] of var SHAPE0:  k;

constraint k = [0, 1, 2];
constraint forall(s in SHIP where k[s] != 0, roff in shape[k[s]])(true);

the comprehension in the final constraint is rewritten to

[forall([k[s]!=0,roff in shape[k[s]]]) -> true | s in SHIP, roff in ub(shape[k[s]])]

Note, however, that the shape[k[s]] access is no longer protected against the 0 access, and causes unsatisfiability.

We should either not have rewritten the constraint in this case, or we should have short-circuited the evaluation of forall

Isn't the undefinedness caused because we evaluate ub(shape[k[s]]) for the generator? I don't see how we can short-circuit the forall to make that not get evaluated.

Actually, I'm not totally sure this is even wrong behaviour (at least according to the MiniZinc spec).

Since we say that iterators with var where clauses are syntactic sugar which move the condition into an if-then-else in the comprehension template, then we wouldn't have the k[s] != 0 guarding against the undefined access in the evaluation of the roff generator.

It is annoying that it is different from the par case though, where we don't generate the s which has k[s] = 0 in the first place.

I think in general to implement the undefinedness semantics for var where clauses to match how we deal with the par case, we'd need to do something like transforming

[x | i in A where p, j in B where q]

Into

[
  % Where clause has to hold, or value is 'absent'
  if p /\ q then
    let {
      % Generators must be defined, or whole array is undefined
      constraint AA.1 /\ BB.1
    } in x
  else
    <>
  endif
|
  AA = (true, A) default (false, {0}),
  i in AA.2,
  BB = (true, B) default (false, {0}),
  j in BB.2
]

MiniZinc / libminizinc

Invalid internally rewritten comprehension #727