https://github.com/theoremprover-museum/CLIN
Tip revision: e7082fbde3634286f458d64846699ae488fe18f3 authored by Michael Kohlhase on 22 December 2016, 09:28:55 UTC
initial commit, thanks to David Plaisted
initial commit, thanks to David Plaisted
Tip revision: e7082fb
replace.old
%%% 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))),
write(''),
not(not(update_sentC_1(Clist))),
sentINST_to_sentC_a,
write(''),
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))),
write(''),
not(not(update_sentC_1(Clist))),
sentINST_to_sentC_a,
write(''),
!,
\+ 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) :-
sent_C(cl(_,_,by(CnM,V11,V11,_,WM),_,CS1,CR1,_,F1,_)),
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) :-
sent_C(cl(_,_,by([L1],V11,V11,_,_),_,_,_,_,_,_)).
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) :-
sent_C(cl(CSize1,CN1,by(Cn1,V21,V21,V2,_),_,_,_,_,_,_)),
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),
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).