%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%  The {log} library  %%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%              November 2001 - by Gianfranco Rossi
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%This file contains the {log} definition of those operations on 
%sets which are not provided as constraints in {log}. 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:
%
% - size/2
% - powerset/2
% - cross_product/3
% - list_to_set/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
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

size(S,N) :- in_size(S,0,N).    % size(?S,?N) is true if N is the cardinality 
in_size('{}',N,N).              % of the set S (i.e., N = |S|)
in_size(S,N,M) :-
    N neq M &
    less(S,_,SS) &
    NN is N + 1 &
    in_size(SS,NN,M).   

powerset(S,PS) :-               % powerset(+S,?PS) is true if PS is the powerset 
     PS = {SS : subset(SS,S)}.  % of S (i.e., PS = 2^S)

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

list_to_set([],{}).             % list_to_set(+L,?S) is true if S denotes the set
list_to_set([X|L],{X/S}) :-     % of all elements of the list L
     list_to_set(L,S).
     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%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)! & 
    call(X in 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)! &
    call(X in 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)! &
    call(X in 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)! & 
    call(X in 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).