/* 

  All different with "explanation" in Picat.

  This model shows which values that are inconsistent with the all different
  constraint. Thus this constraint will never fail.

  Compare with 
   - http://hakank.org/picat/nvalue.pi (and the builtin predicate nvalue/2)
   - http://hakank.org/picat/nvalues.pi
  (global constraints for counting the number of different values in a list)


  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import cp.

main => go.


go ?=>
  N = 5,
  X = new_list(N),
  X :: 1..N,

  % Where are the conflicts?
  S = new_list(N),
  S :: 0..1,
  
  NumConflicts #= sum(S),
  
  alldifferent_explain(X, S),

  % NumConflicts #= 0, % alldifferent (i.e. no duplicates)
  % NumConflicts #<= 1, % we accept atmost 1 duplicated value

  Vars = X ++ S ++ [NumConflicts],
  solve(Vars),
  println(x=X),
  println(s=[I : I in 1..N, S[I] > 0]),
  println(numConflicts=NumConflicts),
  nl,
  fail,

  nl.


go => true.

alldifferent_explain(X, D) =>
   Len = X.len,
   fd_min_max(X[1],Min, Max), % domain of X
   foreach(I in Min..Max)
     % remove values not in X
     sum([X[J] #= I : J in 1..Len]) #= 0 #=> D[I] #= 0,
     % mark duplicates in S
     sum([X[A] #= I #/\ X[B] #= I : A in 1..Len, B in A+1..Len ]) #> 0 #<=> D[I] #= 1
   end.