Re: [eclipse-clp-users] On stating a strange constraint

On 27/03/2023 10:51, Marco Gavanelli wrote:
> 
> Anyway, what about:
> 
> L[0] = 1
> 
> forall i>0
>      L[i] <= maxlist(L[0..(i-1)]) + 1
> ?
> 
> I hope the intuition is clear, with L[0..(1-i)] I mean the sublist of the first 
> i elements of the list L.


Here are two implementations, one of which may be faster in your circumstances.

% version using max(List)
precede1(Xs) :-
         eval_to_array(Xs, Xz),
         arity(Xz, N),
         Xz #:: 1..N,
         Xz[1] #= 1,
         ( for(I,2,N), param(Xz) do
             Xz[I] #=< max(Xz[1..I-1]) + 1
         ).

% incremental version using max(Xi,Xj)
precede2(Xs) :-
         eval_to_array(Xs, Xz),
         arity(Xz, N),
         Xz #:: 1..N,
         ( foreacharg(X,Xz), fromto(0,Max1,Max2,_) do
             X #=< Max1 + 1,
             Max2 #= max(Max1,X)
         ).


-- Joachim