% ---------------------------------------------------------------------- % -- fixing the prolog system % found in my ~/.sicstusrc % :- dynamic(prolog_system/1). % :- assert(prolog_system(sicstus)). % found in my ~/.eclipserc % :- dynamic(prolog_system/1),assert(prolog_system(eclipse)). :- prolog_system(X), (X = sicstus -> compile(sicstus); X = eclipse -> compile(eclipse); true -> error('No Prolog System specified ! ')). % ---------------------------------------------------------------------- % -- operator definitions :- op(900,fy,neg). :- op(700,xfx,\<). :- op(1100,xfy,v). % ---------------------------------------------------------------------- % -- ensure that companion files are charged :- ensure_loaded(grounder). % grounder :- ensure_loaded(pp). % pretty-printer :- ensure_loaded(dlv). % dlv-specific code :- ensure_loaded(smodels). % smodels-specific code % ---------------------------------------------------------------------- % -- the compilation predicates lp2pl(Name) :- concatenate(Name,'.lp',FileIn ), concatenate(Name,'.pl',FileOut), compile_file(FileIn, FileOut). vlp2pl(Name) :- vlp2glp(Name), glp2alp(Name), concatenate(Name,'.alp',FileIn ), concatenate(Name, '.pl',FileOut), compile_file(FileIn, FileOut). compile_file(FileIn, FileOut) :- read_clauses(FileIn,Clauses), write_program('Input Clauses',Clauses), transform_clauses(Clauses,PrefRules), write_program('Intermediate Rules',PrefRules), rules2procedures(PrefRules,Procedures), write_clauses(FileOut,Procedures), write_program('Output Procedures',Procedures). % ---------------------------------------- % lp files vlp2glp(Name) :- concatenate(Name,'.vlp',FileIn ), concatenate(Name,'.glp',FileOut), ground_file(FileIn, FileOut). glp2alp(Name) :- concatenate(Name,'.glp',FileIn ), concatenate(Name,'.alp',FileOut), atomize_file(FileIn, FileOut). % ---------------------------------------- % pl files pl2gpl(Name) :- concatenate(Name, '.pl',FileIn ), concatenate(Name,'.gpl',FileOut), ground_file(FileIn, FileOut). gpl2apl(Name) :- concatenate(Name,'.gpl',FileIn ), concatenate(Name,'.apl',FileOut), atomize_file(FileIn, FileOut). % ---------------------------------------------------------------------- % -- the real transformation transform_clauses( Rules, NewRules ) :- homogenize(Rules,Rules0), apply_to_conjuncts(Rules0,add_preferences,Rules1), ok_rules(Rules0,OKRules), pref_rules(PrefRules), conjoin(OKRules,PrefRules,AuxRules), conjoin(Rules1,AuxRules,NewRules). homogenize( Wff, HWff ) :- Wff = (A :- B) -> homogenize(A,HA), homogenize(B,HB), HWff = (HA :- HB); Wff = (A , B) -> homogenize(A,HA), homogenize(B,HB), HWff = (HA , HB); (Wff = (A ; B) ; Wff = (A | B) ; Wff = (A v B) ) -> homogenize(A,HA), homogenize(B,HB), HWff = (HA ; HB); (Wff = (not A) ; Wff = (~ A) ) -> homogenize(A,HA), HWff = (not HA); (Wff = (neg A) ; Wff = (- A) ) -> homogenize(A,HA), HWff = (neg HA); Wff = (A \< B) -> HWff = (neg (A < B)); Wff = [N] -> HWff = name(N); %true -> Wff = HWff. add_preferences( (Head :- name(N), Body), Rules ) :- add_preferences_body(Body, N, BodyRules), Rule0 = (Head :- ap(N) ), Rule1 = (ap(N) :- name(N), ok(N), Body), % name(N) is left for later usage conjoin(Rule0,Rule1,Rules01), conjoin(Rules01, BodyRules, Rules). add_preferences( (Head :- name(N)), Rules ) :- add_preferences( (Head :- name(N), true), Rules ). add_preferences( F, F ) :- writeln_verbosely('Leaving ':F:' untouched'). add_preferences_body( Body, N, Rules ) :- Body = (Body1,Body2) -> add_preferences_body(Body1,N,Rules1), add_preferences_body(Body2,N,Rules2), conjoin(Rules1,Rules2,Rules); Body = (not Literal) -> Rules = (bl(N) :- ok(N), Literal); Body = Literal -> Rules = (bl(N) :- ok(N), not Literal). ok_rules( Rules, OKRules ) :- extract_oko_literals_from_rules(Rules,N,OKOLiterals), QRule = ( ok(N) :- name(N), OKOLiterals ), CRules = ( (oko(N,M) :- name(N), name(M), not ((N < M)) ), (oko(N,M) :- name(N), name(M), (N < M) , ap(M) ), (oko(N,M) :- name(N), name(M), (N < M) , bl(M) ) ), conjoin(QRule,CRules,OKRules). extract_oko_literals_from_rules( Rules, N, Literals ) :- Rules = (Rules1,Rules2) -> extract_oko_literals_from_rules(Rules1,N,Literals1), extract_oko_literals_from_rules(Rules2,N,Literals2), conjoin(Literals1,Literals2,Literals); Rules = (_ :- name(M), _) -> Literals = oko(N,M); Rules = (_ :- name(M) ) -> Literals = oko(N,M); %true -> Literals = true. pref_rules( PrefRules ) :- ASRule = ( (neg (M < N)) :- name(N), name(M), (N < M) ), TRule = ( (N < M) :- name(N), name(M), name(O), (N < O), (O < M) ), conjoin(ASRule,TRule,PrefRules). % ---------------------------------------------------------------------- % -- Rules to Procedures builtin(not,1). builtin(neg,1). % builtin(-,1). --> neg % builtin(~,1). --> not % builtin(<,2). --> pref builtin(ok,1). builtin(oko,2). builtin(ap,1). builtin(bl,1). rules2procedures(Rules,Procedures) :- extract_names_from_rules(Rules,Rules0,Names), predicates(Rules0,Preds0), reverse(Preds0,Preds), procedures(Preds,Rules0,Procedures0), constraints(Preds,Constraints), conjoin(Procedures0,Constraints,Procedures1), apply_to_conjuncts(Procedures1,simplify_rule,Procedures2), apply_to_conjuncts(Procedures2,adjust_rule,Procedures3), name_predicates(Names,NameLits), conjoin(Procedures3,NameLits,Procedures). extract_names_from_rules( Rules, NewRules, Names ) :- Rules = (Rules1,Rules2) -> extract_names_from_rules(Rules1,NewRules1,Names1), extract_names_from_rules(Rules2,NewRules2,Names2), conjoin(NewRules1,NewRules2,NewRules), union(Names1,Names2,Names); (Rules = (H :- name(M), ok(M), B), nonvar(M) ) -> NewRules = (H :- ok(M), B), Names = [M]; (Rules = name(M) , nonvar(M) ) -> NewRules = true, Names = [M]; %true -> Rules = NewRules, Names = []. predicates(Wff,L) :- Wff = (A :- B) -> predicates(A,L1), predicates(B,L2), union(L2,L1,L); Wff = (A , B) -> predicates(A,L1), predicates(B,L2), union(L2,L1,L); Wff = (A ; B) -> predicates(A,L1), predicates(B,L2), union(L2,L1,L); Wff = (not A) -> predicates(A,L); Wff = (neg A) -> predicates(A,L); %true -> functor(Wff,F,N), L = [[F,N]]. procedures([[name,1]|Preds],Clauses,Procs) :- procedures(Preds,Clauses,Procs). procedures([[P,N]|Preds],Clauses,Procs) :- procedure(P,N,Clauses,Proc), procedures(Preds,Clauses,Procs1), conjoin(Proc,Procs1,Procs). procedures([],_Clauses,true). procedure(P,N,Clauses,Proc) :- Clauses = (A , B) -> procedure(P,N,A,ProcA), procedure(P,N,B,ProcB), conjoin(ProcA,ProcB,Proc); (Clauses = ( A :- _) , functor(A,P,N)) -> Proc = Clauses; (Clauses = ((neg A) :- _) , functor(A,P,N)) -> Proc = Clauses; (Clauses = ((A;B) :- _) , functor(A,P,N)) -> Proc = Clauses; (Clauses = A , functor(A,P,N)) -> Proc = Clauses; (Clauses = (neg A) , functor(A,P,N)) -> Proc = Clauses; %true -> Proc = true. constraints([[name,1]|Preds],Constraints) :- constraints(Preds,Constraints). constraints([[P,N]|Preds],Constraints) :- builtin(P,N), constraints(Preds,Constraints). constraints([[P,_]|Preds],Constraints) :- negative_functor(P), constraints(Preds,Constraints). constraints([[<,2]|Preds],Constraints) :- Lit = (N < M), Constraint = (false :- name(N), name(M), Lit, neg Lit), constraints(Preds,Constraints1), conjoin(Constraint,Constraints1,Constraints). constraints([[P,N]|Preds],Constraints) :- functor(Lit,P,N), Constraint = (false :- Lit, neg Lit), constraints(Preds,Constraints1), conjoin(Constraint,Constraints1,Constraints). constraints([],true). simplify_rule( (Head :- Body), Rule ) :- simplify(Head,SHead), simplify(Body,SBody), (SBody = true -> Rule = SHead; SBody = false -> Rule = true; %true -> Rule = (SHead :- SBody)). simplify_rule( F, F ) :- writeln_verbosely('Leaving ':F:' untouched'). simplify( Wff, SWff ) :- Wff = (Wff1, Wff2) -> simplify(Wff1,Wff3), simplify(Wff2,Wff4), conjoin(Wff3,Wff4,SWff); Wff = (Wff1; Wff2) -> simplify(Wff1,Wff3), simplify(Wff2,Wff4), disjoin(Wff3,Wff4,SWff); Wff = (not not Literal) -> simplify(Literal,SWff); Wff = (not false) -> SWff = true; Wff = (not true) -> SWff = false; Wff = (neg neg Literal) -> simplify(Literal,SWff); Wff = (neg false) -> SWff = true; Wff = (neg true) -> SWff = false; %true -> SWff = Wff. adjust_rule( (Head :- Body), (AHead :- ABody) ) :- adjust(Head,AHead), adjust(Body,ABody). adjust_rule( Fact, AFact ) :- adjust(Fact,AFact). adjust( Wff, AWff ) :- Wff = (Wff1, Wff2) -> adjust(Wff1,Wff3), adjust(Wff2,Wff4), conjoin(Wff3,Wff4,AWff); Wff = (Wff1; Wff2) -> adjust(Wff1,Wff3), adjust(Wff2,Wff4), disjoin(Wff3,Wff4,AWff); Wff = (not Literal) -> adjust(Literal,ALiteral), AWff = (not ALiteral); Wff = (neg Literal) -> adjust(Literal,ALiteral), negated_literal(ALiteral,NegLiteral), AWff = (NegLiteral); Wff = (N < M) -> AWff = prec(N,M); %true -> AWff = Wff. name_predicates( [], true ). name_predicates( [N|Ns], NLs ) :- name_predicates(Ns,NLs1), conjoin(NLs1,name(N),NLs). % ---------------------------------------------------------------------- % -- auxiliary predicates, % -- many of which are taken from Mark Stickel's pttp concatenate(String1,String2,String) :- name(String1,L1), name(String2,L2), append(L1,L2,L), name(String,L), !. conjoin(A,B,C) :- A == true -> C = B; B == true -> C = A; A == false -> C = false; B == false -> C = false; A == B -> C = A; (B = (B1,_), A == B1) -> C = B; (A = (_,A2), B == A2) -> C = A; %true -> C = (A , B). disjoin(A,B,C) :- A == true -> C = true; B == true -> C = true; A == false -> C = B; B == false -> C = A; A == B -> C = A; %true -> C = (A ; B). negated_functor(F,NegF) :- name(F,L), name(neg_,L1), (append(L1,L2,L) -> true; %true -> append(L1,L,L2)), name(NegF,L2). negated_literal(Lit,NegLit) :- Lit =.. [F1|L1], negated_functor(F1,F2), (var(NegLit) -> NegLit =.. [F2|L1]; %true -> NegLit =.. [F2|L2], L1 == L2). negative_functor(F) :- name(F,L), name(neg_,L1), append(L1,_,L). negative_literal(Lit) :- functor(Lit,F,_), negative_functor(F). apply_to_conjuncts(Wff,P,Wff1) :- Wff = (A , B) -> apply_to_conjuncts(A,P,A1), apply_to_conjuncts(B,P,B1), conjoin(A1,B1,Wff1); %true -> T1 =.. [P,Wff,Wff1], call(T1). flatten_conjunction( Wff, FWff ) :- flatten_conjunction(Wff,true,FWff). flatten_conjunction( Wff, AWff, FWff ) :- Wff = (Wff1,Wff2) -> flatten_conjunction(Wff2,AWff,FWff1), flatten_conjunction(Wff1,FWff1,FWff); AWff = true -> FWff = Wff; %true -> FWff = (Wff,AWff). % ---------------------------------------------------------------------- % -- i/o predicates write_clause(A) :- nl, write(A), write(.). write_clause(A,_) :- % 2-ary predicate can be used as write_clause(A). % argument of apply_to_conjuncts write_clauses(C) :- apply_to_conjuncts(C,write_clause,_). write_clauses(File,Wff) :- open(File,write,Stream), write_clauses1(Stream,Wff), close(Stream). write_clauses1(Stream,(A,B)) :- write_clauses1(Stream,A), write_clauses1(Stream,B), !. write_clauses1(Stream,A) :- write(Stream,A), write(Stream,.), nl(Stream), !. write_program(String,Program) :- verbose_flag -> write('--'),nl, write(String),nl, write('--'), apply_to_conjuncts(Program,write_clause,_), nl,write('=='),nl; %true-> true. read_clauses(File,Wff) :- open(File,read,Stream), read_wff_loop(Stream,Wff), close(Stream). read_wff_loop(Stream,Wff) :- read(Stream,Wff1), (Wff1 == end_of_file -> Wff = true; %true -> read_wff_loop(Stream,Wff2), conjoin(Wff1,Wff2,Wff)). % ---------------------------------------------------------------------- % -- verbose predicates, chatting if verbose_mode is turned on :- dynamic(verbose_flag/0). verbose_mode :- % enable verbose mode retract(verbose_flag), fail. verbose_mode :- assert(verbose_flag). no_verbose_mode :- % disable verbose mode retract(verbose_flag), fail. no_verbose_mode. :- verbose_mode. % default is verbose mode writeln_verbosely(X) :- verbose_flag -> write(X),nl; %true-> true.