From 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 12:34:43 +0000 Subject: Updated raytracer test. Added SPASS test. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/spass/rules-split.c | 460 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 460 insertions(+) create mode 100644 test/spass/rules-split.c (limited to 'test/spass/rules-split.c') diff --git a/test/spass/rules-split.c b/test/spass/rules-split.c new file mode 100644 index 00000000..7ee420a9 --- /dev/null +++ b/test/spass/rules-split.c @@ -0,0 +1,460 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * 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: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + +/**************************************************************/ +/* 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; +} -- cgit