/* 

  Global constraint max_n in Picat.

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

      max_n(MAX,RANK,VARIABLES)

  Purpose

      MAX is the maximum value of rank RANK (i.e., the RANKth largest 
      distinct value) of the collection of domain variables VARIABLES. 
      Sources have a rank of 0.

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

      The max_n constraint holds since its first argument MAX=6 is 
      fixed to the second (i.e., RANK+1) largest distinct value 
      of the collection <3, 1, 7, 1, 6>.
  """

  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, 
  TMax :: 1..7,

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

  Variables = [3,1,7,1,6],
  % TMax #= 6,
  Rank #= 1,
  
  max_n(TMax, Rank, Variables),

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

  println(variables=Variables),
  println(tmax=TMax),
  println(rank=Rank),
  nl,
  fail,
  
  nl.

go => true.


%
% This is probably way too complicated, but in some way we must
% handle duplicate values.
%
max_n(TMax, Rank, Variables) =>
  N = Variables.len,
  FirstPos = new_list(N),
  FirstPos :: 0..1,

  % t_max must be in variables (needed for multidirection) 
  sum([TMax #= 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 TMax?
  Rank #= sum([FirstPos[I] #= 1 #/\ Variables[I] #> TMax : I in 1..N]).