blob: c4bee6be2854e9f56684f47df017eba049f2a3e6 [file] [log] [blame]
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * REDUCTION RULES * */
/* * * */
/* * $Module: REDRULES * */
/* * * */
/* * Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001 * */
/* * MPI fuer Informatik * */
/* * * */
/* * This program 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 2 of the License, * */
/* * or (at your option) any later version. * */
/* * * */
/* * This program 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. * */
/* * * */
/* * You should have received a copy of the GNU General * */
/* * Public License along with this program; if not, write * */
/* * to the Free Software Foundation, Inc., 59 Temple * */
/* * Place, Suite 330, Boston, MA 02111-1307 USA * */
/* * * */
/* * * */
/* $Revision$ * */
/* $State$ * */
/* $Date$ * */
/* $Author$ * */
/* * * */
/* * Contact: * */
/* * Christoph Weidenbach * */
/* * MPI fuer Informatik * */
/* * Stuhlsatzenhausweg 85 * */
/* * 66123 Saarbruecken * */
/* * Email: weidenb@mpi-sb.mpg.de * */
/* * Germany * */
/* * * */
/* ********************************************************** */
/**************************************************************/
/* $RCSfile$ */
#include "rules-red.h"
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * Globals * */
/* * * */
/* ********************************************************** */
/**************************************************************/
/* Needed for term stamping in red_RewriteRedUnitClause */
static NAT red_STAMPID;
const NAT red_USABLE = 1;
const NAT red_WORKEDOFF = 2;
const NAT red_ALL = 3;
/**************************************************************/
/* FUNTION PROTOTYPES */
/**************************************************************/
static BOOL red_SortSimplification(SORTTHEORY, CLAUSE, NAT, BOOL, FLAGSTORE,
PRECEDENCE, CLAUSE*);
static BOOL red_SelectedStaticReductions(PROOFSEARCH, CLAUSE*, CLAUSE*, LIST*,
NAT);
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * Functions * */
/* * * */
/* ********************************************************** */
/**************************************************************/
static void red_HandleRedundantIndexedClauses(PROOFSEARCH Search, LIST Blocked,
CLAUSE RedClause)
/*********************************************************
INPUT: A proof search object, a list <Blocked> of clauses from
the proof search object and a clause that causes the
already indexed clauses in <Blocked> to be redundant.
RETURNS: Nothing.
**********************************************************/
{
FLAGSTORE Flags;
CLAUSE Clause;
LIST Scan;
Flags = prfs_Store(Search);
for (Scan = Blocked; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
Clause = (CLAUSE)list_Car(Scan);
if (prfs_SplitLevelCondition(clause_SplitLevel(RedClause),clause_SplitLevel(Clause),
prfs_LastBacktrackLevel(Search)))
split_DeleteClauseAtLevel(Search, Clause, clause_SplitLevel(RedClause));
else {
if (clause_GetFlag(Clause, WORKEDOFF)) {
if (flag_GetFlagValue(Flags, flag_DOCPROOF))
prfs_MoveWorkedOffDocProof(Search, Clause);
else
prfs_DeleteWorkedOff(Search, Clause);
}
else
if (flag_GetFlagValue(Flags, flag_DOCPROOF))
prfs_MoveUsableDocProof(Search, Clause);
else
prfs_DeleteUsable(Search, Clause);
}
}
}
static void red_HandleRedundantDerivedClauses(PROOFSEARCH Search, LIST Blocked,
CLAUSE RedClause)
/*********************************************************
INPUT: A proof search object, a list <Blocked> of clauses from
the proof search object and a clause that causes the
derived clauses in <Blocked> to be redundant.
RETURNS: Nothing.
**********************************************************/
{
CLAUSE Clause;
LIST Scan;
for (Scan = Blocked; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
Clause = (CLAUSE)list_Car(Scan);
if (prfs_SplitLevelCondition(clause_SplitLevel(RedClause),clause_SplitLevel(Clause),
prfs_LastBacktrackLevel(Search))) {
split_KeepClauseAtLevel(Search, Clause, clause_SplitLevel(RedClause));
}
else {
if (flag_GetFlagValue(prfs_Store(Search), flag_DOCPROOF))
prfs_InsertDocProofClause(Search, Clause);
else
clause_Delete(Clause);
}
}
}
void red_Init(void)
/*********************************************************
INPUT: None.
RETURNS: Nothing.
EFFECT: Initializes the Reduction module, in particular
its stampid to stamp terms.
**********************************************************/
{
red_STAMPID = term_GetStampID();
}
static void red_DocumentObviousReductions(CLAUSE Clause, LIST Indexes)
/*********************************************************
INPUT: A clause and a list of literal indexes removed by
obvious reductions.
RETURNS: None
MEMORY: The <Indexes> list is consumed.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nil());
clause_SetParentLiterals(Clause, Indexes);
clause_AddParentClause(Clause,clause_Number(Clause)); /* Has to be done before increasing it! */
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromObviousReductions(Clause);
}
static BOOL red_ObviousReductions(CLAUSE Clause, BOOL Document,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed)
/**********************************************************
INPUT: A clause, a boolean flag for proof
documentation, a flag store and a precedence.
RETURNS: TRUE iff obvious reductions are possible.
If <Document> is false the clause is
destructively changed,
else a reduced copy of the clause is returned
in <*Changed>.
EFFECT: Multiple occurrences of the same literal as
well as trivial equations are removed.
********************************************************/
{
int i, j, end;
LIST Indexes;
TERM Atom, PartnerAtom;
#ifdef CHECK
clause_Check(Clause, Flags, Precedence);
#endif
Indexes = list_Nil();
end = clause_LastAntecedentLitIndex(Clause);
for (i = clause_FirstConstraintLitIndex(Clause); i <= end; i++) {
Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i));
if (fol_IsEquality(Atom) &&
!clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause, i)) &&
term_Equal(term_FirstArgument(Atom),term_SecondArgument(Atom))) {
Indexes = list_Cons((POINTER)i,Indexes);
}
else
for (j = i+1; j <= end; j++) {
PartnerAtom = clause_LiteralAtom(clause_GetLiteral(Clause,j));
if (term_Equal(PartnerAtom, Atom) ||
(fol_IsEquality(Atom) &&
fol_IsEquality(PartnerAtom) &&
term_Equal(term_FirstArgument(Atom),term_SecondArgument(PartnerAtom)) &&
term_Equal(term_FirstArgument(PartnerAtom),term_SecondArgument(Atom)))) {
Indexes = list_Cons((POINTER)i,Indexes);
j = end;
}
}
}
end = clause_LastSuccedentLitIndex(Clause);
for (i = clause_FirstSuccedentLitIndex(Clause); i <= end; i++) {
Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i));
for (j = i+1; j <= end; j++) {
PartnerAtom = clause_LiteralAtom(clause_GetLiteral(Clause,j));
if (term_Equal(PartnerAtom,Atom) ||
(fol_IsEquality(Atom) &&
fol_IsEquality(PartnerAtom) &&
term_Equal(term_FirstArgument(Atom),term_SecondArgument(PartnerAtom)) &&
term_Equal(term_FirstArgument(PartnerAtom),term_SecondArgument(Atom)))) {
Indexes = list_Cons((POINTER)i,Indexes);
j = end;
}
}
}
if (clause_Length(Clause) == 1 &&
clause_NumOfAnteLits(Clause) == 1 &&
!list_PointerMember(Indexes,(POINTER)clause_FirstAntecedentLitIndex(Clause)) &&
fol_IsEquality(clause_GetLiteralAtom(Clause,clause_FirstAntecedentLitIndex(Clause)))) {
cont_StartBinding();
if (unify_UnifyCom(cont_LeftContext(),
term_FirstArgument(clause_LiteralAtom(clause_GetLiteral(Clause,clause_FirstAntecedentLitIndex(Clause)))),
term_SecondArgument(clause_LiteralAtom(clause_GetLiteral(Clause,clause_FirstAntecedentLitIndex(Clause))))))
Indexes = list_Cons((POINTER)clause_FirstAntecedentLitIndex(Clause),Indexes);
cont_BackTrack();
}
if (!list_Empty(Indexes)) {
if (flag_GetFlagValue(Flags, flag_POBV)) {
fputs("\nObvious: ", stdout);
clause_Print(Clause);
fputs(" ==> ", stdout);
}
if (Document) {
CLAUSE Copy;
Copy = clause_Copy(Clause);
clause_DeleteLiterals(Copy,Indexes, Flags, Precedence);
red_DocumentObviousReductions(Copy,Indexes); /* Indexes is consumed */
if (flag_GetFlagValue(Flags, flag_POBV))
clause_Print(Copy);
*Changed = Copy;
}
else {
clause_DeleteLiterals(Clause,Indexes, Flags, Precedence);
list_Delete(Indexes);
if (flag_GetFlagValue(Flags, flag_POBV))
clause_Print(Clause);
}
return TRUE;
}
return FALSE;
}
static void red_DocumentCondensing(CLAUSE Clause, LIST Indexes)
/*********************************************************
INPUT: A clause and a list of literal indexes removed by condensing.
RETURNS: Nothing.
MEMORY: The <Indexes> list is consumed.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nil());
clause_SetParentLiterals(Clause, Indexes);
clause_AddParentClause(Clause,clause_Number(Clause)); /* Has to be done before increasing it! */
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromCondensing(Clause);
}
static BOOL red_Condensing(CLAUSE Clause, BOOL Document, FLAGSTORE Flags,
PRECEDENCE Precedence, CLAUSE *Changed)
/**********************************************************
INPUT: A non-empty unshared clause, a boolean flag
concerning proof documentation, a flag store and
a precedence.
RETURNS: TRUE iff condensing is applicable to <Clause>.
If <Document> is false the clause is
destructively changed else a condensed copy of
the clause is returned in <*Changed>.
***********************************************************/
{
LIST Indexes;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence) ||
(*Changed != (CLAUSE)NULL)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_Condensing : ");
misc_ErrorReport("Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
Indexes = cond_CondFast(Clause);
if (!list_Empty(Indexes)) {
if (flag_GetFlagValue(Flags, flag_PCON)) {
fputs("\nCondensing: ", stdout);
clause_Print(Clause);
fputs(" ==> ", stdout);
}
if (Document) {
CLAUSE Copy;
Copy = clause_Copy(Clause);
clause_DeleteLiterals(Copy, Indexes, Flags, Precedence);
red_DocumentCondensing(Copy, Indexes);
if (flag_GetFlagValue(Flags, flag_PCON))
clause_Print(Copy);
*Changed = Copy;
}
else {
clause_DeleteLiterals(Clause, Indexes, Flags, Precedence);
list_Delete(Indexes);
if (flag_GetFlagValue(Flags, flag_PCON))
clause_Print(Clause);
}
return TRUE;
}
return FALSE;
}
static void red_DocumentAssignmentEquationDeletion(CLAUSE Clause, LIST Indexes,
NAT NonTrivClauseNumber)
/*********************************************************
INPUT: A clause and a list of literal indexes pointing to
redundant equations and the clause number of a clause
implying a non-trivial domain.
RETURNS: Nothing.
MEMORY: The <Indexes> list is consumed.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nil());
clause_SetParentLiterals(Clause, Indexes);
clause_AddParentClause(Clause,clause_Number(Clause)); /* Has to be done before increasing it! */
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromAssignmentEquationDeletion(Clause);
if (NonTrivClauseNumber != 0) { /* Such a clause exists */
clause_AddParentClause(Clause, NonTrivClauseNumber);
clause_AddParentLiteral(Clause, 0); /* The non triv clause has exactly one negative literal */
}
}
static BOOL red_AssignmentEquationDeletion(CLAUSE Clause, FLAGSTORE Flags,
PRECEDENCE Precedence, CLAUSE *Changed,
NAT NonTrivClauseNumber,
BOOL NonTrivDomain)
/**********************************************************
INPUT: A non-empty unshared clause, a flag store, a
precedence, the clause number of a clause
implying a non-trivial domain and a boolean
flag indicating whether the current domain has
more than one element.
RETURNS: TRUE iff equations are removed.
If the <DocProof> flag is false the clause is
destructively changed else a copy of the clause
where redundant equations are removed is
returned in <*Changed>.
***********************************************************/
{
LIST Indexes; /* List of indexes of redundant equations*/
NAT i;
TERM LeftArg, RightArg;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence) ||
(*Changed != (CLAUSE)NULL) ||
(NonTrivDomain && NonTrivClauseNumber == 0) ||
(!NonTrivDomain && NonTrivClauseNumber > 0)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_AssignmentEquationDeletion: ");
misc_ErrorReport("Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
Indexes = list_Nil();
if (clause_ContainsNegativeEquations(Clause)) {
for (i = clause_FirstAntecedentLitIndex(Clause); i <= clause_LastAntecedentLitIndex(Clause); i++) {
if (clause_LiteralIsEquality(clause_GetLiteral(Clause,i))) {
LeftArg = term_FirstArgument(clause_GetLiteralAtom(Clause,i));
RightArg = term_SecondArgument(clause_GetLiteralAtom(Clause,i));
if ((term_IsVariable(LeftArg) &&
clause_NumberOfSymbolOccurrences(Clause, term_TopSymbol(LeftArg)) == 1) ||
(term_IsVariable(RightArg) &&
clause_NumberOfSymbolOccurrences(Clause, term_TopSymbol(RightArg)) == 1))
Indexes = list_Cons((POINTER)i, Indexes);
}
}
}
else
if (NonTrivDomain && clause_ContainsPositiveEquations(Clause)) {
for (i = clause_FirstSuccedentLitIndex(Clause); i <= clause_LastSuccedentLitIndex(Clause); i++) {
if (clause_LiteralIsEquality(clause_GetLiteral(Clause,i))) {
LeftArg = term_FirstArgument(clause_GetLiteralAtom(Clause,i));
RightArg = term_SecondArgument(clause_GetLiteralAtom(Clause,i));
if ((term_IsVariable(LeftArg) &&
clause_NumberOfSymbolOccurrences(Clause, term_TopSymbol(LeftArg)) == 1) ||
(term_IsVariable(RightArg) &&
clause_NumberOfSymbolOccurrences(Clause, term_TopSymbol(RightArg)) == 1))
Indexes = list_Cons((POINTER)i, Indexes);
}
}
}
if (!list_Empty(Indexes)) {
if (flag_GetFlagValue(Flags, flag_PAED)) {
fputs("\nAED: ", stdout);
clause_Print(Clause);
fputs(" ==> ", stdout);
}
if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
CLAUSE Copy;
Copy = clause_Copy(Clause);
clause_DeleteLiterals(Copy, Indexes, Flags, Precedence);
red_DocumentAssignmentEquationDeletion(Copy, Indexes, NonTrivClauseNumber);
if (flag_GetFlagValue(Flags, flag_PAED))
clause_Print(Copy);
*Changed = Copy;
}
else {
clause_DeleteLiterals(Clause, Indexes, Flags, Precedence);
list_Delete(Indexes);
if (flag_GetFlagValue(Flags, flag_PAED))
clause_Print(Clause);
}
return TRUE;
}
return FALSE;
}
static BOOL red_Tautology(CLAUSE Clause, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**********************************************************
INPUT: A non-empty clause, a flag store and a
precedence.
RETURNS: The boolean value TRUE if 'Clause' is a
tautology.
***********************************************************/
{
TERM Atom;
int i,j, la,n;
BOOL Result;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_Tautology :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
la = clause_LastAntecedentLitIndex(Clause);
n = clause_Length(Clause);
Result = FALSE;
for (j = clause_FirstSuccedentLitIndex(Clause); j < n && !Result; j++) {
Atom = clause_LiteralAtom(clause_GetLiteral(Clause, j));
if (fol_IsEquality(Atom) &&
!clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause, j)) &&
term_Equal(term_FirstArgument(Atom),term_SecondArgument(Atom)))
Result = TRUE;
for (i = clause_FirstLitIndex(); i <= la && !Result; i++)
if (term_Equal(Atom, clause_LiteralAtom(clause_GetLiteral(Clause, i))))
Result = TRUE;
}
if (!Result &&
flag_GetFlagValue(Flags, flag_RTAUT) == flag_RTAUTSEMANTIC &&
clause_NumOfAnteLits(Clause) != 0 &&
clause_NumOfSuccLits(Clause) != 0) {
Result = cc_Tautology(Clause);
}
if (Result && flag_GetFlagValue(Flags, flag_PTAUT)) {
fputs("\nTautology: ", stdout);
clause_Print(Clause);
}
return Result;
}
static LITERAL red_GetMRResLit(LITERAL ActLit, SHARED_INDEX ShIndex)
/**************************************************************
INPUT: A literal and an Index.
RETURNS: The most valid clause with a complementary literal,
(CLAUSE)NULL, if no such clause exists.
***************************************************************/
{
LITERAL NextLit;
int i;
CLAUSE ActClause;
TERM CandTerm;
LIST LitScan;
NextLit = (LITERAL)NULL;
ActClause = clause_LiteralOwningClause(ActLit);
i = clause_LiteralGetIndex(ActLit);
CandTerm = st_ExistGen(cont_LeftContext(),
sharing_Index(ShIndex),
clause_LiteralAtom(ActLit));
while (CandTerm) { /* First check units */
if (!term_IsVariable(CandTerm)) { /* Has to be an Atom! */
LitScan = sharing_NAtomDataList(CandTerm); /* CAUTION !!! the List is not a copy */
while (!list_Empty(LitScan)) {
NextLit = list_Car(LitScan);
if (clause_LiteralsAreComplementary(ActLit,NextLit))
if (clause_Length(clause_LiteralOwningClause(NextLit)) == 1 ||
subs_SubsumesBasic(clause_LiteralOwningClause(NextLit),ActClause,
clause_LiteralGetIndex(NextLit),i)) {
st_CancelExistRetrieval();
return NextLit;
}
LitScan = list_Cdr(LitScan);
}
}
CandTerm = st_NextCandidate();
}
return (LITERAL)NULL;
}
static void red_DocumentMatchingReplacementResolution(CLAUSE Clause, LIST LitInds,
LIST ClauseNums, LIST PLitInds)
/*********************************************************
INPUT: A clause, the involved literals indices in <Clause>,
the literal indices of the reduction literals
and the clauses number.
RETURNS: Nothing.
MEMORY: All input lists are consumed.
**********************************************************/
{
LIST Scan,Help;
Help = list_Nil();
for (Scan=LitInds; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
Help = list_Cons((POINTER)clause_Number(Clause), Help);
/* Has to be done before increasing the clause number! */
}
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nconc(Help,ClauseNums));
clause_SetParentLiterals(Clause, list_Nconc(LitInds,PLitInds));
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromMatchingReplacementResolution(Clause);
}
static BOOL red_MatchingReplacementResolution(CLAUSE Clause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed, int Level)
/**************************************************************
INPUT: A clause, an Index, a flag store, a precedence and a
split level indicating the need of a copy if
<Clause> is reduced by a clause of higher split
level than <Level>.
RETURNS: TRUE if reduction wrt the indexed clauses was
possible.
If the <DocProof> flag is true or the clauses used
for reductions have a higher split level then a
changed copy is returned in <*Changed>.
Otherwise <Clause> is destructively changed.
***************************************************************/
{
CLAUSE PClause,Copy;
LITERAL ActLit,PLit;
int i, j, length;
LIST ReducedBy,ReducedLits,PLits,Scan1,Scan2;
BOOL Document;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence) ||
(*Changed != (CLAUSE)NULL)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_MatchingReplacementResolution:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
Copy = Clause;
length = clause_Length(Clause);
ReducedBy = list_Nil();
ReducedLits = list_Nil();
PLits = list_Nil();
i = clause_FirstLitIndex();
j = 0;
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
while (i < length) {
ActLit = clause_GetLiteral(Copy, i);
if (!fol_IsEquality(clause_LiteralAtom(ActLit)) || /* Reduce with negative equations. */
clause_LiteralIsPositive(ActLit)) {
PLit = red_GetMRResLit(ActLit, ShIndex);
if (clause_LiteralExists(PLit)) {
if (list_Empty(PLits) && flag_GetFlagValue(Flags, flag_PMRR)) {
fputs("\nFMatchingReplacementResolution: ", stdout);
clause_Print(Copy);
}
PClause = clause_LiteralOwningClause(PLit);
ReducedBy = list_Cons((POINTER)clause_Number(PClause), ReducedBy);
PLits = list_Cons((POINTER)clause_LiteralGetIndex(PLit),PLits);
ReducedLits = list_Cons((POINTER)(i+j), ReducedLits);
if (Copy == Clause &&
(Document || prfs_SplitLevelCondition(clause_SplitLevel(PClause),clause_SplitLevel(Copy),Level)))
Copy = clause_Copy(Clause);
clause_UpdateSplitDataFromPartner(Copy, PClause);
clause_DeleteLiteral(Copy,i, Flags, Precedence);
length--;
j++;
}
else
i++;
}
else
i++;
}
if (!list_Empty(ReducedBy)) {
if (Document) {
ReducedBy = list_NReverse(ReducedBy);
ReducedLits = list_NReverse(ReducedLits);
PLits = list_NReverse(PLits);
red_DocumentMatchingReplacementResolution(Copy, ReducedLits, ReducedBy, PLits); /* Lists are consumed */
if (flag_GetFlagValue(Flags, flag_PMRR)) {
fputs(" ==> [ ", stdout);
for(Scan1=ReducedBy,Scan2=ReducedLits;!list_Empty(Scan1);
Scan1=list_Cdr(Scan1),Scan2=list_Cdr(Scan2))
printf("%d.%d ",(NAT)list_Car(Scan1),(NAT)list_Car(Scan2));
fputs("] ", stdout);
clause_Print(Copy);
}
}
else {
if (flag_GetFlagValue(Flags, flag_PMRR)) {
fputs(" ==> [ ", stdout);
for(Scan1=ReducedBy,Scan2=ReducedLits;!list_Empty(Scan1);
Scan1=list_Cdr(Scan1),Scan2=list_Cdr(Scan2))
printf("%d.%d ",(NAT)list_Car(Scan1),(NAT)list_Car(Scan2));
fputs("] ", stdout);
clause_Print(Copy);
}
list_Delete(ReducedBy);
list_Delete(ReducedLits);
list_Delete(PLits);
}
if (Copy != Clause)
*Changed = Copy;
return TRUE;
}
return FALSE;
}
static void red_DocumentUnitConflict(CLAUSE Clause, LIST LitInds,
LIST ClauseNums, LIST PLitInds)
/*********************************************************
INPUT: A clause, the involved literals indices and the clauses number.
RETURNS: Nothing.
MEMORY: All input lists are consumed.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nconc(list_List((POINTER)clause_Number(Clause)),ClauseNums));
clause_SetParentLiterals(Clause, list_Nconc(LitInds,PLitInds));
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromUnitConflict(Clause);
}
static BOOL red_UnitConflict(CLAUSE Clause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed, int Level)
/**************************************************************
INPUT: A clause, an Index, a flag store and a splitlevel
indicating the need of a copy if <Clause> is reduced
by a clause of higher split level than <Level>.
RETURNS: TRUE if a unit conflict with <Clause> and the
clauses in <ShIndex> happened.
If the <DocProof> flag is true or the clauses used for
reductions have a higher split level then a changed
copy is returned in <*Changed>.
Otherwise <Clause> is destructively changed.
***************************************************************/
{
CLAUSE PClause,Copy;
LITERAL ActLit,PLit;
LIST Scan;
TERM CandTerm;
BOOL Document;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence) || (*Changed != (CLAUSE)NULL)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ForwardUnitConflict :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
if (clause_Length(Clause) == 1) {
Copy = Clause;
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
ActLit = clause_GetLiteral(Copy, clause_FirstLitIndex());
PLit = (LITERAL)NULL;
CandTerm = st_ExistUnifier(cont_LeftContext(), sharing_Index(ShIndex), cont_RightContext(),
clause_LiteralAtom(ActLit));
while (PLit == (LITERAL)NULL && CandTerm) {
if (!term_IsVariable(CandTerm)) {
Scan = sharing_NAtomDataList(CandTerm); /* CAUTION !!! the List is not a copy */
while (!list_Empty(Scan)) {
PLit = list_Car(Scan);
if (clause_LiteralsAreComplementary(ActLit,PLit) &&
clause_Length(clause_LiteralOwningClause(PLit)) == 1) {
st_CancelExistRetrieval();
Scan = list_Nil();
}
else {
PLit = (LITERAL)NULL;
Scan = list_Cdr(Scan);
}
}
}
if (PLit == (LITERAL)NULL)
CandTerm = st_NextCandidate();
}
if (PLit == (LITERAL)NULL && fol_IsEquality(clause_LiteralAtom(ActLit))) {
TERM Atom;
Atom = term_Create(fol_Equality(),list_Reverse(term_ArgumentList(clause_LiteralAtom(ActLit))));
CandTerm = st_ExistUnifier(cont_LeftContext(), sharing_Index(ShIndex), cont_RightContext(), Atom);
while (PLit == (LITERAL)NULL && CandTerm) {
if (!term_IsVariable(CandTerm)) {
Scan = sharing_NAtomDataList(CandTerm); /* CAUTION !!! the List is not a copy */
while (!list_Empty(Scan)) {
PLit = list_Car(Scan);
if (clause_LiteralsAreComplementary(ActLit,PLit) &&
clause_Length(clause_LiteralOwningClause(PLit)) == 1) {
st_CancelExistRetrieval();
Scan = list_Nil();
}
else {
PLit = (LITERAL)NULL;
Scan = list_Cdr(Scan);
}
}
}
if (PLit == (LITERAL)NULL)
CandTerm = st_NextCandidate();
}
list_Delete(term_ArgumentList(Atom));
term_Free(Atom);
}
if (clause_LiteralExists(PLit)) {
if (flag_GetFlagValue(Flags, flag_PUNC)) {
fputs("\nUnitConflict: ", stdout);
clause_Print(Copy);
}
PClause = clause_LiteralOwningClause(PLit);
if (Copy == Clause &&
(Document || prfs_SplitLevelCondition(clause_SplitLevel(PClause),clause_SplitLevel(Copy),Level)))
Copy = clause_Copy(Clause);
clause_UpdateSplitDataFromPartner(Copy, PClause);
clause_DeleteLiteral(Copy,clause_FirstLitIndex(), Flags, Precedence);
if (Document)
red_DocumentUnitConflict(Copy, list_List((POINTER)clause_FirstLitIndex()),
list_List((POINTER)clause_Number(PClause)),
list_List((POINTER)clause_FirstLitIndex()));
if (flag_GetFlagValue(Flags, flag_PUNC)) {
printf(" ==> [ %d.%d ]", clause_Number(PClause), clause_FirstLitIndex());
clause_Print(Copy);
}
if (Copy != Clause)
*Changed = Copy;
return TRUE;
}
}
return FALSE;
}
static CLAUSE red_ForwardSubsumer(CLAUSE RedCl, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**********************************************************
INPUT: A pointer to a non-empty clause, an index of
clauses, a flag store and a precedence.
RETURNS: A clause that subsumes <RedCl>, or NULL if no such
clause exists.
***********************************************************/
{
TERM Atom,AtomGen;
CLAUSE CandCl;
LITERAL CandLit;
LIST LitScan;
int i, lc, fa, la, fs, ls;
#ifdef CHECK
if (!clause_IsClause(RedCl, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ForwardSubsumer:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedCl, Flags, Precedence);
#endif
lc = clause_LastConstraintLitIndex(RedCl);
fa = clause_FirstAntecedentLitIndex(RedCl);
la = clause_LastAntecedentLitIndex(RedCl);
fs = clause_FirstSuccedentLitIndex(RedCl);
ls = clause_LastSuccedentLitIndex(RedCl);
for (i = 0; i <= ls; i++) {
Atom = clause_GetLiteralAtom(RedCl, i);
AtomGen = st_ExistGen(cont_LeftContext(), sharing_Index(ShIndex), Atom);
while (AtomGen) {
if (!term_IsVariable(AtomGen)) {
for (LitScan = sharing_NAtomDataList(AtomGen);
!list_Empty(LitScan);
LitScan = list_Cdr(LitScan)) {
CandLit = list_Car(LitScan);
CandCl = clause_LiteralOwningClause(CandLit);
if (CandCl != RedCl &&
clause_GetLiteral(CandCl,clause_FirstLitIndex()) == CandLit &&
/* Literals must be from same part of the clause */
((i<=lc && clause_LiteralIsFromConstraint(CandLit)) ||
(i>=fa && i<=la && clause_LiteralIsFromAntecedent(CandLit)) ||
(i>=fs && clause_LiteralIsFromSuccedent(CandLit))) &&
subs_SubsumesBasic(CandCl, RedCl, clause_FirstLitIndex(), i)) {
st_CancelExistRetrieval();
return (CandCl);
}
}
}
AtomGen = st_NextCandidate();
}
if (fol_IsEquality(Atom) &&
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(RedCl,i))) {
Atom = term_Create(fol_Equality(),list_Reverse(term_ArgumentList(Atom)));
AtomGen = st_ExistGen(cont_LeftContext(), sharing_Index(ShIndex), Atom);
while (AtomGen) {
if (!term_IsVariable(AtomGen)) {
for (LitScan = sharing_NAtomDataList(AtomGen);
!list_Empty(LitScan);
LitScan = list_Cdr(LitScan)) {
CandLit = list_Car(LitScan);
CandCl = clause_LiteralOwningClause(CandLit);
if (CandCl != RedCl &&
clause_GetLiteral(CandCl,clause_FirstLitIndex()) == CandLit &&
/* Literals must be from same part of the clause */
((i<=lc && clause_LiteralIsFromConstraint(CandLit)) ||
(i>=fa && i<=la && clause_LiteralIsFromAntecedent(CandLit)) ||
(i>=fs && clause_LiteralIsFromSuccedent(CandLit))) &&
subs_SubsumesBasic(CandCl, RedCl, clause_FirstLitIndex(), i)) {
st_CancelExistRetrieval();
list_Delete(term_ArgumentList(Atom));
term_Free(Atom);
return (CandCl);
}
}
}
AtomGen = st_NextCandidate();
}
list_Delete(term_ArgumentList(Atom));
term_Free(Atom);
}
}
return((CLAUSE)NULL);
}
static CLAUSE red_ForwardSubsumption(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**********************************************************
INPUT: A clause, an index of clauses, a flag store and
a precedence.
RETURNS: The clause <RedClause> is subsumed by in <ShIndex>.
***********************************************************/
{
CLAUSE Subsumer;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ForwardSubsumption:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Subsumer = red_ForwardSubsumer(RedClause, ShIndex, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PSUB) && Subsumer) {
fputs("\nFSubsumption: ", stdout);
clause_Print(RedClause);
printf(" by %d %d ",clause_Number(Subsumer),clause_SplitLevel(Subsumer));
}
return Subsumer;
}
static void red_DocumentRewriting(CLAUSE Clause, int i, CLAUSE Rule, int ri)
/*********************************************************
INPUT: Two clauses and the literal indices involved in the rewrite step.
RETURNS: Nothing.
EFFECT: Documentation in <Clause> is set.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause,
list_List((POINTER)clause_Number(Clause)));
/* Has to be done before increasing the number! */
clause_SetParentLiterals(Clause, list_List((POINTER)i));
clause_NewNumber(Clause);
clause_SetFromRewriting(Clause);
clause_AddParentClause(Clause,clause_Number(Rule));
clause_AddParentLiteral(Clause,ri);
}
static void red_DocumentFurtherRewriting(CLAUSE Clause, int i, CLAUSE Rule, int ri)
/*********************************************************
INPUT: Two clauses and the literal indices involved in the rewrite step.
RETURNS: Nothing.
EFFECT: Documentation in <Clause> is set.
**********************************************************/
{
clause_AddParentClause(Clause,
(int) list_Car(list_Cdr(clause_ParentClauses(Clause))));
clause_AddParentLiteral(Clause, i);
clause_AddParentClause(Clause, clause_Number(Rule));
clause_AddParentLiteral(Clause, ri);
}
static BOOL red_RewriteRedUnitClause(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed, int Level)
/**************************************************************
INPUT: A unit (!) clause, an Index, a flag store, a
precedence and a split level indicating the need of
a copy if <Clause> is reduced by a clause of higher
split level than <Level>.
RETURNS: TRUE iff rewriting was possible.
If the <DocProof> flag is true or the split level of
the rewrite rule is higher a copy of RedClause that
is rewritten wrt. the indexed clauses is returned in
<*Changed>.
Otherwise the clause is destructively rewritten.
***************************************************************/
{
TERM RedAtom, RedTermS;
int B_Stack;
BOOL Rewritten, Result, Oriented, Renamed, Document;
TERM TermS,PartnerEq;
LIST EqList,EqScan,LitScan;
CLAUSE Copy;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence) ||
*Changed != (CLAUSE)NULL ||
clause_Length(RedClause) != 1) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_RewriteRedUnitClause :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Result = FALSE;
Renamed = FALSE;
Copy = RedClause;
RedAtom = clause_GetLiteralAtom(Copy, clause_FirstLitIndex());
Rewritten = TRUE;
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
/* Don't apply this rule on constraint or propositional literals */
if (clause_FirstLitIndex() <= clause_LastConstraintLitIndex(RedClause) ||
list_Empty(term_ArgumentList(RedAtom)))
return Result;
if (term_StampOverflow(red_STAMPID))
term_ResetTermStamp(clause_LiteralSignedAtom(clause_GetLiteral(RedClause, clause_FirstLitIndex())));
term_StartStamp();
while (Rewritten) {
Rewritten = FALSE;
B_Stack = stack_Bottom();
sharing_PushListOnStackNoStamps(term_ArgumentList(RedAtom));
while (!stack_Empty(B_Stack)) {
RedTermS = (TERM)stack_PopResult();
TermS = st_ExistGen(cont_LeftContext(), sharing_Index(ShIndex), RedTermS);
while (TermS && !Rewritten) {
EqList = term_SupertermList(TermS);
for (EqScan = EqList; !list_Empty(EqScan) && !Rewritten;
EqScan = list_Cdr(EqScan)) {
PartnerEq = list_Car(EqScan);
if (fol_IsEquality(PartnerEq)) {
CLAUSE RewriteClause;
LITERAL RewriteLit;
TERM Right;
if (TermS == term_FirstArgument(PartnerEq))
Right = term_SecondArgument(PartnerEq);
else
Right = term_FirstArgument(PartnerEq);
for (LitScan = sharing_NAtomDataList(PartnerEq);
!list_Empty(LitScan) && !Rewritten;
LitScan = list_Cdr(LitScan)) {
RewriteLit = list_Car(LitScan);
RewriteClause = clause_LiteralOwningClause(RewriteLit);
if (clause_LiteralIsPositive(RewriteLit) &&
clause_Length(RewriteClause) == 1) {
Oriented = (clause_LiteralIsOrientedEquality(RewriteLit) &&
TermS == term_FirstArgument(PartnerEq));
if (!Oriented && !clause_LiteralIsOrientedEquality(RewriteLit)) {
Renamed = TRUE; /* If oriented, no renaming needed! */
term_StartMaxRenaming(clause_MaxVar(RewriteClause));
term_Rename(RedAtom); /* Renaming destructive, no extra match needed !! */
Oriented = ord_ContGreater(cont_LeftContext(), TermS,
cont_LeftContext(), Right,
Flags, Precedence);
/*if (Oriented) {
fputs("\n\n\tRedAtom: ",stdout);term_PrintPrefix(RedAtom);
fputs("\n\tSubTerm: ",stdout);term_PrintPrefix(RedTermS);
fputs("\n\tGenTerm: ",stdout);term_PrintPrefix(TermS);
fputs("\n\tGenRight: ",stdout);term_PrintPrefix(Right);
putchar('\n');cont_PrintCurrentTrail();putchar('\n');
}*/
}
if (Oriented) {
TERM TermT;
if (RedClause == Copy &&
(Document ||
prfs_SplitLevelCondition(clause_SplitLevel(RewriteClause),
clause_SplitLevel(RedClause),Level))) {
Copy = clause_Copy(RedClause);
RedAtom = clause_GetLiteralAtom(Copy, clause_FirstLitIndex());
}
if (!Result)
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("\nFRewriting: ", stdout);
clause_Print(Copy);
fputs(" ==>[ ", stdout);
}
if (Document) {
if (!Result)
red_DocumentRewriting(Copy, clause_FirstLitIndex(),
RewriteClause, clause_FirstLitIndex());
else
red_DocumentFurtherRewriting(Copy, clause_FirstLitIndex(),
RewriteClause, clause_FirstLitIndex());
}
Result = TRUE;
TermT = cont_ApplyBindingsModuloMatching(cont_LeftContext(), term_Copy(Right), TRUE);
if (cont_BindingsAreRenamingModuloMatching(cont_RightContext()))
term_SetTermSubtermStamp(TermT);
term_ReplaceSubtermBy(RedAtom, RedTermS, TermT);
Rewritten = TRUE;
clause_UpdateSplitDataFromPartner(Copy, RewriteClause);
term_Delete(TermT);
stack_SetBottom(B_Stack);
if (flag_GetFlagValue(Flags, flag_PREW))
printf("%d.%d ",clause_Number(RewriteClause), clause_FirstLitIndex());
clause_UpdateWeight(Copy, Flags);
}
}
}
}
}
if (!Rewritten)
TermS = st_NextCandidate();
}
st_CancelExistRetrieval();
if (!Rewritten)
term_SetTermStamp(RedTermS);
}
}
term_StopStamp();
if (Result) {
clause_OrientAndReInit(Copy, Flags, Precedence);
if (Copy != RedClause)
clause_OrientAndReInit(RedClause, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("] ", stdout);
clause_Print(Copy);
}
if (Copy != RedClause)
*Changed = Copy;
}
else
if (Renamed)
clause_OrientAndReInit(Copy, Flags, Precedence);
#ifdef CHECK
clause_Check(Copy, Flags, Precedence);
clause_Check(RedClause, Flags, Precedence);
#endif
return Result;
}
static BOOL red_RewriteRedClause(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed, int Level)
/**************************************************************
INPUT: A clause, an Index, a flag store, a precedence and
a split level indicating the need of a copy if
<Clause> is reduced by a clause of higher split
level than <Level>.
RETURNS: NULL, if no rewriting was possible.
If the <DocProof> flag is true or the split level of
the rewrite rule is higher a copy of RedClause
that is rewritten wrt. the indexed clauses.
Otherwise the clause is destructively rewritten and
returned.
***************************************************************/
{
TERM RedAtom, RedTermS;
int B_Stack;
int ci, length;
BOOL Rewritten, Result, Document;
TERM TermS,PartnerEq;
LIST EqScan,LitScan;
CLAUSE Copy;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_RewriteRedClause :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
length = clause_Length(RedClause);
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
if (length == 1)
return red_RewriteRedUnitClause(RedClause, ShIndex, Flags, Precedence,
Changed, Level);
Result = FALSE;
Copy = RedClause;
/* Don't apply this rule on constraint literals! */
for (ci = clause_FirstAntecedentLitIndex(RedClause); ci < length; ci++) {
Rewritten = TRUE;
if (!list_Empty(term_ArgumentList(clause_GetLiteralAtom(Copy, ci)))) {
while (Rewritten) {
Rewritten = FALSE;
RedAtom = clause_GetLiteralAtom(Copy, ci);
B_Stack = stack_Bottom();
/* push subterms on stack except variables */
sharing_PushListReverseOnStack(term_ArgumentList(RedAtom));
while (!stack_Empty(B_Stack)) {
RedTermS = (TERM)stack_PopResult();
TermS = st_ExistGen(cont_LeftContext(), sharing_Index(ShIndex), RedTermS);
while (TermS && !Rewritten) {
/* A variable can't be greater than any other term, */
/* so don't consider any variables here */
if (!term_IsVariable(TermS)) {
EqScan = term_SupertermList(TermS);
for ( ; !list_Empty(EqScan) && !Rewritten;
EqScan = list_Cdr(EqScan)) {
PartnerEq = list_Car(EqScan);
if (fol_IsEquality(PartnerEq) &&
(term_FirstArgument(PartnerEq) == TermS)) {
CLAUSE RewriteClause;
LITERAL RewriteLit;
int ri;
for (LitScan = sharing_NAtomDataList(PartnerEq);
!list_Empty(LitScan) && !Rewritten;
LitScan = list_Cdr(LitScan)) {
RewriteLit = list_Car(LitScan);
RewriteClause = clause_LiteralOwningClause(RewriteLit);
ri = clause_LiteralGetIndex(RewriteLit);
if (clause_LiteralIsPositive(RewriteLit) &&
clause_LiteralIsOrientedEquality(RewriteLit) &&
subs_SubsumesBasic(RewriteClause, Copy, ri, ci)) {
TERM TermT;
if (RedClause == Copy &&
(Document ||
prfs_SplitLevelCondition(clause_SplitLevel(RewriteClause),
clause_SplitLevel(RedClause),Level))) {
Copy = clause_Copy(RedClause);
RedAtom = clause_GetLiteralAtom(Copy, ci);
}
if (!Result) {
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("\nFRewriting: ", stdout);
clause_Print(Copy);
fputs(" ==>[ ", stdout);
}
}
if (Document) {
if (!Result)
red_DocumentRewriting(Copy, ci, RewriteClause, ri);
else
red_DocumentFurtherRewriting(Copy,ci,RewriteClause,ri);
}
Result = TRUE;
/* Since <TermS> is the bigger term of an oriented */
/* equation and all variables in <TermS> are bound, */
/* all variables in the smaller term are bound, too. */
/* So the strict version of cont_Apply... will work. */
TermT = cont_ApplyBindingsModuloMatching(cont_LeftContext(),
term_Copy(term_SecondArgument(PartnerEq)),
TRUE);
/* No variable renaming is necessary before creation */
/* of bindings and replacement of subterms because all */
/* variables of <TermT> are from <RedClause>/<Copy>. */
term_ReplaceSubtermBy(RedAtom, RedTermS, TermT);
Rewritten = TRUE;
clause_UpdateSplitDataFromPartner(Copy,RewriteClause);
term_Delete(TermT);
stack_SetBottom(B_Stack);
if (flag_GetFlagValue(Flags, flag_PREW))
printf("%d.%d ",clause_Number(RewriteClause), ri);
clause_UpdateWeight(Copy, Flags);
}
}
}
}
}
if (!Rewritten)
TermS = st_NextCandidate();
}
st_CancelExistRetrieval();
}
}
}
}
if (Result) {
clause_OrientAndReInit(Copy, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("] ", stdout);
clause_Print(Copy);
}
if (Copy != RedClause) {
clause_OrientAndReInit(RedClause, Flags, Precedence);
*Changed = Copy;
}
}
#ifdef CHECK
clause_Check(Copy, Flags, Precedence);
clause_Check(RedClause, Flags, Precedence);
#endif
return Result;
}
/**************************************************************/
/* FORWARD CONTEXTUAL REWRITING */
/**************************************************************/
static BOOL red_LeftTermOfEquationIsStrictlyMaximalTerm(CLAUSE Clause,
LITERAL Equation,
FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a literal of the clause, that is an
oriented equation, a flag store and a precedence.
RETURNS: TRUE, iff the bigger (i.e. left) term of the equation
is the strictly maximal term of the clause.
A term s is strictly maximal in a clause, iff for every atom
u=v (A=tt) of the clause s > u and s > v (s > A).
***************************************************************/
{
int i, except, last;
TERM LeftTerm, Atom;
LITERAL ActLit;
#ifdef CHECK
if (!clause_LiteralIsOrientedEquality(Equation)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_LeftTermOfEquationIsStrictlyMaximalTerm: ");
misc_ErrorReport("literal is not oriented");
misc_FinishErrorReport();
}
#endif
LeftTerm = term_FirstArgument(clause_LiteralSignedAtom(Equation));
except = clause_LiteralGetIndex(Equation);
/* Compare <LeftTerm> with all terms in the clause */
last = clause_LastLitIndex(Clause);
for (i = clause_FirstLitIndex() ; i <= last; i++) {
if (i != except) {
ActLit = clause_GetLiteral(Clause, i);
Atom = clause_LiteralAtom(ActLit);
if (fol_IsEquality(Atom)) {
/* Atom is an equation */
if (ord_Compare(LeftTerm, term_FirstArgument(Atom), Flags, Precedence)
!= ord_GREATER_THAN ||
(!clause_LiteralIsOrientedEquality(ActLit) &&
ord_Compare(LeftTerm, term_SecondArgument(Atom), Flags, Precedence)
!= ord_GREATER_THAN))
/* Compare only with left (i.e. greater) subterm if the atom is */
/* an oriented equation. */
return FALSE;
} else {
/* Atom is not an equation */
if (ord_Compare(LeftTerm, Atom, Flags, Precedence) != ord_GREATER_THAN)
return FALSE;
}
}
}
return TRUE;
}
static void red_CRwCalculateAdditionalParents(CLAUSE Reduced,
LIST RedundantClauses,
CLAUSE Subsumer,
int OriginalClauseNumber)
/**************************************************************
INPUT: A clause that was just reduced by forward reduction,
a list of intermediate clauses that were derived from
the original clause, a clause that subsumes <Reduced>
(NULL, if <Reduced> is not subsumed), and the clause
number of <Reduced> before it was reduced.
RETURNS: Nothing.
EFFECT: This function collects the information about parent
clauses and parent literals that is necessary for
proof documentation for Contextual Rewriting
and sets the parent information of <Reduced> accordingly.
The clause <Reduced> was derived in several steps
C1 -> C2 -> ... Cn -> <Reduced> from some clause C1.
<RedundantClauses> contains all those clauses C1, ..., Cn.
This function first collects the parent information from
the clauses C1, C2, ..., Cn, <Reduced>. All those clauses
were needed to derive <Reduced>, but for proof documentation
of the rewriting step we have to delete the numbers of
all clauses C1,...,Cn,Reduced.
As a simplification this function doesn't set the
correct parent literals. It simply assumes that every
reduction step was done by literal 0.
This isn't a problem since only the correct parent
clause numbers are really needed for proof documentation.
***************************************************************/
{
LIST Parents, Scan;
int ActNum;
/* First collect all parent clause numbers from the redundant clauses. */
/* Also add number of <Subsumer> if it exists. */
Parents = clause_ParentClauses(Reduced);
clause_SetParentClauses(Reduced, list_Nil());
for (Scan = RedundantClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
Parents = list_Append(clause_ParentClauses(list_Car(Scan)), Parents);
if (Subsumer != NULL)
Parents = list_Cons((POINTER)clause_Number(Subsumer), Parents);
/* Now delete <OriginalClauseNumber> and the numbers of all clauses */
/* that were derived from it. */
Parents = list_PointerDeleteElement(Parents, (POINTER) OriginalClauseNumber);
for (Scan = RedundantClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
ActNum = clause_Number(list_Car(Scan));
Parents = list_PointerDeleteElement(Parents, (POINTER) ActNum);
}
/* Finally set data of result clause <Reduced>. */
Parents = list_PointerDeleteDuplicates(Parents);
clause_SetParentClauses(Reduced, Parents);
/* Build list of literal numbers: in this simple version we just build */
/* a list with the same length as the parent clauses containing only the */
/* literal indices 0. */
Parents = list_Copy(Parents);
for (Scan = Parents; !list_Empty(Scan); Scan = list_Cdr(Scan))
list_Rplaca(Scan, (POINTER)0);
list_Delete(clause_ParentLiterals(Reduced));
clause_SetParentLiterals(Reduced, Parents);
}
static BOOL red_LiteralIsDefinition(LITERAL Literal)
/**************************************************************
INPUT: A literal.
RETURNS: TRUE, iff the literal is a definition, i.e. an equation x=t,
where x is a variable and x doesn't occur in t.
The function needs time O(1), it is independent of the size
of the literal.
CAUTION: The orientation of the literal must be correct.
***************************************************************/
{
TERM Atom;
Atom = clause_LiteralAtom(Literal);
if (fol_IsEquality(Atom) &&
!clause_LiteralIsOrientedEquality(Literal) &&
(term_IsVariable(term_FirstArgument(Atom)) ||
term_IsVariable(term_SecondArgument(Atom))) &&
!term_VariableEqual(term_FirstArgument(Atom),
term_SecondArgument(Atom)))
return TRUE;
else
return FALSE;
}
static BOOL red_PropagateDefinitions(CLAUSE Clause, TERM LeadingTerm,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a term, a flag store and a precedence.
RETURNS: TRUE, iff any definitions in <Clause> where propagated,
false otherwise.
Here, a definitions means a negative literal x=t, where
x is a variable and x doesn't occur in t.
Definitions are only propagated if all terms in the
resulting clause would be smaller than <LeadingTerm>.
The flag store and the precedence are only needed for
term comparisons with respect to the reduction ordering.
CAUTION: <Clause> is changed destructively!
***************************************************************/
{
LITERAL Lit;
TERM Term, Atom;
SYMBOL Var;
int i, last, j, lj;
BOOL success, applied;
LIST litsToRemove;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_PropagateDefinitions: clause is corrupted.");
misc_FinishErrorReport();
}
#endif
applied = FALSE;
litsToRemove = list_Nil(); /* collect indices of redundant literals */
last = clause_LastAntecedentLitIndex(Clause);
for (i = clause_FirstAntecedentLitIndex(Clause); i <= last; i++) {
Lit = clause_GetLiteral(Clause, i);
if (red_LiteralIsDefinition(Lit)) {
/* <Lit> is an equation x=t where the variable x doesn't occur in t. */
Term = term_FirstArgument(clause_LiteralAtom(Lit));
if (term_IsVariable(Term)) {
Var = term_TopSymbol(Term);
Term = term_SecondArgument(clause_LiteralAtom(Lit));
} else {
Var = term_TopSymbol(term_SecondArgument(clause_LiteralAtom(Lit)));
}
/* Establish variable binding x -> t in context */
#ifdef CHECK
cont_SaveState();
#endif
cont_StartBinding();
cont_CreateBinding(cont_LeftContext(), Var, cont_InstanceContext(), Term);
/* Check that for each literal u=v (A=tt) the conditions */
/* u{x->t} < LeadingTerm and v{x->t} < LeadingTerm (A < LeadingTerm) */
/* hold. */
success = TRUE;
Lit = NULL;
lj = clause_LastLitIndex(Clause);
for (j = clause_FirstLitIndex(); j <= lj && success; j++) {
if (j != i) {
success = FALSE;
Lit = clause_GetLiteral(Clause, j);
Atom = clause_LiteralAtom(Lit);
if (fol_IsEquality(Atom)) {
/* Atom is an equation */
if (ord_ContGreater(cont_InstanceContext(), LeadingTerm,
cont_LeftContext(), term_FirstArgument(Atom),
Flags, Precedence) &&
(clause_LiteralIsOrientedEquality(Lit) ||
ord_ContGreater(cont_InstanceContext(), LeadingTerm,
cont_LeftContext(), term_SecondArgument(Atom),
Flags, Precedence)))
/* Compare only with left (i.e. greater) subterm if the atom is */
/* an oriented equation. */
success = TRUE;
} else {
/* Atom is not an equation */
if (ord_ContGreater(cont_InstanceContext(), LeadingTerm,
cont_LeftContext(), Atom, Flags, Precedence))
success = TRUE;
}
}
}
cont_BackTrack();
#ifdef CHECK
cont_CheckState();
#endif
if (success) {
/* Replace variable <Var> in <Clause> by <Term> */
clause_ReplaceVariable(Clause, Var, Term);
/* The clause literals aren't reoriented here. For the detection of */
/* definitions it suffices to know the non-oriented literals in the */
/* original clause. */
litsToRemove = list_Cons((POINTER)i, litsToRemove);
applied = TRUE;
}
}
}
if (applied) {
/* Now remove the definition literals. */
clause_DeleteLiterals(Clause, litsToRemove, Flags, Precedence);
list_Delete(litsToRemove);
/* Equations have to be reoriented. */
clause_OrientEqualities(Clause, Flags, Precedence);
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_PropagateDefinitions: clause is corrupted ");
misc_ErrorReport("after propagation of definitions");
misc_FinishErrorReport();
}
#endif
}
return applied;
}
static CLAUSE red_CRwLitTautologyCheck(PROOFSEARCH Search, CLAUSE RedClause,
int Except, CLAUSE RuleClause, int i,
TERM LeadingTerm, NAT Mode)
/**************************************************************
INPUT: A proof search object, two clauses, two literal indices
(one per clause), a mode defining the clause index used
for intermediate reductions.
RETURNS: NULL, if the tautology check for literal <i> in <RuleClause>
failed.
If the test succeeds an auxiliary clause is returned that
contains part of the splitting information for the current
rewriting step. If the 'DocProof' flag is set, the necessary
parent information is set, too.
MEMORY: Remember to delete the returned clause!
***************************************************************/
{
FLAGSTORE Flags;
PRECEDENCE Precedence;
CLAUSE aux, NewClause;
LITERAL Lit;
TERM Atom;
BOOL DocProof, Negative, Redundant;
LIST NegLits, PosLits, RedundantList;
int OrigNum;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
DocProof = flag_GetFlagValue(Flags, flag_DOCPROOF);
Lit = clause_GetLiteral(RuleClause, i);
Atom = clause_LiteralAtom(Lit);
Negative = clause_LiteralIsNegative(Lit);
#ifdef CRW_DEBUG
printf("\n ----------\n ");
if (Negative)
printf((i <= clause_LastConstraintLitIndex(RuleClause)) ? "Cons" : "Ante");
else
printf("Succ");
printf(" aux = ");
#endif
if (i <= clause_LastConstraintLitIndex(RuleClause)) {
/* Apply Sort Simplification for constraint literals only */
NegLits = list_List(term_Copy(Atom));
aux = clause_Create(NegLits, list_Nil(), list_Nil(), Flags, Precedence);
clause_SetTemporary(aux);
list_Delete(NegLits);
#ifdef CRW_DEBUG
clause_Print(aux);
#endif
NewClause = NULL;
OrigNum = clause_Number(aux);
if (red_SortSimplification(prfs_DynamicSortTheory(Search), aux, NAT_MAX,
DocProof, Flags, Precedence, &NewClause)) {
/* Sort Simplification was possible, so the unit clause was reduced */
/* to the empty clause. */
/* The splitting information is already set in <aux> or <NewClause>. */
if (DocProof)
/* If 'DocProof' is turned on, a copy was created and assigned */
/* to <NewClause>. */
red_CRwCalculateAdditionalParents(NewClause, list_Nil(), NULL, OrigNum);
if (NewClause != NULL) {
clause_Delete(aux);
return NewClause;
} else
return aux;
}
clause_Delete(aux);
#ifdef CRW_DEBUG
printf("\n Cons aux2 = ");
#endif
}
/* Collect literals for tautology test */
if (Negative) {
if (i <= clause_LastConstraintLitIndex(RuleClause))
NegLits = clause_CopyConstraint(RedClause);
else
NegLits = clause_CopyAntecedentExcept(RedClause, Except);
PosLits = list_List(term_Copy(Atom));
} else {
NegLits = list_List(term_Copy(Atom));
PosLits = clause_CopySuccedentExcept(RedClause, Except);
}
/* Create clause for tautology test */
aux = clause_Create(list_Nil(), NegLits, PosLits, Flags, Precedence);
clause_SetTemporary(aux);
list_Delete(NegLits);
list_Delete(PosLits);
#ifdef CRW_DEBUG
clause_Print(aux);
#endif
/* Apply special reduction. Propagate definitions x=t if for all literals */
/* u=v (A=tt) of the resulting clause the conditions holds: */
/* LeadingTerm > u{x->t} and LeadingTerm > v{x->t} (LeadingTerm > A{x->t}. */
if (red_PropagateDefinitions(aux, LeadingTerm, Flags, Precedence)) {
#ifdef CRW_DEBUG
printf("\n After propagation of definitions:\n aux = ");
clause_Print(aux);
#endif
}
/* Invoke forward reduction and tautology test */
NewClause = NULL;
RedundantList = list_Nil();
OrigNum = clause_Number(aux);
Redundant = red_SelectedStaticReductions(Search, &aux, &NewClause,
&RedundantList, Mode);
clause_SetTemporary(aux);
/* <aux> was possibly changed by some reductions, so mark it as */
/* temporary again. */
/* Invoke tautology test if <aux> isn't redundant. */
if (Redundant || (!clause_IsEmptyClause(aux) && cc_Tautology(aux))) {
if (NewClause != NULL)
/* <aux> is subsumed by <NewClause> */
clause_UpdateSplitDataFromPartner(aux, NewClause);
if (DocProof)
red_CRwCalculateAdditionalParents(aux, RedundantList, NewClause, OrigNum);
} else {
/* test failed */
clause_Delete(aux);
aux = NULL;
}
#ifdef CRW_DEBUG
if (aux != NULL) {
if (NewClause != NULL) {
printf("\n Subsumer = ");
clause_Print(NewClause);
}
if (!list_Empty(RedundantList)) {
printf("\n RedundantList: ");
clause_ListPrint(RedundantList);
}
printf("\n aux reduced = ");
clause_Print(aux);
}
printf("\n ----------");
#endif
/* Delete list of redundant clauses */
clause_DeleteClauseList(RedundantList);
return aux;
}
static BOOL red_CRwTautologyCheck(PROOFSEARCH Search, CLAUSE RedClause, int i,
TERM TermSInstance, CLAUSE RuleClause,
int j, NAT Mode, CLAUSE *Result)
/**************************************************************
INPUT: A proof search object, two clauses, two literal indices
(one per clause), <TermSInstance> is a subterm of
literal <i> in <RedClause>, a mode defining the clause
index used for intermediate reductions, and a pointer
to a clause used as return value.
RETURNS: FALSE, if the clauses failed some tautology test or
the literal <i> in <RedClause> is not greater than literal
<j> in <RedClause> with the substitution <sigma> applied.
In this case <Result> is set to NULL.
TRUE is returned if the clauses passed all tautology tests
and literal <i> in <RedClause> is greater than literal <j>
in <RuleClause> with the substitution <sigma> applied.
In some cases <Result> is set to some auxiliary clause.
This is done if some clauses from the index were used to
reduce the intermediate clauses before the tautology test.
The auxiliary clause is used to return the necessary splitting
information for the current rewriting step.
If the <DocProof> flag is true, the information about
parent clauses is set in <Result>, too.
MEMORY: Remember to delete the <Result> clause if it is not NULL.
***************************************************************/
{
FLAGSTORE Flags, BackupFlags;
PRECEDENCE Precedence;
CLAUSE RuleCopy, aux;
TERM TermS;
int last, h;
BOOL Rewrite;
#ifdef CHECK
if (!clause_LiteralIsOrientedEquality(clause_GetLiteral(RuleClause, j))) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_CRwTautologyCheck:");
misc_ErrorReport(" literal %d in <RuleClause> %d", j,
clause_Number(RuleClause));
misc_ErrorReport(" isn't an oriented equation");
misc_FinishErrorReport();
}
#endif
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
*Result = NULL;
/* copy <RuleClause> and rename variables in copy */
RuleCopy = clause_Copy(RuleClause);
clause_RenameVarsBiggerThan(RuleCopy, clause_MaxVar(RedClause));
TermS = term_FirstArgument(clause_GetLiteralAtom(RuleCopy, j));
/* Remove parent information of copied clause and mark it as temporary */
list_Delete(clause_ParentClauses(RuleCopy));
clause_SetParentClauses(RuleCopy, list_Nil());
list_Delete(clause_ParentLiterals(RuleCopy));
clause_SetParentLiterals(RuleCopy, list_Nil());
clause_SetTemporary(RuleCopy);
/* establish bindings */
cont_StartBinding();
if (!unify_MatchBindings(cont_LeftContext(), TermS, TermSInstance)) {
#ifdef CHECK
misc_StartErrorReport();
misc_ErrorReport("\n In red_CRwTautologyCheck: terms aren't matchable");
misc_FinishErrorReport();
#endif
}
/* Apply bindings to equation s=t, where s > t. Here the strict version */
/* of cont_Apply... can be applied, because all variables in s and t */
/* are bound. */
cont_ApplyBindingsModuloMatching(cont_LeftContext(),
clause_GetLiteralAtom(RuleCopy, j),
TRUE);
/* Check whether E > (s=t)sigma. It suffices to check only positive */
/* equations. All other cases imply the condition. */
if (i >= clause_FirstSuccedentLitIndex(RedClause) &&
clause_LiteralIsEquality(clause_GetLiteral(RedClause, i)) &&
ord_LiteralCompare(clause_GetLiteralTerm(RedClause, i),
clause_LiteralIsOrientedEquality(clause_GetLiteral(RedClause, i)),
clause_GetLiteralTerm(RuleCopy, j), TRUE,
FALSE, Flags, Precedence) != ord_GREATER_THAN) {
cont_BackTrack();
clause_Delete(RuleCopy);
return FALSE;
}
/* if (subs_SubsumesBasic(RuleClause, RedClause, j, i)) { Potential improvement, not completely
cont_BackTrack(); developed ....
return TRUE;
} else */
{
int OldClauseCounter;
/* Apply bindings to the rest of <RuleCopy> */
last = clause_LastLitIndex(RuleCopy);
for (h = clause_FirstLitIndex(); h <= last; h++) {
if (h != j)
cont_ApplyBindingsModuloMatching(cont_LeftContext(),
clause_GetLiteralAtom(RuleCopy, h),
FALSE);
}
/* Backtrack bindings before reduction rules are invoked */
cont_BackTrack();
/* Create new flag store and save current settings. Must be improved **** */
/* Then turn off flags for printing and contextual rewriting. */
/* IMPORTANT: the DocProof flag mustn't be changed! */
BackupFlags = flag_CreateStore();
flag_TransferAllFlags(Flags, BackupFlags);
#ifndef CRW_DEBUG
flag_ClearPrinting(Flags);
#else
{ /* HACK: turn on all printing flags for debugging */
FLAG_ID f;
for (f = (FLAG_ID) 0; f < flag_MAXFLAG; f++) {
if (flag_IsPrinting(f))
flag_SetFlagValue(Flags, f, flag_ON);
}
}
#endif
/* ATTENTION: to apply CRw recursively, uncomment the following */
/* line and comment out the following two lines! */
/* flag_SetFlagValue(Flags, flag_RFCRW, flag_RFCRWON); */
flag_SetFlagValue(Flags, flag_RBCRW, flag_RBCRWOFF);
flag_SetFlagValue(Flags, flag_RFCRW, flag_RFCRWOFF);
/* Examine all literals of <RuleCopy> except <j> */
Rewrite = TRUE;
last = clause_LastLitIndex(RuleCopy);
OldClauseCounter = clause_Counter();
for (h = clause_FirstLitIndex(); Rewrite && h <= last; h++) {
if (h != j) {
aux = red_CRwLitTautologyCheck(Search, RedClause, i, RuleCopy, h,
TermSInstance, Mode);
if (aux == NULL)
Rewrite = FALSE;
else {
/* Store splitting data of <aux> in RuleCopy */
clause_UpdateSplitDataFromPartner(RuleCopy, aux);
/* Collect additonal parent information, if <DocProof> is turned on */
if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
clause_SetParentClauses(RuleCopy,
list_Nconc(clause_ParentClauses(aux),
clause_ParentClauses(RuleCopy)));
clause_SetParentLiterals(RuleCopy,
list_Nconc(clause_ParentLiterals(aux),
clause_ParentLiterals(RuleCopy)));
clause_SetParentClauses(aux, list_Nil());
clause_SetParentLiterals(aux, list_Nil());
}
clause_Delete(aux);
}
}
}
/* restore clause counter */
clause_SetCounter(OldClauseCounter);
/* reset flag store of proof search object and free backup store */
flag_TransferAllFlags(BackupFlags, Flags);
flag_DeleteStore(BackupFlags);
}
if (Rewrite)
*Result = RuleCopy;
else
/* cleanup */
clause_Delete(RuleCopy);
return Rewrite;
}
static void red_DocumentContextualRewriting(CLAUSE Clause, int i,
CLAUSE RuleClause, int ri,
LIST AdditionalPClauses,
LIST AdditionalPLits)
/**************************************************************
INPUT: Two clauses and two literal indices (one per clause),
and two lists of additional parent clause numbers and
parent literals.
RETURNS: Nothing.
EFFECT: <Clause> is rewritten for the first time by
Contextual Rewriting. This function sets the parent
clause and parent literal information in <Clause>.
<Clause> gets a new clause number.
CAUTION: The lists are not copied!
***************************************************************/
{
#ifdef CHECK
if (list_Length(AdditionalPClauses) != list_Length(AdditionalPLits)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_DocumentContextualRewriting: lists of parent ");
misc_ErrorReport("clauses\n and literals have different length.");
misc_FinishErrorReport();
}
#endif
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, AdditionalPClauses);
clause_SetParentLiterals(Clause, AdditionalPLits);
/* Add the old number of <Clause> as parent clause, */
/* before it gets a new clause number. */
clause_AddParentClause(Clause, clause_Number(Clause));
clause_AddParentLiteral(Clause, i);
clause_AddParentClause(Clause, clause_Number(RuleClause));
clause_AddParentLiteral(Clause, ri);
clause_NewNumber(Clause);
clause_SetFromContextualRewriting(Clause);
}
static void red_DocumentFurtherCRw(CLAUSE Clause, int i, CLAUSE RuleClause,
int ri, LIST AdditionalPClauses,
LIST AdditionalPLits)
/**************************************************************
INPUT: Two clauses, two literal indices (one per clause),
and two lists of additional parent clause numbers and
parent literal indices.
RETURNS: Nothing.
EFFECT: <Clause> is a clause, that was rewritten before by
Contextual Rewriting. This function adds the parent
clause and parent literal information from one more
rewriting step to <Clause>. The information is added
to the front of the respective lists.
CAUTION: The lists are not copied!
***************************************************************/
{
int PClauseNum;
#ifdef CHECK
if (list_Length(AdditionalPClauses) != list_Length(AdditionalPLits)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_DocumentFurtherCRw: lists of parent ");
misc_ErrorReport("clauses\n and literals have different length.");
misc_FinishErrorReport();
}
#endif
PClauseNum = (int)list_Second(clause_ParentClauses(Clause));
clause_SetParentClauses(Clause, list_Nconc(AdditionalPClauses,
clause_ParentClauses(Clause)));
clause_SetParentLiterals(Clause, list_Nconc(AdditionalPLits,
clause_ParentLiterals(Clause)));
clause_AddParentClause(Clause, PClauseNum);
clause_AddParentLiteral(Clause, i);
clause_AddParentClause(Clause, clause_Number(RuleClause));
clause_AddParentLiteral(Clause, ri);
}
static BOOL red_ContextualRewriting(PROOFSEARCH Search, CLAUSE RedClause,
NAT Mode, int Level, CLAUSE *Changed)
/**************************************************************
INPUT: A proof search object, a clause to reduce, the
reduction mode which defines the clause set used for
reduction, a split level indicating the need of a copy
if <Clause> is reduced by a clause of higher split level
than <Level>, and a pointer to a clause used as return value.
RETURNS: TRUE, if contextual rewriting was possible, FALSE otherwise.
If rewriting was possible and the <DocProof> flag is true
or the split level of the rewrite rule is higher than
<Level>, a copy of <RedClause> that is rewritten wrt.
the indexed clauses is returned in <*Changed>.
Otherwise the clause is destructively rewritten and
returned.
CAUTION: If rewriting wasn't applied, the value of <*Changed>
isn't set explicitely in this function.
***************************************************************/
{
TERM RedAtom, RedTermS;
int B_Stack;
int ri, last;
BOOL Rewritten, Result, Document;
TERM TermS, PartnerEq;
LIST Gen, EqScan, LitScan;
CLAUSE Copy;
FLAGSTORE Flags;
PRECEDENCE Precedence;
SHARED_INDEX ShIndex;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ContextualRewriting: Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
/* Select clause index */
if (red_WorkedOffMode(Mode))
ShIndex = prfs_WorkedOffSharingIndex(Search);
else
ShIndex = prfs_UsableSharingIndex(Search);
last = clause_LastSuccedentLitIndex(RedClause);
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
Result = FALSE;
Copy = RedClause;
/* Don't apply this rule on constraint literals! */
for (ri = clause_FirstAntecedentLitIndex(RedClause); ri <= last; ri++) {
if (!list_Empty(term_ArgumentList(clause_GetLiteralAtom(Copy, ri)))) {
Rewritten = TRUE;
while (Rewritten) {
Rewritten = FALSE;
RedAtom = clause_GetLiteralAtom(Copy, ri);
B_Stack = stack_Bottom();
/* push subterms on stack except variables */
sharing_PushListReverseOnStack(term_ArgumentList(RedAtom));
while (!stack_Empty(B_Stack)) {
RedTermS = (TERM)stack_PopResult();
Gen = st_GetGen(cont_LeftContext(), sharing_Index(ShIndex), RedTermS);
for ( ; !list_Empty(Gen) && !Rewritten; Gen = list_Pop(Gen)) {
TermS = list_Car(Gen);
/* A variable can't be greater than any other term, */
/* so don't consider any variables here. */
if (!term_IsVariable(TermS)) {
EqScan = term_SupertermList(TermS);
for ( ; !list_Empty(EqScan) && !Rewritten;
EqScan = list_Cdr(EqScan)) {
PartnerEq = list_Car(EqScan);
if (fol_IsEquality(PartnerEq) &&
(term_FirstArgument(PartnerEq) == TermS)) {
CLAUSE RuleClause, HelpClause;
LITERAL RuleLit;
int i;
for (LitScan = sharing_NAtomDataList(PartnerEq);
!list_Empty(LitScan) && !Rewritten;
LitScan = list_Cdr(LitScan)) {
RuleLit = list_Car(LitScan);
RuleClause = clause_LiteralOwningClause(RuleLit);
i = clause_LiteralGetIndex(RuleLit);
HelpClause = NULL;
#ifdef CRW_DEBUG
if (clause_LiteralIsPositive(RuleLit) &&
clause_LiteralGetFlag(RuleLit,STRICTMAXIMAL) &&
clause_LiteralIsOrientedEquality(RuleLit) &&
red_LeftTermOfEquationIsStrictlyMaximalTerm(RuleClause,
RuleLit,
Flags,
Precedence)) {
printf("\n------\nFCRw: %s\n%d ", red_WorkedOffMode(Mode)
? "WorkedOff" : "Usable", i);
clause_Print(RuleClause);
printf("\n%d ", ri);
clause_Print(RedClause);
}
#endif
if (clause_LiteralIsPositive(RuleLit) &&
clause_LiteralGetFlag(RuleLit,STRICTMAXIMAL) &&
clause_LiteralIsOrientedEquality(RuleLit) &&
red_LeftTermOfEquationIsStrictlyMaximalTerm(RuleClause,
RuleLit,
Flags,
Precedence) &&
red_CRwTautologyCheck(Search, Copy, ri, RedTermS,
RuleClause, i, Mode,
&HelpClause)) {
TERM TermT;
if (RedClause == Copy &&
(Document ||
prfs_SplitLevelCondition(clause_SplitLevel(RuleClause),
clause_SplitLevel(RedClause),Level) ||
prfs_SplitLevelCondition(clause_SplitLevel(HelpClause),
clause_SplitLevel(RedClause),
Level))) {
Copy = clause_Copy(RedClause);
RedAtom = clause_GetLiteralAtom(Copy, ri);
}
if (!Result && flag_GetFlagValue(Flags, flag_PCRW)) {
/* Clause is rewitten for the first time and */
/* printing is turned on. */
fputs("\nFContRewriting: ", stdout);
clause_Print(Copy);
fputs(" ==>[ ", stdout);
}
if (Document) {
LIST PClauses, PLits;
/* Get additional parent information from */
/* <HelpClause> */
PClauses = PLits = list_Nil();
if (HelpClause != NULL) {
PClauses = clause_ParentClauses(HelpClause);
PLits = clause_ParentLiterals(HelpClause);
clause_SetParentClauses(HelpClause, list_Nil());
clause_SetParentLiterals(HelpClause, list_Nil());
} else
PClauses = PLits = list_Nil();
if (!Result)
red_DocumentContextualRewriting(Copy, ri,
RuleClause, i,
PClauses, PLits);
else
red_DocumentFurtherCRw(Copy, ri, RuleClause, i,
PClauses, PLits);
}
Result = TRUE;
cont_StartBinding();
unify_MatchBindings(cont_LeftContext(), TermS, RedTermS);
TermT = cont_ApplyBindingsModuloMatching(cont_LeftContext(),
term_Copy(term_SecondArgument(PartnerEq)),
TRUE);
cont_BackTrack();
term_ReplaceSubtermBy(RedAtom, RedTermS, TermT);
Rewritten = TRUE;
/* Set splitting data from parents */
clause_UpdateSplitDataFromPartner(Copy, RuleClause);
if (HelpClause != NULL) {
/* Store splitting data from intermediate clauses */
clause_UpdateSplitDataFromPartner(Copy, HelpClause);
clause_Delete(HelpClause);
}
term_Delete(TermT);
stack_SetBottom(B_Stack);
if (flag_GetFlagValue(Flags, flag_PCRW))
printf("%d.%d ",clause_Number(RuleClause), i);
clause_UpdateWeight(Copy, Flags);
}
}
}
}
}
}
list_Delete(Gen);
}
}
}
}
if (Result) {
clause_OrientAndReInit(Copy, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PCRW)) {
fputs("] ", stdout);
clause_Print(Copy);
}
if (Copy != RedClause) {
clause_OrientAndReInit(RedClause, Flags, Precedence);
*Changed = Copy;
}
}
#ifdef CHECK
if (Copy != RedClause)
clause_Check(Copy, Flags, Precedence);
clause_Check(RedClause, Flags, Precedence);
#endif
return Result;
}
static LIST red_BackSubsumption(CLAUSE RedCl, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**********************************************************
INPUT: A pointer to a non-empty clause, an index of
clauses, a flag store and a precedence.
RETURNS: The list of clauses that are subsumed by the
clause RedCl.
***********************************************************/
{
TERM Atom,CandTerm;
CLAUSE SubsumedCl;
LITERAL CandLit;
LIST CandLits, Scan, SubsumedList;
int i, j, lc, fa, la, fs, l;
#ifdef CHECK
if (!clause_IsClause(RedCl, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackSubsumption :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedCl, Flags, Precedence);
#endif
/* Special case: clause is empty */
if (clause_IsEmptyClause(RedCl))
return list_Nil();
SubsumedList = list_Nil();
lc = clause_LastConstraintLitIndex(RedCl);
fa = clause_FirstAntecedentLitIndex(RedCl);
la = clause_LastAntecedentLitIndex(RedCl);
fs = clause_FirstSuccedentLitIndex(RedCl);
l = clause_LastLitIndex(RedCl);
/* Choose the literal with the greatest weight to start the search */
i = clause_FirstLitIndex();
for (j = i + 1; j <= l; j++) {
if (clause_LiteralWeight(clause_GetLiteral(RedCl, j)) >
clause_LiteralWeight(clause_GetLiteral(RedCl, i)))
i = j;
}
Atom = clause_GetLiteralAtom(RedCl, i);
CandTerm = st_ExistInstance(cont_LeftContext(), sharing_Index(ShIndex), Atom);
while (CandTerm) {
CandLits = sharing_NAtomDataList(CandTerm);
for (Scan = CandLits; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
CandLit = list_Car(Scan);
SubsumedCl = clause_LiteralOwningClause(CandLit);
j = clause_LiteralGetIndex(CandLit);
if (RedCl != SubsumedCl &&
/* Literals must be from same part of the clause */
((i<=lc && clause_LiteralIsFromConstraint(CandLit)) ||
(i>=fa && i<=la && clause_LiteralIsFromAntecedent(CandLit)) ||
(i>=fs && clause_LiteralIsFromSuccedent(CandLit))) &&
!list_PointerMember(SubsumedList, SubsumedCl) &&
subs_SubsumesBasic(RedCl, SubsumedCl, i, j))
SubsumedList = list_Cons(SubsumedCl, SubsumedList);
}
CandTerm = st_NextCandidate();
}
if (fol_IsEquality(Atom) &&
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(RedCl, i))) {
Atom = term_Create(fol_Equality(),
list_Reverse(term_ArgumentList(Atom)));
CandTerm = st_ExistInstance(cont_LeftContext(), sharing_Index(ShIndex), Atom);
while (CandTerm) {
CandLits = sharing_NAtomDataList(CandTerm);
for (Scan = CandLits; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
CandLit = list_Car(Scan);
SubsumedCl = clause_LiteralOwningClause(list_Car(Scan));
/* if (!clause_GetFlag(SubsumedCl, BLOCKED)) { */
j = clause_LiteralGetIndex(list_Car(Scan));
if ((RedCl != SubsumedCl) &&
/* Literals must be from same part of the clause */
((i<=lc && clause_LiteralIsFromConstraint(CandLit)) ||
(i>=fa && i<=la && clause_LiteralIsFromAntecedent(CandLit)) ||
(i>=fs && clause_LiteralIsFromSuccedent(CandLit))) &&
!list_PointerMember(SubsumedList, SubsumedCl) &&
subs_SubsumesBasic(RedCl, SubsumedCl, i, j))
SubsumedList = list_Cons(SubsumedCl, SubsumedList);
/* } */
}
CandTerm = st_NextCandidate();
}
list_Delete(term_ArgumentList(Atom));
term_Free(Atom);
}
if (flag_GetFlagValue(Flags, flag_PSUB)) {
for (Scan = SubsumedList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
SubsumedCl = list_Car(Scan);
fputs("\nBSubsumption: ", stdout);
clause_Print(SubsumedCl);
printf(" by %d ",clause_Number(RedCl));
}
}
return SubsumedList;
}
static LIST red_GetBackMRResLits(CLAUSE Clause, LITERAL ActLit, SHARED_INDEX ShIndex)
/**************************************************************
INPUT: A clause, one of its literals and an Index.
RETURNS: A list of clauses with a complementary literal instance
that are subsumed if these literals are ignored.
the empty list if no such clause exists.
MEMORY: Allocates the needed listnodes.
***************************************************************/
{
CLAUSE PClause;
LITERAL PLit;
LIST LitScan, PClLits;
TERM CandTerm;
int i;
PClLits = list_Nil();
i = clause_LiteralGetIndex(ActLit);
CandTerm = st_ExistInstance(cont_LeftContext(),
sharing_Index(ShIndex),
clause_LiteralAtom(ActLit));
while (CandTerm) {
LitScan = sharing_NAtomDataList(CandTerm); /* CAUTION ! */
for ( ; !list_Empty(LitScan); LitScan = list_Cdr(LitScan)) {
PLit = list_Car(LitScan);
PClause = clause_LiteralOwningClause(PLit);
if (PClause != Clause &&
clause_LiteralsAreComplementary(ActLit,PLit) &&
subs_SubsumesBasic(Clause,PClause,i,clause_LiteralGetIndex(PLit)))
PClLits = list_Cons(PLit, PClLits);
}
CandTerm = st_NextCandidate();
}
return PClLits;
}
static LIST red_BackMatchingReplacementResolution(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
LIST* Result)
/**************************************************************
INPUT: A clause, a shared index, a flag store, a
precedence, and a pointer to a result list.
RETURNS: The return value itself contains a list of clauses
from <ShIndex> that is reducible by <RedClause> via
clause reduction.
The return value stored in <*Result> contains the
result of this operation.
If the <DocProof> flag is true then the clauses in
<*Result> contain information about the reduction.
***************************************************************/
{
LIST Blocked;
CLAUSE Copy;
BOOL Document;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackMatchingReplacementResolution:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Blocked = list_Nil();
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
if (clause_Length(RedClause) == 1) {
LITERAL ActLit, PLit;
LIST LitList, Scan, Iter;
TERM CandTerm;
int RedClNum;
ActLit = clause_GetLiteral(RedClause, clause_FirstLitIndex());
if (!fol_IsEquality(clause_LiteralAtom(ActLit)) || /* Reduce with negative equations too */
clause_LiteralIsNegative(ActLit)) {
CLAUSE PClause;
LIST PIndL;
CandTerm = st_ExistInstance(cont_LeftContext(), sharing_Index(ShIndex), clause_LiteralAtom(ActLit));
RedClNum = clause_Number(RedClause);
LitList = list_Nil();
while (CandTerm) {
for (Iter = sharing_NAtomDataList(CandTerm); !list_Empty(Iter); Iter = list_Cdr(Iter))
if (clause_LiteralsAreComplementary(ActLit,list_Car(Iter)))
LitList = list_Cons(list_Car(Iter),LitList);
CandTerm = st_NextCandidate();
}
/* It is important to get all literals first,
because there may be several literals in the same clause which can be reduced by <ActLit> */
while (!list_Empty(LitList)) {
PLit = list_Car(LitList);
PIndL = list_List(PLit);
PClause = clause_LiteralOwningClause(PLit);
Blocked = list_Cons(PClause, Blocked);
if (flag_GetFlagValue(Flags, flag_PMRR)) {
fputs("\nBMatchingReplacementResolution: ", stdout);
clause_Print(PClause);
printf(" ==>[ %d.%d ] ",clause_Number(RedClause),clause_FirstLitIndex());
}
Iter = LitList;
for (Scan=list_Cdr(LitList);!list_Empty(Scan);Scan=list_Cdr(Scan)) /* Get brothers of PLit */
if (PClause == clause_LiteralOwningClause(list_Car(Scan))) {
list_Rplacd(Iter,list_Cdr(Scan));
list_Rplacd(Scan,PIndL);
PIndL = Scan;
Scan = Iter;
}
else
Iter = Scan;
Iter = LitList;
LitList = list_Cdr(LitList);
list_Free(Iter);
Copy = clause_Copy(PClause);
clause_RemoveFlag(Copy,WORKEDOFF);
clause_UpdateSplitDataFromPartner(Copy, RedClause);
for(Scan=PIndL;!list_Empty(Scan);Scan=list_Cdr(Scan)) /* Change lits to indexes */
list_Rplaca(Scan,(POINTER)clause_LiteralGetIndex(list_Car(Scan)));
clause_DeleteLiterals(Copy, PIndL, Flags, Precedence);
if (Document)
/* Lists are consumed */
red_DocumentMatchingReplacementResolution(Copy, PIndL, list_List((POINTER)RedClNum),
list_List((POINTER)clause_FirstLitIndex()));
else
list_Delete(PIndL);
if (flag_GetFlagValue(Flags, flag_PMRR))
clause_Print(Copy);
*Result = list_Cons(Copy, *Result);
}
}
return Blocked;
}
else {
CLAUSE PClause;
LITERAL ActLit, PLit;
LIST LitScan,LitList;
int i,length,RedClNum,PInd;
RedClNum = clause_Number(RedClause);
length = clause_Length(RedClause);
for (i = clause_FirstLitIndex(); i < length; i++) {
ActLit = clause_GetLiteral(RedClause, i);
if (!fol_IsEquality(clause_LiteralAtom(ActLit))) {
LitList = red_GetBackMRResLits(RedClause, ActLit, ShIndex);
for (LitScan = LitList;!list_Empty(LitScan);LitScan = list_Cdr(LitScan)) {
PLit = list_Car(LitScan);
PClause = clause_LiteralOwningClause(PLit);
PInd = clause_LiteralGetIndex(PLit);
Copy = clause_Copy(PClause);
if (list_PointerMember(Blocked,PClause)) {
if (!flag_GetFlagValue(Flags, flag_DOCPROOF))
clause_NewNumber(Copy);
}
else
Blocked = list_Cons(PClause, Blocked);
clause_RemoveFlag(Copy,WORKEDOFF);
clause_UpdateSplitDataFromPartner(Copy, RedClause);
clause_DeleteLiteral(Copy, PInd, Flags, Precedence);
if (Document)
red_DocumentMatchingReplacementResolution(Copy, list_List((POINTER)PInd),
list_List((POINTER)RedClNum),
list_List((POINTER)i));
if (flag_GetFlagValue(Flags, flag_PMRR)) {
fputs("\nBMatchingReplacementResolution: ", stdout);
clause_Print(PClause);
printf(" ==>[ %d.%d ] ",clause_Number(RedClause),i);
clause_Print(Copy);
}
*Result = list_Cons(Copy, *Result);
}
list_Delete(LitList);
}
}
return Blocked;
}
}
static void red_ApplyRewriting(CLAUSE RuleCl, int ri, CLAUSE PartnerClause,
int pli, TERM PartnerTermS, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause to use for rewriting, the index of a
positive equality literal where the first equality
argument is greater, a clause, the index of a
literal with subterm <PartnerTermS> that can be
rewritten, a flag store and a precedence.
RETURNS: Nothing.
EFFECT: The atom of literal pli in PartnerClause is
destructively changed !!!
The <DocProof> flag is considered.
***************************************************************/
{
LITERAL PartnerLit;
TERM ReplaceTermT, NewAtom;
#ifdef CHECK
clause_Check(PartnerClause, Flags, Precedence);
clause_Check(RuleCl, Flags, Precedence);
#endif
if (flag_GetFlagValue(Flags, flag_DOCPROOF))
red_DocumentRewriting(PartnerClause, pli, RuleCl, ri);
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("\nBRewriting: ", stdout);
clause_Print(PartnerClause);
printf(" ==>[ %d.%d ] ", clause_Number(RuleCl), ri);
}
PartnerLit = clause_GetLiteral(PartnerClause, pli);
ReplaceTermT =
cont_ApplyBindingsModuloMatchingReverse(cont_LeftContext(),
term_Copy(term_SecondArgument(clause_GetLiteralTerm(RuleCl, ri))));
NewAtom = clause_LiteralSignedAtom(PartnerLit);
term_ReplaceSubtermBy(NewAtom, PartnerTermS, ReplaceTermT);
term_Delete(ReplaceTermT);
clause_OrientAndReInit(PartnerClause, Flags, Precedence);
clause_UpdateSplitDataFromPartner(PartnerClause, RuleCl);
if (flag_GetFlagValue(Flags, flag_PREW))
clause_Print(PartnerClause);
}
static LIST red_LiteralRewriting(CLAUSE RedClause, LITERAL ActLit, int ri,
SHARED_INDEX ShIndex, FLAGSTORE Flags,
PRECEDENCE Precedence, LIST* Result)
/**************************************************************
INPUT: A clause, a positive equality literal where the
first equality argument is greater, its index, an
index of clauses, a flag store, a precedence and a
pointer to a list of clauses that were rewritten.
RETURNS: The list of clauses from the index that can be
rewritten by <ActLit> and <RedClause>.
The rewritten clauses are stored in <*Result>.
EFFECT: The <DocProof> flag is considered.
***************************************************************/
{
TERM TermS, CandTerm;
LIST Blocked;
#ifdef CHECK
if (!clause_LiteralIsLiteral(ActLit) || !clause_LiteralIsEquality(ActLit) ||
!clause_LiteralIsOrientedEquality(ActLit)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_LiteralRewriting: Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Blocked = list_Nil();
TermS = term_FirstArgument(clause_LiteralSignedAtom(ActLit)); /* Vars can't be greater ! */
CandTerm = st_ExistInstance(cont_LeftContext(), sharing_Index(ShIndex), TermS);
while (CandTerm) {
if (!term_IsVariable(CandTerm) &&
!symbol_IsPredicate(term_TopSymbol(CandTerm))) {
LIST LitList;
LitList = sharing_GetDataList(CandTerm, ShIndex);
for ( ; !list_Empty(LitList); LitList = list_Pop(LitList)){
LITERAL PartnerLit;
CLAUSE PartnerClause;
int pli;
PartnerLit = list_Car(LitList);
pli = clause_LiteralGetIndex(PartnerLit);
PartnerClause = clause_LiteralOwningClause(PartnerLit);
/* Partner literal must be from antecedent or succedent */
if (clause_Number(RedClause) != clause_Number(PartnerClause) &&
pli >= clause_FirstAntecedentLitIndex(PartnerClause) &&
!list_PointerMember(Blocked, PartnerClause) &&
subs_SubsumesBasic(RedClause, PartnerClause, ri, pli)) {
CLAUSE Copy;
Blocked = list_Cons(PartnerClause, Blocked);
Copy = clause_Copy(PartnerClause);
clause_RemoveFlag(Copy, WORKEDOFF);
red_ApplyRewriting(RedClause, ri, Copy, pli, CandTerm,
Flags, Precedence);
*Result = list_Cons(Copy, *Result);
}
}
}
CandTerm = st_NextCandidate();
}
return Blocked;
}
static LIST red_BackRewriting(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
LIST* Result)
/**************************************************************
INPUT: A clause, and Index, a flag store, a precedence and
a pointer to the list of rewritten clauses.
RETURNS: A list of clauses that can be rewritten with
<RedClause> and the result of this operation is
stored in <*Result>.
EFFECT: The <DocProof> flag is considered.
***************************************************************/
{
int i,length;
LITERAL ActLit;
LIST Blocked;
#ifdef CHECK
if (!(clause_IsClause(RedClause, Flags, Precedence))) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackRewriting :");
misc_ErrorReport(" Illegal input.\n");