diff options
Diffstat (limited to 'test/spass/rules-red.c')
| -rw-r--r-- | test/spass/rules-red.c | 4508 |
1 files changed, 4508 insertions, 0 deletions
diff --git a/test/spass/rules-red.c b/test/spass/rules-red.c new file mode 100644 index 0000000..609b3cf --- /dev/null +++ b/test/spass/rules-red.c @@ -0,0 +1,4508 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * 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: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * 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"); + misc_FinishErrorReport(); + } + clause_Check(RedClause, Flags, Precedence); +#endif + + Blocked = list_Nil(); + length = clause_Length(RedClause); + + for (i=clause_FirstSuccedentLitIndex(RedClause); i < length; i++) { + ActLit = clause_GetLiteral(RedClause, i); + if (clause_LiteralIsOrientedEquality(ActLit)) { + Blocked = list_Nconc(red_LiteralRewriting(RedClause, ActLit, i, + ShIndex, Flags, Precedence, + Result), + Blocked); + } + +#ifdef CHECK + if (fol_IsEquality(clause_LiteralSignedAtom(ActLit))) { + ord_RESULT HelpRes; + + HelpRes = + ord_Compare(term_FirstArgument(clause_LiteralSignedAtom(ActLit)), + term_SecondArgument(clause_LiteralSignedAtom(ActLit)), + Flags, Precedence); + + if (ord_IsSmallerThan(HelpRes)){ /* For Debugging */ + misc_StartErrorReport(); + misc_ErrorReport("\n In red_BackRewriting:"); + misc_ErrorReport("First Argument smaller than second in RedClause.\n"); + misc_FinishErrorReport(); + } + } /* end of if (fol_IsEquality). */ +#endif + } /* end of for 'all succedent literals'. */ + Blocked = list_PointerDeleteDuplicates(Blocked); + return Blocked; +} + + +/**************************************************************/ +/* BACKWARD CONTEXTUAL REWRITING */ +/**************************************************************/ + +static LIST red_BackCRwOnLiteral(PROOFSEARCH Search, CLAUSE RuleClause, + LITERAL Lit, int i, NAT Mode, LIST* Result) +/************************************************************** + INPUT: A proof search object, a clause that is used to rewrite + other clauses, a positive literal from the clause, + that is a strictly maximal, oriented equation, the index + of the literal, a mode defining which clause index + is used to find rewritable clauses, and a pointer + to a list that is used as return value. + The left term of the equation has to be the strictly + maximal term in the clause, i.e. it is bigger than + any other term. + RETURNS: The list of clauses from the clause index that can be + rewritten by <Lit> and <RuleClause>. + The rewritten clauses are stored in <*Result>. + EFFECT: The <DocProof> flag is considered. +***************************************************************/ +{ + TERM TermS, CandTerm, ReplaceTermT; + LIST Inst, Blocked; + FLAGSTORE Flags; + PRECEDENCE Precedence; + SHARED_INDEX ShIndex; + + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + if (red_WorkedOffMode(Mode)) + ShIndex = prfs_WorkedOffSharingIndex(Search); + else + ShIndex = prfs_UsableSharingIndex(Search); + +#ifdef CHECK + if (!clause_LiteralIsLiteral(Lit) || !clause_LiteralIsEquality(Lit) || + !clause_LiteralGetFlag(Lit, STRICTMAXIMAL) || + !clause_LiteralIsOrientedEquality(Lit)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_BackCRwOnLiteral: Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(RuleClause, Flags, Precedence); +#endif + + Blocked = list_Nil(); + TermS = term_FirstArgument(clause_LiteralSignedAtom(Lit)); + + /* Get all instances of <TermS> at once. This can't be done iteratively */ + /* since other reduction rules are invoked within the following loop. */ + Inst = st_GetInstance(cont_LeftContext(), sharing_Index(ShIndex), TermS); + + for ( ; !list_Empty(Inst); Inst = list_Pop(Inst)) { + CandTerm = list_Car(Inst); + + 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 RedLit; + CLAUSE RedClause, HelpClause; + int ri; + + RedLit = list_Car(LitList); + ri = clause_LiteralGetIndex(RedLit); + RedClause = clause_LiteralOwningClause(RedLit); + HelpClause = NULL; + +#ifdef CRW_DEBUG + if (clause_Number(RuleClause) != clause_Number(RedClause) && + ri >= clause_FirstAntecedentLitIndex(RedClause) && + !list_PointerMember(Blocked, RedClause)) { + printf("\n------\nBCRw: %s\n%d ", red_WorkedOffMode(Mode) ? + "WorkedOff" : "Usable", i); + clause_Print(RuleClause); + printf("\n%d ", ri); + clause_Print(RedClause); + } +#endif + + /* Partner literal must be from antecedent or succedent */ + if (clause_Number(RuleClause) != clause_Number(RedClause) && + ri >= clause_FirstAntecedentLitIndex(RedClause) && + /* Check that clause wasn't already rewritten by this literal. */ + /* Necessary because then the old version of the clause is still */ + /* in the index, but the rewritten version in not in the index. */ + !list_PointerMember(Blocked, RedClause) && + red_CRwTautologyCheck(Search, RedClause, ri, CandTerm, + RuleClause, i, Mode, &HelpClause)) { + CLAUSE Copy; + + /* The <PartnerClause> has to be copied because it's indexed. */ + Blocked = list_Cons(RedClause, Blocked); + Copy = clause_Copy(RedClause); + clause_RemoveFlag(Copy, WORKEDOFF); + + /* Establish bindings */ + cont_StartBinding(); + if (!unify_MatchBindings(cont_LeftContext(), TermS, CandTerm)) { +#ifdef CHECK + misc_StartErrorReport(); + misc_ErrorReport("\n In red_BackCRwOnLiteral: terms aren't "); + misc_ErrorReport("matchable."); + misc_FinishErrorReport(); +#endif + } + /* The variable check in cont_ApplyBindings... is turned on here */ + /* because all variables is s are bound, and s > t. So all */ + /* variables in t are bound, too. */ + ReplaceTermT = + cont_ApplyBindingsModuloMatching(cont_LeftContext(), + term_Copy(term_SecondArgument(clause_GetLiteralTerm(RuleClause, i))), + TRUE); + cont_BackTrack(); + + /* Modify copied clause */ + term_ReplaceSubtermBy(clause_GetLiteralAtom(Copy, ri), CandTerm, + ReplaceTermT); + term_Delete(ReplaceTermT); + + /* Proof documentation */ + if (flag_GetFlagValue(Flags, flag_DOCPROOF)) { + LIST PClauses, PLits; + + if (HelpClause != NULL) { + /* Get additional parent clauses and literals from the */ + /* tautology check. */ + PClauses = clause_ParentClauses(HelpClause); + PLits = clause_ParentLiterals(HelpClause); + clause_SetParentClauses(HelpClause, list_Nil()); + clause_SetParentLiterals(HelpClause, list_Nil()); + } else + PClauses = PLits = list_Nil(); + + red_DocumentContextualRewriting(Copy, ri, RuleClause, i, + PClauses, PLits); + } + + /* Set splitting data according to all parents */ + clause_UpdateSplitDataFromPartner(Copy, RuleClause); + if (HelpClause != NULL) { + clause_UpdateSplitDataFromPartner(Copy, HelpClause); + clause_Delete(HelpClause); + } + + clause_OrientAndReInit(Copy, Flags, Precedence); + + if (flag_GetFlagValue(Flags, flag_PCRW)) { + fputs("\nBContRewriting: ", stdout); + clause_Print(RedClause); + printf(" ==>[ %d.%d ] ", clause_Number(RuleClause), i); + clause_Print(Copy); + } + + *Result = list_Cons(Copy, *Result); + } + } + } + } + + return Blocked; +} + + +static LIST red_BackContextualRewriting(PROOFSEARCH Search, CLAUSE RuleClause, + NAT Mode, LIST* Result) +/************************************************************** + INPUT: A proof search object, a clause that is used to rewrite + other clauses, a mode flag that indicates which clause + index is used to find rewritable clauses, and a pointer + to a list that is used as return value. + RETURNS: A list of clauses that can be reduced + with Contextual Rewriting with <RuleClause>. + The clauses resulting from the rewriting steps are + stored in <*Result>. + EFFECT: The <DocProof> flag is considered. Every rewritable clause + is copied before rewriting is applied! This has to be done, + because the rewritable clauses are indexed. +***************************************************************/ +{ + BOOL found; + int i, ls; + LITERAL Lit; + LIST Blocked; + FLAGSTORE Flags; + PRECEDENCE Precedence; + + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + +#ifdef CHECK + if (!clause_IsClause(RuleClause, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_BackContextualRewriting: Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(RuleClause, Flags, Precedence); +#endif + + Blocked = list_Nil(); + ls = clause_LastSuccedentLitIndex(RuleClause); + found = FALSE; + + for (i = clause_FirstSuccedentLitIndex(RuleClause); i <= ls && !found; i++) { + Lit = clause_GetLiteral(RuleClause, i); + if (clause_LiteralIsOrientedEquality(Lit) && + clause_LiteralGetFlag(Lit, STRICTMAXIMAL) && + red_LeftTermOfEquationIsStrictlyMaximalTerm(RuleClause, Lit, Flags, + Precedence)) { + Blocked = list_Nconc(red_BackCRwOnLiteral(Search, RuleClause, Lit, i, + Mode, Result), + Blocked); + /* Stop loop: there's only one strictly maximal term per clause */ + found = TRUE; + } + } + + Blocked = list_PointerDeleteDuplicates(Blocked); + return Blocked; +} + + +static void red_DocumentSortSimplification(CLAUSE Clause, LIST Indexes, + LIST Clauses) +/********************************************************* + INPUT: A clause and the literal indices and clauses + involved in sort simplification. + RETURNS: Nothing. + MEMORY: Consumes the input lists. +**********************************************************/ +{ + LIST Scan,Declarations,Self; + + Declarations = list_Nil(); + Self = list_Nil(); + + list_Delete(clause_ParentClauses(Clause)); + list_Delete(clause_ParentLiterals(Clause)); + + for(Scan=Indexes;!list_Empty(Scan);Scan=list_Cdr(Scan)) + Self = list_Cons((POINTER)clause_Number(Clause),Self); + + for(Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Declarations = list_Cons((POINTER)clause_FirstSuccedentLitIndex(list_Car(Scan)),Declarations); + list_Rplaca(Scan,(POINTER)clause_Number(list_Car(Scan))); + } + + clause_SetParentLiterals(Clause, list_Nconc(Indexes,Declarations)); + clause_SetParentClauses(Clause, list_Nconc(Self,Clauses)); + + clause_SetNumber(Clause, clause_IncreaseCounter()); + clause_SetFromSortSimplification(Clause); +} + + +static BOOL red_SortSimplification(SORTTHEORY Theory, CLAUSE Clause, NAT Level, + BOOL Document, FLAGSTORE Flags, + PRECEDENCE Precedence, CLAUSE *Changed) +/********************************************************** + INPUT: A sort theory, a clause, the last backtrack + level of the current proof search, a boolean + flag concerning proof documentation, a flag + store and a precedence. + RETURNS: TRUE iff sort simplification was possible. + If <Document> is true or the split level of the + used declaration clauses requires copying a + simplified copy of the clause is returned in + <*Changed>. + Otherwise the clause is destructively + simplified. +***********************************************************/ +{ + if (Theory != (SORTTHEORY)NULL) { + TERM Atom,Term; + SOJU SortPair; + SORT TermSort,LitSort; + LIST Indexes,NewClauses,Clauses,Scan; + int i,lc,j,OldSplitLevel; + CLAUSE Copy; + CONDITION Cond; + +#ifdef CHECK + if (!clause_IsClause(Clause, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_SortSimplification :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(Clause, Flags, Precedence); +#endif + + lc = clause_LastConstraintLitIndex(Clause); + i = clause_FirstLitIndex(); + j = 0; + OldSplitLevel = clause_SplitLevel(Clause); + Copy = Clause; + Indexes = list_Nil(); + Clauses = list_Nil(); + + while (i <= lc) { + + Atom = clause_LiteralAtom(clause_GetLiteral(Copy, i)); + Term = term_FirstArgument(Atom); + SortPair = sort_ComputeSortNoResidues(Theory, Term, Copy, i, + Flags, Precedence); + TermSort = sort_PairSort(SortPair); + NewClauses = sort_ConditionClauses(sort_PairCondition(SortPair)); + sort_ConditionPutClauses(sort_PairCondition(SortPair),list_Nil()); + LitSort = sort_TheorySortOfSymbol(Theory,term_TopSymbol(Atom)); + + if ((Cond = sort_TheoryIsSubsortOfNoResidues(Theory, TermSort, LitSort)) != (CONDITION)NULL) { + + if (j == 0 && flag_GetFlagValue(Flags, flag_PSSI)) { + fputs("\nSortSimplification: ", stdout); + clause_Print(Copy); + fputs(" ==>[ ", stdout); + } + + NewClauses = list_Nconc(NewClauses,sort_ConditionClauses(Cond)); + sort_ConditionPutClauses(Cond,list_Nil()); + sort_ConditionDelete(Cond); + + for (Scan = NewClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) { + if (Clause == Copy && + (Document || + prfs_SplitLevelCondition(clause_SplitLevel(list_Car(Scan)),OldSplitLevel,Level))) + Copy = clause_Copy(Clause); + clause_UpdateSplitDataFromPartner(Copy, list_Car(Scan)); + if (flag_GetFlagValue(Flags, flag_PSSI)) + printf("%d ",clause_Number(list_Car(Scan))); + } + + if (Document) + Indexes = list_Cons((POINTER)(i+j), Indexes); + + clause_DeleteLiteral(Copy, i, Flags, Precedence); + Clauses = list_Nconc(NewClauses,Clauses); + j++; + lc--; + } + else { + list_Delete(NewClauses); + i++; + } + sort_DeleteSortPair(SortPair); + sort_Delete(LitSort); + } + +#ifdef CHECK + clause_Check(Copy, Flags, Precedence); +#endif + + if (j > 0) { + if (Document) + red_DocumentSortSimplification(Copy,Indexes,Clauses); + else + list_Delete(Clauses); + clause_ReInit(Copy, Flags, Precedence); + if (flag_GetFlagValue(Flags, flag_PSSI)) { + fputs("] ", stdout); + clause_Print(Copy); + } + if (Copy != Clause) + *Changed = Copy; + return TRUE; + } + } + + return FALSE; +} + +static void red_ExchangeClauses(CLAUSE *RedClause, CLAUSE *Copy, LIST *Result) +/********************************************************** + INPUT: Two pointers to clauses and a pointer to a list. + RETURNS: Nothing. + EFFECT: If *Copy is NULL, nothing is done. Otherwise *RedClause + is added to the list, *Copy is assigned to *RedClause, + and NULL is assigned to *Copy. +***********************************************************/ +{ + if (*Copy) { + *Result = list_Cons(*RedClause,*Result); + *RedClause = *Copy; + *Copy = (CLAUSE)NULL; + } +} + + + +static BOOL red_SimpleStaticReductions(CLAUSE *RedClause, FLAGSTORE Flags, + PRECEDENCE Precedence, LIST* Result) +/********************************************************** + INPUT: A clause (by reference), a flag store and a + precedence. + RETURNS: TRUE if <*RedClause> is redundant. + If the <DocProof> flag is false and no copying is necessary + with respect to splitting, the clause is destructively changed, + otherwise (intermediate) copies are made and returned in <*Result>. + EFFECT: Used reductions are tautology deletion and + obvious reductions. +***********************************************************/ +{ + CLAUSE Copy; + BOOL DocProof; + +#ifdef CHECK + if (!clause_IsClause(*RedClause, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_SimpleStaticReductions :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(*RedClause, Flags, Precedence); +#endif + + Copy = (CLAUSE)NULL; + DocProof = flag_GetFlagValue(Flags, flag_DOCPROOF); + + if (flag_GetFlagValue(Flags, flag_RTAUT) != flag_RTAUTOFF && + red_Tautology(*RedClause, Flags, Precedence)) + return TRUE; + + if (flag_GetFlagValue(Flags, flag_ROBV)) { + red_ObviousReductions(*RedClause, DocProof, Flags, Precedence, &Copy); + red_ExchangeClauses(RedClause, &Copy, Result); + } + + if (flag_GetFlagValue(Flags, flag_RCON)) { + red_Condensing(*RedClause, DocProof, Flags, Precedence, &Copy); + red_ExchangeClauses(RedClause, &Copy, Result); + } + + return FALSE; +} + + + + +static BOOL red_StaticReductions(PROOFSEARCH Search, CLAUSE *Clause, + CLAUSE *Subsumer, LIST* Result, NAT Mode) +/********************************************************** + INPUT: A proof search object, a clause (by reference) to be reduced, + a shared index of clauses and the mode of the reductions, + determining which sets (Usable, WorkedOff) in <Search> + are considered for reductions. + RETURNS: TRUE iff the clause is redundant. + If the <DocProof> flag is false and no copying is necessary + with respect to splitting, the clause is destructively changed, + otherwise (intermediate) copies are made and returned in <*Result>. + If <Clause> gets redundant with respect to forward subsumption, + the subsuming clause is returned in <*Subsumer>. + EFFECT: Used reductions are tautology deletion, obvious reductions, + forward subsumption, forward rewriting, forward contextual + rewriting, forward matching replacement resolution, + sort simplification, unit conflict and static soft typing. + Depending on <Mode>, then clauses are reduced with respect + to WorkedOff or Usable Clauses. +***********************************************************/ +{ + CLAUSE Copy; + BOOL Redundant; + SHARED_INDEX Index; + FLAGSTORE Flags; + PRECEDENCE Precedence; + + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + +#ifdef CHECK + if (!clause_IsClause(*Clause, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_StaticReductions:"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(*Clause, Flags, Precedence); +#endif + + Index = (red_OnlyWorkedOffMode(Mode) ? + prfs_WorkedOffSharingIndex(Search) : prfs_UsableSharingIndex(Search)); + Copy = (CLAUSE)NULL; + Redundant = red_SimpleStaticReductions(Clause, Flags, Precedence, Result); + + if (Redundant) + return Redundant; + + /* Assignment Equation Deletion */ + if (flag_GetFlagValue(Flags, flag_RAED) != flag_RAEDOFF && + red_AssignmentEquationDeletion(*Clause, Flags, Precedence, &Copy, + prfs_NonTrivClauseNumber(Search), + (flag_GetFlagValue(Flags, flag_RAED) == flag_RAEDPOTUNSOUND))) { + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + } + + /* Subsumption */ + if (flag_GetFlagValue(Flags, flag_RFSUB)) { + *Subsumer = red_ForwardSubsumption(*Clause, Index, Flags, Precedence); + if ((Redundant = (*Subsumer != (CLAUSE)NULL))) + return Redundant; + } + + /* Forward Rewriting and Forward Contextual Rewriting */ + if ((flag_GetFlagValue(Flags, flag_RFREW) && + red_RewriteRedClause(*Clause, Index, Flags, Precedence, + &Copy, prfs_LastBacktrackLevel(Search))) || + (flag_GetFlagValue(Flags, flag_RFCRW) && + red_ContextualRewriting(Search, *Clause, Mode, + prfs_LastBacktrackLevel(Search), &Copy))) { + red_ExchangeClauses(Clause, &Copy, Result); + Redundant = red_SimpleStaticReductions(Clause, Flags, Precedence, Result); + if (Redundant) + return Redundant; + if (clause_IsEmptyClause(*Clause)) + return FALSE; + if (flag_GetFlagValue(Flags, flag_RFSUB)) { + *Subsumer = red_ForwardSubsumption(*Clause, Index, Flags, Precedence); + if ((Redundant = (*Subsumer != (CLAUSE)NULL))) + return Redundant; + } + } + + /* Sort Simplification */ + if (red_OnlyWorkedOffMode(Mode) && flag_GetFlagValue(Flags, flag_RSSI)) { + red_SortSimplification(prfs_DynamicSortTheory(Search), *Clause, + prfs_LastBacktrackLevel(Search), + flag_GetFlagValue(Flags, flag_DOCPROOF), + Flags, Precedence, &Copy); + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + } + + /* Matching Replacement Resolution */ + if (flag_GetFlagValue(Flags, flag_RFMRR)) { + red_MatchingReplacementResolution(*Clause, Index, Flags, Precedence, + &Copy, prfs_LastBacktrackLevel(Search)); + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + } + + /* Unit Conflict */ + if (flag_GetFlagValue(Flags, flag_RUNC)) { + red_UnitConflict(*Clause, Index, Flags, Precedence, + &Copy, prfs_LastBacktrackLevel(Search)); + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + } + + /* Static Soft Typing */ + if (red_OnlyWorkedOffMode(Mode) && flag_GetFlagValue(Flags, flag_RSST)) + Redundant = red_ClauseDeletion(prfs_StaticSortTheory(Search),*Clause, + Flags, Precedence); + +#ifdef CHECK + clause_Check(*Clause, Flags, Precedence); +#endif + + return Redundant; +} + +static BOOL red_SelectedStaticReductions(PROOFSEARCH Search, CLAUSE *Clause, + CLAUSE *Subsumer, LIST* Result, + NAT Mode) +/********************************************************** + INPUT: A proof search object, a clause (by reference) to be reduced, + and the mode of the reductions, determining which sets + (Usable, WorkedOff) in <Search> are considered for reductions. + EFFECT: Used reductions are tautology deletion, obvious reductions, + forward subsumption, forward rewriting, forward matching + replacement resolution, sort simplification, unit conflict + and static soft typing. + Depending on <Mode>, the clauses are reduced with respect + to WorkedOff and/or Usable Clauses. + RETURNS: TRUE iff the clause is redundant. + If the <DocProof> flag is false and no copying is necessary + with respect to splitting, the clause is destructively changed, + otherwise (intermediate) copies are made and returned in <*Result>. + If <Clause> gets redundant with respect to forward subsumption, + the subsuming clause is returned in <*Subsumer>. +***********************************************************/ +{ + CLAUSE Copy; + BOOL Redundant ,Rewritten, Tried, ContextualRew, StandardRew; + SHARED_INDEX WoIndex,UsIndex; + FLAGSTORE Flags; + PRECEDENCE Precedence; + + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + +#ifdef CHECK + if (!clause_IsClause(*Clause, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_SelectedStaticReductions:"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(*Clause, Flags, Precedence); +#endif + + WoIndex = (SHARED_INDEX)NULL; + UsIndex = (SHARED_INDEX)NULL; + if (red_WorkedOffMode(Mode)) + WoIndex = prfs_WorkedOffSharingIndex(Search); + if (red_UsableMode(Mode)) + UsIndex = prfs_UsableSharingIndex(Search); + Copy = (CLAUSE)NULL; + Redundant = red_SimpleStaticReductions(Clause, Flags, Precedence, Result); + + if (Redundant) + return Redundant; + + if (flag_GetFlagValue(Flags, flag_RAED) != flag_RAEDOFF && + red_AssignmentEquationDeletion(*Clause, Flags, Precedence, &Copy, + prfs_NonTrivClauseNumber(Search), + (flag_GetFlagValue(Flags, flag_RAED)==flag_RAEDPOTUNSOUND))) { + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + } + + if (flag_GetFlagValue(Flags, flag_RFSUB)) { + *Subsumer = (CLAUSE)NULL; + if (WoIndex != NULL) { + *Subsumer = red_ForwardSubsumption(*Clause, WoIndex, Flags, Precedence); + if (*Subsumer != (CLAUSE)NULL) + return TRUE; + } + if (UsIndex != NULL) { + *Subsumer = red_ForwardSubsumption(*Clause, UsIndex, Flags, Precedence); + if (*Subsumer != (CLAUSE)NULL) + return TRUE; + } + } + + StandardRew = flag_GetFlagValue(Flags, flag_RFREW); + ContextualRew = flag_GetFlagValue(Flags, flag_RFCRW); + + Rewritten = (StandardRew || ContextualRew); + Tried = FALSE; + while (Rewritten) { + Rewritten = FALSE; + + if (WoIndex != NULL && + ((StandardRew && + red_RewriteRedClause(*Clause, WoIndex, Flags, Precedence, &Copy, + prfs_LastBacktrackLevel(Search))) || + (ContextualRew && + red_ContextualRewriting(Search, *Clause, red_WORKEDOFF, + prfs_LastBacktrackLevel(Search), &Copy)))) { + Rewritten = TRUE; + red_ExchangeClauses(Clause, &Copy, Result); + Redundant = red_SimpleStaticReductions(Clause, Flags, + Precedence, Result); + if (Redundant) + return Redundant; + if (clause_IsEmptyClause(*Clause)) + return FALSE; + if (flag_GetFlagValue(Flags, flag_RFSUB)) { + *Subsumer = (CLAUSE)NULL; + *Subsumer = red_ForwardSubsumption(*Clause, WoIndex, + Flags, Precedence); + if (*Subsumer != (CLAUSE)NULL) + return TRUE; /* Clause is redundant */ + if (UsIndex != NULL) { + *Subsumer = red_ForwardSubsumption(*Clause, UsIndex, + Flags, Precedence); + if (*Subsumer != (CLAUSE)NULL) + return TRUE; + } + } + } + + if (UsIndex != NULL && + (!Tried || Rewritten) && + ((StandardRew && + red_RewriteRedClause(*Clause, UsIndex, Flags, Precedence, + &Copy, prfs_LastBacktrackLevel(Search))) || + (ContextualRew && + red_ContextualRewriting(Search, *Clause, red_USABLE, + prfs_LastBacktrackLevel(Search), &Copy)))) { + Rewritten = TRUE; + red_ExchangeClauses(Clause, &Copy, Result); + Redundant = red_SimpleStaticReductions(Clause, Flags, + Precedence, Result); + if (Redundant) + return Redundant; + if (clause_IsEmptyClause(*Clause)) + return FALSE; + if (flag_GetFlagValue(Flags, flag_RFSUB)) { + *Subsumer = (CLAUSE)NULL; + if (WoIndex != NULL) + *Subsumer = red_ForwardSubsumption(*Clause, WoIndex, + Flags, Precedence); + if (*Subsumer != (CLAUSE)NULL) + return TRUE; + *Subsumer = red_ForwardSubsumption(*Clause, UsIndex, + Flags, Precedence); + if (*Subsumer != (CLAUSE)NULL) + return TRUE; + } + } + + Tried = TRUE; + } /* end of while(Rewritten) */ + + + if (flag_GetFlagValue(Flags, flag_RSSI)) { + red_SortSimplification(prfs_DynamicSortTheory(Search), *Clause, + prfs_LastBacktrackLevel(Search), + flag_GetFlagValue(Flags, flag_DOCPROOF), + Flags, Precedence, &Copy); + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + } + + if (flag_GetFlagValue(Flags, flag_RFMRR)) { + if (WoIndex) + red_MatchingReplacementResolution(*Clause, WoIndex, Flags, Precedence, + &Copy, prfs_LastBacktrackLevel(Search)); + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + if (UsIndex) + red_MatchingReplacementResolution(*Clause, UsIndex, Flags, Precedence, + &Copy, prfs_LastBacktrackLevel(Search)); + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + } + + if (flag_GetFlagValue(Flags, flag_RUNC)) { + if (WoIndex) + red_UnitConflict(*Clause, WoIndex, Flags, Precedence, + &Copy, prfs_LastBacktrackLevel(Search)); + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + if (UsIndex) + red_UnitConflict(*Clause, UsIndex, Flags, Precedence, + &Copy, prfs_LastBacktrackLevel(Search)); + red_ExchangeClauses(Clause, &Copy, Result); + if (clause_IsEmptyClause(*Clause)) + return FALSE; + } + + if (flag_GetFlagValue(Flags, flag_RSST)) + Redundant = red_ClauseDeletion(prfs_StaticSortTheory(Search),*Clause, + Flags, Precedence); + +#ifdef CHECK + clause_Check(*Clause, Flags, Precedence); +#endif + + return Redundant; +} + + +CLAUSE red_ReductionOnDerivedClause(PROOFSEARCH Search, CLAUSE Clause, + NAT Mode) +/************************************************************** + INPUT: A proof search object, a derived clause and a mode + indicating which indexes should be used for reductions. + RETURNS: The non-redundant clause after reducing <Clause>, + NULL if <Clause> is redundant. + EFFECT: Clauses probably generated, but redundant are kept according + to the <DocProof> flag and the split level of involved clauses. + depending on <Mode>, then clauses are reduced + with respect to WorkedOff and/or Usable Clauses. +***************************************************************/ +{ + CLAUSE RedClause; + LIST Redundant; + +#ifdef CHECK + cont_SaveState(); +#endif + + Redundant = list_Nil(); + RedClause = (CLAUSE)NULL; + + if (red_StaticReductions(Search,&Clause,&RedClause,&Redundant,Mode)) { + /* Clause is redundant */ + red_HandleRedundantDerivedClauses(Search, Redundant, Clause); + list_Delete(Redundant); + if (RedClause && + 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); + Clause = (CLAUSE)NULL; + } + else { + red_HandleRedundantDerivedClauses(Search, Redundant, Clause); + list_Delete(Redundant); + } + +#ifdef CHECK + cont_CheckState(); +#endif + + return Clause; +} + +CLAUSE red_CompleteReductionOnDerivedClause(PROOFSEARCH Search, CLAUSE Clause, + NAT Mode) +/************************************************************** + INPUT: A proof search object, a derived clause and a mode determining + which clauses to consider for reduction. + RETURNS: The non-redundant clause after reducing <Clause>, + NULL if <Clause> is redundant. + EFFECT: Clauses probably generated, but redundant are kept according + to the <DocProof> flag and the split level of involved clauses. + The clause is reduced with respect to all indexes determined + by <Mode> +***************************************************************/ +{ + CLAUSE RedClause; + LIST Redundant; + +#ifdef CHECK + cont_SaveState(); +#endif + + Redundant = list_Nil(); + RedClause = (CLAUSE)NULL; + + if (red_SelectedStaticReductions(Search,&Clause,&RedClause,&Redundant,Mode)) { + /* <Clause> is redundant */ + red_HandleRedundantDerivedClauses(Search, Redundant, Clause); + list_Delete(Redundant); + if (RedClause && + 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); + Clause = (CLAUSE)NULL; + } + else { + red_HandleRedundantDerivedClauses(Search, Redundant, Clause); + list_Delete(Redundant); + } + +#ifdef CHECK + cont_CheckState(); +#endif + + return Clause; +} + + +LIST red_BackReduction(PROOFSEARCH Search, CLAUSE Clause, NAT Mode) +/************************************************************** + INPUT: A proof search object, a clause and a mode flag. + RETURNS: A list of reduced clauses in usable and worked-off + (depending on <Mode>) in <Search> with respect to <Clause>. + The original clauses that become redundant are either deleted + or kept for proof documentation or splitting. + EFFECT: The original clauses that become redundant are either deleted + or kept for proof documentation or splitting. +***************************************************************/ +{ + LIST Result, Redundant; + FLAGSTORE Flags; + PRECEDENCE Precedence; + +#ifdef CHECK + cont_SaveState(); +#endif + + Result = list_Nil(); + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + /* Subsumption */ + if (flag_GetFlagValue(Flags, flag_RBSUB)) { + Redundant = list_Nil(); + if (red_WorkedOffMode(Mode)) + Redundant = red_BackSubsumption(Clause, + prfs_WorkedOffSharingIndex(Search), + Flags, Precedence); + if (red_UsableMode(Mode)) + Redundant = list_Nconc(Redundant, + red_BackSubsumption(Clause, + prfs_UsableSharingIndex(Search), + Flags, Precedence)); + red_HandleRedundantIndexedClauses(Search, Redundant, Clause); + list_Delete(Redundant); + } + + /* Matching Replacement Resolution */ + if (flag_GetFlagValue(Flags, flag_RBMRR)) { + Redundant = list_Nil(); + if (red_WorkedOffMode(Mode)) + Redundant = red_BackMatchingReplacementResolution(Clause, + prfs_WorkedOffSharingIndex(Search), + Flags, Precedence, &Result); + if (red_UsableMode(Mode)) + Redundant = list_Nconc(Redundant, + red_BackMatchingReplacementResolution(Clause, + prfs_UsableSharingIndex(Search), + Flags, Precedence, &Result)); + red_HandleRedundantIndexedClauses(Search, Redundant, Clause); + list_Delete(Redundant); + } + + /* Standard Rewriting */ + if (flag_GetFlagValue(Flags, flag_RBREW)) { + Redundant = list_Nil(); + if (red_WorkedOffMode(Mode)) + Redundant = red_BackRewriting(Clause,prfs_WorkedOffSharingIndex(Search), + Flags, Precedence, &Result); + if (red_UsableMode(Mode)) + Redundant = list_Nconc(Redundant, + red_BackRewriting(Clause, + prfs_UsableSharingIndex(Search), + Flags, Precedence, &Result)); + + red_HandleRedundantIndexedClauses(Search, Redundant, Clause); + list_Delete(Redundant); + } + + /* Contextual Rewriting */ + if (flag_GetFlagValue(Flags, flag_RBCRW)) { + Redundant = list_Nil(); + if (red_WorkedOffMode(Mode)) + Redundant = red_BackContextualRewriting(Search, Clause, red_WORKEDOFF, + &Result); + if (red_UsableMode(Mode)) + Redundant = list_Nconc(Redundant, + red_BackContextualRewriting(Search, Clause, + red_USABLE, &Result)); + + red_HandleRedundantIndexedClauses(Search, Redundant, Clause); + list_Delete(Redundant); + } + +#ifdef CHECK + cont_CheckState(); +#endif + + return Result; +} + + +static __inline__ LIST red_MergeClauseListsByWeight(LIST L1, LIST L2) +/************************************************************** + INPUT: Two lists of clauses, sorted by weight. + RETURNS: + EFFECT: +***************************************************************/ +{ + return list_NNumberMerge(L1, L2, (NAT (*)(POINTER))clause_Weight); +} + + +LIST red_CompleteReductionOnDerivedClauses(PROOFSEARCH Search, + LIST DerivedClauses, NAT Mode, + int Bound, NAT BoundMode, + int *BoundApplied) +/************************************************************** + INPUT: A proof search object, a list of newly derived (unshared) clauses, + a mode determining which clause lists to consider for reduction, + a bound and a bound mode to cut off generated clauses. + RETURNS: A list of empty clauses that may be derived during the + reduction process. + <*BoundApplied> is set to the mode dependent value of the + smallest clause if a clause is deleted because of a bound. + EFFECT: The <DerivedClauses> are destructively reduced and reduced clauses + from the indexes are checked out and all finally reduced clauses + are checked into the indexes. Depending on <Mode> either the + WorkedOff, Usable or both indexes are considered. + The <DocProof> Flag is considered. +***************************************************************/ +{ + LIST EmptyClauses,NewClauses,Scan; + NAT ClauseBound; + CLAUSE Clause; + FLAGSTORE Flags; + +#ifdef CHECK + cont_SaveState(); +#endif + + EmptyClauses = list_Nil(); + DerivedClauses = clause_ListSortWeighed(DerivedClauses); + ClauseBound = 0; + Flags = prfs_Store(Search); + + while (!list_Empty(DerivedClauses)) { +#ifdef WIN + clock_PingOneSecond(); +#endif + Clause = list_NCar(&DerivedClauses); + if (prfs_SplitStackEmpty(Search)) /* Otherwise splitting not compatible with bound deletion */ + Clause = red_CompleteReductionOnDerivedClause(Search, Clause, Mode); + + if (Clause != NULL && BoundMode != flag_BOUNDMODEUNLIMITED && + Bound != flag_BOUNDSTARTUNLIMITED && !clause_IsFromInput(Clause) && + !clause_IsFromSplitting(Clause)) { + switch (BoundMode) { + case flag_BOUNDMODERESTRICTEDBYWEIGHT: + ClauseBound = clause_Weight(Clause); + break; + case flag_BOUNDMODERESTRICTEDBYDEPTH: + ClauseBound = clause_ComputeTermDepth(Clause); + break; + default: + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error while applying bound restrictions:"); + misc_UserErrorReport("\n You selected an unknown bound mode.\n"); + misc_FinishUserErrorReport(); + } + if (ClauseBound > Bound) { + if (flag_GetFlagValue(Flags, flag_PBDC)) { + fputs("\nDeleted by bound: ", stdout); + clause_Print(Clause); + } + clause_Delete(Clause); + if (*BoundApplied == -1 || ClauseBound < *BoundApplied) + *BoundApplied = ClauseBound; + Clause = (CLAUSE)NULL; + } + } + + if (Clause != (CLAUSE)NULL && /* For clauses below bound, splitting is */ + !prfs_SplitStackEmpty(Search)) /* compatible with bound deletion */ + Clause = red_CompleteReductionOnDerivedClause(Search, Clause, Mode); + + if (Clause) { + prfs_IncKeptClauses(Search); + if (flag_GetFlagValue(Flags, flag_PKEPT)) { + fputs("\nKept: ", stdout); + clause_Print(Clause); + } + if (clause_IsEmptyClause(Clause)) + EmptyClauses = list_Cons(Clause,EmptyClauses); + else { + NewClauses = red_BackReduction(Search, Clause, Mode); + prfs_IncDerivedClauses(Search, list_Length(NewClauses)); + if (flag_GetFlagValue(Flags, flag_PDER)) + for (Scan=NewClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) { + fputs("\nDerived: ", stdout); + clause_Print(list_Car(Scan)); + } + NewClauses = split_ExtractEmptyClauses(NewClauses,&EmptyClauses); + + prfs_InsertUsableClause(Search,Clause); + NewClauses = list_NumberSort(NewClauses, (NAT (*) (POINTER)) clause_Weight); + DerivedClauses = red_MergeClauseListsByWeight(DerivedClauses,NewClauses); + } + } + } + +#ifdef CHECK + cont_CheckState(); +#endif + + return EmptyClauses; +} + + + +static CLAUSE red_CDForwardSubsumer(CLAUSE RedCl, st_INDEX Index, + FLAGSTORE Flags, PRECEDENCE Precedence) +/********************************************************** + INPUT: A pointer to a non-empty clause, an index of + clauses, a flag store and a precedence. + RETURNS: The first clause from the Approx Set which + subsumes 'RedCl'. +***********************************************************/ +{ + TERM Atom,AtomGen; + LIST LitScan; + int i,length; + CLAUSE CandCl; + +#ifdef CHECK + if (!clause_IsClause(RedCl, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_CDForwardSubsumer :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(RedCl, Flags, Precedence); +#endif + + length = clause_Length(RedCl); + + for (i = 0; i < length; i++) { + Atom = clause_GetLiteralAtom(RedCl, i); + AtomGen = st_ExistGen(cont_LeftContext(), Index, Atom); + + while (AtomGen) { + for (LitScan = term_SupertermList(AtomGen); + !list_Empty(LitScan); LitScan = list_Cdr(LitScan)) { + CandCl = clause_LiteralOwningClause(list_Car(LitScan)); + + if (clause_GetLiteral(CandCl,clause_FirstLitIndex()) == (LITERAL)list_Car(LitScan) && + subs_Subsumes(CandCl, RedCl, clause_FirstLitIndex(), i)) { + st_CancelExistRetrieval(); + return CandCl; + } + } + AtomGen = st_NextCandidate(); + } + } + return (CLAUSE)NULL; +} + + +static BOOL red_CDForwardSubsumption(CLAUSE RedClause, st_INDEX Index, + FLAGSTORE Flags, PRECEDENCE Precedence) +/********************************************************** + INPUT: A clause, an index of clauses, a flag store and + a precedence. + RETURNS: The boolean value TRUE if the clause is subsumed + by an indexed clause, if so, the clause is deleted, + either really or locally. +***********************************************************/ +{ + BOOL IsSubsumed; + CLAUSE Subsumer; + +#ifdef CHECK + if (!clause_IsClause(RedClause, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_CDForwardSubSumption :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(RedClause, Flags, Precedence); +#endif + IsSubsumed = FALSE; + Subsumer = red_CDForwardSubsumer(RedClause, Index, Flags, Precedence); + + if (clause_Exists(Subsumer)) { + IsSubsumed = TRUE; + + if (flag_GetFlagValue(Flags, flag_DOCSST) && + flag_GetFlagValue(Flags, flag_PSUB)) { + fputs("\nFSubsumption:", stdout); + clause_Print(RedClause); + printf(" by %d ",clause_Number(Subsumer)); + } + } + return IsSubsumed; +} + + +static void red_CDBackSubsumption(CLAUSE RedCl, FLAGSTORE Flags, + PRECEDENCE Precedence, + LIST* UsListPt, LIST* WOListPt, + st_INDEX Index) +/********************************************************** + INPUT: A pointer to a non-empty clause, a flag store, + a precedence, and an index of clauses. + RETURNS: Nothing. +***********************************************************/ +{ + TERM Atom,AtomInst; + CLAUSE SubsumedCl; + LIST Scan, SubsumedList; + +#ifdef CHECK + if (!clause_IsClause(RedCl, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_CDBackupSubSumption :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(RedCl, Flags, Precedence); +#endif + + SubsumedList = list_Nil(); + + if (!clause_IsEmptyClause(RedCl)) { + Atom = clause_GetLiteralAtom(RedCl, clause_FirstLitIndex()); + AtomInst = st_ExistInstance(cont_LeftContext(), Index, Atom); + + while(AtomInst) { + for (Scan = term_SupertermList(AtomInst); !list_Empty(Scan); Scan = list_Cdr(Scan)) { + SubsumedCl = clause_LiteralOwningClause(list_Car(Scan)); + if ((RedCl != SubsumedCl) && + subs_Subsumes(RedCl, SubsumedCl, clause_FirstLitIndex(), + clause_LiteralGetIndex(list_Car(Scan))) && + !list_PointerMember(SubsumedList, SubsumedCl)) + SubsumedList = list_Cons(SubsumedCl, SubsumedList); + } + AtomInst = st_NextCandidate(); + } + + for (Scan = SubsumedList; !list_Empty(Scan); Scan = list_Cdr(Scan)) { + SubsumedCl = list_Car(Scan); + + if (flag_GetFlagValue(Flags, flag_DOCSST) && flag_GetFlagValue(Flags, flag_PSUB)) { + fputs("\nBSubsumption: ", stdout); + clause_Print(SubsumedCl); + printf(" by %d ",clause_Number(RedCl)); + } + + + if (clause_GetFlag(SubsumedCl,WORKEDOFF)) { + *WOListPt = list_PointerDeleteOneElement(*WOListPt, SubsumedCl); + }else { + *UsListPt = list_PointerDeleteOneElement(*UsListPt, SubsumedCl); + } + clause_DeleteFlatFromIndex(SubsumedCl, Index); + } + list_Delete(SubsumedList); + } +} + + +static LIST red_CDDerivables(SORTTHEORY Theory, CLAUSE GivenClause, + FLAGSTORE Flags, PRECEDENCE Precedence) +/************************************************************** + INPUT: A sort theory, a clause, a flag store and a + precedence. + RETURNS: A list of clauses derivable from <GivenClause> and + the declaration clauses in <Theory>. +***************************************************************/ +{ + LIST ListOfDerivedClauses; + +#ifdef CHECK + if (!(clause_IsClause(GivenClause, Flags, Precedence))) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_CDDeriveables :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(GivenClause, Flags, Precedence); +#endif + + if (clause_HasTermSortConstraintLits(GivenClause)) + ListOfDerivedClauses = inf_ForwardSortResolution(GivenClause, + sort_TheoryIndex(Theory), + Theory, TRUE, + Flags, Precedence); + else + ListOfDerivedClauses = inf_ForwardEmptySort(GivenClause, + sort_TheoryIndex(Theory), + Theory, TRUE, + Flags, Precedence); + + return ListOfDerivedClauses; +} + + +static BOOL red_CDReduce(SORTTHEORY Theory, CLAUSE RedClause, + FLAGSTORE Flags, PRECEDENCE Precedence, + LIST *ApproxUsListPt, LIST *ApproxWOListPt, + st_INDEX Index) +/************************************************************** + INPUT: A sort theory, an unshared clause, a flag store, + a precedence, their index and two pointers to the + sort reduction subproof usable and worked off list. + RETURNS: TRUE iff <RedClause> is redundant with respect to + clauses in the index or theory. + EFFECT: <RedClause> is destructively changed. + The <DocProof> flag is changed temporarily. +***************************************************************/ +{ + CLAUSE Copy; + +#ifdef CHECK + clause_Check(RedClause, Flags, Precedence); +#endif + + Copy = (CLAUSE)NULL; /* Only needed for interface */ + + red_ObviousReductions(RedClause, FALSE, Flags, Precedence, &Copy); + red_SortSimplification(Theory, RedClause, NAT_MAX, FALSE, + Flags, Precedence, &Copy); + + if (clause_IsEmptyClause(RedClause)) + return FALSE; + + red_Condensing(RedClause, FALSE, Flags, Precedence, &Copy); + + if (red_CDForwardSubsumption(RedClause, Index, Flags, Precedence)) + return TRUE; + else { /* RedClause isn't subsumed! */ + red_CDBackSubsumption(RedClause, Flags, Precedence, + ApproxUsListPt, ApproxWOListPt, Index); + clause_InsertFlatIntoIndex(RedClause, Index); + *ApproxUsListPt = list_Cons(RedClause, *ApproxUsListPt); + } + +#ifdef CHECK + clause_Check(RedClause, Flags, Precedence); + if (Copy != (CLAUSE)NULL) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_CDReduce :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + +#endif + + return FALSE; +} + + +BOOL red_ClauseDeletion(SORTTHEORY Theory, CLAUSE RedClause, FLAGSTORE Flags, + PRECEDENCE Precedence) +/************************************************************** + INPUT: A sort theory, a clause (unshared), a flag store + and a precedence. + RETURNS: TRUE iff the sort constraint of the clause is + unsolvable with respect to the sort theory. +***************************************************************/ +{ + if (Theory != (SORTTHEORY)NULL) { + CLAUSE ConstraintClause, GivenClause; + LIST ApproxUsableList, ApproxWOList, EmptyClauses, ApproxDerivables, Scan; + int i,nc, Count, OldClauseCounter; + st_INDEX Index; + +#ifdef CHECK + if (!(clause_IsClause(RedClause, Flags, Precedence))) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_ClauseDeletion :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } + clause_Check(RedClause, Flags, Precedence); +#endif + + if (clause_HasEmptyConstraint(RedClause) || !flag_GetFlagValue(Flags, flag_RSST)) + return FALSE; + + if (flag_GetFlagValue(Flags, flag_DOCSST)) { + fputs("\n\nStatic Soft Typing tried on: ", stdout); + clause_Print(RedClause); + } + + Index = st_IndexCreate(); + Scan = list_Nil(); + nc = clause_NumOfConsLits(RedClause); + OldClauseCounter = clause_Counter(); + + /* Make constraint clause, insert it into the Approx-usable-list: */ + + for (i = clause_FirstLitIndex(); i < nc; i++) + Scan = list_Cons(term_Copy(clause_LiteralAtom( + clause_GetLiteral(RedClause, i))), Scan); + + Scan = list_NReverse(Scan); + ConstraintClause = clause_Create(Scan, list_Nil(), list_Nil(), + Flags, Precedence); + list_Delete(Scan); + clause_InitSplitData(ConstraintClause); + clause_AddParentClause(ConstraintClause, clause_Number(RedClause)); + clause_AddParentLiteral(ConstraintClause, clause_FirstLitIndex()); + clause_SetFromClauseDeletion(ConstraintClause); + clause_InsertFlatIntoIndex(ConstraintClause, Index); + ApproxUsableList = list_List(ConstraintClause); + ApproxWOList = list_Nil(); + + /* fputs("\nConstraint clause: ",stdout); clause_Print(ConstraintClause); */ + + /* Now the lists are initialized, the subproof is started: */ + + EmptyClauses = list_Nil(); + Count = 0; + + if (flag_GetFlagValue(Flags, flag_DOCSST)) { + puts("\n*************** Static Soft Typing Subproof: ***************"); + puts("The usable list:"); + clause_ListPrint(ApproxUsableList); + puts("\nThe worked-off list:"); + clause_ListPrint(ApproxWOList); + /* fputs("\nAll indexed clauses: ", stdout); + clause_PrintAllIndexedClauses(ShIndex); */ + } + while (!list_Empty(ApproxUsableList) && list_Empty(EmptyClauses)) { + GivenClause = list_Car(ApproxUsableList); + clause_SetFlag(GivenClause,WORKEDOFF); + + if (flag_GetFlagValue(Flags, flag_DOCSST)) { + fputs("\n\tSubproof Given clause: ", stdout); + clause_Print(GivenClause); fflush(stdout); + } + ApproxWOList = list_Cons(GivenClause, ApproxWOList); + ApproxUsableList = list_PointerDeleteOneElement(ApproxUsableList,GivenClause); + ApproxDerivables = red_CDDerivables(Theory,GivenClause, Flags, Precedence); + ApproxDerivables = split_ExtractEmptyClauses(ApproxDerivables, &EmptyClauses); + + if (!list_Empty(EmptyClauses)) { /* Exit while loop! */ + if (flag_GetFlagValue(Flags, flag_DOCSST)) { + fputs("\nStatic Soft Typing not successful: ", stdout); + clause_Print(list_Car(EmptyClauses)); + } + clause_DeleteClauseList(ApproxDerivables); + ApproxDerivables = list_Nil(); + } + else { + CLAUSE DerClause; + for (Scan = ApproxDerivables; !list_Empty(Scan) && list_Empty(EmptyClauses); + Scan = list_Cdr(Scan)) { + DerClause = (CLAUSE)list_Car(Scan); + if (red_CDReduce(Theory, DerClause, Flags, Precedence, + &ApproxUsableList, &ApproxWOList, Index)) + clause_Delete(DerClause); + else{ + Count++; + if (flag_GetFlagValue(Flags, flag_DOCSST)) { + putchar('\n'); + clause_Print(DerClause); + } + if (clause_IsEmptyClause(DerClause)) + EmptyClauses = list_Cons(DerClause,EmptyClauses); + } + list_Rplaca(Scan,(CLAUSE)NULL); + } + + if (!list_Empty(EmptyClauses)) { + if (flag_GetFlagValue(Flags, flag_DOCSST)) { + fputs(" Static Soft Typing not successful!", stdout); + clause_Print(list_Car(EmptyClauses)); + } + clause_DeleteClauseList(ApproxDerivables); /* There still may be clauses in the list */ + ApproxDerivables = list_Nil(); + } + else { + list_Delete(ApproxDerivables); + ApproxDerivables = list_Nil(); + } + } + } + + if (!list_Empty(EmptyClauses)) { + if (flag_GetFlagValue(Flags, flag_DOCSST)) { + puts("\nStatic Soft Typing failed, constraint solvable."); + puts("************ Static Soft Typing Subproof finished. ************"); + } + } + else + if (flag_GetFlagValue(Flags, flag_PSST)) { + fputs("\nStatic Soft Typing deleted: ", stdout); + clause_Print(RedClause); + } + + /* Cleanup */ + clause_DeleteClauseListFlatFromIndex(ApproxUsableList, Index); + clause_DeleteClauseListFlatFromIndex(ApproxWOList, Index); + st_IndexDelete(Index); + clause_SetCounter(OldClauseCounter); + + if (!list_Empty(EmptyClauses)) { + clause_DeleteClauseList(EmptyClauses); + return FALSE; + } + + return TRUE; + +#ifdef CHECK + clause_Check(RedClause, Flags, Precedence); +#endif + } + return FALSE; +} + +LIST red_SatUnit(PROOFSEARCH Search, LIST ClauseList) +/********************************************************* + INPUT: A proof search object and a list of unshared clauses. + RETURNS: A possibly empty list of empty clauses. + EFFECT: Does a shallow saturation of the conclauses depending on the + flag_SATUNIT flag. + The <DocProof> flag is considered. +**********************************************************/ +{ + CLAUSE Given,Clause; + LIST Scan, Derivables, EmptyClauses, BackReduced; + NAT n, Derived; + FLAGSTORE Flags; + PRECEDENCE Precedence; + + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + Derived = flag_GetFlagValue(Flags, flag_CNFPROOFSTEPS); + EmptyClauses = list_Nil(); + + ClauseList = clause_ListSortWeighed(ClauseList); + + while (!list_Empty(ClauseList) && list_Empty(EmptyClauses)) { + Given = (CLAUSE)list_NCar(&ClauseList); + Given = red_ReductionOnDerivedClause(Search, Given, red_USABLE); + if (Given) { + if (clause_IsEmptyClause(Given)) + EmptyClauses = list_List(Given); + else { + BackReduced = red_BackReduction(Search, Given, red_USABLE); + + if (Derived != 0) { + Derivables = inf_BoundedDepthUnitResolution(Given, + prfs_UsableSharingIndex(Search), + FALSE, Flags, Precedence); + n = list_Length(Derivables); + if (n > Derived) + Derived = 0; + else + Derived = Derived - n; + } + else + Derivables = list_Nil(); + + Derivables = list_Nconc(BackReduced,Derivables); + Derivables = split_ExtractEmptyClauses(Derivables, &EmptyClauses); + + prfs_InsertUsableClause(Search, Given); + + for(Scan = Derivables; !list_Empty(Scan); Scan = list_Cdr(Scan)) { + Clause = (CLAUSE)list_Car(Scan); + clause_SetDepth(Clause,0); + } + ClauseList = list_Nconc(ClauseList,Derivables); + Derivables = list_Nil(); + } + } + } + for(Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan)) + prfs_InsertUsableClause(Search, list_Car(Scan)); + list_Delete(ClauseList); + return EmptyClauses; +} + +static CLAUSE red_SpecialInputReductions(CLAUSE Clause, FLAGSTORE Flags, + PRECEDENCE Precedence) +/********************************************************* + INPUT: A clause and a flag store. + RETURNS: The clause where the logical constants TRUE, FALSE + are removed. + EFFECT: The clause is destructively changed. +**********************************************************/ +{ + int i,end; + LIST Indexes; + TERM Atom; + +#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_IsTrue(Atom)) + Indexes = list_Cons((POINTER)i,Indexes); + } + + end = clause_LastSuccedentLitIndex(Clause); + + for (i = clause_FirstSuccedentLitIndex(Clause); i <= end; i++) { + Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i)); + if (fol_IsFalse(Atom)) + Indexes = list_Cons((POINTER)i,Indexes); + } + + clause_DeleteLiterals(Clause,Indexes, Flags, Precedence); + list_Delete(Indexes); + + return Clause; +} + + +LIST red_ReduceInput(PROOFSEARCH Search, LIST ClauseList) +/********************************************************* + INPUT: A proof search object and a list of unshared clauses. + RETURNS: A list of empty clauses. + EFFECT: Interreduces the clause list and inserts the clauses into <Search>. + Keeps track of derived and kept clauses. + Time limits and the DocProof flag are considered. +**********************************************************/ +{ + CLAUSE Given; + LIST Scan, EmptyClauses, BackReduced; + FLAGSTORE Flags; + PRECEDENCE Precedence; + + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + EmptyClauses = list_Nil(); + ClauseList = clause_ListSortWeighed(list_Copy(ClauseList)); + ClauseList = split_ExtractEmptyClauses(ClauseList, &EmptyClauses); + + while (!list_Empty(ClauseList) && list_Empty(EmptyClauses) && + (flag_GetFlagValue(Flags,flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED || + flag_GetFlagValue(Flags, flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) { + Given = (CLAUSE)list_NCar(&ClauseList); +#ifdef CHECK + if (!clause_IsClause(Given, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_ReduceInput :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + Given = red_SpecialInputReductions(Given, Flags, Precedence); + Given = red_ReductionOnDerivedClause(Search, Given, red_USABLE); + if (Given) { + prfs_IncKeptClauses(Search); + if (clause_IsEmptyClause(Given)) + EmptyClauses = list_List(Given); + else { + BackReduced = red_BackReduction(Search, Given, red_USABLE); + prfs_IncDerivedClauses(Search, list_Length(BackReduced)); + BackReduced = split_ExtractEmptyClauses(BackReduced, &EmptyClauses); + prfs_InsertUsableClause(Search, Given); + BackReduced = clause_ListSortWeighed(BackReduced); + ClauseList = red_MergeClauseListsByWeight(ClauseList, BackReduced); + } + } + } + for(Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan)) + prfs_InsertUsableClause(Search, list_Car(Scan)); + list_Delete(ClauseList); + return EmptyClauses; +} + + +LIST red_SatInput(PROOFSEARCH Search) +/********************************************************* + INPUT: A proof search object. + RETURNS: A list of derived empty clauses. + EFFECT: Does a saturation from the conjectures into the axioms/conjectures + Keeps track of derived and kept clauses. Keeps track of a possible + time limit. + Considers the Usable clauses in <Search> and a possible time limit. +**********************************************************/ +{ + CLAUSE Given; + LIST Scan, ClauseList, Derivables, EmptyClauses; + int n; + FLAGSTORE Flags; + PRECEDENCE Precedence; + + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + EmptyClauses = list_Nil(); + ClauseList = list_Nil(); + Scan = prfs_UsableClauses(Search); + n = list_Length(Scan); + + while(!list_Empty(Scan) && + n > 0 && + (flag_GetFlagValue(Flags,flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED || + flag_GetFlagValue(Flags, flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) { + Given = (CLAUSE)list_Car(Scan); + if (clause_GetFlag(Given,CONCLAUSE)) { + Derivables = inf_BoundedDepthUnitResolution(Given, + prfs_UsableSharingIndex(Search), + FALSE, Flags, Precedence); + n -= list_Length(Derivables); + ClauseList = list_Nconc(Derivables,ClauseList); + } + Scan = list_Cdr(Scan); + } + + prfs_IncDerivedClauses(Search, list_Length(ClauseList)); + EmptyClauses = red_ReduceInput(Search, ClauseList); + list_Delete(ClauseList); + ClauseList = list_Nil(); + if (list_Empty(EmptyClauses)) { + Scan=prfs_UsableClauses(Search); + while (!list_Empty(Scan) && + n > 0 && + (flag_GetFlagValue(Flags,flag_TIMELIMIT)==flag_TIMELIMITUNLIMITED || + flag_GetFlagValue(Flags, flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) { + Given = (CLAUSE)list_Car(Scan); + if (clause_GetFlag(Given,CONCLAUSE) && clause_IsFromInput(Given)) { + Derivables = inf_BoundedDepthUnitResolution(Given, + prfs_UsableSharingIndex(Search), + TRUE, Flags, Precedence); + n -= list_Length(Derivables); + ClauseList = list_Nconc(Derivables,ClauseList); + } + Scan = list_Cdr(Scan); + } + prfs_IncDerivedClauses(Search, list_Length(ClauseList)); + EmptyClauses = red_ReduceInput(Search, ClauseList); + list_Delete(ClauseList); + } + return EmptyClauses; +} + +void red_CheckSplitSubsumptionCondition(PROOFSEARCH Search) +/********************************************************* + INPUT: A proof search object. + EFFECT: For all deleted clauses in the split stack, it + is checked whether they are subsumed by some + existing clause. If they are not, a core is dumped. + Used for debugging. +**********************************************************/ +{ + LIST Scan1,Scan2; + CLAUSE Clause; + FLAGSTORE Flags; + PRECEDENCE Precedence; + + Flags = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + for (Scan1=prfs_SplitStack(Search);!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) + for (Scan2=prfs_SplitDeletedClauses(list_Car(Scan1));!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) { + Clause = (CLAUSE)list_Car(Scan2); + if (!red_ForwardSubsumer(Clause, prfs_WorkedOffSharingIndex(Search), + Flags, Precedence) && + !red_ForwardSubsumer(Clause, prfs_UsableSharingIndex(Search), + Flags, Precedence) && + !red_ClauseDeletion(prfs_StaticSortTheory(Search),Clause, + Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In red_CheckSplitSubsumptionCondition: No clause found implying "); + clause_Print(Clause); + misc_ErrorReport("\n Current Split: "); + prfs_PrintSplit(list_Car(Scan1)); + misc_FinishErrorReport(); + } + } +} |