How to produce a reified `array_int_maximum` in Flatzinc output?

78 views Asked by At

Given the following minizinc program:

var 0..4: a;
var 0..5: b;
var -5..2: c;
var -8..-3: d;
var 0..8: m;
var bool: r;
constraint r <-> m = max([a,b,c,d]);
solve satisfy;

and the redefinitions-2.0.mzn file

predicate array_int_maximum(var int: m, array[int] of var int: x);                                      
predicate array_int_maximum_reif(var int: m, array[int] of var int: x, var bool: r);                    
predicate array_int_maximum_imp(var int: m, array[int] of var int: x, var bool: r); 

I would expect to get a reified version as output of flattening, but I do get:

predicate array_int_maximum(var int: m,array [int] of var int: x);
predicate int_eq_imp(var int: a,var int: b,var bool: r);
var 0..4: a:: output_var;
var 0..13: b:: output_var;
var -5..2: c:: output_var;
var -8..-3: d:: output_var;
var 0..16: m:: output_var;
var bool: r:: output_var;
var -8..13: X_INTRODUCED_1_ ::var_is_introduced :: is_defined_var;
array [1..4] of var int: X_INTRODUCED_0_ ::var_is_introduced  = [a,b,c,d];
constraint array_int_maximum(X_INTRODUCED_1_,X_INTRODUCED_0_):: defines_var(X_INTRODUCED_1_);
constraint int_eq_imp(m,X_INTRODUCED_1_,r);
solve  satisfy;

How and where do I add the information that I do support the reif and imp version of this predicate, and therefore have a possibly faster handling than the automatic translation? (duplicate of this unsolved issue)

1

There are 1 answers

3
Dekker1 On

The simple answer is that array_int_maximum_reif is currently unused. It would have to be generated by the compiler, but the compiler instead chooses to just create a array_int_maximum constraint and use an int_eq_reif constraint.

It is still not fully clear when to reify a function. It is pretty clear that total functions should never be reified as it offers no additional benefits. For partial functions it is still a question when it is a good idea. max is a partial function in MiniZinc, but it is made total before it makes in to array_int_maximum. Hopefully there will be more information on this issue soon.