Checking for items in a MiniZinc array

Question

I want to create two arrays in MiniZinc with the same items, not necessarily in the same order. Here, every item in A0 should also be in A1:

array[1..3] of var int:A0;
array[1..3] of var int:A1;

constraint forall(A2 in A0)(
  (A2 in A1) /\ A2 < 5
 );

But here, there seems to be a type error:

MiniZinc: type error: type error in operator application for `'in''. No matching operator found with left-hand side type `var int' and right-hand side type `array[int] of var int'

How is it possible to check if an array contains the same item that is in another array?

Answer 1

Edit: There is an array2set in the file builtins.mzn but it is not documented in https://www.minizinc.org/doc-2.4.2/ .

The following model works for most FlatZinc solvers such as Gecode, Google-OR-tools, Choco, PicatSAT, and JaCoP, but not for Chuffed (see below). Note the include of "nosets.mzn" so that solvers without innate support for set variables can run the model. Also, I added a smaller domain of A0 and A1 for easier testing.

include "nosets.mzn"; % Support for set variables for all solvers
array[1..3] of var 0..10: A0;
array[1..3] of var 0..10: A1;

constraint
   forall(A2 in A0)( 
     A2 in array2set(A1) /\ A2 < 5
   )
   /\
   forall(A2 in A1)(
     A2 in array2set(A0) /\ A2 < 5
   );

   solve satisfy;

   output [ "A0: \(A0) A1: \(A1)\n" ];

However, some solvers don't like this:

• Chuffed: Throws "Error: Registry: Constraint bool_lin_eq not found in line no. 101"

Even later note: If the domains is var int (instead of my var 0..10) then MiniZinc croaks with a weird (and long) error:

...
in array comprehension expression
  comprehension iterates over an infinite set

So array2set seems to require that the variable domains must be bounded.

This is the first answer Here is an approach that seems to work, i.e. using exists and check for element equality:

constraint forall(A2 in A0)(
              exists(i in 1..3) ( A2 = A1[i] /\ A2 < 5)
);

Note: This constraint only ensures that the elements in A0 is in A1. Thus there might be elements in A1 that is not in A0. E.g.

A0: [1,1,4]

A1: [1,4,3]

I guess that you also want the converse i.e. that all elements in A1 is in A0 as well:

constraint forall(A2 in A1) (
   exists(i in 1..3) ( A2 = A0[i] /\ A2 < 5)
);

Note: The following DOES NOT work but would be nice to have. Both yield the error MiniZinc: internal error: var set comprehensions not supported yet.

% idea 1
constraint forall(A2 in A0)(
   A2 in {A1[i] | i in 1..3} /\ A2 < 5
);

% idea 2
constraint forall(A2 in A0) (
     A2 in {a | a in A1} /\ A2 < 5         
);