\begin{verbatim}

% Our goal is to be able to represent the following.
%
% 4 <= {l1: 1, not l2: 2, l3: 2, not l4: 3} <= 7  <---   p
% p
%

 lit(p).
 lit(p').
 lit(l1).
 lit(l1').
 lit(l2).
 lit(l2').
 lit(l3).
 lit(l3').
 lit(l4).
 lit(l4').

 contrary(p, p').
 contrary(p', p).
 contrary(l1, l1').
 contrary(l1', l1).
 contrary(l2, l2').
 contrary(l2', l2).
 contrary(l3, l3').
 contrary(l3', l3).
 contrary(l4, l4').
 contrary(l4', l4).
 wt(r, l1, 1).
 wt(r, l2', 2).
 wt(r, l3, 2).
 wt(r, l4', 3).

 rule(r).

 holds(r,L) :-
    holds(p),
    lit(L),
    lit(LL),
    wt(r,L,X),
    contrary(L,LL),
    not holds(r,LL).

 holds(r,L) :-
    holds(p),
    lit(L),
    lit(LL),
    wt(r,LL,X),
    contrary(L,LL),
    not holds(r,LL).

 holds(r,L,X)   :-
    lit(L),
    holds(r,L),
    wt(r,L,X).

 holds(r,L,0)   :-
    lit(L),
    lit(LL),
    holds(r,L),
    wt(r,LL,X).

 holds(p).

 holds(L)   :-
    lit(L),
    holds(r,L).

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 const total=6.
 const max=20.

 num(1..total).
 numm(1..max).
 number(0..max).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


not_assg(X,Y,J) :-
    rule(X),
    num(D),
    num(DD),
    lit(Y),
    lit(YY),
    holds(X,Y,D),
    holds(X,YY,DD),
    num(J),
    assg(X,YY,J),
    neq(Y,YY).

not_assg(X,Y,J) :-
    rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D),
    num(J),
    num(JJ),
    assg(X,Y,JJ),
    neq(J,JJ).

assg(X,Y,J) :-
    rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D),
    num(J),
    not not_assg(X,Y,J).


numbered(X,J) :-
    rule(X),
    num(D),
    lit(Y),
    num(J),
    holds(X,Y,D),
    assg(X,Y,J).

:-  num(J),
    rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D),
    numbered(X,J+1),
    not numbered(X,J).




one_is_assigned(X) :-
    rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D),
    assg(X,Y,1).

:-  rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D),
    not one_is_assigned(X).


initialize(sum,D,D):-
    rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D),
    assg(X,Y,1).

update(sum, W, Y, W+Y) :-
    numm(W),
    numm(Y).


aggr(sum,1,X,D) :-
    rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D),
    initialize(sum,D,D).

aggr(sum,J+1,X,Z) :-
    rule(X),
    num(D),
    lit(Y),
    num(J),
    0 < J,
    J <= total-1,
    numm(W),
    holds(X,Y,D),
    aggr(sum,J,X,W),
    assg(X,Y,J+1),
    update(sum,W,D,Z).


last_number(X,J) :-
    num(J),
    rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D),
    numbered(X,J),
    not numbered(X,J+1).

sum_holds(X,Q) :-
    rule(X),
    num(J),
    numm(Q),
    last_number(X,J),
    aggr(sum,J,X,Q).

sum_holds(X,0) :-
    rule(X),
    not some(X).

some(X)  :-
    rule(X),
    num(D),
    lit(Y),
    holds(X,Y,D).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


:- sum_holds(r,W), number(W), W < 4.

:- sum_holds(r,W), number(W), W > 7.


%Instead of `numm' we use
%`number' here to allow W to be 0.




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

hide holds(X,Y,D).
hide num(X).
hide numm(X).
hide numbered(X,J).
hide one_is_assigned(X).
hide initialize(X,Y,Z).
hide update(X,Y,Z,T).
hide aggr(U,V,W,X).
hide last_number(X,Y).
hide not_assg(X,Y,J).
hide contrary(X,XX).
hide lit(X).
hide rule(R).
hide wt(X,Y,Z).
hide holds(X,Y).
hide assg(X,Y,Z).
hide some(X).
hide number(X).

\end{verbatim}