/**************************************************************/ /* ********************************************************** */ /* * * */ /* * REDUCTION RULES * */ /* * * */ /* * $Module: REDRULES * */ /* * * */ /* * Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001 * */ /* * MPI fuer Informatik * */ /* * * */ /* * This program is free software; you can redistribute * */ /* * it and/or modify it under the terms of the GNU * */ /* * General Public License as published by the Free * */ /* * Software Foundation; either version 2 of the License, * */ /* * or (at your option) any later version. * */ /* * * */ /* * This program is distributed in the hope that it will * */ /* * be useful, but WITHOUT ANY WARRANTY; without even * */ /* * the implied warranty of MERCHANTABILITY or FITNESS * */ /* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ /* * License for more details. * */ /* * * */ /* * You should have received a copy of the GNU General * */ /* * Public License along with this program; if not, write * */ /* * to the Free Software Foundation, Inc., 59 Temple * */ /* * Place, Suite 330, Boston, MA 02111-1307 USA * */ /* * * */ /* * * */ /* $Revision$ * */ /* $State$ * */ /* $Date$ * */ /* $Author$ * */ /* * * */ /* * Contact: * */ /* * Christoph Weidenbach * */ /* * MPI fuer Informatik * */ /* * Stuhlsatzenhausweg 85 * */ /* * 66123 Saarbruecken * */ /* * Email: weidenb@mpi-sb.mpg.de * */ /* * Germany * */ /* * * */ /* ********************************************************** */ /**************************************************************/ /* $RCSfile$ */ #include "rules-red.h" /**************************************************************/ /* ********************************************************** */ /* * * */ /* * Globals * */ /* * * */ /* ********************************************************** */ /**************************************************************/ /* Needed for term stamping in red_RewriteRedUnitClause */ static NAT red_STAMPID; const NAT red_USABLE = 1; const NAT red_WORKEDOFF = 2; const NAT red_ALL = 3; /**************************************************************/ /* FUNTION PROTOTYPES */ /**************************************************************/ static BOOL red_SortSimplification(SORTTHEORY, CLAUSE, NAT, BOOL, FLAGSTORE, PRECEDENCE, CLAUSE*); static BOOL red_SelectedStaticReductions(PROOFSEARCH, CLAUSE*, CLAUSE*, LIST*, NAT); /**************************************************************/ /* ********************************************************** */ /* * * */ /* * Functions * */ /* * * */ /* ********************************************************** */ /**************************************************************/ static void red_HandleRedundantIndexedClauses(PROOFSEARCH Search, LIST Blocked, CLAUSE RedClause) /********************************************************* INPUT: A proof search object, a list of clauses from the proof search object and a clause that causes the already indexed clauses in 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 of clauses from the proof search object and a clause that causes the derived clauses in 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 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 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 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 . If 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 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 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 , 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 is reduced by a clause of higher split level than . RETURNS: TRUE if reduction wrt the indexed clauses was possible. If the flag is true or the clauses used for reductions have a higher split level then a changed copy is returned in <*Changed>. Otherwise 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 is reduced by a clause of higher split level than . RETURNS: TRUE if a unit conflict with and the clauses in happened. If the flag is true or the clauses used for reductions have a higher split level then a changed copy is returned in <*Changed>. Otherwise 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 , 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 is subsumed by in . ***********************************************************/ { 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 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 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 is reduced by a clause of higher split level than . RETURNS: TRUE iff rewriting was possible. If the 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 is reduced by a clause of higher split level than . RETURNS: NULL, if no rewriting was possible. If the 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 is the bigger term of an oriented */ /* equation and all variables in 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 are from /. */ 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 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 (NULL, if is not subsumed), and the clause number of 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 accordingly. The clause was derived in several steps C1 -> C2 -> ... Cn -> from some clause C1. contains all those clauses C1, ..., Cn. This function first collects the parent information from the clauses C1, C2, ..., Cn, . All those clauses were needed to derive , 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 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 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 . */ 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 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 . The flag store and the precedence are only needed for term comparisons with respect to the reduction ordering. CAUTION: 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)) { /* 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 in by */ 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 in 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 or . */ if (DocProof) /* If 'DocProof' is turned on, a copy was created and assigned */ /* to . */ 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); /* was possibly changed by some reductions, so mark it as */ /* temporary again. */ /* Invoke tautology test if isn't redundant. */ if (Redundant || (!clause_IsEmptyClause(aux) && cc_Tautology(aux))) { if (NewClause != NULL) /* is subsumed by */ 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), is a subterm of literal in , 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 in is not greater than literal in with the substitution applied. In this case is set to NULL. TRUE is returned if the clauses passed all tautology tests and literal in is greater than literal in with the substitution applied. In some cases 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 flag is true, the information about parent clauses is set in , too. MEMORY: Remember to delete the 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 %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 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 */ 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 except */ 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 in RuleCopy */ clause_UpdateSplitDataFromPartner(RuleCopy, aux); /* Collect additonal parent information, if 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: is rewritten for the first time by Contextual Rewriting. This function sets the parent clause and parent literal information in . 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 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: 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 . 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 is reduced by a clause of higher split level than , 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 flag is true or the split level of the rewrite rule is higher than , a copy of 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 */ /* */ 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 that is reducible by via clause reduction. The return value stored in <*Result> contains the result of this operation. If the 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 */ 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 that can be rewritten, a flag store and a precedence. RETURNS: Nothing. EFFECT: The atom of literal pli in PartnerClause is destructively changed !!! The 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 and . The rewritten clauses are stored in <*Result>. EFFECT: The 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 and the result of this operation is stored in <*Result>. EFFECT: The 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 and . The rewritten clauses are stored in <*Result>. EFFECT: The 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 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 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 . The clauses resulting from the rewriting steps are stored in <*Result>. EFFECT: The 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 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 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 are considered for reductions. RETURNS: TRUE iff the clause is redundant. If the 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 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 , 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 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 , the clauses are reduced with respect to WorkedOff and/or Usable Clauses. RETURNS: TRUE iff the clause is redundant. If the 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 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 , NULL if is redundant. EFFECT: Clauses probably generated, but redundant are kept according to the flag and the split level of involved clauses. depending on , 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 , NULL if is redundant. EFFECT: Clauses probably generated, but redundant are kept according to the flag and the split level of involved clauses. The clause is reduced with respect to all indexes determined by ***************************************************************/ { CLAUSE RedClause; LIST Redundant; #ifdef CHECK cont_SaveState(); #endif Redundant = list_Nil(); RedClause = (CLAUSE)NULL; if (red_SelectedStaticReductions(Search,&Clause,&RedClause,&Redundant,Mode)) { /* 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 ) in with respect to . 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 are destructively reduced and reduced clauses from the indexes are checked out and all finally reduced clauses are checked into the indexes. Depending on either the WorkedOff, Usable or both indexes are considered. The 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 and the declaration clauses in . ***************************************************************/ { 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 is redundant with respect to clauses in the index or theory. EFFECT: is destructively changed. The 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 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 . 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 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(); } } }