You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
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
]
I found that in the following model
the comprehension in the final constraint is rewritten to
Note, however, that the
shape[k[s]]
access is no longer protected against the0
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
The text was updated successfully, but these errors were encountered: