##### 10.35.9.4 A Global Constraint Example

The following example defines a new global constraint `exactly(`X`,`L`,`N`)`, which is true if X occurs exactly N times in the list L of integers and domain variables. N must be an integer when the constraint is posted. A version without this restriction and defined in terms of reified equalities was presented earlier; see Reified Constraints.

This example illustrates the use of state information. The state has two components: the list of variables that could still be X, and the number of variables still required to be X.

The constraint is defined to wake up on any domain change.

```                               % exactly.pl

/*
An implementation of exactly(I, X[1]...X[m], N):

Necessary condition: 0 =< N =< m.
Rewrite rules:

[1] |= X[i]=I  ==> exactly(I, X[1]...X[i-1],X[i+1]...X[m], N-1):
[2] |= X[i]\=I ==> exactly(I, X[1]...X[i-1],X[i+1]...X[m], N):
[3] |= N=0     ==> X[1]\=I ... X[m]\=I
[4] |= N=m     ==> X[1]=I  ... X[m]=I
*/
:- use_module(library(clpfd)).

% the entrypoint
exactly(I, Xs, N) :-
dom_suspensions(Xs, Susp),
fd_global(exactly(I,Xs,N), state(Xs,N), Susp).

dom_suspensions([], []).
dom_suspensions([X|Xs], [dom(X)|Susp]) :-
dom_suspensions(Xs, Susp).

% the solver method
:- multifile clpfd:dispatch_global/4.
clpfd:dispatch_global(exactly(I,_,_), state(Xs0,N0), state(Xs,N), Actions) :-
exactly_solver(I, Xs0, Xs, N0, N, Actions).

exactly_solver(I, Xs0, Xs, N0, N, Actions) :-
ex_filter(Xs0, Xs, N0, N, I),
length(Xs, M),
(   N=:=0 -> Actions = [exit|Ps], ex_neq(Xs, I, Ps)
;   N=:=M -> Actions = [exit|Ps], ex_eq(Xs, I, Ps)
;   N>0, N<M -> Actions = []
;   Actions = [fail]
).

% exactly.pl

% rules [1,2]: filter the X's, decrementing N
ex_filter([], [], N, N, _).
ex_filter([X|Xs], Ys, L, N, I) :- X==I, !,
M is L-1,
ex_filter(Xs, Ys, M, N, I).
ex_filter([X|Xs], Ys0, L, N, I) :-
fd_set(X, Set),
fdset_member(I, Set), !,
Ys0 = [X|Ys],
ex_filter(Xs, Ys, L, N, I).
ex_filter([_|Xs], Ys, L, N, I) :-
ex_filter(Xs, Ys, L, N, I).

% rule [3]: all must be neq I
ex_neq(Xs, I, Ps) :-
fdset_singleton(Set0, I),
fdset_complement(Set0, Set),
eq_all(Xs, Set, Ps).

% rule [4]: all must be eq I
ex_eq(Xs, I, Ps) :-
fdset_singleton(Set, I),
eq_all(Xs, Set, Ps).

eq_all([], _, []).
eq_all([X|Xs], Set, [X in_set Set|Ps]) :-
eq_all(Xs, Set, Ps).

end_of_file.

% sample queries: | ?- exactly(5,[A,B,C],1), A=5.  A = 5, B
in(inf..4)\/(6..sup), C in(inf..4)\/(6..sup)

| ?- exactly(5,[A,B,C],1), A in 1..2, B in 3..4.
C = 5,
A in 1..2,
B in 3..4
```

Send feedback on this subject.