How to propagate set of int domains during mzn2fzn conversion?

Question

I have the following MiniZinc code sample:

include "globals.mzn";

var int: i;
array[-3..3] of var set of 1..10: x;
var set of 1..100: y;

constraint element(i, x, y);

solve satisfy;

output [
    show(i), "\n",
    show(x), "\n",
    show(y), "\n",
];

The mzn2fzn command, executed with the standard library, outputs the following FlatZinc code:

var set of 1..10: X_INTRODUCED_0_;
var set of 1..10: X_INTRODUCED_1_;
var set of 1..10: X_INTRODUCED_2_;
var set of 1..10: X_INTRODUCED_3_;
var set of 1..10: X_INTRODUCED_4_;
var set of 1..10: X_INTRODUCED_5_;
var set of 1..10: X_INTRODUCED_6_;
var -3..3: i:: output_var;
var set of 1..10: y:: output_var;
var 1..7: X_INTRODUCED_9_ ::var_is_introduced :: is_defined_var;
array [1..7] of var set of int: x:: output_array([-3..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_];
constraint array_var_set_element(X_INTRODUCED_9_,[X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_],y):: defines_var(y);
constraint int_lin_eq([1,-1],[i,X_INTRODUCED_9_],-4):: defines_var(X_INTRODUCED_9_):: domain;
solve  satisfy;

Here, notice that originally y was declared to be a set of 1..100 in the MiniZinc model, but mzn2fzn correctly propagates the bounds on the elements of array x onto y, so that the FlatZinc model declares y to be a set of 1..10.

Now, I want to customize the content of element_set.mzn so that my own predicate is called when element_set is used, so I changed it to be as follows:

predicate element_set(var int: i, array[int] of var set of int: x,
        var set of int: y) =
    min(index_set(x)) <= i /\ i <= max(index_set(x)) /\
    optimathsat_element_set(i, x, y, index_set(x));

predicate optimathsat_element_set(var int: i,
                                  array[int] of var set of int: x,
                                  var set of int: y,
                                  set of int: xdom);

However, this code will not propagate the bounds on the elements of array x onto y, so the resulting FlatZinc file has y still declared to be a set of 1..100:

predicate optimathsat_element_set(var int: i,array [int] of var set of int: x,var set of int: y,set of int: xdom);
var set of 1..10: X_INTRODUCED_0_;
var set of 1..10: X_INTRODUCED_1_;
var set of 1..10: X_INTRODUCED_2_;
var set of 1..10: X_INTRODUCED_3_;
var set of 1..10: X_INTRODUCED_4_;
var set of 1..10: X_INTRODUCED_5_;
var set of 1..10: X_INTRODUCED_6_;
var -3..3: i:: output_var;
var set of 1..100: y:: output_var; %%% OFFENSIVE LINE %%%
array [1..7] of var set of int: x:: output_array([-3..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_,X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_,X_INTRODUCED_6_];
constraint optimathsat_element_set(i,x,y,-3..3);
solve  satisfy;

I would like to know if anyone knows what is the correct encoding for propagating the domain of x over y. I managed to do this for other element_T constraints, but I am unable to find an elegant solution for element_set, because I can't find the proper builtins for doing this.

In other words, I would like to get

var set of 1..10: y:: output_var;

instead of

var set of 1..100: y:: output_var;

How would I do that?

Answer 1

The family of element/element_T predicates are internally mapped onto the family of element/element_T functions.

In MiniZinc version 2.0.2 and above, these functions are mapped on the following predicates:

% This file contains redefinitions of standard builtins for version 2.0.2
% that can be overridden by solvers.

...    

predicate array_var_bool_element_nonshifted(var int: idx, array[int] of var bool: x, var bool: c) =
  array_var_bool_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

predicate array_var_int_element_nonshifted(var int: idx, array[int] of var int: x, var int: c) =
  array_var_int_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

predicate array_var_float_element_nonshifted(var int: idx, array[int] of var float: x, var float: c) =
  array_var_float_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

predicate array_var_set_element_nonshifted(var int: idx, array[int] of var set of int: x, var set of int: c) =
  array_var_set_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

The best solution is to override these predicates instead of messing with element/element_T ones.

Answer 2

Although it is a little hard to find, the domain of the index is actually propagated in the MiniZinc definition of the element function. The definition is found in builtins.mzn, as is as follows:

function var set of int: element(var int: idx, array[int] of var set of int: x) =
  if mzn_in_root_context(idx) then let {
    constraint idx in index_set(x)
  } in element_t(idx,x)
  elseif (has_bounds(idx) /\ lb(idx) >= min(index_set(x)) /\ ub(idx) <= max(index_set(x))) then
    element_t(idx,x)
  else let {
    constraint idx in index_set(x)
  } in element_mt(idx,x)
  endif;

You can see that your element constraint is evaluated to be in the first if-then branch. The more important question is, why is the element constraint so complicated. The answer is that it has to do with undefinedness.

Say we have an array[1..3] of int: a, then what does a[4] evaluate to? It might seem easy to make such a thing illegal, but what about the expression a[i] > 5 \/ i > 10. This could be a well thought out model that should be satisfiable for i = 11. In MiniZinc these illegal values are called undefined and are bubbled up to the nearest boolean expression to be false.

Now when we look back at the element constraint we can understand that in the root context, like in your example, we can just enforce the domain and use the "safe" element constraint. Similarly if the bounds of the index are smaller than the array bounds we can use the "safe" element constraint, but if the bounds are bigger we use the "unsafe" element constraint and make sure that true is only returned when the value is defined.

I would suggest you either use a similar approach or redefine later stage predicates. (It's possible to redefine array_var_set_element instead)

More information about undefinedness in MiniZinc can be found in the following paper:

Frisch, A. M., & Stuckey, P. J. (2009). The Proper Treatment of Undefinedness in Constraint Languages. CP, 5732, 367-382.

MiniZinc uses relational semantics.