

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                                                          
%%                        The {log} interpreter                   
%%                                                           
%%                 VERSION 4.5.16 (for SICStus Prolog)  
%%                                                          
%%                      original development by
%%                                                          
%%                Agostino Dovier     Eugenio Omodeo          
%%                Enrico Pontelli     Gianfranco Rossi  
%%
%%                    subsequent enhancements by
%%
%%                        Gianfranco Rossi
%%
%%                    with the contribution of 
%%
%%              B.Bazzan  S.Manzoli  S.Monica  C.Piazza  
%%
%%          Last revision by Gianfranco Rossi (April 2008)           
%%                                                              
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- module(setlog,[
             setlog/0,
             setlog_start/0,
             setlog_call/1,
             setlog_call/2,
             setlog_consult/1,
             setlog_clause/1,
             setlog_sc/3,
             setlog_help/0,
             h/0 
   ]).

:- use_module(library(clpfd)).          % SICStus Prolog
%:- use_module(library('clp/bounds')).   % SWI-Prolog

:-op(1000,xfx,\).     
:-op(980,xfx,:).
:-op(970,xfy,or).
:-op(950,xfy,&).
:-op(900,fy,[neg,naf]).
:-op(800,xf,!).
:-op(700,xfx,[in,neq,nin]). 
:-op(650,yfx,[with,mwith]).	
:-op(150,fx,*).

:- dynamic setlog/2.                                  
:- dynamic newpred_counter/1. 
:- dynamic context/1. 
:- dynamic nolabel/0.                                 
                

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%    Starting predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

setlog :- 
       op_define,  % not necessary in SICStus Prolog
       top_level.

op_define :-
       op(1000,xfx,\),     
       op(980,xfx,:),
       op(970,xfy,or),
       op(950,xfy,&),
       op(900,fy,[neg,naf]),
       op(800,xf,!),
       op(700,xfx,[in,neq,nin]),
       op(650,yfx,[with,mwith]),	
       op(150,fx,*).
  
setlog_start :- 
       welcome_message,
       setlog.                         

welcome_message :-                                     
       nl, nl,
       write('              WELCOME TO {log} - version 4.6           '),
       nl, nl.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%% The top-level user interface %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

top_level :-
       nl, write('{log}=> '),
       setlog_read_term(Goal,[variable_names(VarNames)]),
       solve(Goal,Constr),
       add_FDc(Constr,ConstrAll,Warning),
       top_level_warning(Warning),
       chvar([],_,v(VarNames,ConstrAll),_,_,v(VarNames1,Constr1)),  
       mk_subs_ext(VarNames1,VarNames_ext1),	
       extract_vars(VarNames_ext1,Vars),
       nl, write_subs_constr(VarNames_ext1,Constr1,Vars),  
       top_level.
top_level :-
       nl,write(no),nl,
       top_level.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

setlog_read_term(Goal,Vars) :- 
       on_exception(syntax_error(_,_,Msg,_,_),read_term(Goal,Vars),syntax_error_msg(Msg)).

syntax_error_msg(Text) :-
       write('Syntax error'), nl,
       write(Text), 
       top_level.

%add_FDc(SETc,SETFDc,R)       
%SETFDc is the list of contraints obtained by appending the list FDc
%of interval constraints still occurring in the FD constraint store
%to the list of constraints SETc. R is either 'y' if at least one 
%such interval constraints is found; otherwise, R is uninitialized

add_FDc([],[],_) :- !.                                          
add_FDc([C|SETc],[C|FDc],Warning) :-  
       \+(C = integer(_)),!,
       add_FDc(SETc,FDc,Warning).                                           
add_FDc([integer(X)|SETc],[integer(X)|FDc],Warning) :-  
       \+get_domain(X,X in _D),!,
       add_FDc(SETc,FDc,Warning).  
add_FDc([integer(X)|SETc],FDc,Warning) :-  
       get_domain(X,FD),
       tau(X in D,FD), 
       (nolabel,! ; Warning = y),
       (D == int(inf,sup),!,FDc = [integer(X)|FDcCont]
        ;
        FDc = [(X in D)|FDcCont]
       ),
       add_FDc(SETc,FDcCont,Warning).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

top_level_warning(R) :- 
       var(R),!.
top_level_warning(_) :- 
       nl,write('WARNING: no finite domain specified for uninstantiated'),
       write(' variables in integer terms'),nl.

retract_nolabel :-
       retract(nolabel),!.
retract_nolabel.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

mk_subs_ext(VarSubs,VarSubsMin) :-      
       postproc(VarSubs,VarSubsExt),
       mk_subs_vv(VarSubsExt,VarSubsMin).

mk_subs_vv([],[]).                  
mk_subs_vv([N1=V1|Subs],R) :-
       var(V1),!,
       V1 = N1,
       mk_subs_vv(Subs,SubsMin),
       append(SubsMin,[true],R).  
mk_subs_vv([N1=V1|Subs],[N1=V1|R]) :-
       mk_subs_vv(Subs,R).  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% write substitutions and constraints

write_subs_constr([],[],_) :- !,    
       write(yes), nl.                       
write_subs_constr(Subs,Constr,Vars) :- 	
      (Subs = [],!, true
       ; 
       Subs = [true|_],!,write('true'),Prn=y
       ;
       write_subs_all(Subs,Prn)
      ), 
       write_constr(Constr,Vars,Prn), 
       ask_the_user(Prn).

ask_the_user(Prn):-
       var(Prn),!.
ask_the_user(_):-
       nl,	
       nl, write('Another solution?  (y/n)'),
       get(C), skip(10),
       (C \== 121,! ; fail).

write_subs_all([],_).
write_subs_all([N1=V1|R],Prn) :-
        write(N1), write(' = '), write(V1), Prn=y,
       (R = [],!,true ; 
        R = [true|_],!,true ;
        write(',  '), nl, write_subs_all(R,Prn) ).  

write_constr(Constr,Vars,Prn) :-             
       postproc(Constr,Constr_ext),
       write_constr_first(Constr_ext,Vars,Prn).

write_constr_first([],_,_) :- !.                
write_constr_first([C|Constr],Vars,Prn) :-             
       nl, write('Constraint: '), 
       write_atomic_constr(C), Prn=y,
       write_constr_all(Constr,Vars).

write_constr_all([],_) :- !.                
write_constr_all([C|Constr],Vars) :-             
       write(', '), write_atomic_constr(C),
       write_constr_all(Constr,Vars).
         
write_atomic_constr(solved(C,_)) :- !,
       write(C).
write_atomic_constr(C) :- !,
       write(C).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%     The inference engine     %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
        
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%% solve(+Goal,-Constraint)   Goal: {log} goal in external form

solve(Goal_int_ruq,Constr):-            
       sf_in_goal(Goal_int_ruq,Goal_ruqL),
%% write(Goal_ruqL),nl,             %% only for debugging purposes
       list_to_conj(Goal_ruq,Goal_ruqL),
%% write(Goal_ruq),nl,
       preproc_goal(Goal_ruq,Goal),!,
%% write(Goal),nl,
       ruq_in_goal(Goal,B),
       solve_goal(B,Constr1),
       final_sat(Constr1,Constr).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%% solve_goal(+Goal,-Constraint)   Goal: {log} goal in internal form

solve_goal(G,ClistNew) :-
       constrlist(G,GClist,GAlist),
       solve_goal(GClist,GAlist,ClistNew). 

%%%% solve_goal(+Constraint,+Non_Constraint,-Constraint)

%solve_goal(Clist,C,_CListCan):-   %only for debugging purposes
%       write('**********************************'),nl, 
%       write('calling goal: input constraint '),write(Clist),nl, 
%       write('calling goal: input atoms'),write(C),nl,nl,
%       fail. 
solve_goal(Clist,[],CListCan):- !, 
       sat(Clist,CListCan,nf). 
solve_goal(Clist,[true],CListCan):- !, 
       sat(Clist,CListCan,nf). 
solve_goal(Clist,[A|B],CListOut):-
       sat(Clist,ClistSolved,nf),
       ssolve(A,ClistCl,AlistCl),
       append(ClistSolved,ClistCl,ClistNew),
       append(AlistCl,B,AlistNew),
       solve_goal(ClistNew,AlistNew,CListOut).

solve_goal_fin(G,ClistNew) :-
       constrlist(G,GClist,GAlist),
       solve_goal_fin(GClist,GAlist,ClistNew).

solve_goal_fin(GClist,GAlist,ClistNew):-  
       solve_goal(GClist,GAlist,Clist),  
       final_sat(Clist,ClistNew).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%% ssolve(+Atom,-Constraint,-Non_Constraint)

ssolve(true,[],[]):- !.                  %% unit goal

ssolve(neg A,ClistNew,[]):-              %% simplified constructive negation
        !,c_negate(A,ClistNew).
ssolve(naf A,ClistNew,[]):-              %% negation as failure
        !,naf_negate(A,ClistNew).

ssolve((G1 or G2),ClistNew,[]):-         %% goal disjunction 
        !,(solve_goal(G1,ClistNew)
          ;
           solve_goal(G2,ClistNew) ).

ssolve(call(A),C,[]):-                   %% meta call    
        !,solve_goal(A,C).

ssolve((A)!,C,[]):-                      %% deterministic call
        !,solve_goal(A,C),!.
  
ssolve(ruq_call(S,InName,VarList),Cout,[]) :-       %% RUQs
        !,solve_RUQ(S,InName,VarList,[],Cout).   

ssolve(sf_call(S,GName,PName,VarList),Cout,[]) :-   %% SF
        !, solve_SF(S,GName,PName,VarList,[],Cout).   

ssolve(prolog_call(A),[],[]):-    %% Prolog call (any predicate)
        nonvar(A),!,A.   
                 
ssolve(A,[],[]):-                 %% Prolog built-in predicates
        nonvar(A),functor(A,F,N),
        sys(F,N),!,A.   

ssolve(A,C,[]):-                  %% {log} built-in predicates
        sys_special(A,C),!.   

ssolve(labeling(X),[],[]):- !,    %% explicit clpfd labeling
        get_domain(X,X in D), 
        labeling1(X,D).                

ssolve(label,[],[]):- !,          %% activate automatic clpfd labeling
        retract_nolabel.

ssolve(nolabel,[],[]):-           %% deactivate automatic clpfd labeling
        nolabel,!.
ssolve(nolabel,[],[]):-    
        assert(nolabel).

ssolve(A,C,D):-                   %% program defined predicates
        our_clause(A,B,C1),
        constrlist(B,C2,D),
        append(C1,C2,C).
        
our_clause(A,B,C):-
        functor(A,Pname,N),
        functor(P,Pname,N),
        setlog((P :- B),_), 
        sunify(P,A,C).

%%%% constrlist(+Atom_conj,-Constraint_list,-Non_Constraint_list)

constrlist(A & B,[A|B1],B2):-
        atomic_constr(A),!,
        constrlist(B,B1,B2).         
constrlist(A & B,B1,[A|B2]):-
        !,constrlist(B,B1,B2).                       
constrlist(A,[A],[]):-
        atomic_constr(A),!.        
constrlist(A,[],[A]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%   Negation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

naf_negate(A,[]) :-                 %% Negation as Failure
       \+ solve_goal_fin(A,_).

%naf_negate(A,[]) :-
%        extract_vars(A,B),
%        constrlist(A,Clist,Alist),
%        solve_goal_fin(Clist,Alist,Clist1),
%        ( alldist(B), Clist == Clist1, !, fail
%          ;
%          write('WARNING: unsafe use of negation'),nl, fail).       
%naf_negate(_A,[]). 

%alldist([]).
%alldist([A|R]):-
%    var(A), not_in_vars(A,R),
%    alldist(R).
    
%not_in_vars(_X,[]).
%not_in_vars(X,[A|R]):-
%    X \== A, not_in_vars(X,R).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

c_negate(A,ClistNew) :-             %% Simplified Constructive Negation 
       chvar([],L1,A,[],L1new,B),
       constrlist(B,Clist,Alist),
       solve_goal_fin(Clist,Alist,Clist0),
       final_sat(Clist0,Clist1),!, 
       dis(L1,L1new,Dis),
       append(Clist1,Dis,CC),
       neg_solve(CC,ClistNew,L1).
c_negate(_A,[]). 
	   
neg_solve([],[],_) :- !, fail.
neg_solve(Clist,ClistNew,LVars) :-
       neg_constr_l(Clist,ClistNew,LVars). 	   

neg_constr_l([],_,_) :- !,fail.
neg_constr_l(Clist,ClistNew,LVars) :-
       member(C,Clist),
       neg_constr(C,ClistNew,LVars).	   

neg_constr(A nin B,[A in B],_) :- !.           
neg_constr(A neq B,[],LVars) :- !,            
      extract_vars(B,V),
      subset_strong(V,LVars),
      sunify(A,B,_).     
neg_constr(A = B,[A neq B],LVars) :-   
      extract_vars(B,V),
      subset_strong(V,LVars),!.
neg_constr(_A = _B,_,_) :-   
      nl, write('WARNING: unimplemented form of negation '),
      write('(universally quantified inequality). Sorry!').

dis([],[],[]):-!.
dis([X|L1],[Y|L2],[X=Y|L3]):-
      nonvar(Y),!,
      dis(L1,L2,L3).
dis([X|L1],[Y|L2],[X=Y|L3]):-
      var(Y),
      member_strong(Y,L2),!,
      dis(L1,L2,L3).
dis([X|L1],[Y|L2],L3):-
      X=Y,
      dis(L1,L2,L3).	 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%  Intensional sets and RUQs processing   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Intensional sets

solve_SF(S,GName,_PName,VarList,_Cin,Cout) :- 
        ground(VarList),!,
        InPred =.. [GName,X|VarList],
        setof(X,solve_goal_fin(InPred,C1),L),
        list_to_set(L,S,C2),
        append(C2,C1,Cout).
solve_SF(S,GName,PName,VarList,Cin,Cout) :-
        solve_RUQ(S,GName,VarList,Cin,C1),
        InPred =.. [PName,S|VarList],
        solve_goal_fin(C1,[neg(InPred & true)],Cout).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% RUQs

solve_RUQ(S,_,_,C,C) :-
        nonvar(S), 
        empty_aggr(S),!.
solve_RUQ(S,InName,VarList,Cin,Cout) :-
        nonvar(S), S = int(L,H),!,                % solve RUQ's over intervals
        force_bounds_values(L,H),
        solve_RUQ_int(int(L,H),InName,VarList,Cin,Cout).
solve_RUQ(S,InName,VarList,Cin,Cout) :-           % over a given aggregate
        nonvar(S),!,
        aggr_comps(S,X,R),
        InPred =.. [InName,X|VarList],
        solve_goal_fin(Cin,[InPred],C2),
        solve_RUQ(R,InName,VarList,C2,Cout).
solve_RUQ(S,_,_,C,C) :-
        var(S), S = {}.
solve_RUQ(S,InName,VarList,Cin,Cout) :-           % over an unspecified aggregate
        var(S), S = R with X,                             
        InPred =.. [InName,X|VarList],
        solve_goal_fin([X nin R|Cin],[InPred],C2),
        solve_RUQ(R,InName,VarList,C2,Cout),
        aggr_ordered(S).

solve_RUQ_int(S,_,_,C,C) :-
        nonvar(S), is_int(S,L,H),          
        L > H, !.
solve_RUQ_int(S,InName,VarList,Cin,Cout) :-    
        nonvar(S), is_int(S,L,H),          % forall(X in int(L,H),InName(X,VarList))
        L =< H,!, 
        InPred =.. [InName,L|VarList],
        solve_goal_fin(Cin,[InPred],C2),
        L1 is L + 1,
        solve_RUQ(int(L1,H),InName,VarList,C2,Cout).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% auxiliary predicates for solve_RUQ/5

aggr_ordered(S) :- var(S),!.
aggr_ordered({}) :- !.
aggr_ordered(S) :- 
       S = R with X,
       in_order(X,R), 
       aggr_ordered(R).

in_order(_A,S) :- var(S),!.
in_order(_A,{}) :- !.
in_order(A,S) :-  
       S = _R with _B,
       var(A), !.
in_order(A,S) :-  
       S = R with B,
       var(B), in_order(A,R),!.
in_order(A,S) :-  
       S = _R with B,
       A @=< B.

force_bounds_values(A,B) :-
       (var(A),!, labeling(A) ; true),
       (var(B),!, labeling(B) ; true).
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%  "Built-in" predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Prolog built-in predicates

sys(nl,0).
sys(ground,1).
sys(var,1).
sys(nonvar,1).
sys(name,2).
sys(functor,3).
sys(arg,3).
sys(=..,2).
sys(==,2).
sys(\==,2).
sys(@<,2).
sys(@>,2).
sys(@=<,2).
sys(@>=,2).
%%********* list to be completed!!********* 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% {log} built-in predicates

sys_special(write(T),[]) :-            %% write
      !,postproc(T,NewT),
      write(NewT).

sys_special(read(T),C) :-              %% read
      !,setlog_read(Tout),
      preproc(Tout,T,C).

sys_special(assert(Clause),[]):-       %% assert
      !,setassert(Clause).

sys_special(consult(lib),[]):-         %% consult library file                         
      !,rem_clause(lib), rem_clause(tmp(lib)),             
      setlog_open('setloglib_4_5.slog',read,FileStream), 
      switch_ctxt(lib,OldCtxt),
      read_loop_np(FileStream),
      switch_ctxt(OldCtxt,_),
      close(FileStream). 

sys_special(consult(File),[]):-        %% consult                          
      !,setlog_open(File,read,FileStream), 
      write('consulting file '), write(File), write(' ...'), nl,
      sys_special(abolish,_),
      read_loop(FileStream,1),
      write('file '), write(File), write(' consulted.'), nl,
      close(FileStream). 

sys_special(consult(File,mute),[]):-   %% consult using mute mode 
      !,setlog_open(File,read,FileStream), 
      sys_special(abolish,_),
      read_loop_np(FileStream),
      close(FileStream). 

sys_special(listing,[]):-              %% listing
      !,nl, list_all.
          
sys_special(abolish,[]):-              %% abolish
      !,rem_clause(usr),
      rem_clause(tmp(usr)).

sys_special(abort,[]):-                %% abort
      !,nl, write('Execution aborted'), nl,
      setlog. 

sys_special(help,[]):- !, setlog_help(gen).    %% help
sys_special(help(X),[]):- !, setlog_help(X). 
sys_special(h,[]):- !, setlog_help(gen). 

sys_special(halt,[]):-                 %% halt
%     confirm, !, 
      abort.     
% sys_special(halt,[]). 

sys_special(time(G,T),C):-             %% time
      statistics(runtime,_),
      write('STARTING ...'),nl,
      solve_goal_fin(G,C),
      write('END'),nl,
      statistics(runtime,[_,T]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% auxiliary predicate for sys_special/2

setlog_read(Term) :- 
       on_exception(syntax_error(_,_,Msg,_,_),read(Term),syntax_error_msg(Msg)).

setlog_open(File,Mode,Stream) :- 
       on_exception(existence_error(_,_,_,Msg,_),open(File,Mode,Stream),existence_error_msg(Msg)).

existence_error_msg(Text) :-
       write('Existence error'), nl,
       write('file '), write(Text), write(' does not exist'), 
       top_level.

rem_clause(Ctxt):-              
      retract(setlog(_,Ctxt)), 
      fail. 
rem_clause(_).

confirm :-
      nl, write('Are you sure you want to leave {log}? (y/n)'),
      get(C), skip(10),
      C == 121,
      nl, write('Bye, bye. See you later').


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%                                      %%%%%%%%%%%%               
%%%%%%%%%%%  Set/Multiset Unification Algorithm  %%%%%%%%%%%%               
%%%%%%%%%%%                                      %%%%%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
         
sunify(X,Y,[]) :-                   % X = X  (rule 1)
      var(X),var(Y),
      X == Y,!.
sunify(X,Y,C) :-                    % X = t  (rules 5 and 6)
      var(X),!,
      sunifyXt(X,Y,C).
sunify(X,Y,C) :-                    % T = Y  (rule 2)
      var(Y),!,
      sunify(Y,X,C).  
sunify(T1,T2,C) :-                  % intervals (rules 11 and 12)
       int_unify(T1,T2,C), !. 
sunify(R,S,C) :-                    % {...} = {...}  (rules 9 and 10)                     
      tail(R,TR),
      tail(S,TS),!,
      (samevar(TR,TS),!,
       stunify_samevar(R,S,TR,C)
       ;
       stunify_ss(R,S,C) ). 
sunify(X,Y,C) :-                    % bag unification +{...} = +{...}
      bag_tail(X,BX),
      bag_tail(Y,BY),!,
      (samevar(BX,BY),!,
       stunify_bag_same(X,Y,C)
       ;
       stunify_bag(X,Y,C) ).
sunify(X,Y,C) :-                    % f(...) = f(...)  (rule 8)
      X=..[F|Ax],Y=..[F|Ay],!,
      sunifylist(Ax,Ay,C).

sunifyXt(X,Y,[set(N)]) :-           % X = {...|X}  (rule 6)
      nonvar(Y),tail(Y,TY),samevar(X,TY),!,
      replace_tail(Y,N,NewY),
      occur_check(X,NewY),  
      X = NewY.               
sunifyXt(X,Y,[]) :-                 % X = t  (rule 5)
      occur_check(X,Y),     
      (get_domain(X,_),!,    % if X is a domain variable
       simple_integer_expr(Y)       % then Y must be a simple_integer_expr;
       ;                            % otherwise, it fails (without doing var. substitution)
       true),
      X = Y.             

%%%%%%%%%%% Set unification %%%%%%%%%%%%%%%%%
%%  distinct tail vars.

stunify_ss(R with X,S with Y,C) :-  % ground case: {...} = {...}
      ground(X), ground(Y),!,
      (sunify(X,Y,_),!, stunify1_2_3(R,S,X,Y,C)
      ;
       sunify(R,N with Y,C1), 
       sunify(S,N with X,C2),
       append(C1,C2,C3),
       C = [set(N)|C3] ).		
stunify_ss(R with X,S with Y,C) :-  % {...|X} = {...|Y} (rule 9)                        
      sunify(X,Y,C1),
      stunify1_2_3(R,S,X,Y,C2),
      append(C1,C2,C).
stunify_ss(R with X,S with Y,C) :-  % 9.4
      sunify(R,N with Y,C1),
      sunify(S,N with X,C2),
      append(C1,C2,C3),
      C = [set(N)|C3].		

stunify1_2_3(R,S,_,_,C) :-          % 9.1
      sunify(R,S,C).
stunify1_2_3(R,S,_,Y,C) :-          % 9.2
      sunify(R,S with Y,C).
stunify1_2_3(R,S,X,_,C) :-          % 9.3 
      sunify(R with X,S,C).

%%  same tail vars.
stunify_samevar(R with X,S with Y,_TR,C):-   % {...|X} = {...|X} (rule 10)
      select_var(Z,S with Y,Rest),
      sunify(X,Z,C1),
      (sunify(R,Rest,C2)            % 10.1
      ;
       sunify(R with X,Rest,C2)     % 10.2
      ;
       sunify(R,S with Y,C2)),      % 10.3
      append(C1,C2,C).
stunify_samevar(R with X,S with Y,TR,C):-    % 10.4
      replace_tail(R,N,NewR),
      replace_tail(S with Y,N,NewSS),
      sunify(TR,N with X,C1),
      sunify(NewR,NewSS,C2),
      append(C1,C2,C3),
      C = [set(N)|C3].		

sunifylist([],[],[]).
sunifylist([X|AX],[Y|AY],C):-
      sunify(X,Y,C1),
      sunifylist(AX,AY,C2),
      append(C1,C2,C).

%%%%%%%%%%% Interval unification %%%%%%%%%%%%%%%%%

int_unify(int(L,H),int(L,H),[]) :- !.   % (rule 11.1)
int_unify(T1,T2,[]) :-              % (rule 11.2)
      is_int(T1,L1,H1), H1 < L1, 
      is_int(T2,L2,H2), H2 < L2, !.
int_unify(T1,{},[]) :-              % (rule ...)
      is_int(T1,L,H), H < L,!.
int_unify({},T2,[]) :-              % (rule ...)
      is_int(T2,L,H), H < L,!.
int_unify(T1,T2,C) :-               % {...} = int(L,H) (rule 12)
      (T1 = _R with _T, is_int(T2,_L,_H),!
       ;
       is_int(T1,_L,_H), T2 = _R with _T ),
       C = [subset(T1,T2),subset(T2,T1)].

%%%%%%%%%%% Multiset unification %%%%%%%%%%%%%%%%%

stunify_bag_same(R mwith X, S mwith Y, C) :-   % +{...|X} = +{...|X} 
	de_tail(R mwith X,ZX),
	de_tail(S mwith Y,ZY),
	sunify(ZX,ZY,C).

stunify_bag(R mwith X, S mwith Y, C) :-        % +{...|X} = +{...|Y} 
	sunify(X,Y,C1),
	sunify(R,S,C2),
	append(C1,C2,C).
stunify_bag(R mwith X, S mwith Y,C) :-
	sunify(R, N mwith Y, C1),
	sunify(S, N mwith X, C2),
        append(C1,C2,C3),
        C = [bag(N)|C3].		

%%%%%%%%%%%%%% Auxiliary predicates for unification

select_var(_,S,_):-
      var(S), !, fail.
select_var(Z, R with Z, R).
select_var(Z, R with Y, A with Y):-
      select_var(Z, R, A).

occur_check(X,Y):-    % occur_check(X,T): true if variable X does not occur in term T
      var(Y),!,X \== Y.
occur_check(X,Y):-
      Y =.. [_|R],
      occur_check_list(X,R).
occur_check_list(_X,[]):-!.
occur_check_list(X,[A|R]):-
      occur_check(X,A),
      occur_check_list(X,R).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%     The Constraint Solver    %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%% Atomic constraints %%%%%%%%%%%%%%%%%%%%%%

atomic_constr(_ nin _).
atomic_constr(_ in _). 
atomic_constr(_ neq _).  
atomic_constr(_ = _).      
atomic_constr(type(_)).
atomic_constr(set(_)).
atomic_constr(integer(_)).        
atomic_constr(delay(_,_)).
atomic_constr(un(_,_,_)).
atomic_constr(subset(_,_)).  
atomic_constr(disj(_,_)).
atomic_constr(size(_,_)).   
atomic_constr(ninteger(_)).        
atomic_constr(bag(_)).
atomic_constr(list(_)).
atomic_constr(nun(_,_,_)).
atomic_constr(ndisj(_,_)).
atomic_constr(solved(_,_)).   
atomic_constr(_ is _).     
atomic_constr(_ =< _).      
atomic_constr(_ < _).       
atomic_constr(_ >= _).      
atomic_constr(_ > _).       


%%%%%%%%%%%%  Constraint solver main procedure %%%%%%%%%%%%              

%%%% sat(+Constraint,-Solved_Form_Constraint,+final/non-final)

%%%sat(C,_SFC,_F):-                      %only for debugging purposes
%%%      nl,write('>>>>> checking constraint: '),write(C),nl,
%%%      fail. 
sat(C,SFC,F):- 
      sat_step(C,NewC,R,F),  
%%%write('Solved flag: '),write(R),nl,   %only for debugging purposes
      sat_cont(R,NewC,SFC,F).
sat_cont(R,NewC,SFC,F) :-           %if R=='stop', then no rule has changed the CS in the last 
      R == stop,!,                  %call to 'sat_step' (-> fixpoint); otherwise, call 'sat' again
      norep_in_list(NewC,RedC),     %remove possibly repeated constraints in the CS
      global_check(RedC,RedC,RevC), %rewrite RedC to RevC
      (RevC == RedC,!,SFC=RevC      %if RedC==RevC, then no rewriting has been applied:
       ;                            %RevC is the resulting constraint; 
       sat(RevC,SFC,F)              %otherwise, call 'sat' again
      ).
sat_cont(_R,NewC,SFC,F) :-
      sat(NewC,SFC,F).

%%%sat_step(InC,_OutC,_Stop,_F):-   %only for debugging purposes
%%%          write('    >>>>> sat step: '), write(InC),nl,
%%%          get0(_),
%%%          fail. 
sat_step([],[],stop,_F) :- !.
%%%%%%%%%%%%%             % general constraints
sat_step([X neq Y|R1],R2,Z,F):- !,
          sat_neq([X neq Y|R1],R2,Z,F).
sat_step([X = Y|R1],R2,Z,F):- !,
          sat_eq([X = Y|R1],R2,Z,F).
%%%%%%%%%%%%%             % set/bag/list/interval constraints
sat_step([X nin Y|R1],R2,Z,F):- !,
          sat_nin([X nin Y|R1],R2,Z,F).
sat_step([X in Y|R1],R2,Z,F):- !,
          sat_in([X in Y|R1],R2,Z,F).
%%%%%%%%%%%%%             % set/interval constraints
sat_step([un(X,Y,W)|R1],R2,Z,F):- !,
          sat_un([un(X,Y,W)|R1],R2,Z,F).
sat_step([subset(X,Y)|R1],R2,Z,F):- !,     
          sat_sub([subset(X,Y)|R1],R2,Z,F).
sat_step([disj(X,Y)|R1],R2,Z,F):- !,
          sat_disj([disj(X,Y)|R1],R2,Z,F).
sat_step([nun(X,Y,W)|R1],R2,Z,F):- !,
          sat_nun([nun(X,Y,W)|R1],R2,Z,F).
sat_step([ndisj(X,Y)|R1],R2,Z,F):- !,
          sat_ndisj([ndisj(X,Y)|R1],R2,Z,F).
sat_step([size(X,Y)|R1],R2,Z,F):- !,       
          simple_integer_expr(Y), 
          sat_size([size(X,Y)|R1],R2,Z,F).
%%%%%%%%%%%%%             % type constraints
sat_step([set(X)|R1],R2,Z,F):- !,             
          sat_set([set(X)|R1],R2,Z,F).
sat_step([integer(X)|R1],R2,Z,F):-!,            
          sat_integer([integer(X)|R1],R2,Z,F).
sat_step([type(aggr(X))|R1],R2,Z,F):- !,
          (sat_set([set(X)|R1],R2,Z,F) ; 
           sat_bag([bag(X)|R1],R2,Z,F) ; 
           sat_list([list(X)|R1],R2,Z,F)).
sat_step([type(TypeC)|R1],R2,Z,F):- !,         % type(C), where C is a type constraint, 
          sat_step([TypeC|R1],R2,Z,F).         % is dealt with as C, but it is not printed
sat_step([bag(X)|R1],R2,Z,F):- !,              % when listing a program
          sat_bag([bag(X)|R1],R2,Z,F).
sat_step([list(X)|R1],R2,Z,F):- !,
          sat_list([list(X)|R1],R2,Z,F).
sat_step([ninteger(X)|R1],R2,Z,F):-!,            
          sat_ninteger([ninteger(X)|R1],R2,Z,F).
%%%%%%%%%%%%%             % control constraints
sat_step([delay(A,G)|R1],R2,Z,F):- !,
          sat_delay([delay(A,G)|R1],R2,Z,F).
sat_step([solved(C,LG)|R1],R2,Z,F):- !,          % 'solved' constraints: used to 
          sat_solved([solved(C,LG)|R1],R2,Z,F).  % avoid repeated additions of the same constraints
%%%%%%%%%%%%%             % arithmetic constraints
sat_step([X is Y|R1],R2,Z,F):- !,          %% integer equality
          sat_eeq([X is Y|R1],R2,Z,F).
sat_step([C|R1],R2,Z,F):-                  %% integer comparison relations
          C =.. [OP,X,Y], 
          member(OP,['=<','<','>=','>']),!,
          sat_crel([[OP,X,Y]|R1],R2,Z,F).

%%%%%%%%%%%% Rewriting rules for general constraints %%%%%%%%%%%%%              

%%%%%%%%%%%%%%%%%%%%%% equality (=/2)

sat_eq([T1 = T2|R1],R2,c,F):-                    
        sunify(T1,T2,C),
        append(C,R1,R3), 
        sat_step(R3,R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% inequality (neq/2)

sat_neq([T1 neq T2|R1],R2,R,F):-  
         var(T1), nonvar(T2),!,
         sat_neq_vn([T1 neq T2|R1],R2,R,F).                         
sat_neq([T1 neq T2|R1],R2,c,F):-                        % t neq X  (rule 4)
         nonvar(T1), var(T2),!,
         sat_neq([T2 neq T1|R1],R2,_,F).                         
sat_neq([T1 neq T2|R1],R2,R,F):-  
         var(T1), var(T2),!,
         sat_neq_vv([T1 neq T2|R1],R2,R,F).    
sat_neq([T1 neq T2|R1],R2,R,F):-  
         is_int(T1,_,_), T2 = _ with _, !,
         sat_neq_i([T1 neq T2|R1],R2,R,F).    
sat_neq([T1 neq T2|R1],R2,R,F):-  
         is_int(T2,_,_), T1 = _ with _, !,
         sat_neq_i([T2 neq T1|R1],R2,R,F).    
sat_neq([T1 neq T2|R1],R2,R,F):-  
         nonvar(T1), nonvar(T2),!,
         sat_neq_nn([T1 neq T2|R1],R2,R,F).                         

sat_neq_vn([X neq T|R1],R2,c,F):-                       % X neq t[X] (rule 5)
         is_ker(T),
         occurs(X,T),!,
         sat_step(R1,R2,_,F).
sat_neq_vn([X neq T|R1],R2,c,F):-                       % X neq {... | X}  (rule 7)
         T = _S with _T,
         tail(T,TS),samevar(X,TS),!,
         split(T,_,L), 
         member(Ti,L) ,
         sat_step([Ti nin X|R1],R2,_,F).
sat_neq_vn([X neq T|R1],R2,c,F):-                       % X neq {...,t[X],...} (rule 6)
         T = _S with _T,
         occurs(X,T),!,
         sat_step(R1,R2,_,F).
sat_neq_vn([X neq T|R1],[X neq T|R2],Stop,F):-          % X neq t, t simple integer expr (rule 9)
         simple_integer_expr(T),   % to catch and handle type errors within {log} 
         get_domain(X,_), !,
         solve_FD(X neq T),
         sat_step(R1,R2,Stop,F).  
sat_neq_vn([C|R1],[C|R2],Stop,F):-                      % X neq t (solved form)
         sat_step(R1,R2,Stop,F).
sat_neq_vv([X neq Y|_],_,_,_F):-                        % X neq X (rule 3)
         samevar(X,Y),!,fail.
sat_neq_vv([X neq Y|R1],[X neq Y|R2],Stop,F):-          % X neq Y, X,Y domain variables  (rule 9)
         get_domain(X,_),
         get_domain(Y,_),!,
         solve_FD(X neq Y),
         sat_step(R1,R2,Stop,F).
sat_neq_vv([C|R1],[C|R2],Stop,F):-                      % X neq Y (solved form)
         sat_step(R1,R2,Stop,F).
sat_neq_i([T1 neq T2|R1],R2,c,F):-                      % int(A,B) neq {S|R} (special)
         set_length(T2,SetL),
         int_length(T1,IntL),
         SetL < IntL, !,
         sat_step(R1,R2,_,F).
sat_neq_i([T1 neq T2|R1],R2,c,F):-                      % int(A,B) neq {S|R} (rule 11(i))
         sat_step([Z in T1, Z nin T2, integer(Z) | R1],R2,_,F).
sat_neq_i([T1 neq T2|R1],R2,c,F):-                      % int(A,B) neq {S|R} (rule 11(ii))
         sat_step([Z nin T1, Z in T2| R1],R2,_,F).
sat_neq_nn([F neq G|R1],R2,c,Fin):-                     % ground case: t1 neq t2
         ground(F),ground(G),!,
         g_neq(F,G),
         sat_step(R1,R2,_,Fin).
sat_neq_nn([F neq G|R1],R2,c,Fin):-                     % t1 neq t2 (rule 1)
         functor(F,Fname,Far),functor(G,Gname,Gar),
         (Fname \== Gname ; Far \== Gar),!,
         sat_step(R1,R2,_,Fin).
sat_neq_nn([F neq G|R1],R2,c,Fin):-                     % t1 neq t2 (rules 2 and 3)
         functor(F,Fname,Far),functor(G,Gname,Gar),
         Fname == Gname, Far == Gar, 
         Fname \== with, Fname \== mwith,
         F =.. [_|Flist], G =.. [_|Glist],!,
         memberall(A,B,Flist,Glist),
         sat_step([A neq B|R1],R2,_,Fin).
sat_neq_nn([T1 neq T2|R1],R2,c,F):-                     % inequality between sets
         T1 = _S with _A, T2 = _R with _B,              % {A|S} neq {B|R} (rule 8(i))
         sat_step([Z in T1, Z nin T2 | R1],R2,_,F).
sat_neq_nn([T1 neq T2|R1],R2,c,F):-                     % inequality between sets
         T1 = _S with _A, T2 = _R with _B,!,            % {A|S} neq {B|R} (rule 8(ii))
         sat_step([Z in T2, Z nin T1 | R1],R2,_,F).
%%%%%%%%%%%% multisets 
sat_neq_nn([T1 neq T2|R1],R2,c,F):-          % inequality between multisets
         nonvar(T1),nonvar(T2),              % with the same tail variables
         bag_tail(T1,TT1), bag_tail(T2,TT2), 
         samevar(TT1,TT2),!,
         de_tail(T1,DT1), de_tail(T2,DT2),
         sat_step([DT1 neq DT2|R1],R2,_,F).
sat_neq_nn([T1 neq T2|R1],R2,c,F):-          % inequality between multisets
         T1 = _S mwith A, T2 = R mwith B,    % with distinct tail variables
         sat_step([A neq B, A nin R| R1],R2,_,F).
sat_neq_nn([T1 neq T2|R1],R2,c,F):-      
         T1 = _S mwith A, T2 = R mwith B,!,
         sunify(R mwith B, _N mwith A,C),
         append(C,R1,R3),
         sat_step([Z in T2, Z nin T1 | R3],R2,_,F).


%%%%%%%% Rewriting rules for arithmetic constraints %%%%%%%%              

sat_eeq([X is E|R1],R2,c,F):-       % integer equality (is/2)            
        ground(E),!,
        simple_arithm_expr(X),      % to catch type errors within {log} 
        arithm_expr(E),           
        X is E,
        sat_step(R1,R2,_,F).
sat_eeq([X is E|R1],R2,c,F):-       % integer equality             
        simple_integer_expr(X),     % to catch type errors within {log} 
        integer_expr(E),           
        solve_FD(X is E),
        allintvars(X is E,Intc),
        append(Intc,R1,Newc),
        sat_step(Newc,R2,_,F).

sat_crel([[OP,E1,E2]|R1],R2,c,F):-   % integer comparison relations (=<,<,>=,>)                 
        ground(E1), ground(E2),!,
        arithm_expr(E1),             % to catch type errors within {log} 
        arithm_expr(E2), 
        Rel =.. [OP,E1,E2],
        call(Rel),          
        sat_step(R1,R2,_,F).
sat_crel([[OP,E1,E2]|R1],R2,c,F):-                   
        integer_expr(E1),            % to catch type errors within {log} 
        integer_expr(E2),
        Rel =.. [OP,E1,E2],
        solve_FD(Rel),
        allintvars(Rel,Intc),
        append(Intc,R1,Newc),
        sat_step(Newc,R2,_,F).

allintvars(E,Evars) :-     % true if E is an arithmetic expression and Evars
    E =.. [_F|Args],       % is a list containing a contraint integer(X) for 
    addint(Args,Evars).    % each variable X in E
    
addint([],[]):-!.
addint([X|R],[integer(X)|Rvars]) :-
    var(X),!,
    addint(R,Rvars).
addint([E|R],Allvars) :-
    allintvars(E,Evars),
    addint(R,Rvars),
    append(Evars,Rvars,Allvars).

%%%%%%% Rewriting rules for set/bag/list/interval constraints %%%%%%%              

%%%%%%%%%%%%%%%%%%%%%% membership (in/2)

sat_in([T in I|R1],R2,R,F):-                          
         var(I), F==f,!,
         sat_in_v([T in I|R1],R2,R,F).                         
sat_in([T in I|R1],R2,c,F):-                          
         var(I), F==nf,!,
         sat_step([delay(T in I,nonvar(I))|R1],R2,_,F).                         
sat_in([T in I|R1],R2,R,F):-                            
         nonvar(I), is_int(I,L,H),!,
         sat_in_i([T in int(L,H)|R1],R2,R,F).                         
sat_in([T in I|R1],R2,R,F):-                          
         nonvar(I),!,
         sat_in_s([T in I|R1],R2,R,F).                         

sat_in_v([T in X|R1],R2,c,F):-               % t in X, set (rule 4)
         sunify(X,N with T,_),
         sat_step([set(N)|R1],R2,_,F).
sat_in_v([T in X|R1],R2,c,F):-               % t in X, multiset
         sunify(X,N mwith T,_),
         sat_step([bag(N)|R1],R2,_,F).
sat_in_v([T in X|R1],[solved(T in X,l),list(X)|R2],Stop,F):-  % t in X, list (pre-solved form)
         occur_check(X,T),
         sat_step(R1,R2,Stop,F).
sat_in_i([T in int(A,B)|R1],R2,c,F):-        % t in int(L,H) (rule 5 - intervals)
%         simple_integer_expr(T),!,  % to catch type errors within {log} 
         solve_FD(T in int(A,B)),
         sat_step([integer(T)|R1],R2,_,F).   
sat_in_s([T in Aggr|R1],R2,c,F):-            % ground case: t in {A|R} 
         ground(T), ground(Aggr),!,
         g_member(T,Aggr), 
         sat_step(R1,R2,_,F).
sat_in_s([T in Aggr|R1],R2,c,F):-            % t in {A|R} (rule 3(i))
         aggr_comps(Aggr,A,_R),
         sunify(A,T,C), 
         append(C,R1,R3), 
         sat_step(R3,R2,_,F).
sat_in_s([T in Aggr|R1],R2,c,F):-            % t in {A|R} (rule 3(ii))
         aggr_comps(Aggr,_A,R),!,
         sat_step([T in R|R1],R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% non-membership (nin/2)

sat_nin([T nin A|R1],R2,c,F):-              % ground case: t nin {A|R}  or t nin int(L,H)
        ground(T), ground(A),!,             % (or t nin +{A|R} or t nin [A|R])
        \+g_member(T,A), 
        sat_step(R1,R2,_,F).
sat_nin([T nin A|R1],R2,c,F):-              % t nin X, t[X] (rule 3)
        var(A), occurs(A,T),!,                          
        sat_step(R1,R2,_,F).
sat_nin([T nin A|R1],[T nin A|R2],Stop,F):- % solved form
        var(A),!, 
        sat_step(R1,R2,Stop,F).
sat_nin([_T nin A|R1],R2,c,F):-             % t nin {} (rule 1)
        nonvar(A), empty_aggr(A),!,         % (or t1 nin [])
        sat_step(R1,R2,_,F).
sat_nin([R nin I|R1], R2, c, F) :-          % r nin int(s,t) (rule 4)
        nonvar(I), is_int(I, S, _T),        % 4.1
        solve_FD(R + 1 =< S),
        sat_step([integer(R)|R1], R2, c, F).
sat_nin([R nin I|R1], R2, c, F) :-          % 4.2
        nonvar(I), is_int(I, _S, T),
        solve_FD(T + 1 =< R),
        sat_step([integer(R)|R1], R2, c, F).
sat_nin([R nin I|R1], R2, c, F) :-          % 4.3
        nonvar(I), is_int(I, _S, _T),!,
        sat_step([ninteger(R)|R1], R2, c, F).
sat_nin([T1 nin A|R1],R2,c,F):-             % t1 nin {t2|S} (rule 2) 
        nonvar(A), aggr_comps(A,T2,S),!,    % (or t1 nin +{t2|S} or t1 nin [t2|S])
        sat_step([T1 neq T2,T1 nin S|R1],R2,_,F).

%%%%%%% Rewriting rules for set/interval constraints %%%%%%%              

%%%%%%%%%%%%%%%%%%%%%% subset (subset/2)  

sat_sub([subset(S1,S2)|R1],R2,c,F):-                 % ground case: subset({X|R},S2)            
         ground(S1), ground(S2),
         set_term(S1), set_term(S2),!,
         g_subset(S1,S2),
         sat_step(R1,R2,_,F).
sat_sub([subset(S1,I2)|R1],R2,c,F):-                 % subset(X,int(L,H))    
         var(S1), nonvar(I2), is_int(I2,_,_),!,      % (TO BE IMPROVED!)
         int_to_set(I2,S2),     
         sat_step([un(S1,S2,S2)|R1],R2,_,F). 
sat_sub([subset(S1,S2)|R1],R2,c,F):-                 % subset(X,S2)                   
         var(S1),!,
         sat_step([un(S1,S2,S2)|R1],R2,_,F). 
sat_sub([subset({},_S2)|R1],R2,c,F):- !,             % subset({},S2)                  
         sat_step(R1,R2,_,F). 
sat_sub([subset(R with X,I2)|R1],R2,c,F):-           % subset({X|R},int(L,H))                 
         nonvar(I2), is_int(I2,_,_),!,
         sat_step([X in I2,subset(R,I2)|R1],R2,_,F).
sat_sub([subset(R with X,S2)|R1],R2,c,F):- !,        % subset({X|R},S2)            
         sunify(S2,N with X,_),
         sat_step([set(N),subset(R,S2)|R1],R2,_,F).
sat_sub([subset(I,_)|R1],R2,c,F):-                   % subset(int(L,H),S2), with L>H
         is_int(I,L,H),L>H,!,
         sat_step(R1,R2,_,F). 
sat_sub([subset(I,I2)|R1],R2,c,F):-                  % subset(int(L,H),int(L2,H2))
         is_int(I,L,H), nonvar(I2), is_int(I2,L2,H2),!,
         L2 =< L, H2 >= H,
         sat_step(R1,R2,_,F). 
sat_sub([subset(I,S2)|R1],R2,c,F):-                  % subset(int(L,H),{L|N})
         is_int(I,L,H),
         L1 is L+1,
         sat_step([L in S2,subset(int(L1,H),S2)|R1],R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% union (un/3)

sat_un([un(S1,S2,T)|R1],R2,c,F):-                    % un(s,s,t) (rule 1)
         S1==S2,!, 
         sunify(S1,T,C), 
         append(C,R1,R3), 
         sat_step(R3,R2,_,F). 
sat_un([un(X,Y,Z)|R1],NewR2,c,F):-                % (pre-)solved form
         var(X),var(Y),var(Z),!,                     
         NewR2=[solved(un(X,Y,Z),l),size(X,NX),size(Y,NY),size(Z,NZ),integer(NX),integer(NY),integer(NZ)|R2],
         solve_FD(NX =< NZ),
         solve_FD(NY =< NZ),
         solve_FD(NX + NY >= NZ),
         sat_step(R1,R2,_,F).
sat_un([un(T1,T2,T3)|R1],R2,c,F):-                   % un(s,t,{}) (rule 2 + 10)
         nonvar(T3), is_empty(T3),!, 
         unify_empty(T1), unify_empty(T2), 
         sat_step(R1,R2,_,F).
sat_un([un(T1,T2,S)|R1],R2,c,F):-                    % un({},{},X) (rule ...)
         var(S),
         nonvar(T1), is_empty(T1),
         nonvar(T2), is_empty(T2), !, 
         S = {},
         sat_step(R1,R2,_,F).
sat_un([un(T1,T2,S)|R1],R2,c,F):-                    % un({},t,X) (rule 3.a + 11.a)
         nonvar(T1), is_empty(T1), var(S),!, 
         sunify(S,T2,C), 
         append(C,R1,R3), 
         sat_step(R3,R2,_,F).         
sat_un([un(T1,T2,S)|R1],R2,c,F):-                    % un(t,{},X) (rule 3.b + 11.b)
         nonvar(T2), is_empty(T2), var(S),!,
         sunify(S,T1,C), 
         append(C,R1,R3),  
         sat_step(R3,R2,_,F).         
sat_un([un(S1,S2,I)|R1], R2, c, F) :-              % un(s1,s2,int(...)) (rule 8(i))
         nonvar(I), is_int(I,T1,T2), T1 =< T2,
         sunify(N1 with T1,S1,C1), append(C1,R1,C2),
         T3 is T1 + 1,
         sat_step([T1 nin N1,set(N1),un(N1,S2,int(T3,T2)) | C2], R2, _, F).               
sat_un([un(S1,S2,I)|R1], R2, c, F) :-              % un(s1,s2,int(...)) (rule 8(ii))
         nonvar(I), is_int(I,T1,T2), T1 =< T2,
         sunify(N1 with T1,S2,C1), append(C1,R1,C2),
         T3 is T1 + 1,
         sat_step([T1 nin N1,set(N1),un(S1,N1,int(T3,T2)) | C2], R2, _, F).
sat_un([un(S1,S2,I)|R1], R2, c, F) :-              % un(s1,s2,int(...)) (rule 8(iii))
         nonvar(I), is_int(I,T1,T2), T1 =< T2, !,
         sunify(N1 with T1,S1,C1),
         sunify(N2 with T1,S2,C2),
         append(C1,R1,C3), append(C2,C3,C4),
         T3 is T1 + 1,
         sat_step([T1 nin N1,T1 nin N2,set(N1),set(N2),un(N1,N2,int(T3,T2)) | C4], R2, _, F).
sat_un([un(S1,S2,S3)|R1],R2,c,F):-                  % un(s1,s2,{...})  (rule 4)  
         nonvar(S3), S3=_T2 with T1,!, 
         sunify(N with T1,S3,C1),
         ( sunify(N1 with T1,S1,C2),                             % 4(i)
           append(C1,C2,C3), 
           R = [T1 nin N,T1 nin N1,T1 nin S2,set(N1),set(N),un(N1,S2,N)|C3]
         ;
           sunify(N1 with T1,S2,C2),                             % 4(ii)
           append(C1,C2,C3), 
           R = [T1 nin N,T1 nin N1,T1 nin S1,set(N1),set(N),un(S1,N1,N)|C3]
         ;
           sunify(N1 with T1,S1,C21), sunify(N2 with T1,S2,C22), % 4(iii)
           append(C21,C22,C2), append(C1,C2,C3), 
           R = [T1 nin N,T1 nin N1,T1 nin N2,set(N1),set(N2),set(N),un(N1,N2,N)|C3] 
         ),                
         append(R,R1,R3),
         sat_step(R3,R2,_,F).
sat_un([un(I, S, X)|R1], R2, c, F) :-                % un(int(...),s,X) (rule 9.a(i))
         var(X), 
         nonvar(I), is_int(I, T1, T2), T1 =< T2,
         T3 is T1 + 1,
         sunify(N with T1, X, C1),
         append(C1, R1, C2),
         sat_step([T1 nin N,T1 nin S,set(N),un(int(T3,T2),S,N) | C2], R2, _, F).
sat_un([un(I, S, X)|R1], R2, c, F) :-                % un(int(...),s,X) (rule 9.a(ii))
         var(X), 
         nonvar(I), is_int(I, T1, T2), T1 =< T2,!,
         T3 is T1 + 1,
         sunify(N with T1, X, C1),
         sunify(N1 with T1, S, C2),
         append(C1, R1, C3),
         append(C2, C3, C4),
         sat_step([T1 nin N,T1 nin N1,set(N),set(N1),un(int(T3,T2),N1,N) | C4], R2, _, F).
sat_un([un(S,I,X)|R1],R2,c,F):-                      % un(s,int(...),X) (rule 9.b(i) and 9.b(ii))            
         var(X),
         nonvar(I), is_int(I, _T1, _T2),!,
         sat_step([un(I,S,X)|R1],R2,_,F).   
sat_un([un(S,T,X)|R1],R2,c,F):-                      % un({...},s2,X) (rule 5.a(i))
         var(X), 
         nonvar(S), S=_T2 with T1, 
         sunify(N1 with T1,S,C), append(C,R1,R3),
         X = N with T1,
         sat_step([T1 nin N1,T1 nin T,T1 nin N,set(N),set(N1),un(N1,T,N)|R3],R2,_,F).
sat_un([un(S,T,X)|R1],R2,c,F):-                      % un({...},s2,X)  (rule 5.a(ii))
         var(X), 
         nonvar(S), S =_T2 with T1,!,                        
         sunify(N1 with T1,S,C1), sunify(N2 with T1,T,C2),
         append(C1,C2,C3), append(C3,R1,R3),
         X = N with T1, 
         sat_step([T1 nin N1,T1 nin N2,T1 nin N,set(N),set(N1),set(N2),un(N1,N2,N)|R3],R2,_,F).
sat_un([un(T,S,X)|R1],R2,c,F):-                      % un(s1,{...},X)  (rule 5.b(i) and 5.b(ii))            
         nonvar(S), S=_T2 with _T1, var(X),!,
         sat_step([un(S,T,X)|R1],R2,_,F).   

unify_empty(S) :-
       var(S), !, S = {}.
unify_empty({}) :- !.
unify_empty(S) :- !,
       is_int(S,L,H),
       L > H.

%%%%%%%%%%%%%%%%%%%%%% disjointness (disj/2)

sat_disj([disj(X,Y)|R1],R2,c,F):-                            % disj(X,X) (rule 2)
        var(X), var(Y), samevar(X,Y),!,
        X = {},
        sat_step(R1,R2,_,F).                                 
sat_disj([disj(X,Y)|R1],[disj(X,Y)|R2],Stop,F):-             % disj(X,Y) (pre-)solved form
        var(X), var(Y),!,
        sat_step(R1,R2,Stop,F).
sat_disj([disj(Set1,Set2)|R1],R2,c,F):-                      % disj({...},{...}) (rule 4)
        nonvar(Set1), Set1 = S1 with T1,
        nonvar(Set2), Set2 = S2 with T2,!,
        sat_step([T1 neq T2,T1 nin S2,T2 nin S1,set(S1),set(S2),disj(S1,S2)|R1],R2,_,F).
sat_disj([disj(Set,X)|R1],R2,c,F):-                          % disj({...},X)   (rule 3.a)
        nonvar(Set), Set = T2 with T1,
        var(X),!,
        sat_step([T1 nin X,set(T2),disj(X,T2)|R1],R2,_,F).
sat_disj([disj(X,Set)|R1],R2,c,F):-                          % disj(X,{...})   (rule 3.b)
        nonvar(Set), Set = T2 with T1,
        var(X),!,
        sat_step([T1 nin X,set(T2),disj(X,T2)|R1],R2,_,F).
sat_disj([disj(Set1,_)|R1],R2,c,F):-                         % disj({},t)  (rule 1.a + 6(ii).a)
        nonvar(Set1), is_empty(Set1),!,
        sat_step(R1,R2,_,F).
sat_disj([disj(_,Set2)|R1],R2,c,F):-                         % disj(t,{})  (rule 1.b + 6(ii).b)
        nonvar(Set2), is_empty(Set2),!,
        sat_step(R1,R2,_,F).
sat_disj([disj(I1,I2)|R1],R2,c,F):-               % disj(int(...),int(...))  (rule 5)
        nonvar(I1), is_int(I1,S1,S2),        
        nonvar(I2), is_int(I2,T1,T2),!,        
        (solve_FD(S2 + 1 =< T1)
         ;
         solve_FD(T2 + 1 =< S1)
         ;
         solve_FD(S2 + 1 =< T1), solve_FD(T2 + 1 =< S1)
        ),
        sat_step(R1,R2,c,F).
sat_disj([disj(I1,Set)|R1],R2,c,F):-               % disj(int(...),t)  (rule 6.a)
        nonvar(I1), is_int(I1,S1,S2),!,
        S3 is S1 + 1,
        sat_step([S1 nin Set, disj(int(S3,S2),Set)|R1],R2,c,F).
sat_disj([disj(Set,I1)|R1],R2,c,F):-               % disj(t,int(...))  (rule 6.b)
        nonvar(I1), is_int(I1,S1,S2),!,
        S3 is S1 + 1,
        sat_step([S1 nin Set, disj(int(S3,S2),Set)|R1],R2,c,F).
       
%%%%%%%%%%%%%%%%%%%%%% not union (nun/3)

sat_nun([nun(S1,S2,S3)|R1],R2,c,F):-                         % nun(s1,s2,s3) (rule 1(i))
        sat_step([N in S3,N nin S1,N nin S2|R1],R2,_,F).
sat_nun([nun(S1,_S2,S3)|R1],R2,c,F):-                        % (rule 1(ii))
        sat_step([N in S1,N nin S3|R1],R2,_,F).
sat_nun([nun(_S1,S2,S3)|R1],R2,c,F):-                        % (rule 1(iii))
        sat_step([N in S2,N nin S3|R1],R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% not disjointness (ndisj/2)

sat_ndisj([ndisj(I1,I2)|R1],R2,c,F):-                       % ndisj(int(...),int(...)) (rule 1)
        nonvar(I1), is_int(I1,S1,S2),        
        nonvar(I2), is_int(I2,T1,T2),!,        
        (solve_FD(S1 =< T1), solve_FD(T1 =< S2)
         ;
         solve_FD(T1 =< S1), solve_FD(S1 =< T2)
        ),
        sat_step(R1,R2,c,F).
sat_ndisj([ndisj(S,T)|R1],R2,c,F):-                          % ndisj({...},{...}) (rule 2)
        sat_step([N in S, N in T|R1],R2,_,F).


%%%%%%%%%%%%%%%% set cardinality (size/2)              

sat_size([size(S,N)|R1],[solved(size(S,N),l)|R2],c,F):-  
        var(S),var(N),!,                                     % size(S,N) (pre-solved form)
        solve_FD(N >= 0),
%        solve_FD(N < 10000),    %to fix an a-priori upper limit to set cardinality
        sat_step(R1,R2,_,F).
sat_size([size({},0)|R1],R2,c,F):-!,                         % size({},t)
        sat_step(R1,R2,_,F).
sat_size([size(I,T)|R1],R2,c,F):-                            % size(int(a,b),t)
        nonvar(I), I=int(A,B),!,
        solve_FD(T is B-A+1),
        sat_step(R1,R2,_,F).
sat_size([size(S,T)|R1],R2,c,F):-                            % ground case
        ground(S),
        norep_in_set(S,SS),
        g_size(SS,T),!,
        sat_step(R1,R2,_,F).
sat_size([size(S,T)|R1],R2,c,F):-                            % size(S,k), k integer constant,
        var(S),!,                                            % S variable
        solve_FD(T >= 1),
        S = R with X,
        solve_FD(M is T-1),
        sat_step([X nin R,set(R),integer(M),size(R,M)|R1],R2,_,F). 
sat_size([size(R with X,T)|R1],R2,c,F):-                            % size({...},t)
        solve_FD(T >= 1),
        solve_FD(M is T-1),
        sat_step([X nin R,set(R),integer(M),size(R,M)|R1],R2,_,F). 
sat_size([size(R with X,T)|R1],R2,c,F):-                            % size({...},t)
        solve_FD(T >= 1),
        solve_FD(M is T-1),
        sat_step([R=N with X,set(N),X nin N,integer(M),size(N,M)|R1],R2,_,F).


%%%%%%%%%%%%%%%% Rewriting rules for type constraints %%%%%%%%%%%%%%%%%%%              

%%%%%%%%%%%%%%%%%%%%%% set (set/1)

sat_set([set(X)|R1],[set(X)|R2],Stop,F):-        % solved form
        var(X),!,
        sat_step(R1,R2,Stop,F).
sat_set([set(X)|R1],R2,c,F):-                    % set({}) (rule 1)
        X == {}, !,
        sat_step(R1,R2,_,F).
sat_set([set(X)|R1],R2,c,F):-                    % set({...}) (rule 2.a)
        X = _S with _A, !,
        sat_step(R1,R2,_,F).
sat_set([set(int(A,B))|R1],R2,c,F):-             % set(int(...)) (rule 2.b)
        int_term(int(A,B)),!, 
        sat_step([integer(A),integer(B)|R1],R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% bag (bag/1)

sat_bag([bag(X)|R1],[bag(X)|R2],Stop,F):-       % solved form
        var(X),!, 
        sat_step(R1,R2,Stop,F).
sat_bag([bag(X)|R1],R2,c,F):- 
        X == {}, !,
        sat_step(R1,R2,_,F).
sat_bag([bag(X)|R1],R2,c,F):-                    
        X = _S mwith _A,
        sat_step(R1,R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% list (list/1)

sat_list([list(X)|R1],[list(X)|R2],Stop,F):-       % solved form
        var(X),!, 
        sat_step(R1,R2,Stop,F).
sat_list([list(X)|R1],R2,c,F):- 
        X == [], !,
        sat_step(R1,R2,_,F).
sat_list([list(X)|R1],R2,c,F):-                    
        X = [_A|_S],
        sat_step(R1,R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% integer (integer/1)

sat_integer([integer(X)|R1],[integer(X)|R2],Stop,F):-  % solved form
        var(X),!,    
        sat_step(R1,R2,Stop,F).
sat_integer([integer(T)|R1],R2,c,F):-                  % integer(t), t is an integer constant            
        integer(T),
        sat_step(R1,R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% not integer (ninteger/1)

sat_ninteger([ninteger(X)|R1],[ninteger(X)|R2],Stop,F) :-  % solved form
       var(X), !,    
       sat_step(R1, R2, Stop, F).
sat_ninteger([ninteger(X)|R1], R2, c, F) :-
       \+integer(X),
       sat_step(R1, R2, _, F).

%%%%%%%%%%%%%%%%%%%%%%% delay mechanism %%%%%%%%%%%%%%%%%%%%%%%%%%%%%              

sat_delay([delay(A,_G)|R1],R2,c,f) :- !,
        solve_goal_nodel(A,C2),
        append(C2,R1,R3),
        sat_step(R3,R2,_,f).
sat_delay([delay(A,G)|R1],R2,c,F) :- 
        solve_goal(G,C1),!,
        solve_goal(A,C2),
        append(C1,C2,C3),
        append(C3,R1,R3),
        sat_step(R3,R2,_,F).
sat_delay([X|R1],[X|R2],Stop,F):-
        sat_step(R1,R2,Stop,F).

%%%Solve goal G without generating any new delay
solve_goal_nodel(G,ClistNew) :-
       constrlist(G,GClist,GAlist),
       solve_goal_nodel(GClist,GAlist,ClistNew). 
solve_goal_nodel(Clist,[],CListCan):- !, 
       sat(Clist,CListCan,f). 
solve_goal_nodel(Clist,[true],CListCan):- !, 
       sat(Clist,CListCan,f). 
solve_goal_nodel(Clist,[A|B],CListOut):-
       sat(Clist,ClistSolved,f),
       ssolve(A,ClistCl,AlistCl),
       append(ClistSolved,ClistCl,ClistNew),
       append(AlistCl,B,AlistNew),
       solve_goal_nodel(ClistNew,AlistNew,CListOut).


%%%%%%%%%%%%%%%%%%%%%%%%% solved mechanism %%%%%%%%%%%%%%%%%%%%%%%%%%%              

sat_solved([solved(T in I,LG)|R1],[solved(T in I,LG)|R2],Stop,F):-                          
       var(I),                               % t in X, X list (pre-solved form)
       occur_check(I,T), !,                    
       sat_step(R1,R2,Stop,F).
sat_solved([solved(T in I,_)|R1],R2,R,F):- !,                        
       sat_in([T in I|R1],R2,R,F).

sat_solved([solved(un(X,Y,Z),LG)|R1],[solved(un(X,Y,Z),LG)|R2],Stop,F):-                          
       X \== Y, var(X), var(Y), var(Z), !,  % un(X,Y,Z)  (pre-solved form)
       sat_step(R1,R2,Stop,F).
sat_solved([solved(un(X,Y,Z),_)|R1],R2,R,F):- !,                        
       sat_un([un(X,Y,Z)|R1],R2,R,F).

sat_solved([solved(size(S,N),LG)|R1],[solved(size(S,N),LG)|R2],Stop,F):-                          
       var(S),var(N),!,                      % size(S,N)  (pre-solved form)
       sat_step(R1,R2,Stop,F).
sat_solved([solved(size(S,N),_)|R1],R2,R,F):- !,                        
       sat_size([size(S,N)|R1],R2,R,F).


%%%%%%%%%%%%%%%%%%%%%%% ground implementation %%%%%%%%%%%%%%%%%%%%%%%              

g_neq(T1,T2) :-
         \+sunify(T1,T2,_).

% deterministic membership (for intervals/sets/multisets/lists): 
% g_member(T,A) is true if A contains T (T, A non-variable terms)
g_member(X,int(A,B)):- !,     
        integer(X), X >= A, X =< B.
g_member(X,S):-
        aggr_comps(S,Y,_R),
        sunify(X,Y,_), !.
g_member(X,S):-
        aggr_comps(S,_Y,R),
        g_member(X,R).

g_subset({},_).
g_subset(R with X,S2) :-
         g_member(X,S2),
         g_subset(R,S2).

g_size({},0).
g_size(R with A,N):-
       g_member(A,R),!,
       g_size(R,N).
g_size(R with _A,N):-
       solve_FD(N is M+1),
       g_size(R,M).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%  Global checks   %%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
global_check([],_,[]) :- !.
global_check([W neq T|RC],GC,NewC) :-    % un and neq
    find_un(W,GC),!,
    mk_new_constr(W,T,OutC),
    append(OutC,CC,NewC),
    global_check(RC,GC,CC).
global_check([C|RC],GC,[C|NewC]) :-      % type clashes
    type_constr(C,_,_),!,
    \+type_err(C,RC),   
    global_check(RC,GC,NewC).
global_check([solved(T in X,l)|RC],GC,[solved(T in X,g),T neq T1|NewC]) :-    	  
    var(X),                              % lists: T in X & T1 nin X
    find_nin(X,GC,T1),!,
    global_check(RC,GC,NewC).
global_check([solved(size(X,N),_)|RC],GC,NewC) :- 
    var(X),var(N),                       % conflicting sizes for the same set
    find_size(X,RC,M),!,
    N = M,
    global_check(RC,GC,NewC).
global_check([C|RC],GC,[C|NewC]) :-
    global_check(RC,GC,NewC).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% auxiliary predicates for global_check/3

mk_new_constr(W,T,OutC):-
       (W = M with N, OutC = [N nin T,set(M)] ;
        OutC = [N in T,N nin W] ;
        W = {}, OutC = [T neq {}]).

type_constr(set(X),X,set) :-!.
type_constr(bag(X),X,bag) :-!.
type_constr(list(X),X,list) :-!.
type_constr(integer(X),X,integer).

type_err(integer(X),[ninteger(X)|_R]):- !.
type_err(C,[B|_R]):- 
     type_constr(C,X,F1), type_constr(B,Y,F2),
     X == Y, F1 \== F2,!.
type_err(A,[_|R]):- 
     type_err(A,R).

find_un(X,[solved(un(A,_,_),_)|_]) :- X == A,!.
find_un(X,[solved(un(_,A,_),_)|_]) :- X == A,!.
find_un(X,[solved(un(_,_,A),_)|_]) :- X == A,!.
find_un(X,[_|R]) :- 
       find_un(X,R).

find_integer(X,[integer(Y)|_]) :- 
       X == Y,!.
find_integer(X,[_|R]) :- 
       find_integer(X,R).

find_size(X,[solved(size(Y,N),_)|_],N) :-
       X == Y,!.
find_size(X,[_|R],M) :- 
       find_size(X,R,M).

find_nin(X,[T1 nin Y|_],T1) :-
       X == Y,!.
find_nin(X,[_|R],T1) :-
       find_nin(X,R,T1).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%  Labeling and final check   %%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
final_sat(C,SFC):- 
      check_domain(C),              %force labeling for integer variables;  
      sat(C,RevC,f),                %call the constraint solver (in 'final' mode); 
      final_sat_cont(RevC,C,SFC).
final_sat_cont(RevC,C,RevC) :-
      RevC == C,!.                  %if C==RevC, then no rewriting has been applied:
final_sat_cont(RevC,_C,SFC) :-      %RevC is the resulting constraint; 
      final_sat(RevC,SFC).          %otherwise, call 'final_sat' again
  
check_domain(C):-                        %to force labeling (if possible) for integer variables  
      memberrest(integer(X),C,CRest),!,  %that are still uninstantiated in the constraint C 
      labeling(X),
      check_domain(CRest).
check_domain(_).
                       

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     FD constraints 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

solve_FD(Constr) :-             % Solve the constraint 'Constr' using the FD solver
       tau(Constr,FD_Constr),
       call(FD_Constr).

tau(X is E,X #= E).             % The translation function: from SET constraints to FD
tau(X =< Y,X #=< Y).            % constraints, and vice versa
tau(X >= Y,X #>= Y).             
tau(X < Y,X #< Y).              
tau(X > Y,X #> Y).              
tau(X neq T,X #\= T).
tau(T in int(A,B),T in A..B) :- !.
tau(T in D,T in D).

labeling(_) :-                     % if nolabel, do nothing        
       nolabel,!.                     
labeling(X) :-                     % if the variable X has a closed domain associated 
       get_domain(X,X in D),!,     % with it, then X is (non-deterministically) instantiated 
       labeling1(X,D).             % to every value belonging to the domain.             
labeling(_).                       % Otherwise, the predicate is true and X remains unchanghed


%%%%%%%%%%%%%%%%% for SICStus Prolog

get_domain(X,(X in D)) :-          % get_domain(X,FDc): true if X is a variable and 
       var(X),                     % FDc is the interval membership constraint for X
       frozen(X,(X in D)).

labeling1(_X,inf.._B) :- !.        % e.g., X in inf..1  --> no labeling
labeling1(_X,_A..sup) :- !.        % e.g., X in 1..sup  --> no labeling
labeling1(X,(I) \/ (A..sup)) :-    % e.g., X in (inf..2)\/(4..5)\/(7..9)\/(11..sup)
        first_int(I,inf..B,J),!,   % --> labeling on the bounded part
       (X in J,
        indomain(X)
        ;
        X in (inf..B)
        ;
        X in (A..sup)).
labeling1(X,(I) \/ (A..sup)) :- !, % e.g., X in (1..2)\/(4..5)\/(7..sup)
       (X in I,                    % --> labeling on the bounded part
        indomain(X)
        ;
        X in (A..sup)).
labeling1(X,(I) \/ (In)) :-        % e.g., X in (inf..2)\/(4..5)\/(7..9)
        first_int(I,inf..B,J),!,   % --> labeling on the bounded part
       (X in (J) \/ (In),
        indomain(X)
        ;
        X in (inf..B)).
labeling1(X,_D) :-                 % e.g., X in (1..2)\/(4..5)\/(7..9)
        indomain(X).

first_int((_A .. _B),(_A .. _B),(1 .. 0)) :- !.  % first_int(+Int,?Rest,?First) 
first_int((I) \/ (In),I0,(IRest) \/ (In)) :-     % 'Int' is a disj. of intervals and
       first_int(I,I0,IRest).                    % 'First' is the first disjunct
                                                 % 'Rest' the remaining part

%%%%%%%%%%%%%%%%% for SWI-Prolog

%get_domain(X,FDc) :-              % get_domain_constr(X,FDc): true if X is a variable and 
%       var(X),                    % FDc is the interval membership constraint for X
%       get_attr(X,bounds,FDc).

%labeling1(...) 
%   ...
%*** TO BE COMPLETED


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Program defined constraints 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

setlog((true :- true),sys).
setlog((less(A,B,C) :- A=C with B & B nin C & set(C) & true),sys).
setlog((nsubset(A,B) :- C in A & C nin B & set(B) & true),sys).
setlog((ssubset(A,B) :- A neq B & subset(A,B) & true),sys).
setlog((int(A,B,C) :- un(D,C,A) & un(E,C,B) & disj(D,E) & 
                      set(A) & set(B) & set(C) & true),sys).
setlog((nint(A,B,C) :- D in C & 
                       (D nin A & set(A) & true or D nin B & set(B) & true) & 
                       true),sys).
setlog((diff(A,B,C) :- subset(C,A) & un(B,C,D) & subset(A,D) & disj(B,C) & 
                       set(B) & true),sys).
%%%Alternative implementation of diff(A,B,C)
%%% subset(C,A) & disj(B,C) & size(C,NC) & size(A,NA) & size(B,NB) & NC >= NA - NB

setlog((ndiff(A,B,C) :- diff(A,B,D) & D neq C & set(C) & true),sys).
setlog((sdiff(A,B,C) :- diff(A,B,D) & diff(B,A,E) & un(D,E,C) & set(C) & true),sys).

setlog((A =:= B :- X is A & Y is B & X = Y & true),sys).
setlog((A =\= B :- X is A & Y is B & X neq Y & true),sys).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%        The front-end         %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%   Consulting and storing {log} clauses  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

context(usr).

read_loop_np(FileStream):-
        setlog_read(FileStream,Clause), 
        Clause \== end_of_file,!, 
        setassert(Clause),
        read_loop_np(FileStream).
read_loop_np(_).

read_loop(FileStream,N):-
        setlog_read(FileStream,Clause), 
        Clause \== end_of_file,!, 
        assert_or_solve(Clause,N),
        N1 is N + 1,
        read_loop(FileStream,N1).
read_loop(_,_).

setlog_read(Stream,Term) :- 
       on_exception(syntax_error(_,_,Msg,_,_),read(Stream,Term),syntax_error_cont_msg(Msg)).

assert_or_solve((:- Goal),_):-!,
        solve(Goal,_).
assert_or_solve(Clause,N):- 
        setassert(Clause),
        write('Clause '), write(N), write(' stored'), nl.

setassert(Clause):- 
    context(Ctxt),
    setassert(Clause,Ctxt).
setassert(Clause,Ctxt):- 
    sf_in_clause(Clause,ExplClause),
    preproc_clause(ExplClause,ExtClause),
    ruq_in_clause(ExtClause,BaseClause),
    assert(setlog:setlog(BaseClause,Ctxt)).

ssetassert(Clause):- 
    context(Ctxt),
    ssetassert(Clause,Ctxt). 
ssetassert(Clause,Ctxt):- 
    ruq_in_clause(Clause,BaseClause),
    assert(setlog:setlog(BaseClause,Ctxt)).

switch_ctxt(NewCtxt,OldCtxt) :-
    retract(context(OldCtxt)),
    assert(context(NewCtxt)).

tmp_switch_ctxt(OldCtxt) :-
    context(OldCtxt), 
    functor(OldCtxt,tmp,_),!.
tmp_switch_ctxt(OldCtxt) :-
    retract(context(OldCtxt)),
    NewCtxt =.. [tmp,OldCtxt],
    assert(context(NewCtxt)).

syntax_error_cont_msg(Text) :-
       write('Syntax error'), nl,
       write(Text), nl.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%   Program listing
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

list_all :-                            
      setlog((H :- B),usr), 
      postproc(H,Hnew), write(Hnew), 
      write_body(B).
list_all. 

write_body(true) :-
      !, write('.'),nl,nl,
      fail.
write_body(type(_) & true) :-
      !, write('.'),nl,nl,
      fail.
write_body(B) :-
      write((':-')), nl, 
      write('   '), postproc(B,Bnew), write_atoms(Bnew), write('.'),nl,nl,
      fail.

write_atoms(B & true) :-
      !, write_atom(B).
write_atoms(B1 & B2) :- 
      write_atom(B1), 
      (B2 = (type(_) & _), ! 
      ;
       write(' & '), nl, write('   ')), 
      write_atoms(B2).

write_atom(ruq_call(Aggr,Goal_name,FV)) :- 
      !, write('forall('),write(X),write(' in '),write(Aggr),write(','), 
      RUQ_body_pred =.. [Goal_name,X|FV], setlog((RUQ_body_pred :- RUQ_body),_),
      extract_vars(RUQ_body,Vars),
      remove_list([X|FV],Vars,LocalVars),
      postproc(RUQ_body,RUQ_bodyNew),
      (LocalVars = [],!,
       write_atoms(RUQ_bodyNew), write(')')
       ;
       write('exists('),write(LocalVars),write(','),
       write_atoms(RUQ_bodyNew), write('))') 
      ).
write_atom(type(_)) :- !.
write_atom(neg A) :- !,
      write('neg '), 
      write('('), write_atoms(A), write(')').
write_atom(naf A) :- !,
      write('naf '), 
      write('('), write_atoms(A), write(')').
write_atom(call(A)) :- !,
      write(call),
      write('('), write_atoms(A), write(')').
write_atom((A)!) :- !,
      write('('),
      write_atoms(A),
      write(')!').
write_atom(delay(A,G)) :- !,
      write(delay),write('('),
      write_atoms(A),write(','),
      write_atoms(G),
      write(')').
write_atom((A1 or A2)) :- !,
      write('('), write_atoms(A1),
      write(' or '),
      write_atoms(A2), write(')').
write_atom(B) :- 
      write(B).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Preprocessing 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%% Set (multiset) preprocessor: 
%%%%%%%%%%%%% from {...} (*{...}) to 'with' ('mwith') notation  

preproc_goal(G,PGext) :-
        preproc(G,PG,TypeCL), 
        norep_in_list(TypeCL,TypeCLRid),   
        list_to_conj(TypeCC,TypeCLRid),
        conj_append(PG,TypeCC,PGext).

preproc_clause(Cl,(PA ':-' PBext)) :-
        preproc(Cl,(PA ':-' PB),TypeCL), 
        norep_in_list(TypeCL,TypeCLRid),   
        list_to_conj(TypeCC,TypeCLRid),
        conj_append(PB,TypeCC,PBext).

preproc(X,X,[]):- 
        var(X),!.      
preproc(X,X,[]):-
        atomic(X),!.
preproc(X,Y1,C):-
        is_set_ext(X), !,
        set_preproc(X,Y,C),
        norep_in_set(Y,Y1). 
preproc(X,Y,C):-
        is_bag_ext(X),!,
        bag_preproc(X,Y,C).
preproc([A|X],[A1|X],[type(list(X))|C]):- 
        var(X), !,
        preproc(A,A1,C).
preproc((A & B),(A1 & B1),C):-
        !, preproc(A,A1,C1), preproc(B,B1,C2),
        append(C1,C2,C).
preproc((A ':-' B ),(A1 ':-' B1 ),C) :-
        !, preproc(A,A1,C1), preproc(B,B1,C2),
        append(C1,C2,C).
preproc(X,Z,C):-
        nonvar(X), 
        functor(X,F,_A), 
        =..(X,[F|ListX]),
        preproc_all(ListX,ListZ,C1),
        =..(Z,[F|ListZ]),
        (gen_type_constrs(Z,TypeC),!,
         append(C1,TypeC,C)
        ;
         C1 = C
        ).

preproc_all([],[],[]).
preproc_all([A|L1],[B|L2],C):-
        preproc(A,B,C1),
        preproc_all(L1,L2,C2),
        append(C1,C2,C).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% set preprocessing

set_preproc({},{},[]):- !.
set_preproc(X with A,X with B,[type(set(X))|Constrs]) :-
        var(X),!, preproc(A,B,Constrs).       
set_preproc(X with A,Y with B,Constrs) :-
        is_set_ext(X),!,
        preproc(A,B,Constrs1), preproc(X,Y,Constrs2),
        append(Constrs1,Constrs2,Constrs). 
set_preproc('{}'(A),B,Constrs):-
        set_preproc_elems(A,B,Constrs),!.
set_preproc(_,_,_):-
        msg_sort_error(set), 
        setlog.

set_preproc_elems(A,{} with A,[]):-
        var(A), !.
set_preproc_elems((A1,B1),B2 with A2,Constrs):- !,
        preproc(A1,A2,Constrs1),
        set_preproc_elems(B1,B2,Constrs2),
        append(Constrs1,Constrs2,Constrs).
set_preproc_elems(S,WT,Constrs):- 
        aggr_comps_ext(S,_A,_X),!,
        set_preproc_set(S,WT,Constrs). 
set_preproc_elems(A1,{} with A2,Constrs):-
        preproc(A1,A2,Constrs).

set_preproc_set(S,X with B,[type(set(X))|Constrs]):-  
        aggr_comps_ext(S,A,X), 
        var(X),!, 
        preproc(A,B,Constrs).
set_preproc_set(S,Y with B,Constrs):-   
        aggr_comps_ext(S,A,X), 
        is_set_ext(X),!,
        preproc(A,B,Constrs1), preproc(X,Y,Constrs2),
        append(Constrs1,Constrs2,Constrs).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% bag preprocessing

bag_preproc({},{},[]):-!.	
bag_preproc(X mwith A,X mwith B,[type(bag(X))|Constrs]) :-
        var(X),!, preproc(A,B,Constrs).       
bag_preproc(X mwith A,Y with B,Constrs) :-
        is_bag_ext(X),!,
        preproc(A,B,Constrs1), preproc(X,Y,Constrs2),
        append(Constrs1,Constrs2,Constrs). 
bag_preproc((*{}(A)),B,Constrs):- 
	  bag_preproc_elems(A,B,Constrs),!.
bag_preproc(_,_,_):-
	  msg_sort_error(bag), 
        setlog.	

bag_preproc_elems(A, {} mwith A,[]):-
	  var(A),!.
bag_preproc_elems((A1,B1),B2 mwith A2,Constrs):-
	  !,preproc(A1,A2,Constrs1),
        bag_preproc_elems(B1,B2,Constrs2),
        append(Constrs1,Constrs2,Constrs).
bag_preproc_elems(M,MWT,Constrs):-         
        aggr_comps_ext(M,_A,_X),!,
        bag_preproc_bag(M,MWT,Constrs).    
bag_preproc_elems(A1,{} mwith A2,Constrs):-
	  preproc(A1,A2,Constrs).

bag_preproc_bag(M,X mwith B,[type(bag(X))|Constrs]):-       
	  aggr_comps_ext(M,A,X), var(X),!,
        preproc(A,B,Constrs).
bag_preproc_bag(M,Y mwith B,Constrs):-!,    
	  aggr_comps_ext(M,A,X), is_bag_ext(X),!,
        preproc(A,B,Constrs1), preproc(X,Y,Constrs2),
        append(Constrs1,Constrs2,Constrs).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% type constraints generation

gen_type_constrs(_T1 in T2,[type(aggr(T2))]) :- !.
gen_type_constrs(_T1 nin T2,[type(aggr(T2))]) :- !.
gen_type_constrs(un(T1,T2,T3),[type(set(T1)),type(set(T2)),type(set(T3))]) :- !.
gen_type_constrs(nun(T1,T2,T3),[type(set(T1)),type(set(T2)),type(set(T3))]) :- !.
gen_type_constrs(disj(T1,T2),[type(set(T1)),type(set(T2))]) :- !.
gen_type_constrs(ndisj(T1,T2),[type(set(T1)),type(set(T2))]) :- !.
gen_type_constrs(subset(T1,T2),[type(set(T1)),type(set(T2))]) :- !.
gen_type_constrs(size(T1,T2),[type(set(T1)),type(integer(T2))]).   

%%%%%%%%%%%%% Auxiliary predicates for set/multiset preprocessing

is_set_ext(X):- functor(X,{},_),!.
is_set_ext(_ with _).

is_bag_ext({}):-!.
is_bag_ext(X):- X = *A, functor(A,{},_), !.
is_bag_ext(_ mwith _).

aggr_comps_ext((A \ R),A,R) :-!.
aggr_comps_ext((A / R),A,R). %for compatibility with previous releases

is_ker(T) :-
        nonvar(T), functor(T,F,N),
        (F \== with,! ; N \== 2).

msg_sort_error(set) :- 
       write(' wrong set term '), nl.
msg_sort_error(bag) :- 
       write(' wrong multiset term '), nl.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%   Intensional set preprocessing        
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
                            
sf_in_clause((H :- B),(H1 :- B1)):-
    !,sf_in_literal(H,[H1|List1]),
    sf_in_goal(B,List2),
    append(List1,List2,List),
    list_to_conj(B1,List).      
sf_in_clause(A,(H :- B)):-
    sf_in_hliteral(A,[H|List]),
    list_to_conj(B,List).

sf_in_goal(A,[A]):-
    var(A),!.    
sf_in_goal(A & B,NewL):-    
    !, sf_in_literal(A,A1),
    sf_in_goal(B,B1),
    append(A1,B1,NewL).
sf_in_goal(A,NewL):-
    !, sf_in_literal(A,NewL).    

sf_in_literal(A or B,[A1 or B1]):-
    !, sf_in_goal(A,L1),
    sf_in_goal(B,L2),
    list_to_conj(A1,L1),
    list_to_conj(B1,L2).
sf_in_literal(neg A,[neg A1]):-
    !, sf_in_goal(A,L1),
    list_to_conj(A1,L1).
sf_in_literal(naf A,[naf A1]):-
    !, sf_in_goal(A,L1),
    list_to_conj(A1,L1).
sf_in_literal(call(A),[call(A1)]):-
    !, sf_in_goal(A,L1),
    list_to_conj(A1,L1).
sf_in_literal(assert(Cl),[assert(Cl1)]):-
    !, sf_in_clause(Cl,Cl1).
sf_in_literal((A)!,[(A1)!]):-
    !, sf_in_goal(A,L1),
    list_to_conj(A1,L1).
sf_in_literal(delay(A,G),[delay(A1,G1)]):-
    !, sf_in_goal(A,L1),
    sf_in_goal(G,L2),
    list_to_conj(A1,L1),
    list_to_conj(G1,L2).
sf_in_literal(forall(X in S,exists(V,A)),L):-
    !, sf_find([S],[S1],L1),
    sf_in_goal(A,L2),
    list_to_conj(A1,L2),
    append(L1,[forall(X in S1,exists(V,A1))],L).
sf_in_literal(forall(X in S,A),L):-
    !, sf_find([S],[S1],L1),
    sf_in_goal(A,L2),
    list_to_conj(A1,L2),
    append(L1,[forall(X in S1,A1)],L).
sf_in_literal(A,NewA):-                                     
    A =.. [Pname|Args],
    sf_find(Args,Args1,NewL),
    B =.. [Pname|Args1],
    append(NewL,[B],NewA).
        
sf_in_hliteral(A,[B|NewL]):-                                      
    A =.. [Pname|Args],
    sf_find(Args,Args1,NewL),
    B =.. [Pname|Args1].
        
sf_find([],[],[]).
sf_find([Int|R],[Var|S],List):-
    is_sf(Int,X,G),!,
    extract_vars(G,Vars),
    remove_var(X,Vars,Finalvars),
    (Vars = Finalvars, 
          write('ERROR - Formula of a set former must'),
          write(' contain the set former control variable'), nl, 
          setlog ; true),
    sf_translate(Int,Var,L1,Finalvars),
    sf_find(R,S,L2),
    append(L1,L2,List).    
sf_find([A|R],[B|S],List):-
    nonvar(A),
    A =.. [Fname|Rest],
    Rest \== [],!,
    sf_find(Rest,Newrest,List1),
    B =.. [Fname|Newrest],
    sf_find(R,S,List2),
    append(List1,List2,List).
sf_find([A|R],[A|S],List):-
    sf_find(R,S,List).

sf_translate(SF,Y,[Pred],Vars):-
    (SF={X:exists(_Var,Goal)},! ; SF={X : Goal}),
    length([_|Vars],N),    
    newpred(Aux,N,"setlogSF_"),
    Aux=..[AuxName,Y|Vars],
    newpred(Aux1,N,"setlogSF_"), 
    Aux1 =.. [Aux1Name,X|Vars],
    Pred = sf_call(Y,Aux1Name,AuxName,Vars),
    setassert((Aux1 :- Goal)),
    setassert((Aux:- X nin Y & Aux1)).
        
is_sf(Int,X,Phi) :-
    nonvar(Int), Int = {SExpr}, 
    nonvar(SExpr), SExpr = (X : Phi),
    (nonvar(X), !,
     write('ERROR - Control variable in a set former'),
     write(' must be a variable term!'), nl, 
     setlog ; true).
               

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%    R.U.Q. preprocessing  %%%%%%%%%%%           
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
                      
ruq_in_clause((H :- B),(H :- B1)):-    
    ruq_in_goal(B,B1),!.    
ruq_in_clause(H,H).

ruq_in_goal(A,A):-
    var(A),!.    
ruq_in_goal(A & B,GExt):-
    !, ruq_in_goal(A,A1), ruq_in_goal(B,B1),
    conj_append(A1,B1,GExt).    
ruq_in_goal((A or B),((A1) or (B1))):-
    !, ruq_in_goal(A,A1), ruq_in_goal(B,B1).    
ruq_in_goal(neg A,neg(A1)):-
    !, ruq_in_goal(A,A1).    
ruq_in_goal(naf A,naf(A1)):-
    !, ruq_in_goal(A,A1).    
ruq_in_goal(call(A),call(A1)):-
    !, ruq_in_goal(A,A1).    
ruq_in_goal((A)!,(A1)!):-
    !, ruq_in_goal(A,A1).    
ruq_in_goal(delay(A,G),delay(A1,G1)):-
    !, ruq_in_goal(A,A1),
    ruq_in_goal(G,G1).    
ruq_in_goal(forall(X in _S,_Y),_):- 
    nonvar(X), !, 
    write('ERROR - Control variable in a R.U.Q. must be a variable term!'),
    nl, setlog.
ruq_in_goal(forall(X in S,G),NewG):-
    !, extract_vars(G,V),
    remove_var(X,V,Vars),
    ( V = Vars, write('ERROR - Formula of a R.U.Q. must contain'),
          write(' the R.U.Q.control variable'), nl, setlog ; 
      true ),
    length(V,N),
    newpred(Gpred,N,"setlogRUQ_"),
    Gpred =.. [_,X|Vars],
    tmp_switch_ctxt(OldCtxt),
    ( G = exists(_Var,B),!, 
      ssetassert((Gpred :- B)) 
     ;
      ssetassert((Gpred :- G)) ),
    switch_ctxt(OldCtxt,_),
    functor(Gpred,F,N),
    NewG = ruq_call(S,F,Vars).
ruq_in_goal(A,A).
    %% N.B. no check for 'forall(X in {...,t[X],...})'
    %% add 'occur_check(X,S)' to enforce it

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% New predicate generation

newpred_counter(0).

newpred(P,A,T):-
    retract(newpred_counter(Y)), !,
    Z is Y + 1,
    assert(setlog:newpred_counter(Z)),
    name(Y,Ylist),
    append(T,Ylist,Plist),
    name(Pred,Plist),
    mklist(L,A),
    P =.. [Pred|L].


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Postprocessing 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%% Set (multiset) postprocessor:  
%%%%%%%%%%%%% from 'with' ('mwith') to {...} (*{...}) notation  

postproc(X,X):- 
        var(X),!.      
postproc(X,X):-
        atomic(X),!.
postproc(X,Y):-
        nonvar(X), X = _ with _,!,
        norep_in_set(X,X1),
        with_postproc(X1,Y). 
postproc(X,Y):-
	  nonvar(X), X = _ mwith _,!,
	  mwith_postproc(X,Z),
	  mwith_out(Z,Y).
postproc(X,Z):-
        nonvar(X), 
        =..(X,[F|ListX]),
        postproc_all(ListX,ListZ),
        =..(Z,[F|ListZ]).

postproc_all([],[]).
postproc_all([A|L1],[B|L2]):-
        postproc(A,B),
        postproc_all(L1,L2).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% set postprocessing 

with_postproc(A,A) :- var(A),!.
with_postproc(K,K):- is_ker(K), !.
with_postproc(A,'{}'(B)):-
        postproc_list(A,B).

postproc_list(X with A1,(A2 \ X)) :-  
        var(X),!,postproc(A1,A2).
postproc_list({} with A1,A2):- !,
        postproc(A1,A2).
postproc_list(K with A1,(A2 \ K)) :-  
        is_ker(K),!,postproc(A1,A2).
postproc_list(B1 with A1,(A2,B2)):-
        postproc(A1,A2),postproc_list(B1,B2).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% bag postprocessing

mwith_out('{}'(X),*'{}'(X)).

mwith_postproc(A,A) :- var(A),!.
mwith_postproc('{}','{}'):- !.
mwith_postproc(A,'{}'(B)):-
	bag_postproc_list(A,B).

bag_postproc_list(X mwith A1,(A2 \ X)) :-   
	var(X),!,postproc(A1,A2).
bag_postproc_list('{}' mwith A, A):-
	var(A),!.
bag_postproc_list('{}' mwith A1,A2):-!,
	postproc(A1,A2).
bag_postproc_list(B1 mwith A1,(A2,B2)):-
	postproc(A1,A2), bag_postproc_list(B1,B2).

    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%        The help sub-system   %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

setlog_help(gen) :- 
   nl,    
   write('%%%%%%%%%   Syntactic conventions  %%%%%%%%%'),
   nl, nl,
write('   1.  Extensional set/multiset terms:'), nl,                  
   write('        - {a,b,c} is a set containing three elements, a, b, c'),nl,
   write('          (equivalent to {} with c with b with a)'), nl,         
   write('        - {a,b\\R} is the set {a,b} U R'), nl,          
   write('          (equivalent to R with b with a)'), nl,       
   write('        - *{a,b,b} is a multiset containing the elements,'),nl,
   write('          ''a'' (1 occurrence) and  ''b'' (2 occurrences)'),nl,   
   write('          (equivalent to {} mwith c mwith b mwith a)'), nl,         
   write('        - *{a,b\\R} is the multiset *{a,b} U R'), nl,       
   write('          (equivalent to R mwith b mwith a)'), nl,       
   write('        - {} is the empty set/multiset'), nl,                             
   write('        - int(h,k) (interval) is the set of integer numbers'), nl,
   write('          ranging from h to k (h,k integer constants)'), nl, nl,      
write('   2.  General constraints:'), nl,
   write('       (''t1'', ''t2'' any term)'), nl,
   write('        - t1 = t2  (equality)'), nl,
   write('        - t1 neq t2  (non-equality)'), nl, nl, 
write('   3.  Set/multiset/list constraints:'), nl,
   write('       (''t'' any term, ''s'' either a set or an interval,'), nl,
   write('        ''a'' any aggregate (set, interval, multiset, list)'), nl,
   write('        - t in a (membership)'), nl,
   write('        - t nin a (non-membership)'), nl,   
   write('        - un(s1,s2,s3) (union)'), nl,
   write('        - nun(s1,s2,s3) (non-union)'), nl,   
   write('        - disj(s1,s2) (disjointness)'), nl,
   write('        - ndisj(s1,s2) (non-disjointness)'), nl,  
   write('        - less(s1,t,s3) (element removal)'), nl,
   write('        - subset(s1,s2) (subset)'), nl,
   write('        - nsubset(s1,s2,s3) (not subset)'), nl,
   write('        - ssubset(s1,s2) (strict subset)'), nl,
   write('        - int(s1,s2,s3) (intersection)'), nl,
   write('        - nint(s1,s2,s3) (not intersection)'), nl,
   write('        - diff(s1,s2,s3) (difference)'), nl,
   write('        - ndiff(s1,s2,s3) (not difference)'), nl,
   write('        - sdiff(s1,s2,s3) (symmetric difference)'), nl,
   write('        - size(s,n) (cardinality)'), nl,
   write('        - set(s) (s is a set)'), nl,  
   write('        - bag(t) (t is a multiset)'), nl, 
   write('        - list(t) (t is a list)'), nl, nl,
write('   4.  Arithmetic constraints:'), nl,
   write('       (e1, e2 integer expressions, n variable or integer constant)'), nl,
   write('        - n is e1 (equality - with evaluation of expression e)'), nl,
   write('        - e1 =< e2 (less or equal), e1 < e2 (less)'), nl,  
   write('        - e1 >= e2 (greater or equal), e1 > e2 (greater)'), nl,  
   write('        - e1 =:= e2 (equal), e1 =\\= e2 (not equal)'), nl,  
   write('        - integer(n) (n is an integer number)'), nl,  
   write('        - ninteger(n) (n is not an integer number)'), nl, nl,
write('   5.  RUQs: '), nl,                            
   write('       (''a'' either a set or a multiset or a list or an interval int(h,k))'), nl,
   write('        - forall(X in a, G),'), nl, 
   write('          X variable and G any {log} goal containing X'), nl,  
   write('        - forall(X in a, exists(V,G)),'),nl,
   write('        - forall(X in a, exists([V1,...,Vn],G)),'), nl, 
   write('          V1,...,Vn variables local to G'), nl,nl,
write('   6.  Intensional set terms:'), nl,                                 
   write('        - {X : G}, X variable and G any {log} goal containing X'), nl,
   write('        - {X : exists(V,G)}, V variable local to G'), nl,
   write('        - {X : exists([V1,...,Vn],G)}, '), nl, 
   write('          V1,...,Vn variables local to G'), nl,nl,
write('   7.  Syntactic differences w.r.t. std Prolog:'), nl,
   write('        - &  is used in place of  ,  in clause bodies'), nl,
   write('        - or  is used in place of  ;'),
                    write('  to represent goal disjunction.'), nl,
   write('        - neg or naf are used in place of  \\+'),
                    write('  to represent negation (resp., '), nl,
   write('          simplified Constructive Negation and Negation as Failure).'),  
   nl,setlog_help(sbuilt),nl.    
            
setlog_help(built) :-
   setlog_help(sbuilt), 
   nl,
   setlog_help(pbuilt).

setlog_help(sbuilt) :-
   nl,
   write('%%%%%%%%% {log} specific built-in predicates %%%%%%%%%'),
   nl, nl,
   write('   -   setlog/0, setlog_start/0 to (re-)enter {log}'), 
        write('  from the SICStus environment'),nl,   
   write('   -   help/0, help(built), help(lib), help(prolog) to get help information '),
        nl,write('       (resp., general, about {log} built-in predicates, '),
        nl,write('       {log} library predicates, Prolog predicates'),
        nl,write('       for accessing {log})'), nl,
   write('   -   halt/0     to leave {log}'),
        write(' (go back to the SICStus environment) '), nl,
   write('   -   prolog_call/1   to call any Prolog goal'), 
        write('  from the {log} environment'),nl,   
   write('   -   !/1 (used postfix): G!, G any {log} goal: '),
        write('makes G deterministic'), nl,
   write('   -   delay(G,C), G, C any {log} goals: delays '),
        write('execution of G until C holds'), nl,
   write('   -   nolabel/0 - label/0 to deactivate/reactivate the automatic '), 
        nl,write('       FD labeling function'), nl, 
   write('   -   labeling(X) to force labeling for a domain variable X').

setlog_help(pbuilt) :-
   nl,
   write('%%%%%%%% Prolog-like built-in predicates %%%%%%%%'),
   nl, nl,
   write_built_list,
   write('   -   read/1'),nl,
   write('   -   write/1'),nl,
   write('   -   call/1'),nl,
   write('   -   assert/1'),nl,
   write('   -   consult/1'),nl,
   write('   -   listing/0'),nl,
   write('   -   abolish/0'),nl.
  
setlog_help(lib) :-
   nl,
   write('%%%%%%%% {log} library predicates %%%%%%%%'), nl, nl,
   check_lib. 
   
setlog_help(prolog) :- 
   nl,
   write('%%%%%%%% Prolog predicates for accessing {log} facilities %%%%%%%%%'),
   nl, nl,
   write('   -   setlog_call(G), setlog_call(G,C): to call a {log} '), nl,
   write('       goal G, possibly getting an (output) {log} constraint C'), nl,
   write('   -   setlog_sc(C,InCLst,OutCLst): to solve a {log} constraint C'), nl,
   write('       with a (possibly empty) input constraint list InCLst and output'), nl,
   write('       constraint list OutCLst '), nl,
   write('   -   setlog_consult(F): to consult a {log} file F '),nl,
   write('   -   setlog_clause(Cl): to add a {log} clause Cl to the current {log} program '),nl,
   write('   -   setlog_help/0, h/0: to get general help information about {log}'),nl,
   write('   -   setlog/0: to enter the {log} interactive environment'),nl.

write_built_list :-
   sys(N,Ar),
   write('   -   '),write(N),write('/'),write(Ar),nl,
   fail.
write_built_list.
 
check_lib :-
   solve(setlog_lib_help,_),!.
check_lib :-
   write('{log} library predicates not available'),nl,
   write('Type consult(lib) to load the {log} library '),nl.
 
h :- setlog_help(gen).
setlog_help :- setlog_help(gen).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%   Prolog to {log} interface  %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The following predicates allow a Prolog program to use the 
% {log} facilities for set/bag definition and manipulation
% (without leaving the Prolog execution environment).
% In particular, they provide a (Prolog) predicate for calling 
% any {log} goal G, possibly involving {log} set constraints.
% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

setlog_call(Goal) :-
       setlog_call(Goal,_).
setlog_call(Goal,Constr_ext) :-
       op_define,      % not necessary in SICStus Prolog
       copy_term(Goal,NewGoal),
       solve(NewGoal,C),
       add_FDc(C,Constr,_),
       postproc(Constr,Constr_ext),
       postproc(NewGoal,NewGoal_ext),
       postproc(Goal,Goal_ext),
       Goal_ext = NewGoal_ext.

setlog_consult(File) :-    %like setlog_call(consult(File),_)
       op_define,          %but no message is sent to the std output
       setlog_open(File,read,FileStream), 
       sys_special(abolish,_),
       read_loop_np(FileStream),
       close(FileStream). 

setlog_clause(Clause) :-
       setlog_call(assert(Clause),_).

%%%% setlog_sc(+Constraint,+InConstraintList,-OutConstraintList) 

setlog_sc(Constr,InConstrLst,OutConstrLst) :-   %to solve {log} set constraints
       op_define,      
       list_to_conj(InConstr,InConstrLst),      %from list (InConstrLst) to conjunction (InConstr) 
       conj_append(Constr,InConstr,CS),
       copy_term(CS,NewCS),
       preproc_goal(NewCS,NewCSIntl),           %from {...} to 'with' notation;  
       list_to_conj(NewCSIntl,CLstIntl),        %from conjunction (NewCSIntl) to list (CLstIntl) 
       sat(CLstIntl,ResCLstIntl,nf),            %call the constraint solver (in 'non-final' mode); 
       final_sat(ResCLstIntl,OutCLstIntl),      %call the constraint solver again (in 'final' mode); 
       add_FDc(OutCLstIntl,OutFinalCLstIntl,_), %add the possibly remaining interval constraints;
       postproc(OutFinalCLstIntl,OutConstrLst), %from 'with' to {...} notation;  
       postproc(CS,CSExt),
       postproc(NewCS,NewCSExt),
       CSExt = NewCSExt.                        %apply sustitutions to the original variables


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%     Auxiliary predicates     %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%                              %%%%%%%%%%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     List manipulation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

list_term(T) :- 
       nonvar(T), 
       (T=[],! ; T=[_ | _]).  

mklist([],0):- !.
mklist([_|R],N):-
    M is N-1,
    mklist(R,M).

member(X,[X|_R]).
member(X,[_|R]):-member(X,R).

memberrest(X,[X|R],R) :- !.
memberrest(X,[_|R],L):-memberrest(X,R,L).

memberall(A,B,[A|_R],[B|_S]).
memberall(A,B,[_|R],[_|S]):- 
        memberall(A,B,R,S).

append([],L,L).                                     
append([X|L1],L2,[X|L3]):-
        append(L1,L2,L3).

member_strong(A,[B|_R]):- 
         A == B, !.
member_strong(A,[_|R]):- 
         member_strong(A,R).

notin(_,[]).       % not member strong
notin(A,[B|R]):-
    A \== B, notin(A,R).

listunion([],L,L).   
listunion([A|R],X,[A|S]):- 
    notin(A,X),!,
    listunion(R,X,S).
listunion([_A|R],X,S):-
    listunion(R,X,S).

subset_strong([],_L):-!.
subset_strong([X|L1],L2) :-
      member_strong(X,L2),
      subset_strong(L1,L2).

norep_in_list([],[]):-!.
norep_in_list([A|R],S):-
        member_strong(A,R),!,
        norep_in_list(R,S).
norep_in_list([A|R],[A|S]):-
        norep_in_list(R,S).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Set manipulation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

set_term(T) :- 
       nonvar(T), 
       (T={},! ; T=_ with _).        

tail(R with _,R) :- var(R),!.
tail({} with _,{}) :- !.
tail(int(_A,_B) with _,{}) :- !.
tail(R with _,T) :- 
      tail(R,T).

replace_tail(R,N,N) :- var(R),!.
replace_tail({},N,N) :- !.
replace_tail(R1 with X,N,R2 with X) :- 
      replace_tail(R1,N,R2).

%%%% split(S,N,L) true if S is a set term of the form N with tn with ... with t1
%%%% (n >= 0) and L is the list [t1,...,tn]
split(N,N,[]):-
        var(N),!.
split(S with T, N, [T|R]):-
        split(S,N,R).

norep_in_set(X,X):- var(X),!.
norep_in_set(K,K) :- is_ker(K), !.
norep_in_set(R with A,S):-
       set_member_strong(A,R),!,
       norep_in_set(R,S).
norep_in_set(R with A,S with A):-
       norep_in_set(R,S).        

set_length(S,N) :-
        set_length(S,0,N).
set_length(X,_,_) :-
        var(X), !, fail.
set_length(S,N,N) :-
        is_empty(S), !.
set_length(int(A,B),N,M) :- !,
        M is N + (B - A) + 1.
set_length(R with _X,N,M):-
        N1 is N + 1,
        set_length(R,N1,M).

set_member(X,_R with Y,C):-
        sunify(X,Y,C).
set_member(X,R with _Y,C):-
        set_member(X,R,C).

set_member_strong(A,B):-
       nonvar(B),
       B = _ with X, 
       A == X,!.
set_member_strong(A,B):-
       nonvar(B), 
       B = Y with _,
       set_member_strong(A,Y).

list_to_set(L,S,[]) :-            % list_to_set(+list,?set,-constraint)
     var(S),!, 
     mk_set(L,S).             
list_to_set(L,S,C) :-            
     mk_test_set(L,S,C).   
          
mk_set([],{}) :- !.             
mk_set([X|L],R with X) :-
     mk_set(L,R).
mk_test_set([],{},[]) :- !.
mk_test_set([X|L],S,Cout) :-
     sunify(S,R with X,C1),
     list_to_set(L,R,C2),
     append(C1,C2,Cout).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Interval manipulation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

int_term(T) :- 
       nonvar(T), 
       T=int(A,B), 
       (var(A),! ; integer(A)),
       (var(B),! ; integer(B)). 

is_int(int(A,B),A,B) :-  %used for run-time checks
       nonvar(A), nonvar(B),!,
       int_term(int(A,B)).
is_int(int(_A,_B),_,_) :-  
       write('INSTANTIATION ERROR: interval bounds must be known values'), nl,
       setlog.

int_to_set(int(A,B),{}) :-        % int_to_set(+I,?S) is true if S denotes the set
       A > B.                     % of all elements of the interval I
int_to_set(int(A,B),S with A) :-     
       A =< B,
       A1 is A + 1,
       int_to_set(int(A1,B),S).

int_length(int(A,B),L) :-
         N is B - A + 1,
        (N < 0,!, L = 0
         ;
         L = N).       


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Bag manipulation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

bag_term(T) :- 
       nonvar(T), 
       (T={},! ; T=_ mwith _).  

bag_tail(R mwith _ ,R) :- var(R),!.
bag_tail({} mwith _ ,{}) :- !.
bag_tail(R mwith _ ,T) :- 
	bag_tail(R,T).

de_tail(R,{}) :- var(R),!.
de_tail({},{}) :- !.
de_tail(R mwith S,K mwith S) :- de_tail(R,K).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%   List/Set/Bag/Interval manipulation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

empty_aggr(A) :-
         (A == {},! ; A == []).
                                  % *** To be merged into a single predicate
is_empty({}) :- !.                % is_empty_aggr/1
is_empty(S) :- !,
       is_int(S,L,H),
       L > H.

aggr_comps(R with X,X,R) :- !.    % set
aggr_comps(R mwith X,X,R) :- !.   % bag
aggr_comps([X | R],X,R).          % list


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%  Variable manipulation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

samevar(X,Y) :- 
      var(X), var(Y), X == Y.

chvar(L1,[X|L1],X,L2,[Y|L2],Y):-
    var(X), notin(X,L1), !.
chvar(L1,L1,X,L2,L2,Y):-
    var(X), find_corr(X,Y,L1,L2),!.
chvar(L1,L1new,(H :- B),L2,L2new,(H1 :- B1)):-
    !, chvar(L1,L1a,H,L2,L2a,H1),
    chvar(L1a,L1new,B,L2a,L2new,B1).
chvar(L1,L1new,(B1 & B2),L2,L2new,(B1a & B2a)):-
    !, chvar(L1,L1a,B1,L2,L2a,B1a),
    chvar(L1a,L1new,B2,L2a,L2new,B2a).       
chvar(L1,L1,F,L2,L2,F):-
    atomic(F),!.
chvar(L1,L1new,F,L2,L2new,F1):-
    F =.. [Fname|Args],
    chvar_all(L1,L1new,Args,L2,L2new,Brgs),
    F1 =.. [Fname|Brgs].
    
chvar_all(L1,L1,[],L2,L2,[]).
chvar_all(L1,L1b,[A|R],L2,L2b,[B|S]):-
    chvar(L1,L1a,A,L2,L2a,B),
    chvar_all(L1a,L1b,R,L2a,L2b,S).
        
find_corr(X,Y,[A|_R],[Y|_S]):-
    X == A,!.    
find_corr(X,Y,[_|R],[_|S]):-
    find_corr(X,Y,R,S).   

occurs(X,Y):-   % occur(X,T): true if variable X occurs in term T
        var(Y),samevar(X,Y),!.
occurs(X,Y):-
        nonvar(Y),
        Y =.. [_|R],
        occur_list(X,R).

occur_list(_X,[]):-!,fail.
occur_list(X,[A|_R]):-
        occurs(X,A),!.
occur_list(X,[_|R]):-
        occur_list(X,R).

extract_vars(A,[A]):-
    var(A),!.                 
extract_vars(exists(V,B),Vars):-
    var(V),!,
    extract_vars(B,List),
    remove_var(V,List,Vars). 
extract_vars(exists(V,B),Vars):-
    !,extract_vars(B,List),
    remove_list(V,List,Vars).
extract_vars(forall(X in Y,B),Vars):-
    !, extract_vars(Y,L1),
    extract_vars(B,L2),
    listunion(L1,L2,L),
    remove_var(X,L,Vars).    
extract_vars(Int,Vars):-
    is_sf(Int,X,G),!,
    extract_vars(G,Vars1),
    remove_var(X,Vars1,Vars).   
extract_vars(P,Vars):-
    functor(P,_,A),
    !, findallvars(P,A,Vars).
    
findallvars(_P,0,[]):- !.   
findallvars(P,A,Vars):-
    arg(A,P,Arg),
    extract_vars(Arg,L1),
    B is A-1,
    findallvars(P,B,L2),
    listunion(L1,L2,Vars).
        
remove_var(_,[],[]).
remove_var(X,[Y|L],S):-
    X == Y,!,remove_var(X,L,S).
remove_var(X,[Y|L],[Y|S]):-
    remove_var(X,L,S).  
        
remove_list([],L,L).
remove_list([X|R],Vars,Finalvars):-
    remove_var(X,Vars,S),
    remove_list(R,S,Finalvars).   

alldist([]).
alldist([A|R]):-
    var(A), not_in_vars(A,R),
    alldist(R).
    
not_in_vars(_X,[]).
not_in_vars(X,[A|R]):-
    X \== A, not_in_vars(X,R).
   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%  Arithmetic expressions manipulation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

simple_integer_expr(E) :- 
      (var(E),! ; integer(E)).

simple_arithm_expr(E) :-
      (var(E),! ; number(E)).

integer_expr(E) :-       % true if E is an integer expression       
      on_exception(_Error,_X #= E,(write('Problem in arithmetic expression'),nl,fail)).

arithm_expr(E) :-        % true if E is a ground arithmetic expression       
      on_exception(_Error,_X is E,(write('Problem in arithmetic expression'),nl,fail)).

%%%%%%%%%%%%%  for SWI Prolog - to be completed
%integer_expr(E) :-       % true if E is an integer expression       
%      catch(_X #= E,C,(write(C),fail)).
%
%arithm_expr(E) :-        % true if E is a ground arithmetic expression       
%      catch(_X is E,C,(write(C),fail)).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%  Conjunction manipulation 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

list_to_conj(A & B,[A|R]):-
    !,list_to_conj(B,R).
list_to_conj(true,[]):-!.
list_to_conj(A,[A]).

conj_append(true,Cj2,Cj2) :- !.
conj_append((X & Cj1),Cj2,(X & Cj3)) :- !,
        conj_append(Cj1,Cj2,Cj3).
conj_append(X,Cj2,(X & Cj2)).
