% 
% Global constraint alldifferent_cst in MiniZinc.
%
% http://www.emn.fr/x-info/sdemasse/gccat/sec4.5.html
% """
% For all pairs of items​(VARIABLES[i], VARIABLES[j]) (i!=j) of the collection VARIABLES 
% enforce VARIABLES​[i].var+VARIABLES​[i].cst != VARIABLES​[j].var+VARIABLES[j].cst.
%
% 
% Example
%  (<
%     var−5	cst−0,​
%     var−1	cst−1,​
%     var−9	cst−0,​
%    var−3	cst−4
%  >
%  )
% 
% The alldifferent_cst constraint holds since all the expressions 
% 5+0=5, 1+1=2, 9+0=9 and 3+4=7 correspond to distinct values.
% """

% 
% 
% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc

% include "globals.mzn"; 

int: n;
array[1..n] of var 1..9: x;
array[1..n] of int: cst;
% array[1..n] of var int: z;

solve satisfy;

%
% all_different_cst for +
%
predicate all_different_cst(array[int] of var int: xx, array[int] of int: ccst) =
   let {
      int: nn = length(x),
      array[1..nn] of var int: z1 = [xx[i] + ccst[i] | i in 1..nn]
   }
   in
   forall(i,j in 1..nn where i != j) (
       z1[i] != z1[j]
   )
;


%
% all_different_cst for *
%
predicate all_different_cst_mult(array[int] of var int: xx, array[int] of int: ccst) =
   let {
      int: n = length(x),
      array[1..n] of var int: z2 = [xx[i] * ccst[i] | i in 1..n]
   }
   in
   forall(i,j in 1..n where i != j) (
       z2[i] != z2[j]
   )
;


constraint
   x = [5,1,9,3]
   /\
   all_different_cst(x, cst)
%   /\
%   all_different_cst_mult(x, cst)

;

%
%
%
n = 4;
% cst = [0,1,0,4];
cst = [1,2,1,4];