%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%  The {log} library  %%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%                   August 2000 - by Gianfranco Rossi
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%This file contains the {log} definition of most of the usual
%operations on sets. It can be loaded into the {log} environment
%by issuing the goal consult(setlog_lib) (provided setlog_lib is
%the name you give to this file).
%The predicates defined in this file are:
%
% - less/3
% - subset/2
% - nsubset/2
% - ssubset/2
% - un/3
% - int/3
% - nint/3
% - disj/2
% - diff/3
% - ndiff/3
% - sdiff/3
% - size/2
% - powerset/2
% 
%This file provides also alternative definitions for some of these 
%predicates, aimed at reducing the number of repeated solutions.  
%The list of these predicates is 
%
% - xless/3
% - xsubset/2
% - xun/3
% - xint/3
% - xdiff/3
% - xndiff/3
% - xsdiff/3
% - xsize/2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

less(R,X,S) :-                  % remove element 
    R = {X/S} &
    X nin S.

subset(S1,S2) :-                % subset (S1 \subseteq S2)
    forall(X in S1,X in S2).

nsubset(S1,S2) :-               % not subset (S1 \not\subseteq S2) 
     Z in S1 & 
     Z nin S2.

ssubset(S1,S2) :-               % strict subset (S1 \subset S2)
    S1 neq S2 &
    subset(S1,S2).

un('{}',X,X).                   % union  (T = R \cup S)
un(R,S,{X/U}) :-
    less(R,X,RR) &
    un(RR,S,U).

int('{}',_,'{}').               % intersection  (T = R \cap S)
int(R,S,{X/U}) :-
    less(R,X,RR) &
    X in S &
    int(RR,S,U).
int(R,S,T) :-
    less(R,X,RR) &
    X nin S &
    int(RR,S,T).        

nint(R,S,T) :-                  % not intersection (T = R \not\cap S)
    Z in T &
    (Z nin R or Z nin S).

disj(S1,S2) :-                  % disjointness (S1 \cap S2 = \emptyset)
    forall(X in S1, forall(Y in S2,X neq Y)).         

diff('{}',_,'{}').              % difference (T = R \setminus S)
diff(R,S,T) :-
    less(R,X,RR) &
    X in S &
    diff(RR,S,T).
diff(R,S,{X/U}) :-
    less(R,X,RR) &
    X nin S &
    diff(RR,S,U).

ndiff(R,S,T) :-                 % not difference (T = R \not\setminus S)
    diff(R,S,T1) &
    T1 neq T.

sdiff(R,S,T) :-                 % symmetric difference (T = R \triangle S)
    diff(R,S,A) &
    diff(S,R,B) &
    un(A,B,T).                 

size(S,N) :- in_size(S,0,N).    % cardinality (N = |S|)
in_size('{}',N,N).
in_size(S,N,M) :-
    N neq M &
    less(S,_,SS) &
    NN is N + 1 &
    in_size(SS,NN,M).   

powerset(S,PS) :-               % powerset (PS = 2^S) 
   PS = {SS : subset(SS,S)}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%The following predicates are used
%to deal with constraints as program  defined predicates
%(hence, executed when encountered) 

member(X,S) :- X in S.                              
nmember(X,S) :- X nin S.
equal(X,Y) :- X = Y.
nequal(X,Y) :- X neq Y.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%The following predicates provide
%an improved implementation of the basic set-theoretic operations
%that reduces the number of repeated equivalent solutions  

xless(S,X,SS) :-               % remove the element X from S, if S is ground
    (ground(S) & R = g or R = ng)! &  % otherwise, remove any element X from S
    (R = g & less(S,X,SS)! or
     R = ng & less(S,X,SS)). 

xsubset({},S2).                % subset (S1 \subseteq S2)
xsubset(S1,S2) :- 
    xless(S1,X,SS1) & 
    member(X,S2) &
    xsubset(SS1,S2).         

xun('{}',X,X).                   % union  (T = R \cup S)
xun(R,S,{X/U}) :-
    xless(R,X,RR) &
    X nin S &
    xun(RR,S,U).
xun(R,S,U) :-
    xless(R,X,RR) &
    member(X,S) &
    xun(RR,S,U).

xint('{}',_,'{}').               % intersection  (T = R \cap S)
xint(R,S,{X/U}) :-
    xless(R,X,RR) &
     member(X,S) &
     xint(RR,S,U).
xint(R,S,T) :-
    xless(R,X,RR) &
    X nin S &
    xint(RR,S,T).       

xdiff('{}',_,'{}').              % difference (T = R \setminus S)
xdiff(R,S,T) :- 
   xless(R,X,RR) & 
   member(X,S) &
    xdiff(RR,S,T).
xdiff(R,S,{X/U}) :-
    xless(R,X,RR) &
    X nin S &
    xdiff(RR,S,U).

xndiff(R,S,T) :-                 % not difference (T = R \not\setminus S)
    xdiff(R,S,T1) & 
   T1 neq T.

xsdiff(R,S,T) :-                 % symmetric difference (T = R \triangle S) 
   xdiff(R,S,A) &
    xdiff(S,R,B) & 
   xun(A,B,T). 
                  
xsize(S,N) :- xin_size(S,0,N).    % cardinality (N = |S|)
xin_size('{}',N,N).
xin_size(S,N,M) :-
    N neq M &
    xless(S,_,SS) &
    NN is N + 1 &
    xin_size(SS,NN,M).