/* 

  Global constraint min_n in Picat.

  From Global Constraint Catalogue
  http://www.emn.fr/x-info/sdemasse/gccat/Cmin_n.html
  """
  Constraint

      min_n(MIN,RANK,VARIABLES)
  
  Purpose

      MIN is the minimum value of rank RANK (i.e., the RANKth 
      smallest distinct value) of the collection of domain variables 
      VARIABLES. Sources have a rank of 0.

  Example
      (3, 1, <3, 1, 7, 1, 6>)

      The min_n constraint holds since its first argument MIN=3 is 
      fixed to the second (i.e., RANK+1) smallest distinct value of 
      the collection <3, 1, 7, 1, 6>. Observe that identical values 
      are only counted once: this is why the minimum of order 1 is 
      3 instead of 1.
  """


  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,
  
  Variables = new_list(N),
  Variables :: 1..7,

  TMin :: 1..7,
  % rank start from 0, i.e. counts how many values 
  % are larger than TMin
  Rank :: 0..N-1,

  Variables = [3,1,7,1,6],
  % TMin #= 3,
  % Rank #= 1,

  min_n(TMin, Rank, Variables),

  Vars = Variables ++ [TMin,Rank],
  solve(Vars),

  println(variables=Variables),
  println(tmin=TMin),
  println(rank=Rank),
  nl,
  fail,

  nl.

go => true.


min_n(TMin, Rank, Variables) =>
  N = Variables.len,
  FirstPos = new_list(N),
  FirstPos :: 0..1,

  % TMin must be in variables (needed for multidirection) 
  sum([TMin #= Variables[I] : I in 1..N]) #>= 1,

  % set 1 in first_pos where variables[i] is the first
  % occurrence of this value.
  foreach(I in 1..N)
      sum([Variables[J] #= Variables[I] : J in 1..I-1]) #>= 1 #<=> FirstPos[I] #= 0
  end,
   % how many elements are larger than TMin?
  Rank #= sum([FirstPos[I] #= 1 #/\ Variables[I] #< TMin : I in 1..N]).