Feature request: lazy evaluation (short-circuit)

[dan1221]

The MiniZinc Handbook index doesn't mention lazy evaluation, although Section 4.1.7.3 "If-then-else expressions" says:

If the if expression is par bool then evaluation of if-then-else expressions is lazy: the condition is evaluated, and then only one of the then and else branches are evaluated, depending on whether the condition succeeded or failed. This is not the case if it is var bool.

Is there a way to force lazy (short-circuit) evaluation of boolean operations, even when they are "var bool", such as to enforce an alldifferent predicate before calling an inverse function?

This is related to issue %607, where I resorted to calling arg_sort because I don't see a way to enforce alldifferent before calling inverse.

[zayenz]

It is important to note that in the semantics of MiniZinc, there is not really any "before"-relationship between constraints. MiniZinc translates to a flat list of constraints for the selected solver (can be viewed using the "Compile" option in the MiniZinc IDE).

Many constraint can be conditionally valid using reification (or be decomposed into something that is), which is what an if-then-else uses for the translation.

What is the exact problem that you have observed that you are trying to solve?

[dan1221]

The exact problem I'm trying to solve is in Version 2 of issue #615. Originally the predicate was:

predicate equals_inverse(array[N] of var N: b) =  % involution 
  alldifferent(b) /\ (b = inverse(b));   % using inverse doesn't work because the /\ isn't short-circuited

But I had to change inverse to arg_sort as shown below, because the parameter to inverse needs to be alldifferent.

predicate equals_inverse(array[N] of var N: b) =  % involution 
  alldifferent(b) /\ (b = arg_sort(b)); 

[zayenz]

I'm not sure what you mean by not working here. This model produces the expected solutions as far as I can see.

include "globals.mzn";

int: n = 4;
set of int: Domain = 1..n;

array[Domain] of var Domain: x;

predicate equals_inverse(array[Domain] of var Domain: b) =  % involution 
  alldifferent(b) /\ (b = inverse(b));

constraint equals_inverse(x);

solve satisfy;

output [show(x)];

With that said, this predicate is a bit odd: inverse(b, b) implies all_different so the all_different is not strictly needed.

Also, worth noting is that inverse(x, x) is available as it's own global constraint named symmetric_all_different.

[dan1221]

By not working, I mean that this code (using inverse instead of arg_sort)

% Version 2b: count involutions, a permutation that equals its inverse; OEIS:A000085
include "inverse_fn.mzn"; 
include "arg_sort.mzn";

int: n;
set of int: N = 1..n;

predicate equals_inverse(array[N] of var N: b) =  % involution 
%  alldifferent(b) /\ (b = arg_sort(b));  % had to switch to arg_sort instead of inverse #609
    alldifferent(b) /\ (b = inverse(b));  % had to switch to arg_sort instead of inverse #609

var int: total =   % this is both awkward and inefficient
if n==2 then
   sum(i,j in 1..n)(equals_inverse([i,j]))  
elseif n==3 then
   sum(i,j,k in 1..n)(equals_inverse([i,j,k]))         
elseif n==4 then
   sum(i,j,k,l in 1..n)(equals_inverse([i,j,k,l]))
elseif n==5 then
   sum(i,j,k,l,m in 1..n)(equals_inverse([i,j,k,l,m]))
elseif n==6 then
   sum(i,j,k,l,m,q in 1..n)(equals_inverse([i,j,k,l,m,q]))
elseif n==7 then
   sum(i,j,k,l,m,q,r in 1..n)(equals_inverse([i,j,k,l,m,q,r]))
else 0
endif;

solve satisfy;

output ["number of solutions is ", show(total)];

gives a slew of warnings, say when n=3:

model29:13.1-14
  in variable declaration for 'total'
model29:14-1.27-5
  in if-then-else expression
model29:17.4-46
  in call 'sum'
  in array comprehension expression
    with i = <expression>
    with j = <expression>
    with k = <expression>
  in call 'bool2int'
  in call 'equals_inverse'
model29:10.5-39
  in binary '/\' operator expression
  in binary '=' operator expression
  in call 'inverse'
Warning: undefined result becomes false in Boolean context
  (inverse on non-contiguous set of values is undefined)

[zayenz]

As noted in #615, the above code expands to calls with fixed values. In this case, it for example warns about inverse([1,1,4,4, 5]) which has a non-contiguos set of value and is therefore not valid as an argument to inverse.

This is not really about short-circuiting but about the MiniZinc code having an issue that should be fixed. MiniZinc is simply not made to be a programming language with standard sequential operational semantics.

Now, if you still want to run the above code for some reason even though it is not using a solver, there are two things you could do to fix it. The first is to use either

predicate equals_inverse(array[N] of var N: b) =  % involution 
    (b = inverse(b)) default false;

or

predicate equals_inverse(array[N] of var N: b) =  % involution 
    (symmetric_all_different(b)) default false;

Both of these use a default value that takes care of of the undefined result from the inverse or symmetric_all_different.

The other would be to change your loops to

sum(i,j,k in 1..n where i != j /\ j != k /\ k != i)(equals_inverse([i,j,k]))

or even

sum(i,j,k in 1..n where all_different[i,j,k]))(equals_inverse([i,j,k]))

This works because the filtering of the generator is done before the expansion of the predicate call is made.

Still, this is the wrong method to solve the problem, so neither "solution" is actually useful.