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

Hello Everybody,

I am seeking ideas on how to implement in ECLiPSe a specific
constraint in a simple, if possible, and efficient way.

Let L be a list of length N with domain variables ranging
in 1..M. Acceptable lists are the ones that ...
1. ... contain values from 1 up to K (K =< M), but not any
values from K+1 up to M (K is not given).
2. ... satisfy the condition that the first occurrences of
the values from 1 to K appear in this order in the list.

For example, let N = 8 and M = 5. The lists [1,1,2,1,2,3,2,1]
and [1,2,1,3,2,4,3,1] are valid. The first one has K = 3 (only
items 1, 2, 3 appear in the list) and the second one has K = 4
(just 5 is missing from the list). In the first list, the first
occurrences of 1, 2, 3 are in positions 1, 3, 6 and in the second
list, the first occurrences of 1, 2, 3, 4 are in positions 1, 2,
4, 6 in the lists. All fine!

I believe that the requirement 1 above could be implemented
easily with the occurrences constraint (one for each number in
1..M) and a set of implication (=>) constraints, stating that
if the number of occurrences of x in 1..M is 0, then the numbers
of occurrences of x+1, x+2, ... in the list should also be 0.
I cannot predict the propagation level of this approach, but
it seems that, at least, declaratively can be stated.

I don't have any good ideas for the requirement 2. I tried
something that exploits again the occurrences constraint (for
every number in 1..M and every prefix list of the given list)
and then the lex_le constraint. It worked, but if N is around
50 or more, the efficiency is unacceptable.

Any ideas on the above would be more than welcome.

Best Regards,
Panagiotis