
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                                                          
%%                        The {log} interpreter                   
%%                                                           
%%                           VERSION 4.3.18   
%%                                                          
%%                      original development by
%%                                                          
%%                Agostino Dovier     Eugenio Omodeo          
%%                Enrico Pontelli     Gianfranco Rossi  
%%
%%                    subsequent enhancements by
%%
%%                        Gianfranco Rossi
%%
%%                    with the contribution of 
%%
%%                   Carla Piazza  Silvia Monica 
%%
%%          Last revision by Gianfranco Rossi (March 2005)           
%%    
%%                                                          
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- module(setlog,[
             setlog/0,
             start/0,
             setlog_call/1,
             setlog_call/2,
             setlog_consult/1,
             setlog_clause/1,
             setlog_help/0,
             h/0 
   ]).               

:- 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.                 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%    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,*).
  
start :- 
       welcome_message,
       setlog.                         

welcome_message :-                                     
       nl, nl,
       write('              WELCOME TO {log} - version 4.3           '),
       nl, nl.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%    Top-level meta-interpreter            
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

top_level :-
       nl, write('{log}=> '),
       read_term(Goal,[variable_names(VarNames)]),
       solve(Goal,Constr),
       mk_subs_ext(VarNames,VarNames_ext),
       nl, write_subs_constr(VarNames_ext,Constr),
       top_level.
top_level :-
       nl,write(no),nl,
       top_level.

solve(Goal_int_ruq,Constr):-     %% {log} interpreter main predicate
       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),
%%%write(B),nl,
       call_goal_fin(B,Constr).
 
call_goal_fin(G,ClistNew) :-
       constrlist(G,GClist,GAlist),
       solve_goal_fin(GClist,GAlist,ClistNew).
call_goal(G,ClistNew) :-
       constrlist(G,GClist,GAlist),
       solve_goal(GClist,GAlist,ClistNew). 

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_subs_constr([],[]) :- !,
       write(yes), nl.                       
write_subs_constr(Subs,Constr) :- 
      (Subs = [],!,true ; 
       Subs = [true|_],!,write('true') ;
       write_subs_all(Subs)),
       write_constr(Constr), nl,
       nl, write('Another solution?  (y/n)'),
       get(C), skip(10),
       (C \== 121,! ; fail).

write_subs_all([]).
write_subs_all([N1=V1|R]) :-
       nl, write(N1), write(' = '), write(V1),
       (R = [],!,true ; 
        R = [true|_],!,true ;
        write(',  '), write_subs_all(R) ).  

write_constr([]) :-   !.                
write_constr(Constr) :-             
       nl, write('Constraint:'), 
       postproc(Constr,Constr_ext),
       write(Constr_ext).
       
        
%%%%%%%%%%   Extended SLD-Resolution algorithm  %%%%%%%%%                      

%%%% solve_goal(+Constraint,+Non_Constraint,-Constraint)

%%%solve_goal(Clist,C,_CListCan):-   %only for debugging purposes
%%%       write('calling goal: input constraint '),write(Clist),nl, 
%%%       write('calling goal: input atoms'),write(C),nl,nl,
%%%       fail. 
solve_goal_fin(GClist,GAlist,ClistNew):-  
       solve_goal(GClist,GAlist,Clist),  
       sat(Clist,ClistNew,f).
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).


%%%% 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 
        !,(call_goal(G1,ClistNew)
          ;
           call_goal(G2,ClistNew) ).

ssolve(call(A),C,[]):-                   %% meta call    
%?%        !,call_goal(A,C).
        !,call_goal_fin(A,C).

ssolve((A)!,C,[]):-                      %% deterministic call
        !,call_goal_fin(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),!,user: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(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).

solve_SF(S,GName,_PName,VarList,_Cin,Cout) :- 
        ground(VarList),!,
        InPred =.. [GName,X|VarList],
        setof(X,call_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).

solve_RUQ({},_,_,C,C). 
solve_RUQ(S,_,_,C,C) :-
        nonvar(S), S = int(A,B), 
        is_num(A,L), is_num(B,H), L > H, !.
solve_RUQ(S,InName,VarList,Cin,Cout) :-
        nonvar(S), S = int(A,B), 
        is_num(A,L), is_num(B,H), 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).
solve_RUQ(S,InName,VarList,Cin,Cout) :-
        ground(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,InName,VarList,Cin,Cout) :-
        nonvar(S),!, 
        solve_RUQ_goal(S,R,InName,VarList,Cin,C2),
        solve_RUQ(R,InName,VarList,C2,Cout).
solve_RUQ(S,InName,VarList,Cin,Cout) :-
        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_goal(S,R,InName,VarList,Cin,C2) :-
        S = _R with _X,!,
        sunify(S,R with X,C1),
        InPred =.. [InName,X|VarList], 
        append(Cin,C1,C), 
%%%	   solve_goal([X nin R,set(S)|C],[InPred],C2)
        solve_goal_fin([X nin R|C],[InPred],C2).
solve_RUQ_goal(S,R,InName,VarList,Cin,C2) :-
        sunify(S,R mwith X,C1),          
        InPred =.. [InName,X|VarList], 
        append(Cin,C1,C), 
%%%	   solve_goal([bag(S)|C],[InPred],C2)
        solve_goal_fin(C,[InPred],C2).

            
%%%%%%%%%%%%%% Auxiliary predicates for Extended SLD-Resolution                        

%%%% 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]).

aggr_ordered(S) :- var(S),!.
aggr_ordered({}) :- !.
aggr_ordered(S) :- 
       aggr_comps(S,X,R),
       in_order(X,R), aggr_ordered(R).

in_order(_A,S) :- var(S),!.
in_order(_A,{}) :- !.
in_order(A,S) :-  
       aggr_comps(S,_B,_R),
       var(A), !.
in_order(A,S) :-  
       aggr_comps(S,B,R),
       var(B), in_order(A,R),!.
in_order(A,S) :-  
       aggr_comps(S,B,_R),
       A @=< B.


%%%%%%%%%%%%%% "built in" predicates   %%%%%%%%%%%%%              

sys(is,2).
sys(=:=,2).
sys(<,2). 
sys(=<,2).
sys(>,2).
sys(>=,2).
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!!********* 

sys_special(write(T),[]) :-            %% write
      !,postproc(T,NewT),
      write(NewT).

sys_special(read(T),C) :-              %% read
      !,read(Tout),
      preproc(Tout,T,C).

sys_special(assert(Clause),[]):-       %% assert
      !,setassert(Clause).
                      
sys_special(consult(lib),[]):-         %% consult the {log} library file
      !,rem_clause(lib), rem_clause(tmp(lib)),             
      open('setloglib.slog',read,FileStream), 
      switch_ctxt(lib,OldCtxt),
      read_loop_np(FileStream),
      switch_ctxt(OldCtxt,_),
      close(FileStream). 
sys_special(consult(File),[]):-        %% consult                          
      !,open(File,read,FileStream), 
      write('consulting file '), write(File), write(' ...'), nl,
      read_loop(FileStream,1),
      write('file '), write(File), write(' consulted.'), nl,
      close(FileStream). 

sys_special(consult(File,mute),[]):-   %% consult using mute mode 
      !,open(File,read,FileStream), 
      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,[]):-  confirm, !, abort.     %% halt
sys_special(halt,[]). 

sys_special(time(G,T),C):-             %% time
      statistics(runtime,_),
      write('STARTING ...'),nl,
      call_goal_fin(G,C),
      write('END'),nl,
      statistics(runtime,[_,T]).

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').
 
%%%%%%%%%%%%%% Auxiliary predicates for 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).
         

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%  Set/Multiset Unification Algorithm     
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sunify(X,Y,[]) :-                   % 1
      var(X),var(Y),
      X == Y,!.
sunify(X,Y,C) :- 
      var(X),!,
      sunifyXt(X,Y,C).
sunify(X,Y,C) :- 
      var(Y),!,
      sunify(Y,X,C).                % 2
sunify(R,S,C) :-                                         
      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_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) :-                             % 8 
      X=..[F|Ax],Y=..[F|Ay],!,
      sunifylist(Ax,Ay,C).

sunifyXt(X,Y,[set(N)]) :-                    % 5
      nonvar(Y),tail(Y,TY),samevar(X,TY),!,
      replace_tail(Y,N,NewY),
      occur_check(X,NewY),  % occur-check 
      X = NewY.               
sunifyXt(X,Y,[]) :-                          % 6 
      occur_check(X,Y),     % occur-check 
      X = Y.             

%%  Sets: distinct tail vars.
stunify_ss(R with X,S with Y,C) :-    % 9(a) special
      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) :-                           
      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(a).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(a).1
      sunify(R,S,C).
stunify1_2_3(R,S,_,Y,C) :-            % 9(a).2
      sunify(R,S with Y,C).
stunify1_2_3(R,S,X,_,C) :-            % 9(a).3 
      sunify(R with X,S,C).

%% Sets: same tail vars. (action 9(b))
stunify_samevar(R with X,S with Y,_TR,C):-
      select_var(Z,S with Y,Rest),
      sunify(X,Z,C1),
      (sunify(R,Rest,C2)              % 9(b).1
      ;
       sunify(R with X,Rest,C2)       % 9(b).2
      ;
       sunify(R,S with Y,C2)),        % 9(b).3
      append(C1,C2,C).
stunify_samevar(R with X,S with Y,TR,C):-   % 9(b).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).

%% Multisets: same tail vars
stunify_bag_same(R mwith X, S mwith Y, C) :-
	de_tail(R mwith X,ZX),
	de_tail(S mwith Y,ZY),
	sunify(ZX,ZY,C).

%% Multisets: distinct tail vars
stunify_bag(R mwith X, S mwith Y, C) :-
	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).

samevar(X,Y) :- 
      var(X), var(Y), X == Y.

tail(R with _,R) :- var(R),!.
tail({} 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).

occur_check(X,Y):-
      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).

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).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%   Set/Multiset constraints    %%%%%%%%%               
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

atomic_constr(_ = _).      % atomic constraints
atomic_constr(_ in _). 
atomic_constr(_ nin _).
atomic_constr(_ neq _).  
atomic_constr(un(_,_,_)).
atomic_constr(disj(_,_)).
atomic_constr(nun(_,_,_)).
atomic_constr(ndisj(_,_)).
atomic_constr(set(_)).
atomic_constr(bag(_)).
atomic_constr(delay(_,_)).
atomic_constr(type(_)).


%%%%%%%%%   Set/Multiset constraint solver %%%%%%%%%              

%%%% sat(+Constraint,-Solved_Form_Constraint,+final/non-final)

%%%sat(C,_SFC,_F):-                 %only for debugging purposes
%%%      write('************** checking constraint '),write(C),nl,nl,
%%%      fail. 
sat(C,SFC,F):- 
      sat_step(C,NewC,R,F),     
      sat_cont(R,NewC,SFC,F).
sat_cont(R,NewC,SFC,F) :-
      R == stop,!,
      norep_in_list(NewC,RedC),
      check_sat(RedC,RedC,RevC),
      (RevC == RedC,!,SFC=RevC
       ;
       sat(RevC,SFC,F)).
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,
%%%           fail. 
sat_step([],[],stop,_F) :- !.
sat_step([X nin Y|R1],R2,Z,F):- !,
          sat_nin([X nin Y|R1],R2,Z,F).
sat_step([X neq Y|R1],R2,Z,F):- !,
          sat_neq([X neq Y|R1],R2,Z,F).
sat_step([set(X)|R1],R2,Z,F):- !,
          sat_set([set(X)|R1],R2,Z,F).
sat_step([X in Y|R1],R2,Z,F):- !,
          sat_in([X in Y|R1],R2,Z,F).
sat_step([delay(A,G)|R1],R2,Z,F):- !,
          sat_delay([delay(A,G)|R1],R2,Z,F).
sat_step([X = Y|R1],R2,Z,F):- !,
          sat_eq([X = Y|R1],R2,Z,F).
sat_step([X in Y|R1],R2,Z,F):- 
          nonvar(Y),
          (Y==integer; Y==char; Y==float; Y=int(_,_)), !,
          sat_in([X in Y|R1],R2,Z,F).
sat_step([un(X,Y,W)|R1],R2,Z,F):- !,
          sat_un([un(X,Y,W)|R1],R2,Z,F).
sat_step([disj(X,Y)|R1],R2,Z,F):- !,
          sat_disj([disj(X,Y)|R1],R2,Z,F).
sat_step([bag(X)|R1],R2,Z,F):- !,
          sat_bag([bag(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_step([type(TypeC)|R1],R2,Z,F):- !,
          sat_step([TypeC|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).
          
%%%%%%%%%%%%%%%%%%%%%% equality

sat_eq([T1 = T2|R1],R2,c,F):-                    
        sunify(T1,T2,C),
        append(C,R1,R3), 
        sat_step(R3,R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% non-membership

sat_nin([T nin A|R1],R2,c,F):-
        var(A), occurs(A,T),!,                          % 3
        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):-                          % ground case
        ground(T), ground(A),!,
        \+aggr_member(T,A), 
        sat_step(R1,R2,_,F).
sat_nin([_T nin A|R1],R2,c,F):-                         % 1
        nonvar(A), A == {},!,
        sat_step(R1,R2,_,F).
sat_nin([T1 nin A|R1],R2,c,F):-                         % 2
        nonvar(A), aggr_comps(A,T2,S),!,
        sat_step([T1 neq T2,T1 nin S|R1],R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% inequality

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):-  
         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):-  
         nonvar(T1), nonvar(T2),!,
         sat_neq_nn([T1 neq T2|R1],R2,R,F).                         

sat_neq_vn([X neq T|R1],R2,c,F):-                       % 5
         is_ker(T),
         occurs(X,T),!,
         sat_step(R1,R2,_,F).
sat_neq_vn([X neq T|R1],R2,c,F):-                       % 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):-                       % 6         
         T = _S with _T,
         occurs(X,T),!,
         sat_step(R1,R2,_,F).
sat_neq_vn([C|R1],[C|R2],Stop,F):-                      % solved form
         sat_step(R1,R2,Stop,F).
sat_neq_vv([X neq Y|_],_,_,_F):-                        % 3
         samevar(X,Y),!,fail.
sat_neq_vv([C|R1],[C|R2],Stop,F):-                      % solved form
         sat_step(R1,R2,Stop,F).
sat_neq_nn([F neq G|R1],R2,c,Fin):-                     % ground case
         ground(F),ground(G),!,
         \+sunify(F,G,_),
         sat_step(R1,R2,_,Fin).
sat_neq_nn([F neq G|R1],R2,c,Fin):-                     % 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):-                     % 2, 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):-          % 8(i) inequality between sets
         T1 = _S with _A, T2 = _R with _B,
         sat_step([Z in T1, Z nin T2 | R1],R2,_,F).
sat_neq_nn([T1 neq T2|R1],R2,c,F):-          % 8(ii)
         T1 = _S with _A, T2 = _R with _B,!,
         sat_step([Z in T2, Z nin T1 | R1],R2,_,F).
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).

%%%%%%%%%%%%%%%%%%%%%% membership

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),!,
         sat_in_n([T in I|R1],R2,R,F).                         

sat_in_v([T in X|R1],R2,c,F):-                          % 3 - sets
         sunify(X,N with T,_),
         sat_step([set(N)|R1],R2,_,F).
sat_in_v([T in X|R1],R2,c,F):-                          % 3 - multisets
         sunify(X,N mwith T,_),
         sat_step([bag(N)|R1],R2,_,F).
sat_in_n([T in I|R1],R2,c,F):-                          %% predefined sets                     
         I == integer, !,
         test_integer(T),
         sat_step(R1,R2,_,F).
sat_in_n([T in I|R1],R2,c,F):-                          %% predefined sets                     
         I == float, !,
         test_float(T),
         sat_step(R1,R2,_,F).
sat_in_n([T in I|R1],R2,c,F):-                          %% predefined sets
         I == char, !,
         test_or_gen_char(T), 
         sat_step(R1,R2,_,F).
sat_in_n([T in I|R1],R2,c,F):-                          %% intervals
         I = int(A,B), !,
         is_in_int(T,A,B),
         sat_step(R1,R2,_,F).
sat_in_n([T in Aggr|R1],R2,c,F):-                       % ground case
         ground(T), ground(Aggr),!,
         aggr_member(T,Aggr), 
         sat_step(R1,R2,_,F).
sat_in_n([T in Aggr|R1],R2,c,F):-                       % 2(i)
         aggr_comps(Aggr,A,_R),
         sunify(A,T,C), 
         append(C,R1,R3), 
         sat_step(R3,R2,_,F).
sat_in_n([T in Aggr|R1],R2,c,F):-                       % 2(ii)
         aggr_comps(Aggr,_A,R),!,
         sat_step([T in R|R1],R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% union

sat_un([un(S1,S2,T)|R1],R2,c,F):-                        % 1
         S1==S2,!, 
         sunify(S1,T,C), 
         append(C,R1,R3), 
         sat_step(R3,R2,_,F). 
sat_un([un(X,Y,Z)|R1],[un(X,Y,Z)|R2],Stop,F):-           % solved form
         var(X),var(Y),var(Z),!,
         sat_step(R1,R2,Stop,F).
sat_un([un(T1,T2,T3)|R1],R2,c,F):-                       % 2 
         nonvar(T3), T3=={}, !, 
         T1={}, T2={}, 
         sat_step(R1,R2,_,F).
sat_un([un(T1,T2,S)|R1],R2,c,F):-                        % 3
         nonvar(T1), 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):-                        % 3
         nonvar(T2), T2=={}, var(S),!,
         sunify(S,T1,C), 
         append(C,R1,R3),  
         sat_step(R3,R2,_,F).         
sat_un([un(S1,S2,S3)|R1],R2,c,F):-                      
         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,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,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,un(N1,N2,N)|C3] ),                
         append(R,R1,R3),
         sat_step(R3,R2,_,F).
sat_un([un(S,T,X)|R1],R2,c,F):- % 5(i)
         nonvar(S), S=_T2 with T1, var(X),                  
         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, un(N1,T,N)|R3],R2,_,F).
sat_un([un(S,T,X)|R1],R2,c,F):-
         nonvar(S), S =_T2 with T1, var(X), !,                        
         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, un(N1,N2,N)|R3],R2,_,F).
sat_un([un(T,S,X)|R1],R2,c,F):-                                  % 5(ii)
         nonvar(S), S=_T2 with _T1, var(X),!,
         sat_step([un(S,T,X)|R1],R2,_,F).                  

%%%%%%%%%%%%%%%%%%%%%% disjointness

sat_disj([disj(X,Y)|R1],R2,c,F):-                            % 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):-             % solved form
        var(X), var(Y),!,
        sat_step(R1,R2,Stop,F).
sat_disj([disj(Set1,Set2)|R1],R2,c,F):-                      % 4
        nonvar(Set1), Set1 = S1 with T1,
        nonvar(Set2), Set2 = S2 with T2,!,
        sat_step([T1 neq T2,T1 nin S2,T2 nin S1,disj(S1,S2)|R1],R2,_,F).
sat_disj([disj(Set,X)|R1],R2,c,F):-                          % 3
        nonvar(Set), Set = T2 with T1,
        var(X),!,
        sat_step([T1 nin X,disj(X,T2)|R1],R2,_,F).
sat_disj([disj(X,Set)|R1],R2,c,F):-                          % 3
        nonvar(Set), Set = T2 with T1,
        var(X),!,
        sat_step([T1 nin X,disj(X,T2)|R1],R2,_,F).
sat_disj([disj(Set1,_)|R1],R2,c,F):-                         % 1
        nonvar(Set1), Set1 == {},!,
        sat_step(R1,R2,_,F).
sat_disj([disj(_,Set2)|R1],R2,c,F):-                         % 1
        nonvar(Set2), Set2 == {},!,
        sat_step(R1,R2,_,F).
       
%%%%%%%%%%%%%%%%%%%%%% not union

sat_nun([nun(S1,S2,S3)|R1],R2,c,F):-                         % 1
        sat_step([N in S3,N nin S1,N nin S2|R1],R2,_,F).
sat_nun([nun(S1,_S2,S3)|R1],R2,c,F):-                        % 1
        sat_step([N in S1,N nin S3|R1],R2,_,F).
sat_nun([nun(_S1,S2,S3)|R1],R2,c,F):-                        % 1
        sat_step([N in S2,N nin S3|R1],R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% not disjointness

sat_ndisj([ndisj(S,T)|R1],R2,c,F):-                          % 1
        sat_step([N in S, N in T|R1],R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% set

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):-                    % 1
        nonvar(X), X == {}, !,
        sat_step(R1,R2,_,F).
sat_set([set(X)|R1],R2,c,F):-                    % 2
        nonvar(X),!,                  
        X = _S with _A,
        sat_step(R1,R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% bag

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):- 
        nonvar(X), X == {}, !,
        sat_step(R1,R2,_,F).
sat_bag([bag(X)|R1],R2,c,F):-                    
        nonvar(X),!,                  
        X = _S mwith _A,
        sat_step(R1,R2,_,F).

%%%%%%%%%%%%%%%%%%%%%% delay

sat_delay([delay(A,_G)|R1],R2,c,f) :- !,
        call_goal_nodel(A,C2),
        append(C2,R1,R3),
        sat_step(R3,R2,_,f).
sat_delay([delay(A,G)|R1],R2,c,F) :- 
        call_goal(G,C1),!,
        call_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 genrating any new delay
call_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).

%%%%%%%%%%%%%%%%%%%%%% Final check for the solved form %%%%%
     
check_sat([],_,[]) :- !.
check_sat([W neq T|RC],GC,NewC) :-
%%%    set_term(T),
    find_un(W,GC),!,
    mk_new_constr(W,T,OutC),
    append(OutC,CC,NewC),
    check_sat(RC,GC,CC).
check_sat([C|RC],GC,[C|NewC]) :-
    type_constr(C,_,_),!,
    \+type_err(C,RC),   
    check_sat(RC,GC,NewC).
check_sat([C|RC],GC,[C|NewC]) :-
    check_sat(RC,GC,NewC).

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(integer(X),X,integer).

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).


%%%%% Auxiliary predicates for set/multiset constraint management %%%%%
                       
aggr_comps(R with X,X,R) :- !.
aggr_comps(R mwith X,X,R).

aggr_member(X,S):-
        aggr_comps(S,Y,_R),
        sunify(X,Y,_), !.
aggr_member(X,S):-
        aggr_comps(S,_Y,R),
        aggr_member(X,R).

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).

memberall(A,B,[A|_R],[B|_S]).
memberall(A,B,[_|R],[_|S]):- 
        memberall(A,B,R,S).
          
occurs(X,Y):-
        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).

split(N,N,[]):-
        var(N),!.
split(S with T, N, [T|R]):-
        split(S,N,R).

find_un(X,[un(A,_,_)|_]) :- X == A,!.
find_un(X,[un(_,A,_)|_]) :- X == A,!.
find_un(X,[un(_,_,A)|_]) :- X == A,!.
find_un(X,[_|R]) :- 
       find_un(X,R).

set_term(T) :- 
       nonvar(T), (T={},! ; T=_ with _).        

bag_term(T) :- 
       nonvar(T), (T={},! ; T=_ mwith _).        

%%%%% Auxiliary predicates for interval management %%%%%

is_num(X,_N) :-
       var(X), !, 
       write('INSTANTIATION ERROR'), nl,
       setlog.
is_num(X,N) :-
       nonvar(X),  
	  (X == min, !, min_int(N) ; 
	   X == max, !, max_int(N) ;
       integer(X), N = X).

is_in_int(X,A,B) :-
       is_num(A,L), is_num(B,H), 
       L =< H, 
       test_or_gen_int(X,L,H).

test_or_gen_int(X,A,B) :-
       nonvar(X),!,
       integer(X),
       X >= A, X =< B.
test_or_gen_int(X,A,B) :-
       gen_int+(B,A,X).

gen_int+(_F,X,X).
gen_int+(F,X,Y) :- 
       Z is X+1, Z =< F, 
       gen_int+(F,Z,Y).

min_int(-32768).
max_int(32767).

test_or_gen_char(X) :-
       nonvar(X), !,
       simple(X),
       name(X,[_]).
test_or_gen_char(X) :-
       gen_char(30,X).

gen_char(Y,C) :- 
       name(C,[Y]).
gen_char(Y,C) :- 
       Y<122, Z is Y+1, 
       gen_char(Z,C).

test_integer(I) :-
       var(I), !,
       write('INSTANTIATION ERROR'), nl,
       setlog.
test_integer(I) :-
       integer(I).

test_float(F) :-
       var(F), !,
       write('INSTANTIATION ERROR'), nl,
       setlog.
test_float(F) :-
       float(F).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Program defined constraints 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

setlog((true :- true),sys).
setlog((less(A,B,C) :- A=C with B & B nin C & set(C) & true),sys).
setlog((subset(A,B) :- un(A,B,B) & set(A) & set(B) & 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).
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).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%         Negation 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

naf_negate(A,[]) :-                 %% Negation as Failure
       \+ call_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),
       sat(Clist0,Clist1,f),!, 
       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).	 

subset_strong([],_L):-!.
subset_strong([X|L1],L2) :-
      member_strong(X,L2),
      subset_strong(L1,L2).

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).   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%   Consulting and storing {log} clauses  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

context(usr).

read_loop_np(FileStream):-         
        read(FileStream,Clause), 
        Clause \== end_of_file,!, 
        setassert(Clause),
        read_loop_np(FileStream).
read_loop_np(_).

read_loop(FileStream,N):-
        read(FileStream,Clause), 
        Clause \== end_of_file,!, 
        assert_or_solve(Clause,N),
        N1 is N + 1,
        read_loop(FileStream,N1).
read_loop(_,_).

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)).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Preprocessing 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%% Set (multiset) preprocessor: 
%%%%%%%%%%%%% from {...} (*{...}) to 'with' ('mwith') notation  

preproc_goal(G,PGext) :-
        preproc(G,PG,TypeCL), 
        list_to_conj(TypeCC,TypeCL),
        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,Y1,C):-
        nonvar(X), is_set_ext(X), !,
        set_preproc(X,Y,C),
        norep_in_set(Y,Y1). 
preproc(X,Y,C):-
        nonvar(X), is_bag_ext(X),!,
        bag_preproc(X,Y,C).
preproc(X,X,[]):-
        atomic(X),!.
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,C),
        =..(Z,[F|ListZ]).

preproc_all([],[],[]).
preproc_all([A|L1],[B|L2],C):-
        preproc(A,B,C1),
        preproc_all(L1,L2,C2),
        append(C1,C2,C).

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_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).

%%%%%%%%%%%%% 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).

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).

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).

%%%%%%%%%%%%% Auxiliary predicates for set/multiset preprocessing

list_to_conj(A & B,[A|R]):-
    !,list_to_conj(B,R).
list_to_conj(A,[A]):- !.
list_to_conj(true,[]).

conj_append(true,Cj2,Cj2) :- !.
conj_append((X & Cj1),Cj2,(X & Cj3)) :- !,
        conj_append(Cj1,Cj2,Cj3).
conj_append(X,Cj2,(X & Cj2)).

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_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).

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 & A1)) :-
    aggr_constrs(A),!,
    gen_constrs(A,A1).   
ruq_in_goal(A,A).
    %% N.B. no check for 'forall(X in {...,t[X],...})'
    %% add 'occur_check(X,S)' to enforce it

%%%%%%%%%%%%%%% Inferring type constraints %%%%%%%%%%%%%%%%

aggr_constrs(_T1 nin _T2) :- !.
aggr_constrs(un(_T1,_T2,_T3)):- !.
aggr_constrs(nun(_T1,_T2,_T3)) :- !.
aggr_constrs(disj(_T1,_T2)) :- !.
aggr_constrs(ndisj(_T1,_T2)).

gen_constrs(_T1 nin T2,Cj) :- 
        force_aggr(T2,Cj),!.
gen_constrs(un(T1,T2,T3),Cj) :- 
        force_set(T1,Cj1),
        force_set(T2,Cj2),
        force_set(T3,Cj3),!,
        conj_append(Cj1,Cj2,Cj12), conj_append(Cj12,Cj3,Cj).
gen_constrs(nun(T1,T2,T3),Cj) :- 
        force_set(T1,Cj1),
        force_set(T2,Cj2),
        force_set(T3,Cj3),!,
        conj_append(Cj1,Cj2,Cj12), conj_append(Cj12,Cj3,Cj).
gen_constrs(disj(T1,T2),Cj) :- 
        force_set(T1,Cj1),
        force_set(T2,Cj2),!,
        conj_append(Cj1,Cj2,Cj).
gen_constrs(ndisj(T1,T2),Cj) :- 
        force_set(T1,Cj1),
        force_set(T2,Cj2),!,
        conj_append(Cj1,Cj2,Cj).
gen_constrs(_,_) :- 
        write(' type error'), nl,
        setlog.

force_set(T,(type(set(T)) & true)) :- 
        var(T),!.
force_set(T,true) :- 
        set_term(T).

force_aggr(T,(type(aggr(T)) & true)) :- 
        var(T),!.
force_aggr(T,true) :- 
        (set_term(T),! ; bag_term(T)).


%%%%%%%%%%%%   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].
    
mklist([],0):- !.
mklist([_|R],N):-
    M is N-1,
    mklist(R,M).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%   General auxiliary predicates       
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%   Variable extraction and checking   %%%%%%%%%%

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).
   

%%%%%%%%%%%%%  List manipulation pred's %%%%%%%%%%%

member(X,[X|_R]).
member(X,[_|R]):-member(X,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).

notin(_,[]).
notin(A,[B|R]):-
    A \== B, notin(A,R).

append([],L,L).                                     
append([X|L1],L2,[X|L3]):-
        append(L1,L2,L3).

%append3([],L2,L3,L4) :-
%        append(L2,L3,L4).                                        
%append3([X|L1],L2,L3,[X|L4]):-
%        append3(L1,L2,L3,L4).

member_strong(A,[B|_R]):- 
         A == B, !.
member_strong(A,[_|R]):- 
         member_strong(A,R).

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).

           
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%      Help predicates   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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,nl,                             
   write('   2.  Predefined set/multiset predicates (constraints):'), nl,
   write('       (''t'' any term, ''s'' a set, ''a'' either a set or a multiset)'), nl,
   write('        - t in a  (membership)'), nl,
   write('        - t in int(n,m)  (interval membership)'), nl,
   write('        - t nin a  (non-membership)'), nl,   
   write('        - t1 = t2  (equality)'), nl,
   write('        - t1 neq t2  (non-equality)'), 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('        - set(t) (is a set)'), nl,  
   write('        - bag(t) (is a multiset)'), nl,nl,  
   write('   3.  RUQs: '), 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,
   write('   4.  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('   5.  Predefined sets'), nl,
   write('       (only for the membership operation (in) and RUQs'), nl,   
   write('        - int(n1,n2) (interval) is the set of integer numbers'), nl,       
   write('          ranging from n1 to n2 (n1 <= n2)'), nl,       
   write('        - integer, char, float'), nl,nl,       
   write('   6.  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('   -   start/0, setlog/0 to (re-)enter {log}'), 
        write('  from the Prolog environment'),nl,   
   write('   -   help, 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 Prolog 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').

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/0, assert/1'),nl,
   write('   -   consult/0, 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_consult(F): to consult any {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,Constr),
       postproc(Constr,Constr_ext),
       postproc(NewGoal,NewGoal_ext),
       postproc(Goal,Goal_ext),
       Goal_ext = NewGoal_ext.

setlog_consult(File) :- 
       op_define,
       open(File,read,FileStream), 
       read_loop_np(FileStream),
       close(FileStream). 

setlog_clause(Cl) :-
       op_define,
       setassert(Cl).

