Search code examples
minizincflatzinc

How to propagate set of int domains during mzn2fzn conversion?

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?

Solution

  • 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.