MiniZinc
Constant false if statements slow compilation
int: N = 10;
int: T = 6;
array [1..10, 1..N, 1..N] of var bool: A;
constraint forall (t in 2..T, r,c in 2..N-1) (
A[t,r,c] =
if false then false else
A[t-1,r,c] \/
A[t,r-1,c] \/ A[t,r+1,c] \/ A[t,r,c-1] \/ A[t,r,c+1]
endif
);
This is a bit slow to compile (at -O1), and the time seems to grow with T3. Removing the surrounding if false makes it much faster.
The problem here is that removing the surrounding if has a different meaning:
A[t,r,c] =
if false then false else
A[t-1,r,c] \/
A[t,r-1,c] \/ A[t,r+1,c] \/ A[t,r,c-1] \/ A[t,r,c+1]
endif
is not equivalent to
A[t,r,c] =
A[t-1,r,c] \/
A[t,r-1,c] \/ A[t,r+1,c] \/ A[t,r,c-1] \/ A[t,r,c+1]
because the = operator binds more tightly than \/. Once you add parentheses like this:
A[t,r,c] =
(A[t-1,r,c] \/
A[t,r-1,c] \/ A[t,r+1,c] \/ A[t,r,c-1] \/ A[t,r,c+1])
both versions take roughly the same time to compile.
Oh right, sorry. I was hoping to use the if/parenthesized version for larger T, but the compilation time grows too quickly. Is that part expected, or is there a workaround?
Unfortunately this code is triggering a heuristic in the compiler that tries to aggregate disjunctions, which become longer and longer here. We'll need to come up with a tweak to that heuristic to essentially disable aggregating through recursively defined arrays.
One workaround you could use is to split up the constraint into two steps:
int: N = 10;
int: T = 6;
array [1..10, 1..N, 1..N] of var bool: A;
array [1..10, 1..N, 1..N] of var bool: A2;
constraint forall (t in 2..T, r,c in 2..N-1) (
A2[t,r,c] =
(A[t-1,r,c] \/
A[t,r-1,c] \/ A[t,r+1,c] \/ A[t,r,c-1] \/ A[t,r,c+1])
);
constraint A = A2;
That way, during the forall the compiler can't see the definitions of the A[t-1,r,c] yet. From what I can see, the result should be okay (i.e., the compiler gets rid of the additional A2 variables.