MiniZinc - Constraint to enforce two arrays be equal

I'm trying to model a satisfaction problem with MiniZinc but I'm stuck at coding this constraint:

Given two arrays A and B of equal length, enforce that A is a permutation of B

In other words, I'm looking for a constraint that enforces [1,2,2]=[1,2,2] and also [1,2,2]=[2,2,1]. Informally, A and B have to be equal. The arrays are both defined on the same set of integers, in particular the set 1..n-1, for some n. Values in both A and B can be repeated (see example).

Is there such a global constraint in MiniZinc? Thank you.

Solution

Here is the predicate I tend to use for these cases. It requires an extra array (p) which contains the permutations from array a to array b.

/*
  Enforce that a is a permutation of b with the permutation
  array p.
*/
predicate permutation3(array[int] of var int: a,
                       array[int] of var int: p, 
                       array[int] of var int: b) =
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

A simple model using this:

include "globals.mzn"; 

int: n = 3;

array[1..n] of var 1..2: x;
array[1..n] of var 1..2: y;
array[1..n] of var 1..n: p;

/*
  Enforce that array b is a permutation of array a with the permutation
  array p.
*/
predicate permutation3(array[int] of var int: a,
                       array[int] of var int: p, 
                       array[int] of var int: b) =
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

                   
solve satisfy;

constraint
  x = [2,2,1] /\
  permutation3(x,p,y)
;

output [
  "x: \(x)\ny: \(y)\np: \(p)\n"
];

Output:

x: [2, 2, 1]
y: [1, 2, 2]
p: [3, 2, 1]
----------
x: [2, 2, 1]
y: [2, 1, 2]
p: [2, 3, 1]
----------
x: [2, 2, 1]
y: [1, 2, 2]
p: [3, 1, 2]
----------
x: [2, 2, 1]
y: [2, 1, 2]
p: [1, 3, 2]
----------
x: [2, 2, 1]
y: [2, 2, 1]
p: [2, 1, 3]
----------
x: [2, 2, 1]
y: [2, 2, 1]
p: [1, 2, 3]
----------
==========

There is an alternative formulation of this which don't requires the extra permutation p (it's defined inside the predicate):

predicate permutation3b(array[int] of var int: a,
                       array[int] of var int: b) =
  let {
    array[index_set(a)] of var index_set(a): p;
  } in
  forall(i in index_set(a)) (
    b[i] = a[p[i]]
  )
  /\
  all_different(p)
;

For the same problem, this will only output these 3 different solutions (the first model has more solutions since the the permutations differs).

x: [2, 2, 1]
y: [2, 2, 1]

----------
x: [2, 2, 1]
y: [2, 1, 2]

----------
x: [2, 2, 1]
y: [1, 2, 2]

----------
==========

Personally I tend to use the first version since I tend to want to output the permutation and like to have control over the variables.