%%% REPLACEMENTS
%%%
%%% Replace a literal by the definitions.
%%% A set of rules are provided by the user. The rules are stored with
%%%     a list of 0s and 1s. A literal with 1 means that it is a
%%%     distinguished literal and can be replaced by its definitions.
%%% New instances are generated by replacements. An instance is also
%%%     associated with a list of 0s and 1s. A 0 means that the literal
%%%     is a substitutable literal and can be used to generate instances
%%%     of replace rules.
%%% The algorithm is described as follows. First we find a rule and
%%%     all its distinguishded literals Ls. Matched Ls with substitutable
%%%     literals at the same time to generate instances.
%%%     Repeat all the rules.
%%%     Do the process iteratively until no new instances are generated.
%%% Many procedures are defined in the hyper module.
%%%     
%%% An instance is user supported if the literal is.
%%% An instance is backward supported if it is all negative or if all
%%%     substitutable literals for positive distinguished literals are
%%%     backward supported and the nondistinguished literals are all
%%%     negative.
%%% An instance is forward supported if it is all positive or if all
%%%     substitutable literals for negative distinguished literals are
%%%     forward supported and the nondistinguished literals are all
%%%     positive.
%%%
%%% Add an option which only takes ground literals to do replacements.
%%%     The option is ground_substitution.
%%% 
%%% We throw away instances if the sliding priority is used.
%%% 
%%% We keep two lists of literals, one is lit_N which is a list of new 
%%%     literals obtained in the latest round, and the other is lit_ST
%%%     which is a list accumulated from the beginning but not including
%%%     the latest round.
%%%
%%% A matched distinguished literal is not allowed to be more specific
%%%	than the form at the time it was matched.
%%%	For example:
%%%		[p(X), q(X), t(X)], [1,1,0]
%%%	Suppose p(X) is matched to p(s(Y)), then the nucleus becomes
%%%		[p(s(Y)), q(s(Y)), t(s(Y))]
%%%	Now if there is a literal not(q(s(a))), then we can't
%%%	match q(s(Y)) with not(q(s(a))) since this makes the first literal
%%%	more specific than the form at the time it was matched.
%%%	(p(s(a)) is more specific than p(s(Y)))
%%%
%%%	To implement this, we keep a list of variables from electrons.
%%%	Whenever a distinguished literal matches another literal, we
%%%	check if the list can unify with a constant list. If not, than
%%%	the no_specific rule is violated. If so, the matching is allowed
%%%	and we update the variable list.
%%%
%%% Ground literals are matched first.
%%%
%%% Allow two sets of replace rules. Replacements are done iteratively 
%%%	for the first set until no new instances can be generated. 
%%%	Then replacements are done once for the second set of rules. 
%%%	Then replacements are done iteratively for the first set until
%%%	no new instances can be generated.
%%%
%%% Allow replace variables in the electrons by individual constants.
%%%	So we check the variable list. If an element is a constant,
%%%	delete it. If it is a variable, keep it. Otherwise, reject it.
%%%	However, we don't allow a matched electron to be more specific.
%%%
%%% ground restriction. The nucleus is ground after instantiation,
%%%	not that the electrons are ground.
%%%
%%% ground substitution. The matching eletrons are ground.
%%%
%%% Add context literals.
%%%	Allow context literals matching non-ground electrons for
%%%	ground substitution.
%%%
%%% ground restriction on distinguished literals after matching.
%%%     An option is added to require that the distinguished literals
%%%     (not including context literals) after matching are ground.
%%%

     top_level_replace :- not(not(top_level_replace_fail)).

     top_level_replace_fail :-
        replacement,
        cputime(TT1),
        not(not(top_level_replace_0)),
        cputime(TT2),
        TT3 is TT2 - TT1,
        write_line(5,'Top level replace(s): ',TT3),
        !.
     top_level_replace_fail.
       
%%% We have to recompute the largest clause length.
%%% Find all literals from clauses.
%%% Find all instances by replacements.
%%% Do more until no instances are generated.
%%% Recompute the largest clause length.
     top_level_replace_0 :-
	const_list(Clist),
	repeated_replacements_1(Clist),
	once_replacements(Clist),
	repeated_replacements_2(Clist),
	not(not(obtain_largest_clause_length)),
	abolish(lit_ST_G,5),
	abolish(lit_ST_V,5),
	abolish(lit_N_G,5),
	abolish(lit_N_V,5).

     repeated_replacements_1(Clist) :-
        not(not(rpl_lits(0,Clist))),
	not(not(rpl_instances_call(repeated,Clist))).

     rpl_instances_call(Type,Clist) :-
        not(not(rpl_instances(Type,Clist))),
	not(not(litN_to_litST)),
        not(not(rpl_lits(1,Clist))),
	physically_erase(sent_C),
        not(not(update_sentC_1(Clist))),
        sentINST_to_sentC_a,
        not(not(rpl_more(Type,Clist))), !.
 
     once_replacements(Clist) :-
	not(not(litN_to_litST)),
	not(not(rpl_instances_call(once,Clist))).

     repeated_replacements_2(Clist) :-
	not(not(rpl_more(repeated,Clist))).

%%% Find a replace rule.
     rpl_instances(repeated,Clist) :-
        replace_rule_1(Rule,V1,W1,Flags,Contexts),
        rpl_instances_rule(repeated,Rule,V1,W1,Flags,Contexts,Clist),
	check_hl_stop, !.
     rpl_instances(once,Clist) :-
        replace_rule_2(Rule,V1,W1,Flags,Contexts),
        rpl_instances_rule(once,Rule,V1,W1,Flags,Contexts,Clist),
	check_hl_stop, !.
     rpl_instances(_,_).
       
%%% Find all the instance of a replace rule.
%%% We do unit deletion for instances.
%%% A list of 0s and 1s are associated with an instance. The literal with
%%%     1 would be deleted by unit deletion.
     rpl_instances_rule(Type,Rule,V1,W1,Flags,Contexts,Clist) :-
        print_rpl_rule(Rule,V1,Flags,Contexts),
        rpl_sep_clause(Flags,Rule,Contexts,W1,Dg,NDg,DConts,Dw,VRule,VDg,VNDg),
	negate_clause(Dg,NegDg),
        !,
        rpl_inst_rule(Type,Flags,Contexts,Rule,W1,NegDg,NDg,DConts,Dw,
		VRule,VDg,VNDg,Clist).
 
%%% Initialize support and distance information.
%%% Match distinguished literals.
%%% Adjust user distance.
%%% Miscellaneous things.
     rpl_inst_rule(Type,Flags,Contexts,Rule,W1,NegDg,NDg,DConts,Dw,
		VRule,VDg,VNDg,Clist) :-
        rpl_rule_SR(Rule,DS1,DR1),
        rpl_match_dgs(Type,NegDg,DConts,Dw,VDg,DS1,DR1,Clist,VL,DS2,DR2),
	check_ground_disting_after_match(DConts,VDg,NegDg),
        rpl_inst_rule_0(Flags,Contexts,Rule,W1,DS2,DR2,NDg,VRule,VNDg).
 
%%% If ground_disting_after_match is specified.
     check_ground_disting_after_match(DConts,VDg,NegDg) :-
	ground_disting_after_match,
	union_lists(DConts,VDg,YY),
        literals_remain_1(YY,NegDg,XX,_),
	!, numbervars(XX,0,0), !.
     check_ground_disting_after_match(_,_,_) :- !.
	
%%% Initialize support and distance information.
     rpl_rule_SR(X,sp(0,1,1),ds(1,0,1)) :- negclause(X), !.
     rpl_rule_SR(X,sp(0,1,1),ds(1,1,0)) :- posclause(X), !.
     rpl_rule_SR(_,sp(0,1,1),ds(1,1,1)) :- !.
 
     rpl_match_dgs(Type,[D|Ds],[DC|DCs],[W|Dw],[VD|VDs],
		DS1,DR1,Clist,VL1,DS2,DR2) :-
        rpl_match_dg_N(Type,D,DC,W,Dw,VD,DS1,DR1,Clist,VL1,Dw1,DSM,DRM,VLM),
        rpl_match_dgs_R(Ds,DCs,Dw1,VDs,DSM,DRM,Clist,VLM,DS2,DR2).
     rpl_match_dgs(Type,[D|Ds],[DC|DCs],[W|Dw],[VD|VDs],
		DS1,DR1,Clist,VL1,DS2,DR2) :-
        rpl_match_dgs_1(Type,Ds,DCs,Dw,VDs,DS1,DR1,Clist,[D|Kg1],[DC|KDC1],
		[W|Kw1],[VD|VKg1],Kg1,KDC1,Kw1,VKg1,VL1,DS2,DR2).
     rpl_match_dgs_1(Type,[D|Ds],[DC|DCs],[W|Dw],[VD|VDs],DS1,DR1,Clist,
		Kg1,KDC1,Kw1,VKg1,Ds,DCs,Dw,VDs,VL1,DS2,DR2) :-
        rpl_match_dg_N(Type,D,DC,W,Kw1,VD,DS1,DR1,Clist,VL1,Kw2,DSM,DRM,VLM),
        rpl_match_dgs_R(Kg1,KDC1,Kw2,VKg1,DSM,DRM,Clist,VLM,DS2,DR2).
     rpl_match_dgs_1(Type,[D|Ds],[DC|DCs],[W|Dw],[VD|VDs],DS1,DR1,Clist,
		Kg1,KDC1,Kw1,VKg1,[D|Kg2],[DC|KDC2],[W|Kw2],[VD|VKg2],
		VL1,DS2,DR2) :-
        rpl_match_dgs_1(Type,Ds,DCs,Dw,VDs,DS1,DR1,Clist,Kg1,KDC1,Kw1,VKg1,
		Kg2,KDC2,Kw2,VKg2,VL1,DS2,DR2).
 
%%% If the distinguished literal is ground, then no backtracking.
     rpl_match_dg_N(Type,D,DC,W,Dw1,VD,DS1,DR1,Clist,VL1,Dw1,DS2,DR2,VL2) :-
	var(W),
        !,
	rpl_match_new_literal(Type,VD,D,DC,Wn1,LS1,LR1),
	check_electron_vars(Wn1,Wn2),
	expand_VL(Wn2,VL1,VL2),
        onelink_SR(D,DS1,DR1,LS1,LR1,DS2,DR2), !.
     rpl_match_dg_N(Type,D,DC,_,Dw1,VD,DS1,DR1,Clist,VL1,Dw2,DS2,DR2,VL2) :-
	rpl_match_new_literal(Type,VD,D,DC,Wn1,LS1,LR1),
	check_electron_vars(Wn1,Wn2),
	check_electron_vars(VL1,VLM),
	not(not(VLM = Clist)),
	w1_w2(Dw1,Dw2),
	expand_VL(Wn2,VLM,VL2),
        onelink_SR(D,DS1,DR1,LS1,LR1,DS2,DR2).
 
%%% If no ground_substitution, then take all.
%%% If ground_substitution and context literal, take all.
%%% Otherwise, stop.
     rpl_match_new_literal(repeated,VD,D,_,Wn1,LS1,LR1) :-
        lit_N_G(VD,D,Wn1,LS1,LR1).
     rpl_match_new_literal(repeated,VD,D,_,Wn1,LS1,LR1) :-
	\+ ground_substitution,
	!, lit_N_V(VD,D,Wn1,LS1,LR1).
     rpl_match_new_literal(repeated,VD,D,1,Wn1,LS1,LR1) :-
	lit_N_V(VD,D,Wn1,LS1,LR1).
     rpl_match_new_literal(once,VD,D,_,Wn1,LS1,LR1) :-
        lit_ST_G(VD,D,Wn1,LS1,LR1).
     rpl_match_new_literal(once,VD,D,_,Wn1,LS1,LR1) :-
	\+ ground_substitution,
        !, lit_ST_V(VD,D,Wn1,LS1,LR1).
     rpl_match_new_literal(once,VD,D,1,Wn1,LS1,LR1) :-
        lit_ST_V(VD,D,Wn1,LS1,LR1).

%%% If an element is an individual constant, delete it.
%%% If an element is a variable, keep it.
%%% Otherwise, reject it.
     check_electron_vars(VL2,VL2) :-
	var(VL2), !.
     check_electron_vars([X|Xs],VL2) :-
	atomic(X),
	!, check_electron_vars(Xs,VL2).
     check_electron_vars([X|Xs],[X|VL2]) :-
	var(X),
	!, check_electron_vars(Xs,VL2).
     check_electron_vars(_,_) :-
	!, fail.

%%% Match one distinguished literal against lit_N or lit_ST.
     rpl_match_dg_A(0,L1,DC1,T1,DS1,DR1,Clist,VL1,DS2,DR2,VL2) :-
        rpl_match_N_ST(T1,L1,DC1,Wn1,LS1,LR1),
	check_electron_vars(Wn1,Wn2),
	expand_VL(Wn2,VL1,VL2),
        onelink_SR(L1,DS1,DR1,LS1,LR1,DS2,DR2), !.
     rpl_match_dg_A(1,L1,DC1,T1,DS1,DR1,Clist,VL1,DS2,DR2,VL2) :-
        rpl_match_N_ST(T1,L1,DC1,Wn1,LS1,LR1),
	check_electron_vars(Wn1,Wn2),
	check_electron_vars(VL1,VLM),
	not(not(VLM = Clist)),
	expand_VL(Wn2,VLM,VL2),
        onelink_SR(L1,DS1,DR1,LS1,LR1,DS2,DR2).
 
%%% If no ground_substitution, then take all.
%%% If ground_substitution and context literal, take all.
%%% Otherwise, stop.
     rpl_match_N_ST(T1,L1,DC1,Wn1,LS1,LR1) :-
	rpl_match_N_ST_1(T1,L1,DC1,Wn1,LS1,LR1).
     rpl_match_N_ST(T1,L1,DC1,Wn1,LS1,LR1) :-
	rpl_match_N_ST_2(T1,L1,DC1,Wn1,LS1,LR1).

     rpl_match_N_ST_1(T1,L1,_,Wn1,LS1,LR1) :-
        lit_ST_G(T1,L1,Wn1,LS1,LR1).
     rpl_match_N_ST_1(T1,L1,_,Wn1,LS1,LR1) :-
	\+ ground_substitution,
	!, lit_ST_V(T1,L1,Wn1,LS1,LR1).
     rpl_match_N_ST_1(T1,L1,1,Wn1,LS1,LR1) :-
	lit_ST_V(T1,L1,Wn1,LS1,LR1).

     rpl_match_N_ST_2(T1,L1,_,Wn1,LS1,LR1) :-
        lit_N_G(T1,L1,Wn1,LS1,LR1).
     rpl_match_N_ST_2(T1,L1,_,Wn1,LS1,LR1) :-
	\+ ground_substitution,
        !, lit_N_V(T1,L1,Wn1,LS1,LR1).
     rpl_match_N_ST_2(T1,L1,1,Wn1,LS1,LR1) :-
        lit_N_V(T1,L1,Wn1,LS1,LR1).
 
%%% Match the rest distinguished literals against lit_ST and lit_N.
     rpl_match_dgs_R([L|Ls],DCs,Ws,Ts,DS1,DR1,Clist,VL1,DS2,DR2) :-
	rpl_lit_reorder_4(Ws,[L|Ls],DCs,Ts,W1,Ws1,L1,Ls1,DC1,DCs1,T1,Ts1),
        !, rpl_match_dg_A(0,L1,DC1,T1,DS1,DR1,Clist,VL1,DSM,DRM,VLM),
        !, rpl_match_dgs_R(Ls1,DCs1,Ws1,Ts1,DSM,DRM,Clist,VLM,DS2,DR2).
     rpl_match_dgs_R([L1|Ls1],[DC1|DCs1],[_|Ws1],[T1|Ts1],
		DS1,DR1,Clist,VL1,DS2,DR2) :-
        rpl_match_dg_A(1,L1,DC1,T1,DS1,DR1,Clist,VL1,DSM,DRM,VLM),
	w1_w2(Ws1,Ws2),
        rpl_match_dgs_R(Ls1,DCs1,Ws2,Ts1,DSM,DRM,Clist,VLM,DS2,DR2).
     rpl_match_dgs_R([],[],[],[],DS2,DR2,_,_,DS2,DR2).
	
%%% Do unit simplification on undistinguished literals.
     rpl_inst_rule_0(Flags,Contexts,Rule,W1,DS2,DR2,NDg,VRule,VNDg) :-
	negate_clause(NDg,NegNDg),
        rpl_unitsimp(NegNDg,VNDg,RNDg),
	union_lists(VRule,Contexts,Dlist),
        literals_remain_3(Dlist,Rule,W1,Flags,CnM,WM,FM,_),
        rpl_inst_rule_1(CnM,WM,FM,DS2,DR2,RNDg), !.

%%% If the instance is a tautology, removes it.
%%% Turn off tautology checking.
%    rpl_inst_rule_1(C1,_,_,_,_,_) :-
%       fol_tautology_clause(C1), !.
     rpl_inst_rule_1(C1,W1,F1,DS1,DR1,RNDg) :-
        delete_replicate_literals_3(C1,W1,F1,C2,W2,F2),
	vars_W1_V1(W2,V2),
        !,
        check_numbervars(V2,'Number of variables overflows in instances !'),
	!, check_ground_restriction(V2),
        calculate_S(C2,RNDg,DS1,DS2),
        calculate_priority_clause(C2,DS2,DR1,CP2),
        rpl_processC(C2,V2,W2,F2,CP2,DS2,DR1), 
	check_empty_hl(C2), !.
 
     check_ground_restriction(V1) :-
        ground_restriction,
        !,
        var(V1).
     check_ground_restriction(_).
       
%%% Unit simplification.
     rpl_unitsimp([L1|Ls1],[0|Ls2],[L1|Ls3]) :-
        \+ unit_instance(L1), !,
        rpl_unitsimp(Ls1,Ls2,Ls3).
     rpl_unitsimp([L1|Ls1],[1|Ls2],Ls3) :-
        !,
        rpl_unitsimp(Ls1,Ls2,Ls3).
     rpl_unitsimp([],[],[]).
       
%%% Calculate support information.
%%% Notice that RNDg is negated.
     calculate_S(C1,_,sp(S11,_,_),sp(S11,1,0)) :-
        negclause(C1), !.
     calculate_S(C1,_,sp(S11,_,_),sp(S11,0,1)) :-
        posclause(C1), !.
     calculate_S(_,RNDg,sp(S11,S12,_),sp(S11,S12,0)) :-
        posclause(RNDg), !.
     calculate_S(_,RNDg,sp(S11,_,S13),sp(S11,0,S13)) :-
        negclause(RNDg), !.
     calculate_S(_,_,sp(S11,_,_),sp(S11,0,0)).
         
 
%%% If no more instances were generated, done.
%%% Otherwise, do more iterations.
     rpl_more(once,_) :- !.
     rpl_more(Type,_) :-
	\+ new_literal_N, !.
     rpl_more(Type,Clist) :-
        repeat,
		rpl_more_1(Type,Clist).

     rpl_more_1(_,_) :-
	check_hl_stop, !.
     rpl_more_1(Type,Clist) :-
        not(not(rpl_instances(Type,Clist))),
        not(not(litN_to_litST)),
        not(not(rpl_lits(1,Clist))),
	physically_erase(sent_C),
	not(not(update_sentC_1(Clist))),
        sentINST_to_sentC_a,
	!,
	\+ new_literal_N.
 
     new_literal_N :-
        lit_N_G(_,_,_,_,_), !.
     new_literal_N :-
        lit_N_V(_,_,_,_,_), !.

%%% Move lit_N to lit_ST.
     litN_to_litST :-
	litN_to_litST_G,
	litN_to_litST_V, !.

     litN_to_litST_G :-
        retract(lit_N_G(A1,A2,A3,A4,A5)),
        assertz(lit_ST_G(A1,A2,A3,A4,A5)),
        fail.
     litN_to_litST_G.
       
     litN_to_litST_V :-
        retract(lit_N_V(A1,A2,A3,A4,A5)),
        assertz(lit_ST_V(A1,A2,A3,A4,A5)),
        fail.
     litN_to_litST_V.
       
%%% Process the generated instance of the rule.
%%%     As in hyper-linking, deletions may be done
%%%     due to work-unit bound or priority bound.
%%%
     rpl_processC(Cn2,V2,W2,F2,CP2,CS1,CR1) :-
        slidepriority, 
        !, rpl_processC_2(Cn2,V2,W2,F2,CP2,CS1,CR1), !.
     rpl_processC(Cn2,V2,W2,F2,CP2,CS1,CR1) :-
        rpl_processC_1(Cn2,V2,W2,F2,CP2,CS1,CR1), !.
 
     rpl_processC_1(Cn2,V1,W1,F2,CP2,CS1,CR1) :-
        clause_size(Cn2,CSize2),
        rpl_proc_npr(CSize2,CP2,F2,Cn2,V1,W1,CS1,CR1).
 
%%% Consider priority.
     rpl_processC_2(Cn2,V1,W1,F2,CP2,CS1,CR1) :-
        priority_bound(PrioBound),
        !,
        check_prioritybound(CP2,PrioBound),
        clause_size(Cn2,CSize2),
        rpl_proc_pr(CSize2,CP2,F2,Cn2,V1,W1,CS1,CR1).
 
%%% Find literals from clauses.
     rpl_lits(Type,Clist) :-
        rpl_sent(Type,Cn1,W1,CS1,CR1,Unit),
        rpl_lits_clause(Cn1,W1,CS1,CR1,Unit,Clist),
        fail.
     rpl_lits(_,_).
       
%%% In first iteration, we take all literals from sent_C.
%%% We don't count literals with 1.
     rpl_sent(0,Cn1,W1,CS1,CR1,Unit) :-
        clause(sent_C(cl(_,_,by(CnM,V11,V11,_,WM),_,CS1,CR1,_,F1,_)),true,
		Cref),
	not(logically_erased(sent_C,Cref)),
        decide_unit(CnM,Unit),
        literals_remain_2(F1,CnM,WM,Cn1,W1,_).
%%% Otherwise, we take all literals from sent_INST.
%%% We don't count literals with 1.
     rpl_sent(1,Cn1,W1,CS1,CR1,Unit) :-
        sent_INST(cl(_,_,by(CnM,V11,V11,_,WM),_,CS1,CR1,_,F1,_)),
        decide_unit(CnM,Unit),
        literals_remain_2(F1,CnM,WM,Cn1,W1,_).
     rpl_sent(1,Cn1,W1,CS1,CR1,Unit) :-
        sent_T(cl(_,_,by(CnM,V11,V11,_,WM),_,CS1,CR1,_,F1,_)),
        decide_unit(CnM,Unit),
        literals_remain_2(F1,CnM,WM,Cn1,W1,_).
 
%%% Check for duplicates.
%%% Assert the literals.
     rpl_lits_clause([Ln1|Lns1],[Wn1|Wns1],CS1,CR1,LU1,Clist) :-
        \+ rpl_lit_copy(LU1,Ln1,Wn1,CS1,CR1,Clist),
	assert_lit_N(LU1,Ln1,Wn1,CS1,CR1),
        !,
        rpl_lits_clause(Lns1,Wns1,CS1,CR1,LU1,Clist).
     rpl_lits_clause([_|Lns1],[_|Wns1],CS1,CR1,LU1,Clist) :-
        !,
        rpl_lits_clause(Lns1,Wns1,CS1,CR1,LU1,Clist).
     rpl_lits_clause([],[],_,_,_,_).
       
     assert_lit_N(LU1,Ln1,Wn1,CS1,CR1) :-
	var(Wn1),
        !, assertz(lit_N_G(LU1,Ln1,Wn1,CS1,CR1)), !.
     assert_lit_N(LU1,Ln1,Wn1,CS1,CR1) :-
        assertz(lit_N_V(LU1,Ln1,Wn1,CS1,CR1)), !.

%%% Check duplicates against lit_N first.
%%% Check duplicates against lit_ST if necessary.
     rpl_lit_copy(LU1,Ln1,Wn1,CS1,CR1,Clist) :-
	var(Wn1),
	!, rpl_lit_copy_G(LU1,Ln1,CS1,CR1).
     rpl_lit_copy(LU1,Ln1,Clist,CS1,CR1,Clist) :-
	rpl_lit_copy_V(LU1,Ln1,CS1,CR1,Clist).

     rpl_lit_copy_G(LU1,Ln1,CS1,CR1) :-
	lit_N_G(LU2,Ln1,_,CS2,CR2),
	binary_max_ind(LU2,LU1,LU3,Up),
	max_CS_ind(CS2,CS1,CS3,Up),
	min_CR_ind(CR2,CR1,CR3,Up),
	rpl_lit_copy_G_1(Up,0,LU3,CS3,CR3,Ln1), !.
     rpl_lit_copy_G(LU1,Ln1,CS1,CR1) :-
	lit_ST_G(LU2,Ln1,_,CS2,CR2),
	binary_max_ind(LU2,LU1,LU3,Up),
	max_CS_ind(CS2,CS1,CS3,Up),
	min_CR_ind(CR2,CR1,CR3,Up),
	rpl_lit_copy_G_1(Up,1,LU3,CS3,CR3,Ln1), !.

     rpl_lit_copy_V(LU1,Ln1,CS1,CR1,Clist) :-
        lit_N_V(LU2,Ln1,Clist,CS2,CR2),
        binary_max_ind(LU2,LU1,LU3,Up),
        max_CS_ind(CS2,CS1,CS3,Up),
        min_CR_ind(CR2,CR1,CR3,Up),
        rpl_lit_copy_V_1(Up,0,LU3,CS3,CR3,Ln1,Clist), !.
     rpl_lit_copy_V(LU1,Ln1,CS1,CR1,Clist) :-
        lit_ST_V(LU2,Ln1,Clist,CS2,CR2),
        binary_max_ind(LU2,LU1,LU3,Up),
        max_CS_ind(CS2,CS1,CS3,Up),
        min_CR_ind(CR2,CR1,CR3,Up),
        rpl_lit_copy_V_1(Up,1,LU3,CS3,CR3,Ln1,Clist), !.
 
     rpl_lit_copy_G_1(n,_,_,_,_,_) :- !.
     rpl_lit_copy_G_1(_,0,LU3,CS3,CR3,Ln1) :-
	retract(lit_N_G(_,Ln1,Wn1,_,_)),
	assertz(lit_N_G(LU3,Ln1,Wn1,CS3,CR3)).
     rpl_lit_copy_G_1(_,1,LU3,CS3,CR3,Ln1) :-
	retract(lit_ST_G(_,Ln1,Wn1,_,_)),
	assertz(lit_ST_G(LU3,Ln1,Wn1,CS3,CR3)).

%%% Update database for lit_N or lit_ST.
     rpl_lit_copy_V_1(n,_,_,_,_,_,_) :- !.
     rpl_lit_copy_V_1(_,0,LU3,CS3,CR3,Ln1,Clist) :-
        clause(lit_N_V(_,Ln1,Clist,_,_),true,Ref2),
        clause(lit_N_V(_,Ln2,Wn2,_,_),true,Ref2),
        erase(Ref2),
        assertz(lit_N_V(LU3,Ln2,Wn2,CS3,CR3)).
     rpl_lit_copy_V_1(_,1,LU3,CS3,CR3,Ln1,Clist) :-
        clause(lit_ST_V(_,Ln1,Clist,_,_),true,Ref2),
        clause(lit_ST_V(_,Ln2,Wn2,_,_),true,Ref2),
        erase(Ref2),
        assertz(lit_ST_V(LU3,Ln2,Wn2,CS3,CR3)).
 
%%% Check for unit simplification.
     unit_instance(L1) :-
        numbervars(L1,0,_), !,
        unit_instance_1(L1).
 
     unit_instance_1(L1) :-
        clause(sent_C(cl(_,_,by([L1],V11,V11,_,_),_,_,_,_,_,_)),true,
		Cref),
	not(logically_erased(sent_C,Cref)).
     unit_instance_1(L1) :-
        sent_INST(cl(_,_,by([L1],V11,V11,_,_),_,_,_,_,_,_)).
 
%%% Check if the instance is a duplicate. Assert it if it is not.
     rpl_proc_npr(CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1) :-
        rpl_update_INST(CSize1,CP1,F1,Cn1,V1,CS1,CR1), !.
     rpl_proc_npr(CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1) :-
        proc_C(0,_,Cn1,V1,W1,CN1,Cn2,V21,V22,V2,W2),
        print_INST(Cn1,V1,CS1,CR1,F1),
        asserta(sent_INST(cl(CSize1,CN1,by(Cn2,V21,V22,V2,W2),
                0,CS1,CR1,1,F1,CP1))), !.
 
     rpl_proc_pr(CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1) :-
        rpl_update_INST(CSize1,CP1,F1,Cn1,V1,CS1,CR1), !.
     rpl_proc_pr(CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1) :-
        prio_parameters(TotalHm,ExpectWU,TotalWU), !,
        totalhl_test1(rpl,_,0,CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1,
                TotalHm,ExpectWU,TotalWU), !.
 
%%% Check for duplicates.
     rpl_update_INST(CSize1,CP1,F1,Cn1,V1,CS1,CR1) :-
        const_list(V1),
        rpl_update_INST(CSize1,CP1,F1,Cn1,CS1,CR1).
 
%%% Check for duplicates.
%%% Against sent_INST, then sent_C.
     rpl_update_INST(CSize1,CP1,F1,Cn1,CS1,CR1) :-
        update_INST_1(CSize1,CP1,F1,Cn1,CS1,CR1).
     rpl_update_INST(CSize1,CP1,F1,Cn1,CS1,CR1) :-
	update_INST_2(CSize1,CP1,F1,Cn1,CS1,CR1).
     rpl_update_INST(CSize1,CP1,F1,Cn1,CS1,CR1) :-
        rpl_update_INST_2(CSize1,CP1,F1,Cn1,CS1,CR1).
 
%%% Against sent_C.
     rpl_update_INST_2(CSize1,CP1,F1,Cn1,CS1,CR1) :-
        clause(sent_C(cl(CSize1,CN1,by(Cn1,V21,V21,V2,_),_,_,_,_,_,_)),true,
		Cref),
	not(logically_erased(sent_C,Cref)),
        const_list(V2),
        rpl_update_INST_21(CSize1,CN1,Cn1,CS1,CR1,F1,CP1).
 
     rpl_update_INST_21(CSize1,CN1,Cn1,CS1,CR1,F1,CP1) :-
        clause(sent_C(cl(_,_,by(Cn1,V21,V21,V2,_),_,_,_,_,_,_)),true,Ref2),
	not(logically_erased(sent_C,Ref2)),
        const_list(V2),
        clause(sent_C(cl(_,_,BY_2,_,_,_,_,_,_)),true,Ref2),
        asserta(sent_T(cl(CSize1,CN1,BY_2,0,CS1,CR1,1,F1,CP1))).
        
%%% print replace rules and instances.
     print_rpl_rule(C,V,F,X) :-
        outinst,
        write_line(5,'Current Replace Rule is :'),
        print_clause_2(10,C,V),
	tab(15), write(F), write(', '), write(X), nl,
        write_line(5,'Instances are :'), !.
     print_rpl_rule(_,_,_,_) :- !.
       
%%% Separate replace rule.
     rpl_sep_clause([0|Flags],[R|Rule],[_|DC],[_|Ws],Dg,[R|NDg],DCs,Dw,
                [X|VRule],VDg,[X|VNDg]) :-
        rpl_sep_clause(Flags,Rule,DC,Ws,Dg,NDg,DCs,Dw,VRule,VDg,VNDg).
     rpl_sep_clause([1|Flags],[R|Rule],[DC|DCs],[W|Ws],[R|Dg],NDg,
		[DC|DCs1],[W|Dw],[X|VRule],[X|VDg],VNDg) :-
        rpl_sep_clause(Flags,Rule,DCs,Ws,Dg,NDg,DCs1,Dw,VRule,VDg,VNDg).
     rpl_sep_clause([],[],[],[],[],[],[],[],[],[],[]).

%%% Expand variable list.
     expand_VL(Wn1,VL1,VL1) :-
	var(Wn1), !.
     expand_VL([W|Wn1],VL1,VL2) :-
	not_identical_in(W,VL1), !,
	expand_VL(Wn1,[W|VL1],VL2).
     expand_VL([W|Wn1],VL1,VL2) :-
	expand_VL(Wn1,VL1,VL2).

     not_identical_in(W,VL1) :-
	var(VL1), !.
     not_identical_in(W,[V|VL1]) :-
	W == V, !, fail.
     not_identical_in(W,[_|VL1]) :-
	!,
	not_identical_in(W,VL1).

     rpl_lit_reorder_4(Ws,Ls,DCs,Ts,W1,Ws1,L1,Ls1,DC,DCs1,T1,Ts1) :-
	replace_literal_reordering,
	!, sep_gr_lit_4(Ws,Ls,DCs,Ts,W1,Ws1,L1,Ls1,DC,DCs1,T1,Ts1).