%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% The {log} interpreter %% %% VERSION 3.4 (for SICStus Prolog) %% %% original development by %% %% Agostino Dovier Eugenio Omodeo %% Enrico Pontelli Gianfranco Rossi %% %% subsequent enhancements by %% %% Gianfranco Rossi %% %% Last revision by Gianfranco Rossi (December 2000) %% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%% New operators %%%%%%%%%%%%% :-op(1000,xfx,/). :-op(980,xfx,:). :-op(970,xfy,or). :-op(950,xfy,&). :-op(900,fy,neg). :-op(800,xf,!). :-op(700,xfx,in). :-op(700,xfx,neq). :-op(700,xfx,nin). :-op(650,yfx,with). :- dynamic setlog/1. :- dynamic newpred_counter/1. :- multifile no_interactive_mode/0. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%% Top-level meta-interpreter %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% setlog :- top_level. top_level :- 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). :- 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):- !, can(Clist,CListCan). solve_goal(Clist,[true],CListCan):- !, can(Clist,CListCan). solve_goal(Clist,[A|B],CListOut):- can(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,[]):- %% negation !,negate(A,ClistNew). ssolve( (G1 or G2),ClistNew,[]):- %% goal disjunction !,(call_goal(G1,ClistNew) ; call_goal(G2,ClistNew) ). ssolve(call(A),C,[]):- %% !,call_goal(A,C). ssolve((A)!,C,[]):- %% !,call_goal(A,C),!. ssolve(ruq_call(S,InName,VarList),Cout,[]) :- !, solve_RUQ(S,InName,VarList,[],Cout). %% RUQs solve_RUQ('{}',_,_,C,C). solve_RUQ(S,InName,VarList,Cin,Cout) :- ground(S),!, S = R with X, 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), !, sunify(S,R with X,C1), InPred =.. [InName,X|VarList], append(Cin,C1,C), solve_goal([X nin R|C],[InPred],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), set_ordered(S). ssolve(prolog_call(A),[],[]):- %% direct Prolog built-in predicates 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 goals 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):- constraint(A),!, constrlist(B,B1,B2). constrlist(A & B,B1,[A|B2]):- !,constrlist(B,B1,B2). constrlist(A,[A],[]):- constraint(A),!. constrlist(A,[],[A]). set_term(X):- var(X),!. set_term('{}') :- !. set_term(Y with _):- set_term(Y). set_ordered(S) :- var(S),!. set_ordered('{}') :- !. set_ordered(R with A) :- in_order(A,R), set_ordered(R). in_order(_A,S) :- var(S),!. in_order(_A,'{}') :- !. in_order(A,_R with B) :- 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)) :- !,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), close(FileStream). sys_special(listing):- !, nl, list_all. sys_special(abolish):- !, abolish(setlog,1), assert( setlog((true :- true)) ). 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)), H \== true, \+special(H), postproc(H,Hnew), write(Hnew), write_body(B). list_all. special(H) :- functor(H,HPred,_), name(HPred,[115,101,116,108,111,103,82,85,81|_No]). 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(Set,Goal_name,FV)) :- !, write('forall('),write(X),write(' in '),write(Set),write(','), RUQ_body_pred =.. [Goal_name,X|FV], setlog((RUQ_body_pred :- RUQ_body)), selectvars(RUQ_body,Vars), remove_list([X|FV],Vars,LocalVars), (LocalVars = [],!,write_atoms(RUQ_body), write(')') ; write('exists('),write(LocalVars),write(','), write_atoms(RUQ_body), write('))') ). 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'). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%% Unification Algorithm %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) :- % 8 X=..[F|Ax],Y=..[F|Ay],!, sunifylist(Ax,Ay,C). sunifyXt(X,Y,[]) :- % 5 tail(Y,TY),var(TY),samevar(X,TY),!, replace_tail(Y,_N,NewY), % occur_check(X,NewY), X = NewY. sunifyXt(X,Y,[]) :- % 6 % occur_check(X,Y), % occur-check supressed for efficiency X = Y. % reasons (drop % to reactivate it) %% 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,C) ). 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,C). 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). %% 9(b) - same tail vars. 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,C). sunifylist([],[],[]). sunifylist([X|AX],[Y|AY],C):- sunify(X,Y,C1), sunifylist(AX,AY,C2), append(C1,C2,C). :- 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). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%% Set constraints %%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% constraint(_ = _). constraint(_ in _). constraint(_ nin _). constraint(_ neq _). constraint(un(_,_,_)). constraint(disj(_,_)). constraint(nun(_,_,_)). constraint(ndisj(_,_)). %%%%%%%%% Set constraint satsfiability procedure %%%%%%%%% %%%% can(Constraint(in),Solved_Form_Constraint(out)) can(C,SFC):- can_step(C,NewC,R), can_cont(R,NewC,SFC). can_cont(R,NewC,SFC) :- R == stop,!, check_sat(NewC,NewC,RevC), (NewC == RevC,!, norep_in_list(RevC,SFC) ; can(RevC,SFC)). can_cont(_R,NewC,SFC) :- can(NewC,SFC). can_step([],[],stop) :- !. can_step([X = Y|R1],R2,Z):- !, can_eq([X = Y|R1],R2,Z). can_step([X nin Y|R1],R2,Z):- !, set_term(Y), can_nin([X nin Y|R1],R2,Z). can_step([X neq Y|R1],R2,Z):- !, can_neq([X neq Y|R1],R2,Z). can_step([X in Y|R1],R2,Z):- !, set_term(Y), can_in([X in Y|R1],R2,Z). can_step([un(X,Y,W)|R1],R2,Z):- !, set_term(X), set_term(Y), set_term(W), can_un([un(X,Y,W)|R1],R2,Z). can_step([nun(X,Y,W)|R1],R2,Z):- !, set_term(X), set_term(Y), set_term(W), can_nun([nun(X,Y,W)|R1],R2,Z). can_step([disj(X,Y)|R1],R2,Z):- !, set_term(X), set_term(Y), can_disj([disj(X,Y)|R1],R2,Z). can_step([ndisj(X,Y)|R1],R2,Z):- set_term(X), set_term(Y), can_ndisj([ndisj(X,Y)|R1],R2,Z). %% equality can_eq([T1 = T2|R1],R2,c):- sunify(T1,T2,C), append(C,R1,R3), can_step(R3,R2,_). %% non-membership can_nin([T1 nin Set|R1],R2,c):- % ground case ground(T1), ground(Set),!, \+set_member(T1,Set), can_step(R1,R2,_). can_nin([_T1 nin Set|R1],R2,c):- % 1 nonvar(Set), Set == {},!, can_step(R1,R2,_). can_nin([T1 nin Set|R1],R2,c):- % 2 nonvar(Set), Set = S with T2,!, can_step([T1 neq T2,T1 nin S|R1],R2,_). can_nin([T1 nin V|R1],R2,c):- var(V), occurs(V,T1),!, % 3 can_step(R1,R2,_). can_nin([X|R1],[X|R2],Stop):- can_step(R1,R2,Stop). %% inequality can_neq([F neq G|R1],R2,c):- % ground case ground(F),ground(G),!, \+sunify(F,G,_), can_step(R1,R2,_). can_neq([F neq G|R1],R2,c):- % 1 nonvar(F),nonvar(G), functor(F,Fname,Far),functor(G,Gname,Gar), (Fname \== Gname ; Far \== Gar),!, can_step(R1,R2,_). can_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, F =.. [_|Flist], G =.. [_|Glist],!, memberall(A,B,Flist,Glist), can_step([A neq B|R1],R2,_). can_neq([T neq X|R1],R2,c):- % 4 var(X),nonvar(T),! , can_step([X neq T|R1],R2,_). can_neq([X neq Y|_],_,_):- % 3 var(X),var(Y), samevar(X,Y),!,fail. can_neq([X neq T|R1],R2,c):- % 5 var(X),nonvar(T), functor(T,Tname,_),Tname \== with, occurs(X,T),!, can_step(R1,R2,_). can_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) , can_step([Ti nin X|R1],R2,_). can_neq([X neq Set|R1],R2,c):- % 6 var(X), nonvar(Set), Set = _S with _T, occurs(X,Set),!, can_step(R1,R2,_). can_neq([T1 neq T2|R1],R2,c):- % 8(i) nonvar(T1),nonvar(T2), T1 = _A with _S, T2 = _B with _T, can_step([Z in T1, Z nin T2 | R1],R2,_). can_neq([T1 neq T2|R1],R2,c):- % 8(ii) nonvar(T1),nonvar(T2), T1 = _A with _S, T2 = _B with _T,!, can_step([Z in T2, Z nin T1 | R1],R2,_). can_neq([X|R1],[X|R2],Stop):- can_step(R1,R2,Stop). %% membership can_in([T in Set|R1],R2,c):- % ground case ground(T), ground(Set),!, set_member(T,Set), can_step(R1,R2,_). can_in([T in Set|R1],R2,c):- % 2(i) nonvar(Set), Set = _S with A, sunify(A,T,C), append(C,R1,R3), can_step(R3,R2,_). can_in([T in Set|R1],R2,c):- % 2(ii) nonvar(Set), Set = S with _A,!, can_step([T in S|R1],R2,_). can_in([T in X|R1],R2,c):- % 3 var(X), X = _N with T, can_step(R1,R2,_). %N.B.: no test for X in T; replace %'X = N with T' with 'sunify(X,N with T,_)' to enforce it %% union can_un([un(S1,S2,T)|R1],R2,c):- % 1 S1==S2,!, sunify(S1,T,C), append(C,R1,R3), can_step(R3,R2,_). can_un([un(T1,T2,T3)|R1],R2,c):- % 2 nonvar(T3), T3=={}, !, T1={}, T2={}, can_step(R1,R2,_). can_un([un(T1,T2,S)|R1],R2,c):- % 3 %%% nonvar(T1), T1=={},!, nonvar(T1), T1=={}, var(S),!, sunify(S,T2,C), append(C,R1,R3), can_step(R3,R2,_). can_un([un(T1,T2,S)|R1],R2,c):- % 3 %%% nonvar(T2), T2=={},!, nonvar(T2), T2=={}, var(S),!, sunify(S,T1,C), append(C,R1,R3), can_step(R3,R2,_). can_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), can_step(R3,R2,_). can_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, can_step([T1 nin N1, T1 nin T, T1 nin N, un(N1,T,N)|R3],R2,_). can_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, can_step([T1 nin N1, T1 nin N2, T1 nin N, un(N1,N2,N)|R3],R2,_). can_un([un(T,S,X)|R1],R2,c):- % 5(ii) nonvar(S), S=_T2 with _T1, var(X),!, can_step([un(S,T,X)|R1],R2,_). can_un([X|R1],[X|R2],Stop):- can_step(R1,R2,Stop). %% disjointness can_disj([disj(Set1,Set2)|R1],R2,c):- % 4 nonvar(Set1), Set1 = S1 with T1, nonvar(Set2), Set2 = S2 with T2,!, can_step([T1 neq T2,T1 nin S2,T2 nin S1,disj(S1,S2)|R1],R2,_). can_disj([disj(Set,X)|R1],R2,c):- % 3 nonvar(Set), Set = T2 with T1, var(X),!, can_step([T1 nin X,disj(X,T2)|R1],R2,_). can_disj([disj(X,Set)|R1],R2,c):- % 3 nonvar(Set), Set = T2 with T1, var(X),!, can_step([T1 nin X,disj(X,T2)|R1],R2,_). can_disj([disj(X,Y)|R1],R2,c):- % 2 var(X), var(Y), samevar(X,Y),!, X = {}, can_step(R1,R2,_). can_disj([disj(Set1,_)|R1],R2,c):- % 1 nonvar(Set1), Set1 == {},!, can_step(R1,R2,_). can_disj([disj(_,Set2)|R1],R2,c):- % 1 nonvar(Set2), Set2 == {},!, can_step(R1,R2,_). can_disj([X|R1],[X|R2],Stop):- can_step(R1,R2,Stop). %% not union can_nun([nun(S1,S2,S3)|R1],R2,c):- % 1 can_step([N in S3,N nin S1,N nin S2|R1],R2,_). can_nun([nun(S1,_S2,S3)|R1],R2,c):- % 1 can_step([N in S1,N nin S3|R1],R2,_). can_nun([nun(_S1,S2,S3)|R1],R2,c):- % 1 can_step([N in S2,N nin S3|R1],R2,_). %% not disjointness can_ndisj([ndisj(S,T)|R1],R2,c):- % 1 can_step([N in S, N in T|R1],R2,_). %% 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 {}]). %%%%%% Auxiliary predicates for set constraint management %%%%%% 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). set_member(X,_ with Y):- sunify(X,Y,_), !. set_member(X,S with _):- set_member(X,S). 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). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%% Negation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- write('loading {log}...please wait (60%)'), nl. negate(A,[]) :- \+ call_goal(A,_). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%% Consulting and storing {log} clauses %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% readall(FileStream,N):- write('Reading clause '), write(N), read(FileStream,Clause),!, ( Clause \== end_of_file, write(' : OK'),nl, setassert(Clause), N1 is N + 1, readall(FileStream,N1) ; write(' = end_of_file'), nl ). setassert(Clause):- sf_in_clause(Clause,ExplClause), preproc(ExplClause,ExtClause), ruq_in_clause(ExtClause,BaseClause), assert(setlog(BaseClause)). ssetassert(Clause):- ruq_in_clause(Clause,BaseClause), assert(setlog(BaseClause)). setlog((true :- true)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%% Preprocessing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%% Set preprocessor: from {...} to 'with' notation %%%%%% preproc(X,X):- var(X),!. preproc(X,Y1):- nonvar(X), set(X), !, set_preproc(X,Y), norep_in_set(Y,Y1). 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),!. set_preproc('{}','{}'):- !. set_preproc('{}'(A),B):- preproc_list(A,B),!. set_preproc(_,_):- write(' wrong set term '),nl, fail. preproc_list( A, '{}' with A):- var(A), !. preproc_list((A1,B1),B2 with A2):- !, preproc(A1,A2),preproc_list(B1,B2). preproc_list((A / X),X with B):- var(X),!, preproc(A,B). preproc_list((A / X),Y with B):- set(X),!, preproc(A,B), preproc(X,Y). preproc_list((A / X),Y with B):- X = _ with _,!, preproc(A,B), preproc(X,Y). preproc_list(A1,'{}' with A2):- preproc(A1,A2). 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). set(X):- nonvar(X),functor(X,'{}',_). %%%%%% Set postprocessor: from 'with' 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,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). 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(exists(V,G),[exists(V,G1)]):- %%% !, sf_in_goal(G,G1). 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(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(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(call(A),call(A1)):- !, ruq_in_goal(A,A1). ruq_in_goal((A)!,(A1)!):- !, ruq_in_goal(A,A1). 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) ) ; ssetassert( (Gpred :- G) ) ), 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((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). :- 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 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(' - ''{}'' is the empty set'), nl, write(' 2. Predefined set predicates (set constraints):'), nl, write(' - t in s (membership)'), nl, write(' - t nin s (non-membership)'), nl, write(' - t = s (equality)'), nl, write(' - t neq s (non-equality)'), nl, write(' - un(r,s,t) (union)'), nl, write(' - nun(r,s,t) (non-union)'), nl, write(' - disj(r,s) (disjointness)'), nl, write(' - ndisj(r,s) (non-disjointness)'), nl, write(' 3. RUQs: '), nl, write(' - forall(X in t, G),'), write(' X variable and G any {log} goal containing X'), nl, write(' - forall(X in t, exists(V,G)),'),nl, write(' - forall(X in t, 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, 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. 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. write_built_list :- sys(N,Ar), write(' - '),write(N),write('/'),write(Ar),nl, fail. write_built_list. 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('less(R,X,S): S is the set obtained from R by removing X'),nl, write('subset(S1,S2): subset (S1 \subseteq S2)'),nl, write('nsubset(S1,S2): not subset (S1 \not\subseteq S2)'),nl, write('ssubset(S1,S2): strict subset (S1 \subset S2)'),nl, write('int(R,S,T): intersection (T = R \cap S)'),nl, write('nint(R,S,T): not intersection (T = R \not\cap S)'),nl, write('diff(R,S,T): difference (T = R \setminus S)'),nl, write('ndiff(R,S,T): not difference (T = R \not\setminus S)'),nl, write('sdiff(R,S,T): symmetric difference (T = R \triangle S)'),nl, write('size(S,N): cardinality (N = |S|)'),nl, write('powerset(S,PS): powerset (PS = 2^S)'),nl. welcome_message :- no_interactive_mode, !. welcome_message :- nl, nl, write(' WELCOME TO {log} - version 3.4 '),nl, nl, nl. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- welcome_message,top_level.