%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%  The {log} library  %%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%                   November 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
% - int/3
% - nint/3
% - diff/3
% - ndiff/3
% - sdiff/3
% - size/2
% - powerset/2
% - cross_product/3
% 
%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)
    un(S1,S2,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).

int(R,S,T) :-                   % intersection  (T = R \cap S)
    un(A,T,R) & 
    un(B,T,S) & 
    disj(A,B).

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

diff(R,S,T) :-                  % difference (T = R \setminus S)
    subset(T,R) &
    un(S,T,W) &
    subset(R,W) &
    disj(S,T).

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)}.

cross_product(A,B,CP) :-        % CP is the Cartesian product of sets A and B
     CP = {X : exists([Y,Z], X = {Y,Z} & Y in A & Z in B)}.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%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(S1,S2) :-              % subset (S1 \subseteq S2)
    (ground(S1) & R=g or R=ng)! &  
    (R=g & xxsubset(S1,S2) or
     R=ng & subset(S1,S2)). 
xxsubset({},S2).
xxsubset(S1,S2) :- 
    less(S1,X,SS1)! & 
    member(X,S2) &
    xxsubset(SS1,S2).         

xun(R,S,U) :-                  % union  (T = R \cup S)
    (ground(R) & H=g or H=ng)! &  
    (H=g & xxun(R,S,U) or
     H=ng & un(R,S,U)). 
xxun('{}',X,X).                   
xxun(R,S,{X/U}) :-
    less(R,X,RR)! &
    X nin S &
    xxun(RR,S,U).
xxun(R,S,U) :-
    less(R,X,RR)! &
    member(X,S) &
    xun(RR,S,U).

xint(R,S,U) :-                  % intersection  (T = R \cap S)
    (ground(R) & H=g or H=ng)! &  
    (H=g & xxint(R,S,U) or
     H=ng & int(R,S,U)). 
xxint('{}',_,'{}').               
xxint(R,S,{X/U}) :-
    less(R,X,RR)! &
    member(X,S) &
    xxint(RR,S,U).
xint(R,S,T) :-
    less(R,X,RR)! &
    X nin S &
    xxint(RR,S,T).       

xdiff(R,S,U) :-                  % difference (T = R \setminus S)
    (ground(R) & H=g or H=ng)! &  
    (H=g & xxdiff(R,S,U) or
     H=ng & diff(R,S,U)). 
xxdiff('{}',_,'{}').              
xxdiff(R,S,T) :- 
    less(R,X,RR)! & 
    member(X,S) &
    xxdiff(RR,S,T).
xxdiff(R,S,{X/U}) :-
    less(R,X,RR)! &
    X nin S &
    xxdiff(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).