/********************************************************************** % Copyright (C) 1997 Ullrich Hustadt % Max-Planck-Institut fuer Informatik % Im Stadtwald % 66123 Saarbruecken, Germany % simplify.pl is free software; you can redistribute it and/or modify % it under the terms of the GNU General Public License as published by % the Free Software Foundation; either version 1, or (at your option) % any later version. % simplify.pl is distributed in the hope that it will be useful, % but WITHOUT ANY WARRANTY; without even the implied warranty of % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the % GNU General Public License for more details. **********************************************************************/ % simplify_alc(+TERM1,-TERM2) % transform TERM1 to negation normal form and simplify it according to % the rules of Table 1 in the MPII Research report 97-2-003 by Ullrich % Hustadt and Renate A. Schmidt. simplify_pltl(Term1,Term3) :- nnf_term(Term1,Term0), simplify_term(Term0,nnf,NNFTerm), simplifications(SF), (member(flatten,SF) -> simplRand(NNFTerm,Term2) ; Term2 = NNFTerm ), (Term2 = and(L2) -> subsumption(L2,L3), (sortOpt([conjunctions|_]) -> add_num(L3,L4), keysort(L4,L5), del_num(L5,L6) ; L6 = L3 ), rebuild_conjunction(L6,L7), (memberchk(cutOnProp(A),SF) -> Term3 = or([and([not(A),L7]),and([A,L7])]) ; Term3 = L7 ) ; (memberchk(cutOnProp(A),SF) -> Term3 = or([and([not(A),Term2]),and([A,Term2])]) ; Term3 = Term2 ) ), !. nnf_term(not(not(T1)),T2) :- !, nnf_term(T1,T2). nnf_term(not(always(T1)),sometime(T2)) :- !, nnf_term(not(T1),T2). nnf_term(not(sometime(T1)),always(T2)) :- !, nnf_term(not(T1),T2). nnf_term(not(next(T1)),next(T2)) :- !, nnf_term(not(T1),T2). nnf_term(not(and(L1)),or(L2)) :- !, nnf_terms(L1,L2). nnf_term(not(or(L1)),and(L2)) :- !, nnf_terms(L1,L2). nnf_term(T1,T1) :- atomic(T1), !. nnf_term(T1,T2) :- functor(T1,F,N), functor(T2,F,N), nnf_args(N,T1,T2), !. nnf_terms([],[]). nnf_terms([T1|TL1],[T2|TL2]) :- nnf_term(not(T1),T2), nnf_terms(TL1,TL2). nnf_args(1,T1,T2) :- arg(1,T1,A1), nnf_term(A1,A2), arg(1,T2,A2), !. nnf_args(N,T1,T2) :- N >= 2, arg(N,T1,A1), nnf_term(A1,A2), arg(N,T2,A2), M is N-1, nnf_args(M,T1,T2), !. num_symbols(always(C),N) :- num_symbols(C,M), N is M+7. num_symbols(sometime(C),N) :- num_symbols(C,M), N is M+7. num_symbols(next(C),N) :- num_symbols(C,M), N is M+5. num_symbols(and(L),N) :- num_symbols_list(L,N). num_symbols(or(L),N) :- num_symbols_list(L,N). num_symbols(not(C),N) :- num_symbols(C,M), N is M+1. num_symbols(C,1) :- atomic(C), name(C,[114,112|_]), !. num_symbols(C,2) :- atomic(C). num_symbols([L1],N) :- num_symbols(L1,N). num_symbols_list([],0). num_symbols_list([C1|CL],N) :- num_symbols(C1,N1), num_symbols_list(CL,NL), N is N1 + NL. add_num([],[]). add_num([C1|CL],[N1-C1|CLX]) :- num_symbols(C1,N1), add_num(CL,CLX). del_num([],[]). del_num([_-C1|CLX],[C1|CL]) :- del_num(CLX,CL). simplify_lwb(Term1,Term3) :- nnf_term(Term1,Term0), simplify_term(Term0,nnf,Term2), (Term2 = and(L2) -> (simplifyOpt(SOPT), member(units,SOPT) -> unit_propagate(L2,L7) ; L7 = L2 ), (sortOpt([conjunctions|_]) -> (atomic(L7) -> Term3 = L7 ; add_num(L7,L4), keysort(L4,L5), del_num(L5,L6), (orderingOpt(reverse) -> reverse(L6,L3) ; L3 = L6 ), Term3 = and(L3) ) ; Term3 = and(L2) ) ; Term3 = Term2 ). simplify_pltl_cont(Term1,Term4) :- simplify_term(Term1,nnf,Term2), (Term2 = and(L2) -> subsumption(L2,L3), rebuild_conjunction(L3,Term3) ; Term3 = Term2 ), (Term3 = Term1 -> Term4 = Term3 ; simplify_pltl_cont(Term3,Term4) ). simplify_term(and(L1),NegType,T2) :- simplify_conjunction(L1,NegType,T2). simplify_term(or(L1),NegType,T2) :- simplify_disjunction(L1,NegType,T2). simplify_term(not(T1),NegType,T2) :- simplify_term(T1,NegType,T3), (NegType == nnf -> negate_term(T3,T2) ; (atomic(T3) -> negate_term(T3,T2) ; T2 = not(T3) ) ). simplify_term(always(or(L1)),NegType,T2) :- !, simplify_disjunction(L1,NegType,L2), (remove_all_next(L2,L3) -> T2 = next(always(L3)) ; T2 = always(L2) ). simplify_term(always(T1),NegType,T3) :- simplify_term(T1,NegType,T2), rebuild_always(T2,T3). simplify_term(sometime(T1),NegType,T3) :- simplify_term(T1,NegType,T2), rebuild_sometime(T2,T3). simplify_term(next(T1),NegType,T3) :- simplify_term(T1,NegType,T2), rebuild_next(T2,T3). simplify_term(T1,_NegType,T1) :- atomic(T1). remove_all_next(or([]),or([])) :- !. remove_all_next(or([next(T1)|TL1]),or([T1|TL2])) :- !, remove_all_next(or(TL1),or(TL2)). remove_all_next(next(X),X) :- !. %remove_all_next(X,X). rebuild_always(true,true). rebuild_always(false,false). rebuild_always(T1,always(T1)). rebuild_next(true,true). rebuild_next(false,false). rebuild_next(T1,next(T1)). rebuild_sometime(false,false). rebuild_sometime(true,true). rebuild_sometime(T1,sometime(T1)). negate_term(always(true),false). negate_term(not(T1),T1). negate_term(always(T1),sometime(T2)) :- negate_term(T1,T2). negate_term(sometime(T1),always(T2)) :- negate_term(T1,T2). negate_term(next(T1),next(T2)) :- negate_term(T1,T2). negate_term(true,false). negate_term(false,true). negate_term(and(L1),or(L2)) :- negate_terms(L1,L2). negate_term(or(L1),and(L2)) :- negate_terms(L1,L2). negate_term(T1,not(T1)) :- atomic(T1). negate_terms([],[]). negate_terms([T1|TL1],[T2|TL2]) :- negate_term(T1,T2), negate_terms(TL1,TL2). simplify_elements_of_list([],_NegType,[]) :- !. simplify_elements_of_list([T1|TL1],NegType,[T2|TL2]) :- simplify_term(T1,NegType,T2), !, simplify_elements_of_list(TL1,NegType,TL2). simplify_conjunction(L1,NegType,T3) :- simplify_elements_of_list(L1,NegType,L2), (member(false,L2) -> T3 = false ; (sortOpt([conjunctions|_]) -> list_to_set(L2,L3) ; L3 = L2 ), simplify_conjunctive_list(L3,L4), rebuild_conjunction(L4,T3) ). rebuild_conjunction([],true). rebuild_conjunction([T1],T1) :- !. rebuild_conjunction(TL,and(TL)). subsumption([not(T1)|TL1],[not(T1)|TL4]) :- atomic(T1), eliminate_subsumed_disjunctions(TL1,not(T1),TL2), eliminate_from_disjunctions(TL2,T1,TL3), subsumption(TL3,TL4). subsumption([T1|TL1],[T1|TL4]) :- atomic(T1), eliminate_subsumed_disjunctions(TL1,T1,TL2), eliminate_from_disjunctions(TL2,not(T1),TL3), subsumption(TL3,TL4). subsumption([T1|TL1],[T1|TL2]) :- subsumption(TL1,TL2). subsumption([],[]). eliminate_subsumed_disjunctions([],_,[]). eliminate_subsumed_disjunctions([or(L1)|TL1],T1,TL2) :- member(T1,L1), eliminate_subsumed_disjunctions(TL1,T1,TL2). eliminate_subsumed_disjunctions([T1|TL1],T2,[T1|TL2]) :- eliminate_subsumed_disjunctions(TL1,T2,TL2). eliminate_from_disjunctions([],_,[]). eliminate_from_disjunctions([or(L1)|TL1],T1,[T2|TL2]) :- !, delete(L1,T1,L2), (L2 = [T3] -> T2 = T3 ; T2 = or(L2) ), eliminate_from_disjunctions(TL1,T1,TL2). eliminate_from_disjunctions([T1|TL1],T2,[T1|TL2]) :- eliminate_from_disjunctions(TL1,T2,TL2). simplify_disjunction(L1,NegType,T3) :- simplify_elements_of_list(L1,NegType,L2), (member(true,L2) -> T3 = true ; sortOpt(SO), (memberchk(disjunctions,SO) -> list_to_set(L2,L3) ; (memberchk(weight_disjunctions,SO) -> add_num(L2,LH1), keysort(LH1,LH2), del_num(LH2,L3) ; L3 = L2 ) ), (memberchk(lastProp(A),SO) -> (memberchk(A,L3) -> delete(L3,A,LH3), append(LH3,[A],L4) ; L4 = L3 ) ; L4 = L3 ), (memberchk(negateProp(A),SO) -> negateProp(L4,L5,A) ; L5 = L4 ), simplify_disjunctive_list(L5,LH4), rebuild_disjunction(LH4,T3) ). negateProp([],[],_A) :- !. negateProp([A|L1],[not(A)|L2],A) :- !, negateProp(L1,L2,A). negateProp([next(A)|L1],[next(not(A))|L2],A) :- !, negateProp(L1,L2,A). negateProp([not(A)|L1],[A|L2],A) :- !, negateProp(L1,L2,A). negateProp([next(not(A))|L1],[next(A)|L2],A) :- !, negateProp(L1,L2,A). negateProp([L|L1],[L|L2],A) :- negateProp(L1,L2,A), !. rebuild_disjunction([],false). rebuild_disjunction([T1],T1) :- !. rebuild_disjunction(TL,TL1) :- (all_next(TL,TL2) -> !, TL1 = next(or(TL2)) ; TL1 = or(TL) ). all_next([],[]) :- !. all_next([T1|TL1],[T2|TL2]) :- (T1 = next(L) -> !, T2 = L, all_next(TL1,TL2) ; !, fail ). % simplify_conjunctive_list(LISTE1,LISTE2) % Beachte: Die Eingabeliste LISTE1 kann die Konstante `false' nicht % enthalten. simplify_conjunctive_list([],[]) :- !. simplify_conjunctive_list([true|TL1],TL2) :- !, simplify_conjunctive_list(TL1,TL2). simplify_conjunctive_list([not(C1)|TL1],TL2) :- (member(C1,TL1) -> TL2 = [false] ; simplify_conjunctive_list(TL1,TL3), (TL3 = [false] -> TL2 = [false] ; (member(not(C1),TL3) -> TL2 = TL3 ; TL2 = [not(C1)|TL3] ) ) ). simplify_conjunctive_list([C1|TL1],TL2) :- (member(not(C1),TL1) -> TL2 = [false] ; simplify_conjunctive_list(TL1,TL3), (TL3 = [false] -> TL2 = [false] ; (member(C1,TL3) -> TL2 = TL3 ; TL2 = [C1|TL3] ) ) ). % simplify_disjunctive_list(LISTE1,LISTE2) % Beachte: Die Eingabeliste LISTE1 kann die Konstante `true' nicht % enthalten. simplify_disjunctive_list([],[]) :- !. simplify_disjunctive_list([false|TL1],TL2) :- !, simplify_disjunctive_list(TL1,TL2). simplify_disjunctive_list([not(C1)|TL1],TL2) :- (member(C1,TL1) -> TL2 = [true] ; simplify_disjunctive_list(TL1,TL3), (TL3 = [true] -> TL2 = [true] ; (member(not(C1),TL3) -> TL2 = TL3 ; TL2 = [not(C1)|TL3] ) ) ). simplify_disjunctive_list([C1|TL1],TL2) :- (member(not(C1),TL1) -> TL2 = [true] ; simplify_disjunctive_list(TL1,TL3), (TL3 = [true] -> TL2 = [true] ; (member(C1,TL3) -> TL2 = TL3 ; TL2 = [C1|TL3] ) ) ). factor_common_subexpressions(T1,and(T2)) :- common_subexpressions(T1,and(T3),E3), append(T3,E3,T2). common_subexpressions(T1,T3,E3) :- get_all_expression(T1,A1), !, new_predicate(d,P), replace_all_occurrences(T1,A1,P,T2), E1 = [or([not(P),A1]),or([not(A1),P]), always(or([not(P),A1])), always(or([not(A1),P]))], common_subexpressions(T2,T3,E2), append(E1,E2,E3). common_subexpressions(T1,T1,[]). replace_all_occurrences(A1,A1,P,P) :- !. replace_all_occurrences(T1,A1,P,T2) :- T1 =.. [F|Args1], replace_all_occurrences_list(Args1,A1,P,Args2), T2 =.. [F|Args2]. replace_all_occurrences_list([],_A1,_P,[]). replace_all_occurrences_list([T1|TL1],A1,P,[T2|TL2]) :- replace_all_occurrences(T1,A1,P,T2), replace_all_occurrences_list(TL1,A1,P,TL2). get_all_expression(always(T1),T3) :- (get_all_expression(T1,T2) -> T3 = T2 ; T3 = always(T1) ), !. get_all_expression(T1,A1) :- T1 =.. [_|Args], get_all_expression_list(Args,A1). get_all_expression_list([],_) :- !, fail. get_all_expression_list([L1|_],A1) :- get_all_expression(L1,A1), !. get_all_expression_list([_|L2],A1) :- get_all_expression_list(L2,A1). new_predicate(Prefix,Symbol) :- ( retract(new_predicate_counter(Prefix,Value)) ; Value = 100 ), NewValue is Value+1, asserta(new_predicate_counter(Prefix,NewValue)), name(Prefix,P), name(NewValue,N), user:append(P,N,SymbolList), name(Symbol,SymbolList), !. get_units([],[]) :- !. get_units([and(_)|L1],L2) :- !, get_units(L1,L2). get_units([or([A])|L1],L3) :- atomic(A), !, get_units(L1,L2), union([A],L2,L3). get_units([or([not(B)])|L1],L3) :- atomic(B), !, get_units(L1,L2), union([not(B)],L2,L3). get_units([or([_|_])|L1],L2) :- !, get_units(L1,L2). get_units([A|L1],L3) :- atomic(A), !, get_units(L1,L2), union([A],L2,L3). get_units([not(B)|L1],L3) :- atomic(B), !, get_units(L1,L2), union([not(B)],L2,L3). get_units([_|L1],L2) :- !, get_units(L1,L2). unit_propagate(false,false) :- !. unit_propagate(true,true) :- !. unit_propagate(L1,L2) :- get_units(L1,Units), (Units == [] -> L2 = L1 ; (member(false,Units) -> !, L2 = false ; propagate(L1,Units,L3), unit_propagate(L3,L4), (L4 == [] -> L2 = true ; (atomic(L4) -> L2 = L4 ; append(L4,Units,L2) ) ) ) ), !. % propagate(L1,Units,L2) % L2 ist das Ergebnis von unit propagation mit Units auf L1. propagate([],_,[]) :- !. propagate([Disj1|L1],Units,L3) :- propagate1(Units,Disj1,Disj2), (Disj2 == false -> L3 = false ; propagate(L1,Units,L2), (Disj2 == true -> L3 = L2 ; (L2 == false -> L3 = false ; L3 = [Disj2|L2] ) ) ), !. % propagate1(Units,L1,L2) % L2 ist das Ergebnis von unit propagation mit Units auf L1. propagate1([],Disj,Disj) :- !. propagate1([Unit|UL],Disj1,Disj3) :- (Disj1 = or(DL1) -> propagate2(Unit,DL1,Disj2) ; propagate2(Unit,[Disj1],Disj2) ), (Disj2 == true -> Disj3 = true ; (Disj2 == false -> Disj3 = false ; propagate1(UL,Disj2,Disj3) ) ), !. propagate2(Unit,DL,Disj2) :- (member(Unit,DL) -> Disj2 = true ; nnf_term(not(Unit),Neg), delete(DL,Neg,Res), (Res = [] -> Disj2 = false ; (Res == false -> Disj2 = false ; Disj2 = or(Res) ) ) ), !. simplRand(and(Conjuncts0),and(Conjuncts2)) :- !, simplConj(Conjuncts0,NextClauses,SometimeLiterals,PropLiterals), gensym(q,Atom1), buildSometimeClauses(Atom1,SometimeLiterals,SometimeClauses), _C0 = always(or([not(Atom1),next(Atom1)])), gensym(q,Atom2), buildAlwaysClauses(Atom2,PropLiterals,AlwaysClauses), C1 = always(or([not(Atom2),next(Atom2)])), gensym(q,Atom3), C2 = always(or([not(Atom3),next(Atom1),next(Atom2)])), C3 = or([Atom3]), append(NextClauses,[C1,C2,C3|AlwaysClauses],Conjuncts1), append(Conjuncts1,SometimeClauses,Conjuncts2). simplRand(Term,Term). buildAlwaysClauses(_Atom,[],[]) :- !. buildAlwaysClauses(Atom,[L1|LL1],[C1|CL1]) :- C1 = always(or([not(Atom),L1])), buildAlwaysClauses(Atom,LL1,CL1). buildSometimeClauses(_Atom,[],[]) :- !. buildSometimeClauses(Atom,[L1|LL1],[C1|CL1]) :- C1 = always(or([not(Atom),sometime(L1)])), buildSometimeClauses(Atom,LL1,CL1). simplConj([],[],[],[]) :- !. simplConj([always(or(C1))|CL1],NC2,SLL2,NLL2) :- simplConj(CL1,NC1,SLL1,NLL1), (member(sometime(_),C1) -> NC1 = NC2, splitDisj(C1,SLL0,NLL0), append(SLL0,SLL1,SLL2), append(NLL0,NLL1,NLL2) ; NC2 = [always(or(C1))|NC1], SLL2 = SLL1, NLL2 = NLL1 ). simplConj([next(C)|CL1],[next(C)|NC2],SLL2,NLL2) :- simplConj(CL1,NC2,SLL2,NLL2). simplConj([or(C)|CL1],[or(C)|NC2],SLL2,NLL2) :- simplConj(CL1,NC2,SLL2,NLL2). splitDisj([],[],[]) :- !. splitDisj([sometime(L1)|LL1],[L1|SLL1],NLL) :- splitDisj(LL1,SLL1,NLL). splitDisj([not(A)|LL1],SLL1,[not(A)|NLL]) :- atomic(A), splitDisj(LL1,SLL1,NLL). splitDisj([A|LL1],SLL1,[A|NLL]) :- atomic(A), splitDisj(LL1,SLL1,NLL).