/**************************************************************/ /* ********************************************************** */ /* * * */ /* * SPLITTING OF CLAUSES * */ /* * * */ /* * $Module: SPLIT * */ /* * * */ /* * Copyright (C) 1996, 1997, 1998, 2000 * */ /* * 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$ */ /**************************************************************/ /* Includes */ /**************************************************************/ #include "rules-split.h" static LIST split_DeleteClausesDependingOnLevelFromList(PROOFSEARCH,LIST, int, LIST*); static LIST split_DeleteInvalidClausesFromList(PROOFSEARCH, int, LIST); static void split_DeleteInvalidClausesFromStack(PROOFSEARCH); static LIST split_RemoveUnnecessarySplits(PROOFSEARCH, CLAUSE); /**************************************************************/ /* Functions */ /**************************************************************/ LIST split_Backtrack(PROOFSEARCH PS, CLAUSE EmptyClause, CLAUSE* SplitClause) /************************************************************** INPUT: A proofsearch object, an empty clause and a pointer to a clause used as return value. RETURNS: A list of clauses deleted in the backtracked split levels. <*SplitClause> is set to the split clause for the right branch of the splitting step, or NULL, if the tableau is finished. EFFECT: Backtracks the top of the split stack wrt the empty clause's level ***************************************************************/ { SPLIT ActBacktrackSplit; LIST RecoverList, Scan; int Backtracklevel; ActBacktrackSplit = (SPLIT)NULL; RecoverList = split_RemoveUnnecessarySplits(PS, EmptyClause); Backtracklevel = clause_SplitLevel(EmptyClause); *SplitClause = NULL; /* Backtrack all split levels bigger than the level of the empty clause */ while (!prfs_SplitStackEmpty(PS) && (prfs_ValidLevel(PS) > Backtracklevel)) { ActBacktrackSplit = prfs_SplitStackTop(PS); prfs_SplitStackPop(PS); if (prfs_SplitFatherClause(ActBacktrackSplit) != (CLAUSE)NULL) { RecoverList = list_Cons(prfs_SplitFatherClause(ActBacktrackSplit), RecoverList); prfs_SplitSetFatherClause(ActBacktrackSplit, NULL); } RecoverList = list_Nconc(prfs_SplitDeletedClauses(ActBacktrackSplit), RecoverList); clause_DeleteClauseList(prfs_SplitBlockedClauses(ActBacktrackSplit)); prfs_SplitFree(ActBacktrackSplit); prfs_DecValidLevel(PS); } /* Backtrack further for all right branches on top of the stack */ while (!prfs_SplitStackEmpty(PS) && list_Empty(prfs_SplitBlockedClauses(prfs_SplitStackTop(PS)))) { ActBacktrackSplit = prfs_SplitStackTop(PS); prfs_SplitStackPop(PS); if (prfs_SplitFatherClause(ActBacktrackSplit) != (CLAUSE)NULL) RecoverList = list_Cons(prfs_SplitFatherClause(ActBacktrackSplit), RecoverList); RecoverList = list_Nconc(prfs_SplitDeletedClauses(ActBacktrackSplit), RecoverList); prfs_SplitFree(ActBacktrackSplit); prfs_DecValidLevel(PS); } if (!prfs_SplitStackEmpty(PS)) { /* Enter the right branch of the splitting step */ int SplitMinus1; LIST RightClauses; SplitMinus1 = prfs_ValidLevel(PS) - 1; ActBacktrackSplit = prfs_SplitStackTop(PS); RecoverList = list_Nconc(prfs_SplitDeletedClauses(ActBacktrackSplit), RecoverList); prfs_SplitSetDeletedClauses(ActBacktrackSplit, list_Nil()); RecoverList = split_DeleteInvalidClausesFromList(PS, SplitMinus1, RecoverList); RightClauses = prfs_SplitBlockedClauses(ActBacktrackSplit); prfs_SplitSetBlockedClauses(ActBacktrackSplit, list_Nil()); for (Scan = RightClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) { if (clause_Number(list_Car(Scan)) == 0) { /* Found the right clause, the negation clauses have number -1. */ #ifdef CHECK if (*SplitClause != NULL) { misc_StartErrorReport(); misc_ErrorReport("\n In split_Backtrack:"); misc_ErrorReport(" Found two blocked clauses "); misc_ErrorReport("\n with clause number 0 (this marks the clause "); misc_ErrorReport("\n for the right branch of the tableau)."); misc_FinishErrorReport(); } #endif *SplitClause = list_Car(Scan); } clause_NewNumber((CLAUSE) list_Car(Scan)); clause_AddParentClause((CLAUSE) list_Car(Scan), clause_Number(EmptyClause)); clause_AddParentLiteral((CLAUSE) list_Car(Scan), 0); /* dummy literal */ } #ifdef CHECK if (*SplitClause == NULL) { misc_StartErrorReport(); misc_ErrorReport("\n In split_Backtrack: Didnīt find a blocked clause"); misc_ErrorReport("\n with clause number 0. (this marks the clause "); misc_ErrorReport("\n for the right branch of the tableau)."); misc_FinishErrorReport(); } #endif RecoverList = list_Nconc(RightClauses, RecoverList); /* Then, delete clauses from current level (Hack) */ prfs_DecValidLevel(PS); prfs_MoveInvalidClausesDocProof(PS); split_DeleteInvalidClausesFromStack(PS); prfs_IncValidLevel(PS); } else { /* Don't delete clauses from current level (split is top level) */ prfs_MoveInvalidClausesDocProof(PS); for (Scan = RecoverList; !list_Empty(Scan); Scan = list_Cdr(Scan)) prfs_InsertDocProofClause(PS, list_Car(Scan)); list_Delete(RecoverList); RecoverList = list_Nil(); } prfs_SetLastBacktrackLevel(PS, prfs_ValidLevel(PS)); return RecoverList; } static LIST split_DeleteClausesDependingOnLevelFromList(PROOFSEARCH Search, LIST ClauseList, int Level, LIST* New) /************************************************************** INPUT: A proof search object, a list of unshared clauses and a split level. EFFECT: Deletes all clauses depending on split level from . All split stored deleted clauses from the level of the deleted clauses from are stored in <*New>. RETURNS: The updated list and the recover clauses in <*New>. ***************************************************************/ { LIST Scan; CLAUSE Clause; SPLIT Reinsert; for (Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan)) { Clause = list_Car(Scan); if (clause_DependsOnSplitLevel(Clause, Level)) { Reinsert = prfs_GetSplitOfLevel(clause_SplitLevel(Clause), Search); if (prfs_SplitDeletedClauses(Reinsert) != list_Nil()) { *New = list_Nconc(prfs_SplitDeletedClauses(Reinsert), *New); prfs_SplitSetDeletedClauses(Reinsert, list_Nil()); } prfs_InsertDocProofClause(Search,Clause); list_Rplaca(Scan, NULL); } } return list_PointerDeleteElement(ClauseList, NULL); } static LIST split_DeleteClausesDependingOnLevelFromSet(PROOFSEARCH PS, LIST ClauseList, int SplitLevel) /************************************************************** INPUT: A PROOFSEARCH object, a list of shared clauses and a split level. RETURNS: A list of clauses that have to be recovered possibly. EFFECT: Clauses from the clause list depending on are moved to the doc proof index of . All formerly redundant clauses that were reduced by a clause of the same split level as a clause from the list depending on are returned. ***************************************************************/ { LIST scan, delList, recover; CLAUSE clause; SPLIT reinsert; delList = recover = list_Nil(); for (scan = ClauseList; !list_Empty(scan); scan = list_Cdr(scan)){ clause = list_Car(scan); if (clause_DependsOnSplitLevel(clause, SplitLevel)) { reinsert = prfs_GetSplitOfLevel(clause_SplitLevel(clause), PS); recover = list_Nconc(prfs_SplitDeletedClauses(reinsert), recover); prfs_SplitSetDeletedClauses(reinsert, list_Nil()); delList = list_Cons(clause, delList); } } /* WARNING: The following move operations change the worked off */ /* and usable sets of the proof search object destructively. */ /* So it's impossible to move those function calls into the */ /* loop above. */ for ( ; !list_Empty(delList); delList = list_Pop(delList)) { clause = list_Car(delList); if (clause_GetFlag(clause, WORKEDOFF)) prfs_MoveWorkedOffDocProof(PS, clause); else prfs_MoveUsableDocProof(PS, clause); } return recover; } static LIST split_DeleteInvalidClausesFromList(PROOFSEARCH Search, int Level, LIST ClauseList) /************************************************************** INPUT: A proof search object, a split level and a list of clauses. RETURNS: The list where invalid clauses wrt 'Level' are deleted. EFFECT: The invalid clauses are stored in the doc proof index of the proof search object if necessary. ***************************************************************/ { LIST Scan; CLAUSE Clause; /*printf("\nDiese Liste soll von ungueltigen (Level > %d) " "befreit werden: \n",Level);fflush(stdout); clause_ListPrint(ClauseList);*/ for (Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan)) { Clause = list_Car(Scan); if (!prfs_IsClauseValid(Clause,Level)) { prfs_InsertDocProofClause(Search,Clause); list_Rplaca(Scan, NULL); } } return list_PointerDeleteElement(ClauseList, NULL); } static void split_DeleteInvalidClausesFromStack(PROOFSEARCH Search) /************************************************************** INPUT: A proof search object. EFFECT: All clauses in the split stack of that have a higher split level than the current split level are deleted. ***************************************************************/ { LIST Scan1,Scan2,ClauseList; int Level; CLAUSE Clause; Level = prfs_ValidLevel(Search); for (Scan1=prfs_SplitStack(Search);!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) { ClauseList = prfs_SplitDeletedClauses(list_Car(Scan1)); for (Scan2 = ClauseList; !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) { Clause = (CLAUSE)list_Car(Scan2); if (!prfs_IsClauseValid(Clause,Level)) { prfs_InsertDocProofClause(Search,Clause); list_Rplaca(Scan2, NULL); } } prfs_SplitSetDeletedClauses(list_Car(Scan1),list_PointerDeleteElement(ClauseList, NULL)); } } static LIST split_RemoveUnnecessarySplits(PROOFSEARCH PS, CLAUSE EmptyClause) /************************************************************** INPUT: An empty clause and a proof search object EFFECT: Removes all splits up to the last backtrack level that were not necessary to derive the empty clause. RETURNS: A list of recovered clauses. ***************************************************************/ { LIST Scan; LIST Recover, New; LIST Deleted; LIST ScanStack; int SplitLevel; int LastBacktrackLevel; SPLIT Split,ScanSplit; Scan = prfs_SplitStack(PS); SplitLevel = prfs_ValidLevel(PS); LastBacktrackLevel = prfs_LastBacktrackLevel(PS); Recover = list_Nil(); while (SplitLevel > LastBacktrackLevel) { if (prfs_SplitIsUnused(list_Car(Scan)) && !clause_DependsOnSplitLevel(EmptyClause, SplitLevel)) { New = list_Nil(); Split = list_Car(Scan); /*printf("\n\t Removed: %d",prfs_SplitSplitLevel(Split));*/ clause_DeleteClauseList(prfs_SplitBlockedClauses(Split)); prfs_SplitSetBlockedClauses(Split, list_Nil()); Recover = list_Nconc(prfs_SplitDeletedClauses(Split), Recover); prfs_SplitSetDeletedClauses(Split, list_Nil()); if (prfs_SplitFatherClause(Split) != (CLAUSE)NULL) { Recover = list_Cons(prfs_SplitFatherClause(Split),Recover); prfs_SplitSetFatherClause(Split,NULL); } Recover = split_DeleteClausesDependingOnLevelFromList(PS, Recover, SplitLevel, &New); ScanStack = prfs_SplitStack(PS); while (!list_StackEmpty(ScanStack) && prfs_SplitSplitLevel((ScanSplit = (SPLIT)list_Car(ScanStack))) > LastBacktrackLevel) { Deleted = prfs_SplitDeletedClauses(ScanSplit); prfs_SplitSetDeletedClauses(ScanSplit, list_Nil()); /* IMPORTANT!, see next line */ Deleted = split_DeleteClausesDependingOnLevelFromList(PS, Deleted, SplitLevel, &New); prfs_SplitSetDeletedClauses(ScanSplit, Deleted); ScanStack = list_Cdr(ScanStack); } while (!list_Empty(New)) { Deleted = list_Nil(); Recover = list_Nconc(split_DeleteClausesDependingOnLevelFromList(PS, New, SplitLevel, &Deleted), Recover); New = Deleted; } Recover = list_Nconc(Recover, split_DeleteClausesDependingOnLevelFromSet(PS, prfs_UsableClauses(PS), SplitLevel)); Recover = list_Nconc(Recover, split_DeleteClausesDependingOnLevelFromSet(PS, prfs_WorkedOffClauses(PS), SplitLevel)); prfs_SplitSetUsed(Split); } SplitLevel--; Scan = list_Cdr(Scan); } return Recover; } void split_DeleteClauseAtLevel(PROOFSEARCH PS, CLAUSE Clause, int Level) /************************************************************** INPUT: A clause, a level and a proofsearch object RETURNS: Nothing. EFFECT: is deleted from the usable or worked off set and made unshared. ***************************************************************/ { if (clause_GetFlag(Clause,WORKEDOFF)) prfs_ExtractWorkedOff(PS, Clause); else prfs_ExtractUsable(PS, Clause); split_KeepClauseAtLevel(PS, Clause, Level); } void split_KeepClauseAtLevel(PROOFSEARCH PS, CLAUSE Clause, int Level) /************************************************************** INPUT: A clause and a level as int. RETURNS: None. MEMORY: A copy of clause is made and kept within the split stack. ***************************************************************/ { SPLIT Split; Split = prfs_GetSplitOfLevel(Level, PS); prfs_SplitSetDeletedClauses(Split,list_Cons(Clause, prfs_SplitDeletedClauses(Split))); } LIST split_ExtractEmptyClauses(LIST Clauses, LIST* EmptyClauses) /************************************************************** INPUT: A list of clauses and a pointer to a list of empty clauses. RETURNS: without all empty clauses where the empty clauses are moved to MEMORY: Destructive on . ***************************************************************/ { LIST Scan; CLAUSE Clause; for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) { Clause = (CLAUSE)list_Car(Scan); if (clause_IsEmptyClause(Clause)) { *EmptyClauses = list_Cons(Clause,*EmptyClauses); list_Rplaca(Scan,NULL); } } Clauses = list_PointerDeleteElement(Clauses,NULL); return Clauses; } CLAUSE split_SmallestSplitLevelClause(LIST Clauses) /************************************************************** INPUT: A non-empty list of clauses. RETURNS: The clause with the smallest split level. ***************************************************************/ { CLAUSE Result; Result = (CLAUSE)list_Car(Clauses); Clauses = list_Cdr(Clauses); while (!list_Empty(Clauses)) { if (clause_SplitLevel(Result) > clause_SplitLevel(list_Car(Clauses))) Result = list_Car(Clauses); Clauses = list_Cdr(Clauses); } return Result; }