diff options
Diffstat (limited to 'test/spass/proofcheck.c')
| -rw-r--r-- | test/spass/proofcheck.c | 1391 |
1 files changed, 1391 insertions, 0 deletions
diff --git a/test/spass/proofcheck.c b/test/spass/proofcheck.c new file mode 100644 index 00000000..15010d93 --- /dev/null +++ b/test/spass/proofcheck.c @@ -0,0 +1,1391 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * PROOF CHECKING * */ +/* * * */ +/* * Copyright (C) 1998, 1999, 2000, 2001 * */ +/* * MPI fuer Informatik * */ +/* * * */ +/* * This program is free software; you can redistribute * */ +/* * it and/or modify it under the terms of the GNU * */ +/* * General Public License as published by the Free * */ +/* * Software Foundation; either version 2 of the License, * */ +/* * or (at your option) any later version. * */ +/* * * */ +/* * This program is distributed in the hope that it will * */ +/* * be useful, but WITHOUT ANY WARRANTY; without even * */ +/* * the implied warranty of MERCHANTABILITY or FITNESS * */ +/* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ +/* * License for more details. * */ +/* * * */ +/* * You should have received a copy of the GNU General * */ +/* * Public License along with this program; if not, write * */ +/* * to the Free Software Foundation, Inc., 59 Temple * */ +/* * Place, Suite 330, Boston, MA 02111-1307 USA * */ +/* * * */ +/* $Revision: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ + +/* $RCSfile$ */ + +#include "proofcheck.h" + + +/* options */ +int pcheck_Timelimit; +const char *pcheck_ProofFileSuffix; +BOOL pcheck_Quiet; + +/* options for graph generation */ +BOOL pcheck_ClauseCg; +BOOL pcheck_GenNamedCg, pcheck_GenRedCg; +const char *pcheck_CgName, *pcheck_RedCgName; +GRAPHFORMAT pcheck_GraphFormat; + + +static int pcheck_MaxSplitLevel(LIST Clauses) +/************************************************************** + INPUT: A list of clauses. + RETURNS: The maximum split level of a clause. +***************************************************************/ +{ + int Max; + int Act; + + Max = 0; + while (!list_Empty(Clauses)) { + Act = clause_SplitLevel(list_Car(Clauses)); + if (Act > Max) + Max = Act; + Clauses = list_Cdr(Clauses); + } + return Max; +} + + +static __inline__ int pcheck_MaxParentSplitLevel(CLAUSE Clause) +/************************************************************** + INPUT: A clause + RETURNS: The max split level of the parent clauses +***************************************************************/ +{ + return pcheck_MaxSplitLevel(clause_ParentClauses(Clause)); +} + + +static BOOL pcheck_ClauseIsFromLeftSplit(CLAUSE Clause) +/************************************************************** + INPUT : A Clause + RETURNS: TRUE iff the clause is the left half of a split + CAUTION: This works also for clauses without parents, since + pcheck_MaxParentSplitLevel returns 0 in that case. +***************************************************************/ +{ + return (clause_SplitLevel(Clause) > pcheck_MaxParentSplitLevel(Clause)); +} + + +static BOOL pcheck_ClauseIsFromRightSplit(CLAUSE Clause) +/************************************************************** + INPUT: A clause + RETURNS: TRUE iff the clause is from the right half of a split +***************************************************************/ +{ + if (list_Empty(clause_ParentClauses(Clause))) + return FALSE; + + return clause_IsEmptyClause(list_Car(clause_ParentClauses(Clause))); +} + +static BOOL pcheck_ClauseIsFromSplit(CLAUSE Clause) +/************************************************************** + INPUT : A clause + RETURNS: TRUE iff the clause is from a split +***************************************************************/ +{ + return (pcheck_ClauseIsFromRightSplit(Clause) || + pcheck_ClauseIsFromLeftSplit(Clause)); +} + + +static int pcheck_LabelToNumber(const char* Label) +/************************************************************** + INPUT: A clause label + RETURNS: The label converted to a number. + EFFECT: If the conversion fails an error message is printed + and the program exits. +***************************************************************/ +{ + int Number; + + if (!string_StringToInt(Label, FALSE, &Number)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n In pcheck_LabelToNumber:"); + misc_UserErrorReport(" Could not convert clause"); + misc_UserErrorReport(" label %s to a number.\n", Label); + misc_FinishUserErrorReport(); + } + + return Number; +} + + +static int pcheck_CompareNumberAndClause(const void* Number, const void* ClausePtr) +/************************************************************** + INPUT: A number and a pointer to a CLAUSE. + RETURNS: 1) a negative number if <number> is < number of <Clause> + 2) 0 if <Number> is equal to the number of <Clause> + 3) a positive number if <Number> is > number of <Clause> + EFFECT: This function is used as parameter to the bsearch function. +***************************************************************/ +{ + return (int)Number - clause_Number(*(const CLAUSE*)ClausePtr); +} + + +static void pcheck_ParentNumbersToPointersInVector(CLAUSE* ClauseVector, int Size) +/************************************************************** + INPUT: A clause vector without duplicate clauses and the maximal + number of elements in the vector + EFFECTS: All clause parent numbers are replaced by pointers + to the parents. + CAUTION: The clause vector has to be sorted by increasing + clause numbers, since this function performs a binary search + on the vector. +***************************************************************/ +{ + int Position; + LIST NewParents, OldParents; + LIST ScanParents; + int ParentNum; + CLAUSE* Parent; + + for (Position = 0; Position < Size; Position++) { + OldParents = clause_ParentClauses(ClauseVector[Position]); + NewParents = list_Copy(OldParents); + + for (ScanParents = NewParents; !list_Empty(ScanParents); ScanParents = list_Cdr(ScanParents)) { + ParentNum = (int)list_Car(ScanParents); + /* Binary search for parent clause with number <ParentNum>. */ + Parent = bsearch((const void*)ParentNum, ClauseVector, Size, + sizeof(CLAUSE), pcheck_CompareNumberAndClause); + if (Parent != NULL) + list_Rplaca(ScanParents, *Parent); + else { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Missing parent clause %d of clause %d.\n", + ParentNum, clause_Number(ClauseVector[Position])); + misc_FinishUserErrorReport(); + } + } + clause_SetParentClauses(ClauseVector[Position], NewParents); + list_Delete(OldParents); + } +} + + +static LIST pcheck_ForceParentNumbersToPointersInVector(CLAUSE* ClauseVector, + int Size) +/************************************************************** + INPUT: A clause vector, possibly with duplicates + RETURNS: All numbers of clauses <c> that are missing a parent clause + from the transitive hull of parent clauses of <c>. + EFFECTS: All MARKED and HIDDEN flags of the clauses are changed. + All parent numbers are converted to pointers, if the + parents exist, otherwise the parent number is deleted + from the list. + The parent literal list is changed accordingly. + A clause <c> is marked as HIDDEN, if any clause + from the transitive hull of parent clauses of <c> + was missing in <ClauseVector>. +***************************************************************/ +{ + int Position; + LIST NewParents, NewPLits, Parents, PLits, Missing; + int ParentNum, PLitNum; + CLAUSE *Parent, Clause; + + Missing = list_Nil(); + + for (Position = 0; Position < Size; Position++) { + clause_RemoveFlag(ClauseVector[Position], MARKED); + clause_RemoveFlag(ClauseVector[Position], HIDDEN); + } + + for (Position = 0; Position < Size; Position++) { + Clause = ClauseVector[Position]; + if (!clause_GetFlag(Clause, MARKED)) { + clause_SetFlag(Clause, MARKED); + Parents = clause_ParentClauses(Clause); + PLits = clause_ParentLiterals(Clause); + NewParents = list_Nil(); + NewPLits = list_Nil(); + + while (!list_Empty(Parents)) { + ParentNum = (int)list_Car(Parents); + PLitNum = (int)list_Car(PLits); + /* Binary search for parent clause with number <ParentNum>. */ + Parent = bsearch((const void*)ParentNum, ClauseVector, Size, + sizeof(CLAUSE), pcheck_CompareNumberAndClause); + if (Parent == NULL) { + Missing = list_Cons((POINTER)ParentNum, Missing); + clause_SetFlag(Clause, HIDDEN); + } else { + if (clause_GetFlag(*Parent, HIDDEN)) + clause_SetFlag(Clause, HIDDEN); + NewParents = list_Cons((POINTER)*Parent, NewParents); + NewPLits = list_Cons((POINTER)PLitNum, NewPLits); + } + Parents = list_Cdr(Parents); + PLits = list_Cdr(PLits); + } + list_Delete(clause_ParentClauses(Clause)); + list_Delete(clause_ParentLiterals(Clause)); + NewParents = list_NReverse(NewParents); + NewPLits = list_NReverse(NewPLits); + clause_SetParentClauses(Clause, NewParents); + clause_SetParentLiterals(Clause, NewPLits); + } /* if clause is not marked */ + } /* for all clauses */ + + return Missing; +} + + +static int pcheck_CompareClauseNumber(const void* C1, const void* C2) +/************************************************************** + INPUT : Two pointers to CLAUSEs. + RETURNS: 1) a negative number if the number of C1 is < number of C2. + 2) 0 if C1 and C2 have the same clause number + (that means a possible bug in SPASS) + 3) a positive number if number of C1 > number of C2 + EFFECT: This function is used as parameter to the qsort function. +************************************************************/ +{ + return clause_Number(*(const CLAUSE*)C1) - clause_Number(*(const CLAUSE*)C2); +} + + +static LIST pcheck_ConvertParentsInList(LIST List) +/************************************************************** + INPUT: A list of clauses. + RETURNS: The list of missing parent clause numbers from the list + EFFECTS: Parent numbers are converted to pointers +***************************************************************/ +{ + int Size, Index; + CLAUSE* ClauseVector; + LIST Missing; + + Size = list_Length(List); + if (Size == 0) + return list_Nil(); + + /* convert list into vector for binary search */ + ClauseVector = (CLAUSE*)memory_Malloc(sizeof(CLAUSE) * Size); + for (Index = 0; !list_Empty(List); List = list_Cdr(List), Index++) + ClauseVector[Index] = list_Car(List); + + /* sort the clauses in vector by increasing clause number */ + qsort(ClauseVector, Size, sizeof(CLAUSE), pcheck_CompareClauseNumber); + + /* convert parent lists */ + Missing = pcheck_ForceParentNumbersToPointersInVector(ClauseVector, Size); + + memory_Free(ClauseVector, sizeof(CLAUSE) * Size); + return Missing; +} + + +LIST pcheck_ConvertParentsInSPASSProof(PROOFSEARCH Search, LIST EmptyClauses) +/************************************************************** + INPUT : A proofsearch object with clauses sorted by weight + and an unsorted list <EmptyClauses> + RETURNS: The lists, where the clauses in <EmptyClauses> are + now sorted by weight, and parent numbers + in the clauses are replaced by parent pointers +***************************************************************/ +{ + LIST AllLists; + LIST Missing; + + AllLists = list_Nconc(list_Copy(prfs_DocProofClauses(Search)), + list_Copy(EmptyClauses)); + AllLists = list_Nconc(list_Copy(prfs_UsableClauses(Search)), AllLists); + AllLists = list_Nconc(list_Copy(prfs_WorkedOffClauses(Search)), AllLists); + + AllLists = pcheck_ClauseNumberMergeSort(AllLists); + Missing = pcheck_ConvertParentsInList(AllLists); + list_Delete(AllLists); + + return Missing; +} + + +static LIST pcheck_ParentNumbersToParents(LIST Proof) +/************************************************************** + INPUT: A list of clauses, representing a proof. + RETURNS: The list, where parent numbers in the + parent list of clauses are replaced + by the parents (pointers). + CAUTION: For finding the clause corresponding to a + a clause number, the <Proof> list is searched + with binary search. This is correct only if + the clause numbers in <Proof> are increasing. +************************************************************/ +{ + LIST ScanClauses; + int ProofLength, Position; + CLAUSE* ClauseVector; + + if (list_Empty(Proof)) + return list_Nil(); + + /* convert list into vector for binary search */ + ProofLength = list_Length(Proof); + ClauseVector = (CLAUSE*) memory_Malloc(ProofLength * sizeof(CLAUSE)); + + for (ScanClauses = Proof, Position = 0; !list_Empty(ScanClauses); + ScanClauses = list_Cdr(ScanClauses), Position++) { + ClauseVector[Position] = list_Car(ScanClauses); + } + + /* sort the clauses in vector by increasing clause number */ + qsort(ClauseVector, ProofLength, sizeof(CLAUSE), pcheck_CompareClauseNumber); + + /* convert parent lists */ + pcheck_ParentNumbersToPointersInVector(ClauseVector, ProofLength); + + memory_Free(ClauseVector, ProofLength * sizeof(CLAUSE)); + + return Proof; +} + + +LIST pcheck_ParentPointersToParentNumbers(LIST Clauses) +/************************************************************** + INPUT : A list of clauses + RETURNS: The list with parent pointers replaced by + parent numbers + EFFECTS: Sets marks on all clauses. +***************************************************************/ +{ + LIST ScanClauses; + LIST ScanParents; + + pcheck_ClauseListRemoveFlag(Clauses, MARKED); + + for (ScanClauses = Clauses; !list_Empty(ScanClauses); ScanClauses = list_Cdr(ScanClauses)) { + if (!clause_GetFlag(list_Car(ScanClauses), MARKED)) { + for (ScanParents = clause_ParentClauses(list_Car(ScanClauses)); !list_Empty(ScanParents); + ScanParents = list_Cdr(ScanParents)) + list_Rplaca(ScanParents, (POINTER)clause_Number(list_Car(ScanParents))); + clause_SetFlag(list_Car(ScanClauses), MARKED); + } + } + return Clauses; +} + + +LIST pcheck_ConvertTermListToClauseList(LIST ProofRest, FLAGSTORE Flags, + PRECEDENCE Precedence) +/************************************************************** + INPUT: A list of quintupels (lists) representing a proof, + a flag store, and a precedence. + RETURNS: The conversion of this list into the internal clause + structure. For each clause, the numbers of parent + clauses are replaced by pointers to the parents. +***************************************************************/ +{ + LIST Clauses; + LIST ProofLine; + TERM ClauseTerm; + CLAUSE Clause; + int Level; + int ClauseNumber; + LIST ParentLabels; + LIST ParentIds; + LIST ParentLits; /* this is a dummy list; parent lits are not yet specified in a SPASS proof */ + RULE Origin; + char* ClauseLabel; + + Clauses = list_Nil(); /* result */ + + while (!list_Empty(ProofRest)) { + /* break proof line into components */ + ProofLine = list_Car(ProofRest); + + ClauseLabel = list_First(ProofLine); + ClauseTerm = list_Second(ProofLine); + /* replace by NULL clause, since dfg_CreateClauseFromTerm deletes clause ! */ + list_Rplaca(list_Cdr(ProofLine), clause_Null()); + ParentLabels = (LIST)list_Third(ProofLine); + Level = (int)list_Fourth(ProofLine); + Origin = (RULE)list_Fifth(ProofLine); + + /* Conversion */ + Clause = dfg_CreateClauseFromTerm(ClauseTerm, TRUE, Flags,Precedence); + /* It's necessary to update the weight since dfg_CreateClauseFromTerm */ + /* doesn't set it. */ + clause_UpdateWeight(Clause, Flags); + ClauseNumber = pcheck_LabelToNumber(ClauseLabel); + ParentIds = list_Nil(); + ParentLits = list_Nil(); + + while (!list_Empty(ParentLabels)) { + ParentIds = list_Cons((POINTER)pcheck_LabelToNumber(list_Car(ParentLabels)), ParentIds); + ParentLits = list_Cons(0, ParentLits); + ParentLabels = list_Cdr(ParentLabels); + } + + /* set all data */ + clause_SetNumber(Clause, ClauseNumber); + ParentIds = list_NReverse(ParentIds); + clause_SetParentClauses(Clause, ParentIds); + clause_SetParentLiterals(Clause, ParentLits); + Clause->origin = Origin; + + clause_SetSplitLevel(Clause, Level); + if (Level > 0) { + clause_ClearSplitField(Clause); + clause_SetSplitFieldBit(Clause, Level); + } else + clause_SetSplitField(Clause, (SPLITFIELD)NULL,0); + + clause_RemoveFlag(Clause, MARKED); + Clauses = list_Cons(Clause, Clauses); + ProofRest = list_Cdr(ProofRest); + } + Clauses = list_NReverse(Clauses); + + /* convert parent numbers to pointers */ + Clauses = pcheck_ParentNumbersToParents(Clauses); + + return Clauses; +} + + +static BOOL pcheck_ClauseIsUnmarked(CLAUSE C) +/************************************************************** + INPUT: A clause + RETURNS: The value of the clauses MARKED flag +***************************************************************/ +{ + return !clause_GetFlag(C, MARKED); +} + + +static void pcheck_RemoveUnmarkedFromTableau(TABLEAU T) +/************************************************************** + INPUT: A tableau + RETURNS: Nothing. + EFFECTS: Delete all clauses that have the MARKED flag + set from tableau. +***************************************************************/ +{ + if (tab_IsEmpty(T)) + return; + + tab_SetClauses(T, list_DeleteElementIf(tab_Clauses(T), + (BOOL (*)(POINTER))pcheck_ClauseIsUnmarked)); + + pcheck_RemoveUnmarkedFromTableau(tab_LeftBranch(T)); + pcheck_RemoveUnmarkedFromTableau(tab_RightBranch(T)); +} + + +static void pcheck_CollectUnmarkedSplits(TABLEAU T, LIST* Splits) +/************************************************************** + INPUT: A tableau, a list of clauses by reference + RETURNS: Nothing. + EFFECTS: Add all split clauses in the tableau that are not + marked to the <Splits> list. +***************************************************************/ +{ + LIST Scan; + + if (tab_IsEmpty(T)) + return; + + for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) { + if (!clause_GetFlag(list_Car(Scan), MARKED) && clause_IsFromSplitting(list_Car(Scan))) + (*Splits) = list_Cons(list_Car(Scan), *Splits); + } + + pcheck_CollectUnmarkedSplits(tab_LeftBranch(T), Splits); + pcheck_CollectUnmarkedSplits(tab_RightBranch(T), Splits); +} + + +/* EK: unused, only recursive */ +static void pcheck_TableauSplitsComplete(TABLEAU T) +/************************************************************** + INPUT : A tableau + RETURNS: Checks that every split has exactly two or no + successors. This condition must be true after + tab_RemoveRedundantSplits has been called. +***************************************************************/ +{ + if (tab_IsEmpty(T)) + return; + + if (tab_RightBranchIsEmpty(T) && !tab_LeftBranchIsEmpty(T)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Split of clause %d has no right branch.\n", + clause_Number(tab_SplitClause(T))); + misc_FinishUserErrorReport(); + } + + if (!tab_RightBranchIsEmpty(T) && tab_LeftBranchIsEmpty(T)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Split of clause %d has no left branch.\n", + clause_Number(tab_SplitClause(T))); + misc_FinishUserErrorReport(); + } + + pcheck_TableauSplitsComplete(tab_LeftBranch(T)); + pcheck_TableauSplitsComplete(tab_RightBranch(T)); +} + + +static void pcheck_RightSplitParents(CLAUSE SplitClause, CLAUSE RightSplitClause, + CLAUSE LeftSplitClause) +/************************************************************** + INPUT: A split clause, and its left and right successors + EFFECTS: Prints an error message if the split is not correctly + closed. +***************************************************************/ +{ + LIST Scan; + BOOL HasEmpty, ContainsSplitClause; + + HasEmpty = ContainsSplitClause = FALSE; + + for (Scan = clause_ParentClauses(RightSplitClause); + !list_Empty(Scan); Scan = list_Cdr(Scan)) { + if (clause_IsEmptyClause(list_Car(Scan))) + HasEmpty = TRUE; + if (clause_Number(list_Car(Scan)) == clause_Number(SplitClause)) + ContainsSplitClause = TRUE; + } + + if (!HasEmpty) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Right split clause %d has no empty clause as parent.\n", + clause_Number(SplitClause)); + misc_FinishUserErrorReport(); + } + + if (!ContainsSplitClause) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Right split clause %d", clause_Number(SplitClause)); + misc_UserErrorReport(" does not have its split parent as parent clause.\n"); + misc_FinishUserErrorReport(); + } +} + + + +/* EK: unused, only recursive */ +static void pcheck_SplitFormats(TABLEAU T) +/************************************************************** + INPUT : A tableau + RETURNS: TRUE iff all splits: + - have generated negations of the left split clause + if the left split clause is ground + - the conditions for right split clauses are + as demanded in pcheck_RightSplitParents +***************************************************************/ +{ + LIST Scan; + + if (tab_IsEmpty(T)) + return; + + /* for right splits, check that parents have an empty clause */ + /* and the split clause as a parent */ + + for (Scan = tab_RightSplitClauses(T); !list_Empty(Scan); + Scan = list_Cdr(Scan)) { + pcheck_RightSplitParents(tab_SplitClause(T), list_Car(Scan), + tab_LeftSplitClause(T)); + } + + pcheck_SplitFormats(tab_RightBranch(T)); + pcheck_SplitFormats(tab_LeftBranch(T)); +} + + +static void pcheck_SplitLevels(TABLEAU T) +/************************************************************** + INPUT : A Tableau + RETURNS: TRUE iff all clauses in the tableau that + are not splitting clauses have the max split + level of their parents. + CAUTION: We assume that <T> has correct and complete split + entries. See pcheck_SplitToProblems. +***************************************************************/ +{ + LIST Scan; + CLAUSE Clause; + int CorrectLevel; + + if (tab_IsEmpty(T)) + return; + + /* check split levels */ + for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) { + Clause = list_Car(Scan); + if (!list_Empty(clause_ParentClauses(Clause)) + && !clause_IsFromSplitting(Clause)) { + + CorrectLevel = pcheck_MaxParentSplitLevel(Clause); + if (clause_SplitLevel(Clause) != CorrectLevel) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Split level of clause %d should be %d.\n", + clause_Number(Clause), CorrectLevel); + misc_FinishUserErrorReport(); + } + } + } + + pcheck_SplitLevels(tab_RightBranch(T)); + pcheck_SplitLevels(tab_LeftBranch(T)); +} + + +/* EK: unused, only recursive */ +static void pcheck_SplitPrecheck(TABLEAU T) +/************************************************************** + INPUT : A tableau. + EFFECTS: Stops and prints an error message if a left half + of a split does not subsume its parents, or + if negations have been generated for a non-ground + left split clause. +***************************************************************/ +{ + if (tab_IsEmpty(T)) + return; + + if (!subs_Subsumes(tab_LeftSplitClause(T), tab_SplitClause(T), -1, -1)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Incorrect split of %d,", tab_SplitClause(T)); + misc_UserErrorReport(" left half of split does not subsume splitted clause.\n"); + misc_FinishUserErrorReport(); + } + + if (list_Length(tab_RightSplitClauses(T)) > 1 && + !clause_IsGround(tab_LeftSplitClause(T))) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Incorrect split of %d,", tab_SplitClause(T)); + misc_UserErrorReport(" non-ground split generated more than two clause.\n"); + misc_FinishUserErrorReport(); + } + + pcheck_SplitPrecheck(tab_LeftBranch(T)); + pcheck_SplitPrecheck(tab_RightBranch(T)); +} + + +BOOL pcheck_BuildTableauFromProof(LIST Proof, TABLEAU* Tableau) +/************************************************************** + INPUT : A list of clauses representing a proof, and a pointer + to a tableau used as return value. + RETURNS: TRUE iff no errors occurred, FALSE otherwise. + If TRUE is returned <Tableau> is set to a tableau + representing the proof. + EFFECTS: Errors are commented when they occur. +***************************************************************/ +{ + LIST ProofRest; + TABLEAU SplitPos; + TABPATH Path; + CLAUSE Clause; + int ClauseLevel, SplitLevel; + int ProofDepth; + + if (list_Empty(Proof)) { + *Tableau = tab_EmptyTableau(); + return TRUE; + } + + ProofDepth = pcheck_MaxSplitLevel(Proof); + *Tableau = tab_CreateNode(); + Path = tab_PathCreate(ProofDepth, *Tableau); + + ProofRest = Proof; + while (!list_Empty(ProofRest)) { + + SplitLevel = tab_PathLength(Path); + Clause = list_Car(ProofRest); + ClauseLevel = clause_SplitLevel(Clause); + + /* Special treatment for clauses that result from a splitting step */ + if (pcheck_ClauseIsFromSplit(Clause)) { + + if (ClauseLevel == 0) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Split level of split clause %d is 0.\n", clause_Number(Clause)); + misc_FinishUserErrorReport(); + } + + if (ClauseLevel > SplitLevel+1) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Split level of split clause %d", clause_Number(Clause)); + misc_UserErrorReport(" is not increment of current split level.\n"); + misc_FinishUserErrorReport(); + } + + SplitPos = tab_PathNthNode(Path, ClauseLevel-1); + + if (pcheck_ClauseIsFromLeftSplit(Clause)) { + /* Left branch of a splitting step */ + if (!tab_LeftBranchIsEmpty(SplitPos)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Multiple left splits for clause %d.\n", + clause_Number(tab_SplitClause(SplitPos))); + misc_FinishUserErrorReport(); + } + + Path = tab_PathPrefix(ClauseLevel-1, Path); + tab_SetSplitClause(SplitPos, list_Car(clause_ParentClauses(Clause))); + tab_SetLeftSplitClause(SplitPos, Clause); + tab_AddSplitAtCursor(Path, TRUE); + } else { + /* Right branch of a splitting step */ + if (tab_RightBranchIsEmpty(SplitPos)) { + + if (tab_LeftBranchIsEmpty(SplitPos)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Right split with incorrect split level, clause %d.\n", + clause_Number(Clause)); + misc_FinishUserErrorReport(); + } + + Path = tab_PathPrefix(ClauseLevel-1, Path); + tab_AddSplitAtCursor(Path, FALSE); + } + tab_AddRightSplitClause(SplitPos, Clause); + } /* clause from right split */ + } /* clause from split */ + + if (ClauseLevel > tab_PathLength(Path)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Split level of clause %d greater than current level.\n", + clause_Number(Clause)); + misc_FinishUserErrorReport(); + } + tab_AddClauseOnItsLevel(Clause, Path); + + ProofRest = list_Cdr(ProofRest); + } /* while proof is not empty */ + + + tab_PathDelete(Path); + + return TRUE; +} + + +static BOOL pcheck_TableauJustificationsRec(TABLEAU T, TABPATH Path) +/************************************************************** + INPUT : A Tableau <T>, a <Path> in the tableau + RETURNS: TRUE iff all clauses in the last node of the + path are correctly justified. +***************************************************************/ +{ + CLAUSE Clause; + LIST ScanClauses; + LIST ScanParents; + LIST Parents; + CLAUSE Parent; + BOOL Ok, RightSplit; + + if (tab_IsEmpty(T)) + return TRUE; + + Ok = TRUE; + + /* for each clause, check that its parents have been justified */ + + for (ScanClauses = tab_Clauses(tab_PathTop(Path)); + !list_Empty(ScanClauses); ScanClauses = list_Cdr(ScanClauses)) { + + Clause = list_Car(ScanClauses); + Parents = clause_ParentClauses(Clause); + + RightSplit = pcheck_ClauseIsFromRightSplit(Clause); + + /* check all parents */ + + for (ScanParents = Parents; !list_Empty(ScanParents); + ScanParents = list_Cdr(ScanParents)) { + + Parent = list_Car(ScanParents); + + if ((!(RightSplit && clause_IsEmptyClause(Parent)) && + !(RightSplit && pcheck_ClauseIsFromLeftSplit(Parent))) || + (clause_Number(Parent) > clause_Number(Clause)) ) { + if (!tab_PathContainsClause(Path, Parent)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Parent clause with number %d is not yet justified.\n", + clause_Number(Parent)); + misc_FinishUserErrorReport(); + } + } + } + } /* for all clauses in current node */ + + + /* Recursion */ + + if (!tab_LeftBranchIsEmpty(T)) { + Path = tab_PathPush(tab_LeftBranch(T), Path); + Ok = Ok && pcheck_TableauJustificationsRec(tab_LeftBranch(T), Path); + Path = tab_PathPop(Path); + } + + if (!tab_RightBranchIsEmpty(T)) { + Path = tab_PathPush(tab_RightBranch(T), Path); + Ok = Ok && pcheck_TableauJustificationsRec(tab_RightBranch(T), Path); + Path = tab_PathPop(Path); + } + + return Ok; +} + +static BOOL pcheck_TableauJustifications(TABLEAU T) +/************************************************************** + INPUT : A Tableau + RETURNS: TRUE iff for each clause in tableau, all its parent + clauses have been derived in a split on the same level + or below. +***************************************************************/ +{ + TABPATH Path; + BOOL Ok; + + Path = tab_PathCreate(tab_Depth(T),T); + Ok = pcheck_TableauJustificationsRec(T,Path); + tab_PathDelete(Path); + + return Ok; +} + +BOOL pcheck_TableauProof(TABLEAU* Tableau, LIST Proof) +/************************************************************** + INPUT: + RETURNS: +***************************************************************/ +{ + LIST RedundantClauses; + LIST EmptyClauses; + LIST UnmarkedSplits; + + tab_LabelNodes(*Tableau); + /* print out current tableau */ + if (pcheck_GenNamedCg) + tab_WriteTableau(*Tableau, pcheck_CgName, pcheck_GraphFormat); + + RedundantClauses = list_Nil(); + if (!pcheck_Quiet) { + fputs("pruning closed branches...", stdout); + fflush(stdout); + } + (*Tableau) = tab_PruneClosedBranches(*Tableau, &RedundantClauses); /* delete descendants of already closed branches */ + if (!pcheck_Quiet) + puts("finished."); + + if (!pcheck_Quiet) { + fputs("removing incomplete splits...", stdout); + fflush(stdout); + } + (*Tableau) = tab_RemoveIncompleteSplits(*Tableau, &RedundantClauses); /* reduce open node redundancies */ + if (!pcheck_Quiet) + puts("finished."); + + list_Delete(RedundantClauses); + + /* remove all clauses that are not needed for the empty clauses */ + /* of the proof or for the tableau structure (splits) */ + + EmptyClauses = list_Nil(); + tab_GetEarliestEmptyClauses(*Tableau, &EmptyClauses); + pcheck_ClauseListRemoveFlag(Proof, MARKED); + pcheck_MarkRecursive(EmptyClauses); + UnmarkedSplits = list_Nil(); + pcheck_CollectUnmarkedSplits(*Tableau, &UnmarkedSplits); + pcheck_MarkRecursive(UnmarkedSplits); + pcheck_RemoveUnmarkedFromTableau(*Tableau); + list_Delete(UnmarkedSplits); + list_Delete(EmptyClauses); + + /* print reduced graph */ + if (pcheck_GenRedCg) + tab_WriteTableau(*Tableau, pcheck_RedCgName, pcheck_GraphFormat); + + tab_SetSplitLevels(*Tableau); + pcheck_SplitLevels(*Tableau); + tab_CheckEmpties(*Tableau); + + if (!tab_IsClosed(*Tableau)) { + puts("\nerror: tableau is not closed."); + return FALSE; + } + + /* check justifications */ + if (!pcheck_Quiet) { + fputs("checking justifications...", stdout); + fflush(stdout); + } + if (!pcheck_TableauJustifications(*Tableau)) + return FALSE; + if (!pcheck_Quiet) + puts("finished."); + + return TRUE; +} + + +void pcheck_MarkRecursive(LIST Clauses) +/************************************************************** + INPUT: A list of clauses + RETURNS: Nothing. + EFFECTS: Marks all <Clauses> and its ancestors with the + MARKED clause flag. +***************************************************************/ +{ + CLAUSE Clause; + + for (; !list_Empty(Clauses); Clauses = list_Cdr(Clauses)) { + Clause = list_Car(Clauses); + if (!clause_GetFlag(Clause, MARKED)) { + pcheck_MarkRecursive(clause_ParentClauses(Clause)); + clause_SetFlag(Clause, MARKED); + } + } +} + + +static LIST pcheck_CollectTermVariables(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: A list of terms. For each variable in <Term> the list + contains exactly one term representing the variable. + EFFECT: Memory is allocated for the terms. +***************************************************************/ +{ + LIST Result, Scan; + + Result = term_VariableSymbols(Term); + for (Scan = Result; !list_Empty(Scan); Scan = list_Cdr(Scan)) + list_Rplaca(Scan, term_Create((SYMBOL)list_Car(Scan), list_Nil())); + + return Result; +} + + +static BOOL pcheck_IsRightSplitHalf(CLAUSE C) +/************************************************************** + INPUT : A clause. + RETURNS: TRUE iff the following conditions are fulfilled: + - the first parent clause is an empty clause + - the clause subsumes its second parent +***************************************************************/ +{ + LIST Parents; + BOOL Ok; + + Parents = list_Copy(clause_ParentClauses(C)); + Parents = list_PointerDeleteDuplicates(Parents); + + Ok = FALSE; + if (list_Length(Parents) == 2 && clause_IsEmptyClause(list_First(Parents))) + Ok = subs_Subsumes(C, list_Second(Parents), -1, -1); + + list_Delete(Parents); + + return Ok; +} + + +static TERM pcheck_UnivClosure(TERM T) +/************************************************************** + INPUT: A term, representing a formula. + RETURNS: The universal closure of the term. + EFFECTS: <T> is part of the returned term! +***************************************************************/ +{ + LIST Vars; + + Vars = pcheck_CollectTermVariables(T); + + if (list_Empty(Vars)) + return T; + return fol_CreateQuantifier(fol_All(), Vars, list_List(T)); +} + + +static TERM pcheck_ClauseToTerm(CLAUSE Clause) +/************************************************************** + INPUT: A clause. + RETURNS: The clause represented as a TERM. +***************************************************************/ +{ + int LitScan; + LIST Args; + TERM Lit; + TERM ClauseTerm; + + Args = list_Nil(); + + for (LitScan = clause_FirstLitIndex(); LitScan <= clause_LastLitIndex(Clause); + LitScan++) { + Lit = clause_LiteralSignedAtom(clause_GetLiteral(Clause, LitScan)); + Args = list_Cons(term_Copy(Lit), Args); + } + + if (list_Empty(Args)) + Args = list_List(term_Create(fol_False(), list_Nil())); + + /* Build the disjunction of the literals */ + if (list_Empty(list_Cdr(Args))) { /* only one arg */ + ClauseTerm = list_Car(Args); + list_Delete(Args); + } else + ClauseTerm = term_Create(fol_Or(), Args); + ClauseTerm = pcheck_UnivClosure(ClauseTerm); + + return ClauseTerm; +} + + +static LIST pcheck_ClauseListToTermList(LIST Clauses) +/************************************************************** + INPUT : A list of clauses. + RETURNS: A new list containing the clauses represented as TERMs. +***************************************************************/ +{ + LIST Terms; + + Terms = list_Nil(); + for (; !list_Empty(Clauses); Clauses = list_Cdr(Clauses)) + Terms = list_Cons(pcheck_ClauseToTerm(list_Car(Clauses)), Terms); + + return Terms; +} + + +static void pcheck_SaveNumberedDFGProblem(int Number, LIST Axioms, + LIST Conjectures, + const char* ProofFileName, + const char* DestPrefix) +/************************************************************** + INPUT : A (clause) number, a list of axioms and conjectures, + and a filename (of the proof file of the currently + checked proof) + RETURNS: Nothing. + EFFECTS: Saves a DFG file containing <Axioms> and <Conjectures> + under the name "<DestPrefix><Number>_<ProofFileName>" +***************************************************************/ +{ + char *Filename, *Tmp, *NumStr; + FILE *File; + + NumStr = string_IntToString(Number); + Tmp = pcheck_GenericFilename(ProofFileName, NumStr); + Filename = string_Conc(DestPrefix, Tmp); + + File = misc_OpenFile(Filename, "w"); + fol_FPrintDFGProblem(File, "{*Sub Proof*}", "{* Proof Checker *}", + "unsatisfiable", + "{* The problem is the correctness test for a single proof line *}", + Axioms, Conjectures); + misc_CloseFile(File, Filename); + + string_StringFree(NumStr); + string_StringFree(Tmp); + string_StringFree(Filename); +} + + +static void pcheck_SplitToProblems(TABLEAU T, const char* ProofFileName, + const char* DestPrefix) +/************************************************************** + INPUT: A tableau, which isn't a leaf of the tableau tree, + the name of a proof file and a file name prefix used for + generating files. + RETURNS: Nothing. + EFFECT: This function generates proof check tasks for clauses + resulting from splitting steps and writes them to + output files. + CAUTION: We assume that we get non-null clauses when calling + tab_SplitClause and tab_LeftSplitClause. +***************************************************************/ +{ + TERM SplitClauseTerm, LeftClauseTerm, RightClauseTerm; + TERM Equiv, Disj, Tmp; + LIST Conj, Args, Negations; + +#ifdef CHECK + if (tab_IsLeaf(T)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In pcheck_SplitToProblems: Tableau is a leaf of the "); + misc_ErrorReport("tableau tree."); + misc_FinishErrorReport(); + } +#endif + + SplitClauseTerm = pcheck_ClauseToTerm(tab_SplitClause(T)); + LeftClauseTerm = pcheck_ClauseToTerm(tab_LeftSplitClause(T)); + + /* by default, take all right split clauses as negations */ + /* if the first clause is the second half of a split clause, */ + /* take only the rest of the right split clauses as negations. */ + + Negations = tab_RightSplitClauses(T); + if (!list_Empty(Negations) && pcheck_IsRightSplitHalf(list_Car(Negations))) { + /* EK: Meiner Meinung nach ist es eine Invariante, daß die erste */ + /* Elternklausel die rechte Hälfte eines Splittings ist??? */ + Negations = list_Cdr(Negations); + /* build C <=> C' v C'' */ + RightClauseTerm = pcheck_ClauseToTerm(list_Car(tab_RightSplitClauses(T))); + Disj = term_Create(fol_Or(), list_Cons(LeftClauseTerm, list_List(RightClauseTerm))); + Equiv = term_Create(fol_Equiv(), list_Cons(SplitClauseTerm, list_List(Disj))); + Conj = list_List(Equiv); + + pcheck_SaveNumberedDFGProblem(clause_Number(tab_LeftSplitClause(T)), + list_Nil(), Conj, ProofFileName, DestPrefix); + term_DeleteTermList(Conj); + } + + Args = list_Nil(); + + /* build conjunction of negations, if there are any. */ + if (!list_Empty(Negations)) { + LeftClauseTerm = pcheck_ClauseToTerm(tab_LeftSplitClause(T)); + Args = pcheck_ClauseListToTermList(Negations); + /* Build the conjunction */ + if (list_Empty(list_Cdr(Args))) { /* only one arg */ + Tmp = list_Car(Args); + list_Delete(Args); + } else + Tmp = term_Create(fol_And(), Args); + Tmp = term_Create(fol_Not(), list_List(Tmp)); + Equiv = term_Create(fol_Implies(),list_Cons(Tmp,list_List(LeftClauseTerm))); + Conj = list_List(Equiv); + + /* problem id is number of right part of split clause, if it exists, + number of first negation otherwise */ + pcheck_SaveNumberedDFGProblem(clause_Number(list_Car(tab_RightSplitClauses(T))), + list_Nil(), Conj, ProofFileName, DestPrefix); + term_DeleteTermList(Conj); + } +} + + +void pcheck_TableauToProofTask(TABLEAU T, const char* ProofFileName, + const char* DestPrefix) +/************************************************************** + INPUT: A Tableau, two strings for filename generation. + RETURNS: Nothing. + EFFECTS: Generates DFG problem files for each clause in the tableau. + The problem asserts that the clause follows from + its parents. For splits, see pcheck_SplitToProblems +***************************************************************/ +{ + LIST Scan; + LIST Axioms, Conj, Help; + CLAUSE Clause; + + if (tab_IsEmpty(T)) + return; + + /* treat the splitting clauses at inner nodes of the tableau tree */ + if (!tab_IsLeaf(T)) + pcheck_SplitToProblems(T, ProofFileName, DestPrefix); + + /* treat derived clauses that don't result from splitting */ + for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) { + Clause = list_Car(Scan); + if (!clause_IsFromSplitting(Clause) && + !list_Empty(clause_ParentClauses(Clause))) { + Axioms = list_Copy(clause_ParentClauses(Clause)); + Axioms = list_PointerDeleteDuplicates(Axioms); + Help = Axioms; + Axioms = pcheck_ClauseListToTermList(Axioms); + list_Delete(Help); + Conj = list_List(pcheck_ClauseToTerm(Clause)); + pcheck_SaveNumberedDFGProblem(clause_Number(Clause), Axioms, Conj, + ProofFileName, DestPrefix); + term_DeleteTermList(Axioms); + term_DeleteTermList(Conj); + } + } + + /* recursion */ + pcheck_TableauToProofTask(tab_RightBranch(T), ProofFileName, DestPrefix); + pcheck_TableauToProofTask(tab_LeftBranch(T), ProofFileName, DestPrefix); +} + + +int pcheck_SeqProofDepth(LIST Proof) +/************************************************************** + INPUT : A sequential proof (list of clauses) + RETURNS: The maximum clause depth in the proof +***************************************************************/ +{ + int Max; + + Max = 0; + for ( ; !list_Empty(Proof); Proof = list_Cdr(Proof)) + if (clause_Depth(list_Car(Proof)) > Max) + Max = clause_Depth(list_Car(Proof)); + + return Max; +} + + +LIST pcheck_ReduceSPASSProof(LIST Proof) +/************************************************************** + INPUT: A list of clauses representing a SPASS proof. + Parents are pointers. + RETURNS: A list of clauses were incomplete splits + and closed branches with descendants have been + removed. +***************************************************************/ +{ + LIST EmptyClauses, RedundantClauses; + LIST ReducedProof; + TABLEAU Tableau; + LIST UnmarkedSplits; + + if (!pcheck_BuildTableauFromProof(Proof, &Tableau)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Error: Proof could not be translated into a closed tableau.\n"); + misc_FinishUserErrorReport(); + } + + RedundantClauses = list_Nil(); + Tableau = tab_PruneClosedBranches(Tableau, &RedundantClauses); + Tableau = tab_RemoveIncompleteSplits(Tableau, &RedundantClauses); + list_Delete(RedundantClauses); + + tab_SetSplitLevels(Tableau); + + /* + * get minimal proof: First find earliest derived empty clauses, + * then recursively mark ancestors of these clauses. Put + * only marked clauses in <ReducedProof>. + */ + + EmptyClauses = list_Nil(); + tab_GetEarliestEmptyClauses(Tableau, &EmptyClauses); + pcheck_ClauseListRemoveFlag(Proof, MARKED); + pcheck_MarkRecursive(EmptyClauses); + UnmarkedSplits = list_Nil(); + pcheck_CollectUnmarkedSplits(Tableau, &UnmarkedSplits); + pcheck_MarkRecursive(UnmarkedSplits); + pcheck_RemoveUnmarkedFromTableau(Tableau); + list_Delete(UnmarkedSplits); + + ReducedProof = list_Nil(); + tab_ToClauseList(Tableau, &ReducedProof); + ReducedProof = pcheck_ClauseNumberMergeSort(ReducedProof); + + tab_Delete(Tableau); + list_Delete(EmptyClauses); + + return ReducedProof; +} + + +void pcheck_DeleteProof(LIST Proof) +/************************************************************** + INPUT: A Proof + RETURNS: Nothing. + EFFECTS: Frees memory associated with proof +**************************************************************/ +{ + LIST Line, Scan2, Scan1; + + Scan1 = Proof; + while (!list_Empty(Scan1)) { + Line = list_Car(Scan1); + + string_StringFree(list_Car(Line)); + if (list_Second(Line) != clause_Null()) /* clause */ + term_Delete(list_Second(Line)); + + /* delete labels in justification list and list itself */ + + for (Scan2 = list_Third(Line); !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) + string_StringFree(list_Car(Scan2)); + list_Delete(list_Third(Line)); + + /* now contents of line are deleted. Delete line. */ + list_Delete(Line); + Scan1 = list_Cdr(Scan1); + } + list_Delete(Proof); +} + + +char* pcheck_GenericFilename(const char* Filename, const char* Id) +/************************************************************** + INPUT: Two strings. + RETURNS: A string with Suffix as new extension to Filename + (Filename = name.ext -> name_<Id>.prf) + EFFECTS: Memory is allocated for the returned string. +**************************************************************/ +{ + char *Help1, *Help2; + int i; + + Help1 = string_Conc("_", Id); + Help2 = string_Conc(Help1, pcheck_ProofFileSuffix); + string_StringFree(Help1); + + /* remove filename extension */ + for (i = 0; Filename[i] != '.' && i < strlen(Filename); i++) + /* empty */; + Help1 = string_Prefix(Filename, i); + + return string_Nconc(Help1, Help2); /* Help1 and Help2 are freed, too */ +} + + +void pcheck_ClauseListRemoveFlag(LIST Clauses, CLAUSE_FLAGS Flag) +/************************************************************** + INPUT: A list of clauses and a clause flag + RETURNS: Nothing. + EFFECTS: Removes the <Flag> in all clauses in the list +**************************************************************/ +{ + for (; !list_Empty(Clauses); Clauses = list_Cdr(Clauses)) + clause_RemoveFlag(list_Car(Clauses), Flag); +} + + +LIST pcheck_ClauseNumberMergeSort(LIST L) +/************************************************************** + INPUT: A list of clauses + RETURNS: The sorted list: clause_Number(L[i]) < clause_Number(L[i+1]) + EFFECTS: Destructive +***************************************************************/ +{ + return clause_NumberSort(L); +} |