/**********************************************************************
% 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).
