%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% The {log} interpreter %% %% VERSION 4.2.3 (for SICStus Prolog) %% %% 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 (November 2001) %% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- module(setlog,[ solve/2, postproc/2, setlog/0 ]). %%%%%%%%%%%%%%%% New operators %%%%%%%%%%%%% :-op(980,xfx,:). :-op(970,xfy,or). :-op(950,xfy,&). :-op(900,fy,neg). :-op(900,fy,naf). :-op(800,xf,!). :-op(700,xfx,in). :-op(700,xfx,neq). :-op(700,xfx,nin). :-op(650,yfx,with). :-op(650,yfx,mwith). :- dynamic setlog/2. :- dynamic newpred_counter/1. :- multifile prolog2setlog:no_interactive_mode/0. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%% Top-level meta-interpreter %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% setlog :- top_level. top_level :- prolog2setlog:no_interactive_mode, !. 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), list_to_conj(Goal_ruq,Goal_ruqL), preproc(Goal_ruq,Goal),!, ruq_in_goal(Goal,B), call_goal(B,Constr). 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). :- (prolog2setlog:no_interactive_mode,! ; nl, write('loading {log}...please wait (10%)'), nl). %%%%%%%%%% Extended SLD-Resolution algorithm %%%%%%%%% %%%% solve_goal(Constraint(in),Non_Constraint(in),Constraint(out)) solve_goal(Clist,[],CListCan):- !, sat(Clist,CListCan). solve_goal(Clist,[true],CListCan):- !, sat(Clist,CListCan). solve_goal(Clist,[A|B],CListOut):- sat(Clist,ClistSolved), ssolve(A,ClistCl,AlistCl), append(ClistSolved,ClistCl,ClistNew), append(AlistCl,B,AlistNew), solve_goal(ClistNew,AlistNew,CListOut). %%%% ssolve(Atom(in),Constraint(out),Non_Constraint(out)) 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). ssolve((A)!,C,[]):- %% deterministic call !,call_goal(A,C),!. ssolve(ruq_call(S,InName,VarList),Cout,[]) :- %% RUQs !, solve_RUQ(S,InName,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,[],[]):- %% {log} built-in predicates sys_special(A),!. 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). %%%%%%%%%%%%%% Auxiliar predicates for Extended SLD-Resolution %%%% constrlist(Atom_conj(in),Constraint_list(out),Non_Constraint_list(out)) 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]). solve_RUQ({},_,_,C,C). solve_RUQ(S,InName,VarList,Cin,Cout) :- ground(S),!, aggr_comps(S,X,R), InPred =.. [InName,X|VarList], solve_goal(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([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([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(C,[InPred],C2). 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!!********* %setlog_meta(neg A,A) :- !. %setlog_meta(naf A,A) :- !. %setlog_meta(call(A),A) :- !. %setlog_meta((A)!,A) :- !. %setlog_meta(delay(A),A) :- !. %setlog_meta((A1 or A2),A1,A2). sys_special(write(T)) :- !,postproc(T,NewT), write(NewT). sys_special(read(T)) :- !,read(Tout), preproc(Tout,T). sys_special(assert):- !, write('give a clause: '), nl, read(Clause), setassert(Clause). sys_special(assert(Clause)):- !, setassert(Clause). sys_special(consult):- !, write('give file name: '), nl, read(File), sys_special(consult(File)). sys_special(consult(File)):- !, open(File,read,FileStream), readall(FileStream,1,File), close(FileStream). sys_special(listing):- !, nl, list_all. sys_special(abolish):- retract(setlog(_,usr)), fail. sys_special(abolish) :- !. sys_special(help):- !, setlog_help(gen). sys_special(help(X)):- !, setlog_help(X). sys_special(h):- !, setlog_help(gen). sys_special(halt):- confirm, !, abort. sys_special(halt). 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(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), 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),_), selectvars(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(neg A) :- !, write(neg ), write_atoms(A). write_atom(naf A) :- !, write(naf ), write_atoms(A). 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_atoms(A1), write(' or '), write_atoms(A2). write_atom(B) :- write(B). 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,[]) :- % 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 tail(Y,TY),var(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(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,C). append(C1,C2,C3), C = [bag(N)|C3]. :- (prolog2setlog:no_interactive_mode,! ; write('loading {log}...please wait (30%)'), nl). %%%%%%%%%%%%%% Auxiliar predicates for unification select(_,S,_):- var(S), !, fail. select(Z, R with Z, R). select(Z, R with Y, A with Y):- select(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(_,_)). %%%%%%%%% Set/Multiset constraint satisfiability procedure %%%%%%%%% %%%% sat(Constraint(in),Solved_Form_Constraint(out)) sat(C,SFC):- %%% nl,write('*** '),write(C),nl, sat_step(C,NewC,R), %%% disable if set/bag constraint inference is enabled %%% aggr_infer(C,AggrConstr), %%% enable to allow set/bag constraint inference %%% append(AggrConstr,C,ExtC), %%% norep_in_list(ExtC,ExtCR), %%%%%% nl,write('*** '),write(ExtCR),nl, %%% sat_step(ExtCR,NewC,R), sat_cont(R,NewC,SFC). sat_cont(R,NewC,SFC) :- R == stop,!, check_sat(NewC,NewC,RevC), (NewC == RevC,! , norep_in_list(RevC,SFC) %%% (NewC == RevC,!,SFC = RevC %%% enable if set/bag constraint inference is enabled ; sat(RevC,SFC)). sat_cont(_R,NewC,SFC) :- sat(NewC,SFC). sat_step([],[],stop) :- !. sat_step([X = Y|R1],R2,Z):- !, sat_eq([X = Y|R1],R2,Z). sat_step([X nin Y|R1],R2,Z):- !, aggr_term(Y), sat_nin([X nin Y|R1],R2,Z). sat_step([X neq Y|R1],R2,Z):- !, sat_neq([X neq Y|R1],R2,Z). sat_step([X in Y|R1],R2,Z):- !, aggr_term(Y), sat_in([X in Y|R1],R2,Z). sat_step([un(X,Y,W)|R1],R2,Z):- !, set_term(X,_), set_term(Y,_), set_term(W,_), sat_un([un(X,Y,W)|R1],R2,Z). sat_step([nun(X,Y,W)|R1],R2,Z):- !, set_term(X,_), set_term(Y,_), set_term(W,_), sat_nun([nun(X,Y,W)|R1],R2,Z). sat_step([disj(X,Y)|R1],R2,Z):- !, set_term(X,_), set_term(Y,_), sat_disj([disj(X,Y)|R1],R2,Z). sat_step([ndisj(X,Y)|R1],R2,Z):- !, set_term(X,_), set_term(Y,_), sat_ndisj([ndisj(X,Y)|R1],R2,Z). sat_step([set(X)|R1],R2,Z):- !, sat_set([set(X)|R1],R2,Z). sat_step([bag(X)|R1],R2,Z):- !, sat_bag([bag(X)|R1],R2,Z). sat_step([delay(A,G)|R1],R2,Z):- !, sat_delay([delay(A,G)|R1],R2,Z). %% equality sat_eq([T1 = T2|R1],R2,c):- sunify(T1,T2,C), append(C,R1,R3), sat_step(R3,R2,_). %% non-membership sat_nin([T1 nin Aggr|R1],R2,c):- % ground case ground(T1), ground(Aggr),!, \+aggr_member(T1,Aggr), sat_step(R1,R2,_). sat_nin([_T1 nin Aggr|R1],R2,c):- % 1 nonvar(Aggr), Aggr == {},!, sat_step(R1,R2,_). sat_nin([T1 nin Aggr|R1],R2,c):- % 2 nonvar(Aggr), aggr_comps(Aggr,T2,S),!, sat_step([T1 neq T2,T1 nin S|R1],R2,_). sat_nin([T1 nin V|R1],R2,c):- var(V), occurs(V,T1),!, % 3 sat_step(R1,R2,_). sat_nin([X|R1],[X|R2],Stop):- sat_step(R1,R2,Stop). %% inequality sat_neq([F neq G|R1],R2,c):- % ground case ground(F),ground(G),!, \+sunify(F,G,_), sat_step(R1,R2,_). sat_neq([F neq G|R1],R2,c):- % 1 nonvar(F),nonvar(G), functor(F,Fname,Far),functor(G,Gname,Gar), (Fname \== Gname ; Far \== Gar),!, sat_step(R1,R2,_). sat_neq([F neq G|R1],R2,c):- % 2, 3 nonvar(F),nonvar(G), 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,_). sat_neq([T neq X|R1],R2,c):- % 4 var(X),nonvar(T),! , sat_step([X neq T|R1],R2,_). sat_neq([X neq Y|_],_,_):- % 3 var(X),var(Y), samevar(X,Y),!,fail. sat_neq([X neq T|R1],R2,c):- % 5 var(X),nonvar(T), is_ker(T), occurs(X,T),!, sat_step(R1,R2,_). sat_neq([X neq Set|R1],R2,c):- % 7 var(X), nonvar(Set), Set = _S with _T, tail(Set,TS),samevar(X,TS),!, split(Set,_,L), member(Ti,L) , sat_step([Ti nin X|R1],R2,_). sat_neq([X neq Set|R1],R2,c):- % 6 var(X), nonvar(Set), Set = _S with _T, occurs(X,Set),!, sat_step(R1,R2,_). sat_neq([T1 neq T2|R1],R2,c):- % 8(i) inequality between sets nonvar(T1),nonvar(T2), T1 = _S with _A, T2 = _R with _B, sat_step([Z in T1, Z nin T2 | R1],R2,_). sat_neq([T1 neq T2|R1],R2,c):- % 8(ii) nonvar(T1),nonvar(T2), T1 = _S with _A, T2 = _R with _B,!, sat_step([Z in T2, Z nin T1 | R1],R2,_). sat_neq([T1 neq T2|R1],R2,c):- % 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,_). sat_neq([T1 neq T2|R1],R2,c):- % inequality between multisets nonvar(T1),nonvar(T2), % with distinct tail variables T1 = _S mwith A, T2 = R mwith B, sat_step([A neq B, A nin R| R1],R2,_). sat_neq([T1 neq T2|R1],R2,c):- % nonvar(T1),nonvar(T2), 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,_). sat_neq([X|R1],[X|R2],Stop):- sat_step(R1,R2,Stop). %% membership sat_in([T in Aggr|R1],R2,c):- % ground case ground(T), ground(Aggr),!, aggr_member(T,Aggr), sat_step(R1,R2,_). sat_in([T in Aggr|R1],R2,c):- % 2(i) nonvar(Aggr), aggr_comps(Aggr,A,_R), sunify(A,T,C), append(C,R1,R3), sat_step(R3,R2,_). sat_in([T in Aggr|R1],R2,c):- % 2(ii) nonvar(Aggr), aggr_comps(Aggr,_A,R),!, sat_step([T in R|R1],R2,_). sat_in([T in X|R1],R2,c):- % 3 - sets var(X), sunify(X,N with T,_), sat_step([set(N)|R1],R2,_). sat_in([T in X|R1],R2,c):- % 3 - multisets var(X), sunify(X,N mwith T,_), sat_step([bag(N)|R1],R2,_). %% union sat_un([un(S1,S2,T)|R1],R2,c):- % 1 S1==S2,!, sunify(S1,T,C), append(C,R1,R3), sat_step(R3,R2,_). sat_un([un(T1,T2,T3)|R1],R2,c):- % 2 nonvar(T3), T3=={}, !, T1={}, T2={}, sat_step(R1,R2,_). sat_un([un(T1,T2,S)|R1],R2,c):- % 3 nonvar(T1), T1=={}, var(S),!, sunify(S,T2,C), append(C,R1,R3), sat_step(R3,R2,_). sat_un([un(T1,T2,S)|R1],R2,c):- % 3 nonvar(T2), T2=={}, var(S),!, sunify(S,T1,C), append(C,R1,R3), sat_step(R3,R2,_). sat_un([un(S1,S2,S3)|R1],R2,c):- 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,_). sat_un([un(S,T,X)|R1],R2,c):- % 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,_). sat_un([un(S,T,X)|R1],R2,c):- 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,_). sat_un([un(T,S,X)|R1],R2,c):- % 5(ii) nonvar(S), S=_T2 with _T1, var(X),!, sat_step([un(S,T,X)|R1],R2,_). sat_un([X|R1],[X|R2],Stop):- sat_step(R1,R2,Stop). %% disjointness sat_disj([disj(Set1,Set2)|R1],R2,c):- % 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,_). sat_disj([disj(Set,X)|R1],R2,c):- % 3 nonvar(Set), Set = T2 with T1, var(X),!, sat_step([T1 nin X,disj(X,T2)|R1],R2,_). sat_disj([disj(X,Set)|R1],R2,c):- % 3 nonvar(Set), Set = T2 with T1, var(X),!, sat_step([T1 nin X,disj(X,T2)|R1],R2,_). sat_disj([disj(X,Y)|R1],R2,c):- % 2 var(X), var(Y), samevar(X,Y),!, X = {}, sat_step(R1,R2,_). sat_disj([disj(Set1,_)|R1],R2,c):- % 1 nonvar(Set1), Set1 == {},!, sat_step(R1,R2,_). sat_disj([disj(_,Set2)|R1],R2,c):- % 1 nonvar(Set2), Set2 == {},!, sat_step(R1,R2,_). sat_disj([X|R1],[X|R2],Stop):- sat_step(R1,R2,Stop). %% not union sat_nun([nun(S1,S2,S3)|R1],R2,c):- % 1 sat_step([N in S3,N nin S1,N nin S2|R1],R2,_). sat_nun([nun(S1,_S2,S3)|R1],R2,c):- % 1 sat_step([N in S1,N nin S3|R1],R2,_). sat_nun([nun(_S1,S2,S3)|R1],R2,c):- % 1 sat_step([N in S2,N nin S3|R1],R2,_). %% not disjointness sat_ndisj([ndisj(S,T)|R1],R2,c):- % 1 sat_step([N in S, N in T|R1],R2,_). %% set sat_set([set(X)|R1],_,_):- var(X), member_strong(bag(X),R1),!, fail. sat_set([set(X)|R1],R2,c):- % 1 nonvar(X), X == {}, !, sat_step(R1,R2,_). sat_set([set(X)|R1],R2,c):- % 2 nonvar(X),!, set_term(X,Rest), sat_step([set(Rest)|R1],R2,_). sat_set([X|R1],[X|R2],Stop):- sat_step(R1,R2,Stop). %% bag sat_bag([bag(X)|R1],_,_):- var(X), member_strong(set(X),R1),!, fail. sat_bag([bag(X)|R1],R2,c):- nonvar(X), X == {}, !, sat_step(R1,R2,_). sat_bag([bag(X)|R1],R2,c):- nonvar(X),!, bag_term(X,Rest), sat_step([bag(Rest)|R1],R2,_). sat_bag([X|R1],[X|R2],Stop):- sat_step(R1,R2,Stop). %% delay sat_delay([delay(A,G)|R1],R2,c) :- call_goal(G,C1),!, call_goal(A,C2), append(C1,C2,C3), append(C3,R1,R3), sat_step(R3,R2,_). sat_delay([X|R1],[X|R2],Stop):- sat_step(R1,R2,Stop). %%%% final check for the solved form %%%%% check_sat([],_,[]) :- !. check_sat([C|RC],GC,[C|NewC]) :- C = un(X,Y,Z), var(X), var(Y), var(Z), X == Y, !, check_sat(RC,GC,NewC). check_sat([C|RC],GC,[C|NewC]) :- C = un(X,Y,Z), var(X), var(Y), var(Z), check_sat_cond(C,GC,OutC),!, append(OutC,CC,NewC), check_sat(RC,GC,CC). check_sat([C|RC],GC,[C|NewC]) :- check_sat(RC,GC,NewC). check_sat_cond(un(_X,_Y,Z),GC,OutC):- find_neq(Z neq T,GC),!, (OutC = [N in Z, N nin T] ; OutC = [N in T, N nin Z] ; Z = {}, OutC = [T neq {}]). check_sat_cond(un(X,_Y,_Z),GC,OutC):- find_neq(X neq T,GC),!, (OutC = [N in X, N nin T] ; OutC = [N in T, N nin X] ; X = {}, OutC = [T neq {}]). check_sat_cond(un(_X,Y,_Z),GC,OutC):- find_neq(Y neq T,GC), (OutC = [N in Y, N nin T] ; OutC = [N in T, N nin Y] ; Y = {}, OutC = [T neq {}]). %%%%% inference of set/bag constraints %%%%% aggr_infer([],[]). aggr_infer([C1|Rest],CList) :- C1 =.. [_P|Args], find_aggr_list(Args,CL1), aggr_constr(C1,CL2), append(CL1,CL2,CL3), append(CL3,CLRest,CList), aggr_infer(Rest,CLRest). find_aggr_list([],[]). find_aggr_list([T|Terms],AggrConstrs) :- find_aggr(T,AggrC1), append(AggrC1,AggrC2,AggrConstrs), find_aggr_list(Terms,AggrC2). aggr_constr(_T1 in T2,CL) :- !, (CL = [set(T2)] ; CL = [bag(T2)]). aggr_constr(_T1 nin T2,CL) :- !, (CL = [set(T2)] ; CL = [bag(T2)]). aggr_constr(un(T1,T2,T3),[set(T1),set(T2),set(T3)]) :- !. aggr_constr(nun(T1,T2,T3),[set(T1),set(T2),set(T3)]) :- !. aggr_constr(disj(T1,T2),[set(T1),set(T2)]) :- !. aggr_constr(ndisj(T1,T2),[set(T1),set(T2)]) :- !. aggr_constr(_C,[]). find_aggr(X,[]) :- var(X),!. find_aggr(T,CL) :- nonvar(T), T =.. [F|Args], F \== with, F \== mwith,!, find_aggr_list(Args,CL). find_aggr(T,[set(TT)|CR]) :- nonvar(T), T =.. [with|Args], !, tail(T,TT), find_aggr_list(Args,CR). find_aggr(T,[bag(TT)|CR]) :- nonvar(T), T =.. [mwith|Args], !, bag_tail(T,TT), find_aggr_list(Args,CR). %%%%% Auxiliary predicates for set/multiset constraint management %%%%% set_term(X,X) :- var(X),!. set_term({},{}) :- !. set_term(Y with _,R) :- set_term(Y,R). bag_term(X,X) :- var(X),!. bag_term({},{}) :- !. bag_term(Y mwith _,R) :- bag_term(Y,R). aggr_term(A) :- set_term(A,_),!. aggr_term(A) :- bag_term(A,_). aggr_comps(R with X,X,R) :- !. aggr_comps(R mwith X,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). 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). find_neq(X neq _,[A neq _|_]) :- X == A,!. find_neq(X neq _,[_ neq A|_]) :- X == A,!. find_neq(X neq T,[_|R]) :- find_neq(X neq T,R). :- (prolog2setlog:no_interactive_mode,! ; write('loading {log}...please wait (60%)'), nl). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%% Negation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% naf_negate(A,[]) :- \+ call_goal(A,_). %naf_negate(A,[]) :- % selectvars(A,B), % constrlist(A,Clist,Alist), % solve_goal(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) :- chvar([],L1,A,[],L1new,B), constrlist(B,Clist,Alist), solve_goal(Clist,Alist,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) :- !, selectvars(B,V), subset_strong(V,LVars), sunify(A,B,_). neg_constr(A = B,[A neq B],LVars) :- selectvars(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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% readall(FileStream,N,_):- prolog2setlog:no_interactive_mode, !, read_loop_no(FileStream,N). readall(FileStream,N,File):- write('consulting file '), write(File), write(' ...'), nl, read_loop(FileStream,N), write('file '), write(File), write(' consulted.'), nl. read_loop_no(FileStream,N):- read(FileStream,Clause), Clause \== end_of_file,!, setassert(Clause,usr), N1 is N + 1, read_loop_no(FileStream,N1). read_loop_no(_,_). 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,usr), write('Clause '), write(N), write(' stored'), nl. setassert(Clause):- setassert(Clause,usr). setassert(Clause,M):- sf_in_clause(Clause,ExplClause), preproc(ExplClause,ExtClause), ruq_in_clause(ExtClause,BaseClause), assert(setlog:setlog(BaseClause,M)). ssetassert(Clause):- ssetassert(Clause,usr). ssetassert(Clause,M):- ruq_in_clause(Clause,BaseClause), assert(setlog:setlog(BaseClause,M)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%% Program defined constraints %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% setlog((true :- true),sys). setlog((less(A,B,C) :- A=C with B & B nin C & true),sys). setlog((subset(A,B) :- un(A,B,B) & true),sys). setlog((nsubset(A,B) :- C in A & C nin 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) & true),sys). setlog((nint(A,B,C) :- D in C & (D nin A & true or D nin B & true) & true),sys). setlog((diff(A,B,C) :- subset(C,A) & un(B,C,D) & subset(A,D) & disj(B,C) & true),sys). setlog((ndiff(A,B,C) :- diff(A,B,D) & D neq C & true),sys). setlog((sdiff(A,B,C) :- diff(A,B,D) & diff(B,A,E) & un(D,E,C) & true),sys). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%% Preprocessing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%% Set (multiset) preprocessor: %%%%%%% from {...} (+{...}) to 'with' ('mwith') notation preproc(X,X):- var(X),!. preproc(X,Y1):- nonvar(X), is_set(X), !, set_preproc(X,Y), norep_in_set(Y,Y1). preproc(X,Y):- nonvar(X), is_bag(X),!, X = '+'(A), bag_preproc(A,Y). preproc(X,X):- atomic(X),!. preproc((A & B), (A1 & B1)):- !, preproc(A,A1), preproc(B,B1). preproc((A ':-' B ), (A1 ':-' B1 )) :- !, preproc(A,A1), preproc(B,B1). preproc(X,Z):- nonvar(X), functor(X,F,_A), =..(X,[F|ListX]), preproc_all(ListX,ListZ), =..(Z,[F|ListZ]). preproc_all([],[]). preproc_all([A|L1],[B|L2]):- preproc(A,B), preproc_all(L1,L2). %set_preproc(A,A) :- var(A),!. %inutile set_preproc({},{}):- !. set_preproc('{}'(A),B):- set_preproc_elems(A,B),!. set_preproc(_,_):- msg_sort_error(set), fail. set_preproc_elems( A, {} with A):- var(A), !. set_preproc_elems((A1,B1),B2 with A2):- !, preproc(A1,A2),set_preproc_elems(B1,B2). set_preproc_elems((A / X),WT):- !, set_preproc_set((A / X),WT). set_preproc_elems(A1,{} with A2):- preproc(A1,A2). set_preproc_set((A / X),X with B):- var(X),!, preproc(A,B). set_preproc_set((A / X),Y with B):- is_set(X),!, preproc(A,B), preproc(X,Y). set_preproc_set((A / X),Y with B):- X = _ with _,!, preproc(A,B), preproc(X,Y). bag_preproc({},{}):-!. bag_preproc('{}'(A),B):- bag_preproc_elems(A,B),!. bag_preproc(_,_):- msg_sort_error(bag), fail. bag_preproc_elems(A, {} mwith A):- var(A),!. bag_preproc_elems((A1,B1),B2 mwith A2):- !,preproc(A1,A2), bag_preproc_elems(B1,B2). bag_preproc_elems((A / X),MWT):-!, bag_preproc_bag((A / X),MWT). bag_preproc_elems(A1,{} mwith A2):- preproc(A1,A2). bag_preproc_bag((A / X),X mwith B):- var(X),!,preproc(A,B). bag_preproc_bag((A / X),Y mwith B):-!, is_bag(X),!, preproc(A,B), preproc(X,Y). bag_preproc_bag((A / X),Y mwith B):-!, X= _ mwith _,!, preproc(A,B),preproc(X,Y). 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(X):- nonvar(X),functor(X,{},_). is_bag({}):-!. is_bag(X):- nonvar(X), X = '+'(A), is_set(A). msg_sort_error(set) :- write(' wrong set term '), nl. msg_sort_error(bag) :- write(' wrong multiset term '), nl. %%%%%% 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). is_ker(T) :- nonvar(T), functor(T,F,N), (F \== with,! ; N \== 2). %%%%%%%%%%% 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((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),!, selectvars(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, abort ; 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({X:exists(_Var,B)},Y,[Pred],Vars):- !, length([_|Vars],N), newpred(Pred,N,"setlogSF_"), Pred=..[_,Y|Vars], newpred(Aux,N,"setlogSF_"), Aux=..[_,Y|Vars], newpred(Aux1,N,"setlogSF_"), Aux1=..[_,X|Vars], setassert((Pred:-forall(X in Y, Aux1) & neg Aux)), setassert((Aux1:- B)), setassert((Aux:- X nin Y & Aux1)). sf_translate({X : Goal},Y,[Pred],Vars):- length([_|Vars],N), newpred(Pred,N,"setlogSF_"), Pred =.. [_,Y|Vars], newpred(Aux,N,"setlogSF_"), Aux =.. [_,Y|Vars], setassert((Pred :- forall(X in Y,Goal) & neg Aux)), setassert((Aux :- X nin Y & Goal)). 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 avariable term!'), nl, abort ; true). list_to_conj(A & B,[A|R]):- !,list_to_conj(B,R). list_to_conj(A,[A]):- !. list_to_conj(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,A1 & B1):- !, ruq_in_goal(A,A1), ruq_in_goal(B,B1). 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, abort. ruq_in_goal(forall(X in S,G),NewG):- !, selectvars(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, abort ; true ), length(V,N), newpred(Gpred,N,"setlogRUQ_"), Gpred =.. [_,X|Vars], ( G = exists(_Var,B),!, ssetassert((Gpred :- B),sys) ; ssetassert((Gpred :- G),sys) ), 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]. mklist([],0):- !. mklist([_|R],N):- M is N-1, mklist(R,M). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%% Auxiliary predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%% Variable extraction and checking %%%%%%%%%% selectvars(A,[A]):- var(A),!. selectvars(exists(V,B),Vars):- var(V),!, selectvars(B,List), remove_var(V,List,Vars). selectvars(exists(V,B),Vars):- !,selectvars(B,List), remove_list(V,List,Vars). selectvars(forall(X in Y,B),Vars):- !, selectvars(Y,L1), selectvars(B,L2), listunion(L1,L2,L), remove_var(X,L,Vars). selectvars(Int,Vars):- is_sf(Int,X,G),!, selectvars(G,Vars1), remove_var(X,Vars1,Vars). selectvars(P,Vars):- functor(P,_,A), !, findallvars(P,A,Vars). findallvars(_P,0,[]):- !. findallvars(P,A,Vars):- arg(A,P,Arg), selectvars(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). :- (prolog2setlog:no_interactive_mode,! ; write('loading {log}...please wait (90%)'), nl). %%%%%%%%%%%%% 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). member_strong(A,[B|_R]):- A == B, !. member_strong(A,[_|R]):- member_strong(A,R). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%% Help information %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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 multisetset +{a,b} U R'), nl, write(' (equivalent to R mwith b mwith a)'), nl, write(' - {} is the empty set/multiset'), nl, write(' 2. Predefined set/multiset predicates (constraints):'), nl, write(' (''s'' is a set, ''m'' a multiset, ''a'' either a set or a multiset)'), nl, write(' - t in a (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, write(' 3. RUQs: '), nl, write(' - forall(X in a, G),'), 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)),'), 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)}, '), write('V1,...,Vn variables local to G'), nl, write(' 5. 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,nl, write('%%%%%%%% {log} specific built-in predicates %%%%%%%%%'), nl, 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(' - halt/0 to leave {log}'), write(' (go back to the SICStus environment '), nl, write(' - setlog/0 to re-enter {log}'), write(' (from the SICStus environment'),nl, write(' - help/0, help(built), help(lib) to get help information '), nl,write(' (resp., general, about {log} built-in predicates, '), nl,write(' about {log} library predicates)'), nl. setlog_help(built) :- nl, write('%%%%%%%% {log} specific built-in predicates %%%%%%%%%'), nl, nl, write(' - !/1 (used postfix): G!, G any {log} goal: '), write('makes G deterministic'), nl, write(' - halt/0 to leave {log}'), write(' (go back to the SICStus environment '), nl, write(' - setlog/0 to re-enter {log}'), write(' (from the SICStus environment'),nl, write(' - help/0, help(built), help(lib) to get help information '), nl,write(' (resp., general, about {log} built-in predicates, '), nl,write(' about {log} library predicates)'), nl, nl, write('%%%%%%%% Other available built-in predicates %%%%%%%%'), nl, nl, write_built_list, write(' - read/1'),nl, write(' - write/1'),nl, write(' - call/1'),nl, write(' - prolog_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, write('Type consult(''setlog.lib'') to load the {log} library '), write('predicate definitions'),nl, write(' - see the list below'), nl, nl, write('Available {log} library predicates'), nl, nl, write('size(S,N): cardinality (N = |S|)'),nl, write('powerset(S,PS): powerset (PS = 2^S)'),nl, write('cross_product(A,B,CP): the Cartesian product of sets A and B'),nl. write_built_list :- sys(N,Ar), write(' - '),write(N),write('/'),write(Ar),nl, fail. write_built_list. welcome_message :- prolog2setlog:no_interactive_mode, !. welcome_message :- nl, nl, write(' WELCOME TO {log} - version 4.2 '),nl, nl, nl. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- welcome_message,top_level.