include "globals.mzn"; 

%Données

%Ensemble des valeurs possibles
set of int: X = 0..9;

%Ensemble des couleurss possibles
set of int: C = 1..3;

%Nombre de chiffres dans le code
int: n = 5;

%Variables

%Valeur de chaque chiffre du code
array [1..n] of var X: x;

%Couleur de chaque chiffre du code
array [1..n] of var C: c;

%Nombre d'occurence de chaque chiffre dans le code
array [1..10] of var 0..2: count;

%Contraintes

%Les chiffres sont en ordre croissant
constraint forall (i in 1..n-1) (x[i] <= x[i+1]);

%Les chiffres autres que 5 sont noir ou blanc
constraint forall (i in 1..n where x[i] != 5)(c[i] <= 2);

%Les 5 sont verts
constraint forall (i in 1..n where x[i] == 5)(c[i] = 3);

%Les chiffres autres que 5 qui apparaissent deux fois sont d'abord noir puis blanc
constraint forall (i in 1..n-1 where x[i] == x[i+1] /\ x[i] != 5)(c[i] = 1 /\ c[i+1] = 2);

%count est le nombre d'occurence de chaque valeur dans le code (ce qui impose qu'une valeur apparaît au plus 2 fois)
constraint global_cardinality(x, X, count);

%Deux chiffres du code ont la même valeur
constraint count(count, 2) >= 1;

%Les trois premiers chiffres du code sont les seuls chiffres adjacents ayant la même couleur
constraint c[1] == c [2] /\ c[2] == c [3] /\ forall (i in 3..n-1)(c[i] != c[i+1]);

%La somme des valeurs des trois derniers chiffres vaut 7
constraint x[n-2] + x[n-1] + x[n] = 7;

solve satisfy;

output [show(x) ++ show(c) ++ show(count)];