| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * 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 |
| <ClauseList>. |
| All split stored deleted clauses from the level of |
| the deleted clauses from <ClauseList> 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 <SplitLevel> |
| are moved to the doc proof index of <PS>. |
| All formerly redundant clauses that were reduced by a clause |
| of the same split level as a clause from the list depending |
| on <SplitLevel> 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 <Search> that have a higher |
| split level than the current <Search> 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: <Clause> 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: <Clauses> without all empty clauses where the empty clauses |
| are moved to <EmptyClauses> |
| MEMORY: Destructive on <Clauses>. |
| ***************************************************************/ |
| { |
| 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; |
| } |