/* 

  Global constraint max_nvalue in Picat.

  From Global Constraint Catalogue
  http://www.emn.fr/x-info/sdemasse/gccat/Cmax_nvalue.html
  """
      max_nvalue<U+200B>(MAX,<U+200B>VARIABLES)<U+200B>

  Purpose

      MAX is the maximum number of times that the same value is taken by 
      the variables of the collection VARIABLES.

  Example
      (
      3, <
      var-9,
      var-1,
      var-7,
      var-1,
      var-1,
      var-6,
      var-7,
      var-7,
      var-4,
      var-9
      >
      )

      In the example, values 1, 4, 6, 7, 9 are respectively used 
      3, 1, 1, 3, 2 times. So the maximum number of time MAX that 
      a same value occurs is 3. Consequently the max_nvalue 
      constraint holds.

  Usage

      This constraint may be used in order to replace a set of 
      count or among constraints were one would have to generate 
      explicitly one constraint for each potential value. Also 
      useful for constraining the number of occurrences of the mostly 
      used value without knowing this value in advance and without 
      giving explicitly an upper limit on the number of occurrences 
      of each value as it is done in the global_cardinality constraint.
  """

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

  Variables = [9,1,7,1,1,6,7,7,4,9],
  % TMax #= 3,

  max_nvalue(TMax, Variables),

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

  println(variables=Variables),
  println(tmax=TMax),
  nl,
  fail,

  nl.

go => true.


max_nvalue(TMax, Variables) =>
   fd_max(Variables[1]) = Max,
   Occ = new_list(Max),
   Occ :: 0..Variables.len,
   global_cardinality2(Variables, Occ),
   TMax #= max(Occ).


%
% global_cardinality(A, Gcc)
%
% This version is bidirectional but limited:
%
% Both A and Gcc are (plain) lists.
%  
% The list A can contain only values 1..Max (i.e. the length of Gcc).
% This means that the caller must know the max values of A.
% Or rather: if A contains another values they will not be counted.
% 
global_cardinality2(A, Gcc) =>
   Len = length(A),
   Max = length(Gcc),
   Gcc :: 0..Len,
   foreach(I in 1..Max) count(I,A,#=,Gcc[I]) end.