/* 

  Global constraint int_value_precede in Picat.

  From Global Constraint Catalogue
  http://www.emn.fr/x-info/sdemasse/gccat/Cint_value_precede.html
  """
  If value T occurs in the collection of variables VARIABLES then its first 
  occurrence should be preceded by an occurrence of value S.

  Example
      (0,1, <4, 0, 6, 1, 0>
  """


  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 :: 0..6,

  X = [4, 0, 6, 1, 0],
  % X = [0,2,3,0,2],  % no t -> ok
  % X = [4, 1, 6, 0, 0], % constraint don't hold
  % X = [_,_,2,3,_],
  int_value_precede(0, 1, X),

  solve(X),

  println(X),
  fail,


  nl.

go => true.

%
% precedence
% 
% Note: This implementation is different from Walsh's suggestion.
%
int_value_precede(S, T, X) =>
  N = X.len,
  SPos :: 1..N,
  TPos :: 1..N,
  ( % no t?  
    sum([X[I] #= T : I in 1..N])  #= 0
    #/\
    (SPos #= 1 #/\ TPos #= 1) % dummy values
    )
    #\/
    ( % there is a t
     SPos #< TPos
     #/\
     % % x[s_pos] = s
     % element(SPos,X,S)
     % #/\
     % % x[t_pos] = t
     % element(TPos,X,T)
     % #/\ 
     % % forall(i in lbx..ubx) (
     % %  (i <= x[s_pos]) -> x[i] != t
     % )
     sum([(I #<= S) #=> (X[I] #!= T) : I in 1..N, element(SPos,X,S), element(TPos,X,T)]) #= N
    ).