/* 

  Global constraint alldifferent_interval in Picat.

  From Global Constraint Catalogue
  http://www.emn.fr/x-info/sdemasse/gccat/Calldifferent_interval.html
  """
  
  Enforce all variables of the collection VARIABLES to belong to 
  distinct intervals. The intervals are defined by 
    [SIZE_INTERVAL*k, SIZE_INTERVAL*k+SIZE_INTERVAL-1] where k is an integer.
  
  Example
      (〈2,3,10〉,3)
  
  In the example, the second argument SIZE_INTERVAL=3 defines the 
  following family of intervals [3*k, 3*k+2], where k is an integer. 
  Since the three variables of the collection VARIABLES take values that 
  are respectively located within the three following distinct intervals 
  [0, 2], [3, 5] and [9, 11], the alldifferent_interval constraint holds.
  """


  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 = 3,
  X = new_list(N),
  X :: 1..10,
  Intervals = new_array(N,2),
  Intervals :: 0..10*2,
  
  SizeInterval :: 1..9,

  X = [2,3,10],

  alldifferent_interval(X, SizeInterval, Intervals),
  SizeInterval #= 3,

  Vars = X ++ Intervals,
  solve(Vars),
  
  println(x=X),
  println(sizeInterval=SizeInterval),
  println(intervals=Intervals),
  nl,
  fail,

  nl.


go => true.


alldifferent_interval(Variables, SizeInterval, Intervals) =>
  N = Variables.len,
  all_different(Variables),

  % interval[i] > interval[i-1]
  foreach(I in 2..N) 
     Intervals[I,1] #> Intervals[I-1,2]
  end,
  % ensure the size of interval 
  % and check that x[i] is in the i'th interval
  foreach(I in 1..N) 
    Intervals[I, 2] - Intervals[I, 1] #= SizeInterval - 1,
    Variables[I] #>= Intervals[I, 1],
    Variables[I] #<= Intervals[I, 2]      
  end,
  % get the k (redundant)
  sum([Intervals[K,1] #= SizeInterval*K #/\ Intervals[K,2] #= SizeInterval*K+SizeInterval-1 : K in 1..N]) #>= 0.