| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * REPRESENTATION OF PROOF SEARCH * */ |
| /* * * */ |
| /* * $Module: PROOF SEARCH * */ |
| /* * * */ |
| /* * Copyright (C) 1997, 1998, 1999, 2000, 2001 * */ |
| /* * MPI fuer Informatik * */ |
| /* * * */ |
| /* * This program is free software; you can redistribute * */ |
| /* * it and/or modify it under the terms of the GNU * */ |
| /* * General Public License as published by the Free * */ |
| /* * Software Foundation; either version 2 of the License, * */ |
| /* * or (at your option) any later version. * */ |
| /* * * */ |
| /* * This program is distributed in the hope that it will * */ |
| /* * be useful, but WITHOUT ANY WARRANTY; without even * */ |
| /* * the implied warranty of MERCHANTABILITY or FITNESS * */ |
| /* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ |
| /* * License for more details. * */ |
| /* * * */ |
| /* * You should have received a copy of the GNU General * */ |
| /* * Public License along with this program; if not, write * */ |
| /* * to the Free Software Foundation, Inc., 59 Temple * */ |
| /* * Place, Suite 330, Boston, MA 02111-1307 USA * */ |
| /* * * */ |
| /* * * */ |
| /* $Revision$ * */ |
| /* $State$ * */ |
| /* $Date$ * */ |
| /* $Author$ * */ |
| /* * * */ |
| /* * Contact: * */ |
| /* * Christoph Weidenbach * */ |
| /* * MPI fuer Informatik * */ |
| /* * Stuhlsatzenhausweg 85 * */ |
| /* * 66123 Saarbruecken * */ |
| /* * Email: weidenb@mpi-sb.mpg.de * */ |
| /* * Germany * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| /* $RCSfile$ */ |
| |
| |
| #include "search.h" |
| #include "defs.h" |
| |
| |
| /**************************************************************/ |
| /* Functions */ |
| /**************************************************************/ |
| |
| static SPLIT prfs_SplitCreate(PROOFSEARCH PS) |
| /************************************************************** |
| INPUT: A proofsearch object |
| RETURNS: A new split object, which is initialized. |
| MEMORY: Allocates memory for the SPLIT_NODE. |
| EFFECT: Increases the split level of the proof search object. |
| ***************************************************************/ |
| { |
| SPLIT Result; |
| |
| prfs_IncValidLevel(PS); |
| |
| Result = (SPLIT)memory_Malloc(sizeof(SPLIT_NODE)); |
| Result->splitlevel = prfs_ValidLevel(PS); |
| Result->used = FALSE; |
| Result->blockedClauses = list_Nil(); |
| Result->deletedClauses = list_Nil(); |
| Result->father = (CLAUSE) NULL; |
| return Result; |
| } |
| |
| |
| static void prfs_SplitDelete(SPLIT S) |
| /************************************************************** |
| INPUT: A split |
| RETURNS: Nothing. |
| MEMORY: Deletes blocked and deleted clauses. Frees the split. |
| ***************************************************************/ |
| { |
| clause_DeleteClauseList(S->blockedClauses); |
| clause_DeleteClauseList(S->deletedClauses); |
| if (S->father != (CLAUSE)NULL) |
| clause_Delete(S->father); |
| prfs_SplitFree(S); |
| } |
| |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * DEBUGGING FUNCTIONS * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| BOOL prfs_Check(PROOFSEARCH Search) |
| /************************************************************** |
| INPUT: A proof search object. |
| EFFECT: None. |
| RETURNS: TRUE if all invariants about <Search> are valid. |
| ***************************************************************/ |
| { |
| LIST Scan,Clauses; |
| SPLIT Split; |
| CLAUSE Clause; |
| |
| for (Scan=prfs_UsableClauses(Search);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| Clause = (CLAUSE)list_Car(Scan); |
| if (!clause_IsClause(Clause, prfs_Store(Search), prfs_Precedence(Search)) || |
| clause_GetFlag(Clause, WORKEDOFF) || |
| !prfs_IsClauseValid(Clause, prfs_ValidLevel(Search))) |
| return FALSE; |
| } |
| |
| for (Scan=prfs_WorkedOffClauses(Search);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| Clause = (CLAUSE)list_Car(Scan); |
| if (!clause_IsClause(Clause, prfs_Store(Search), prfs_Precedence(Search)) || |
| !clause_GetFlag(Clause,WORKEDOFF) || |
| !prfs_IsClauseValid(Clause, prfs_ValidLevel(Search))) |
| return FALSE; |
| } |
| |
| for (Scan=prfs_SplitStack(Search); !list_Empty(Scan); Scan=list_Cdr(Scan)) { |
| Split = (SPLIT)list_Car(Scan); |
| if (prfs_SplitIsUsed(Split)) { |
| if (!list_Empty(prfs_SplitBlockedClauses(Split)) || |
| !list_Empty(prfs_SplitDeletedClauses(Split))) { |
| /*putchar('\n');prfs_PrintSplit(Split); putchar('\n');*/ |
| return FALSE; |
| } else { |
| for (Clauses=prfs_UsableClauses(Search);!list_Empty(Clauses);Clauses=list_Cdr(Clauses)) |
| if (clause_SplitLevel(list_Car(Clauses)) == prfs_SplitSplitLevel(Split)) { |
| /*puts("\n");prfs_PrintSplit(Split); |
| fputs("\n Clause must not exist: ",stdout); |
| clause_Print(list_Car(Clauses)); putchar('\n');*/ |
| return FALSE; |
| } |
| for (Clauses=prfs_WorkedOffClauses(Search);!list_Empty(Clauses);Clauses=list_Cdr(Clauses)) |
| if (clause_SplitLevel(list_Car(Clauses)) == prfs_SplitSplitLevel(Split)) { |
| /*puts("\n");prfs_PrintSplit(Split); |
| fputs("\n Clause must not exist: ",stdout); |
| clause_Print(list_Car(Clauses)); putchar('\n');*/ |
| return FALSE; |
| } |
| } |
| } |
| } |
| |
| if (prfs_ValidLevel(Search) == 0) { |
| if (!prfs_SplitStackEmpty(Search)) |
| return FALSE; |
| } else { |
| if (prfs_ValidLevel(Search) != prfs_SplitSplitLevel(prfs_SplitStackTop(Search))) |
| return FALSE; |
| } |
| |
| if (prfs_ValidLevel(Search) < prfs_LastBacktrackLevel(Search)) |
| return FALSE; |
| |
| return TRUE; |
| } |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * HIGH LEVEL FUNCTIONS * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| static void prfs_InsertInSortTheories(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| EFFECT: If the clause is a declaration clause it is inserted |
| into the dynamic and approximated dynamic sort theory. |
| RETURNS: Nothing. |
| ***************************************************************/ |
| { |
| if ((prfs_DynamicSortTheory(Search) != (SORTTHEORY)NULL || |
| prfs_ApproximatedDynamicSortTheory(Search) != (SORTTHEORY)NULL) && |
| clause_IsDeclarationClause(Clause)) { |
| int i,l; |
| LITERAL lit; |
| CLAUSE copy; |
| LIST approx; |
| l = clause_Length(Clause); |
| for (i = clause_FirstSuccedentLitIndex(Clause); i < l; i++) { |
| lit = clause_GetLiteral(Clause,i); |
| if (clause_LiteralIsMaximal(lit) && |
| symbol_IsBaseSort(term_TopSymbol(clause_LiteralSignedAtom(lit)))) { |
| if (prfs_DynamicSortTheory(Search) != (SORTTHEORY)NULL) { |
| copy = clause_Copy(Clause); |
| list_Delete(clause_ParentClauses(copy)); |
| clause_SetParentClauses(copy,list_Nil()); |
| list_Delete(clause_ParentLiterals(copy)); |
| clause_SetParentLiterals(copy,list_Nil()); |
| clause_SetNumber(copy,clause_Number(Clause)); |
| sort_TheoryInsertClause(prfs_DynamicSortTheory(Search),Clause, |
| copy,clause_GetLiteral(copy,i)); |
| } |
| if (prfs_ApproximatedDynamicSortTheory(Search) != (SORTTHEORY)NULL) { |
| approx = sort_ApproxMaxDeclClauses(Clause, prfs_Store(Search), |
| prfs_Precedence(Search)); |
| for ( ; !list_Empty(approx); approx = list_Pop(approx)) { |
| copy = (CLAUSE)list_Car(approx); |
| sort_TheoryInsertClause(prfs_ApproximatedDynamicSortTheory(Search), |
| Clause, copy, |
| clause_GetLiteral(copy,clause_FirstSuccedentLitIndex(copy))); |
| } |
| } |
| } |
| } |
| } |
| } |
| |
| |
| static void prfs_DeleteFromSortTheories(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: If the clause is a declaration clause it is deleted |
| from the dynamic and approximated dynamic sort theory. |
| ***************************************************************/ |
| { |
| if (clause_IsDeclarationClause(Clause)) { |
| if (prfs_DynamicSortTheory(Search) != (SORTTHEORY)NULL) |
| sort_TheoryDeleteClause(prfs_DynamicSortTheory(Search), Clause); |
| if (prfs_ApproximatedDynamicSortTheory(Search) != (SORTTHEORY)NULL) |
| sort_TheoryDeleteClause(prfs_ApproximatedDynamicSortTheory(Search), Clause); |
| } |
| } |
| |
| |
| void prfs_DeleteDocProof(PROOFSEARCH Search) |
| /************************************************************** |
| INPUT: A proof search object. |
| RETURNS: Nothing. |
| EFFECT: The docproof structures are deleted. |
| ***************************************************************/ |
| { |
| clause_DeleteSharedClauseList(prfs_DocProofClauses(Search), |
| prfs_DocProofSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| if (prfs_DocProofSharingIndex(Search)) |
| sharing_IndexDelete(prfs_DocProofSharingIndex(Search)); |
| Search->dpindex = NULL; |
| Search->dplist = list_Nil(); |
| } |
| |
| |
| static void prfs_InternalDelete(PROOFSEARCH Search) |
| /************************************************************** |
| INPUT: A proof search object. |
| RETURNS: Nothing. |
| EFFECT: Most of the proofsearch object is deleted. |
| This function implements the common subset of |
| functionality of prfs_Clean and prfs_Delete. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| clause_DeleteClauseList(prfs_EmptyClauses(Search)); |
| list_DeleteWithElement(prfs_Definitions(Search), |
| (void (*)(POINTER)) def_Delete); |
| list_Delete(prfs_UsedEmptyClauses(Search)); |
| sort_TheoryDelete(prfs_StaticSortTheory(Search)); |
| sort_TheoryDelete(prfs_DynamicSortTheory(Search)); |
| sort_TheoryDelete(prfs_ApproximatedDynamicSortTheory(Search)); |
| clause_DeleteSharedClauseList(prfs_WorkedOffClauses(Search), |
| prfs_WorkedOffSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| clause_DeleteSharedClauseList(prfs_UsableClauses(Search), |
| prfs_UsableSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| clause_DeleteSharedClauseList(prfs_DocProofClauses(Search), |
| prfs_DocProofSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| prfs_DeleteFinMonPreds(Search); |
| for (Scan=prfs_SplitStack(Search); !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| prfs_SplitDelete(list_Car(Scan)); |
| list_Delete(prfs_SplitStack(Search)); |
| } |
| |
| |
| void prfs_Delete(PROOFSEARCH Search) |
| /************************************************************** |
| INPUT: A proof search object. |
| RETURNS: Nothing. |
| EFFECT: The whole structure including all its substructures |
| is deleted. |
| ***************************************************************/ |
| { |
| prfs_InternalDelete(Search); |
| |
| sharing_IndexDelete(prfs_WorkedOffSharingIndex(Search)); |
| sharing_IndexDelete(prfs_UsableSharingIndex(Search)); |
| if (prfs_DocProofSharingIndex(Search)) |
| sharing_IndexDelete(prfs_DocProofSharingIndex(Search)); |
| flag_DeleteStore(prfs_Store(Search)); |
| symbol_DeletePrecedence(prfs_Precedence(Search)); |
| memory_Free(Search,sizeof(PROOFSEARCH_NODE)); |
| } |
| |
| |
| void prfs_Clean(PROOFSEARCH Search) |
| /************************************************************** |
| INPUT: A proof search object. |
| RETURNS: Nothing. |
| EFFECT: All clauses are deleted. The structure is cleaned |
| and initialized. |
| ***************************************************************/ |
| { |
| prfs_InternalDelete(Search); |
| |
| Search->emptyclauses = list_Nil(); |
| Search->definitions = list_Nil(); |
| Search->usedemptyclauses = list_Nil(); |
| Search->wolist = list_Nil(); |
| Search->uslist = list_Nil(); |
| Search->finmonpreds = list_Nil(); |
| Search->astatic = (SORTTHEORY)NULL; |
| Search->adynamic = (SORTTHEORY)NULL; |
| Search->dynamic = (SORTTHEORY)NULL; |
| Search->dplist = list_Nil(); |
| |
| Search->stack = list_StackBottom(); |
| Search->validlevel = 0; |
| Search->lastbacktrack = 0; |
| Search->splitcounter = 0; |
| Search->keptclauses = 0; |
| Search->derivedclauses = 0; |
| Search->loops = 0; |
| Search->backtracked = 0; |
| Search->nontrivclausenumber = 0; |
| |
| symbol_ClearPrecedence(prfs_Precedence(Search)); |
| } |
| |
| |
| void prfs_SwapIndexes(PROOFSEARCH Search) |
| /************************************************************** |
| INPUT: A proof search object. |
| RETURNS: Nothing. |
| EFFECT: The usable and worked-off indexes are exchanged. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| SHARED_INDEX Help; |
| |
| Help = prfs_WorkedOffSharingIndex(Search); |
| Scan = prfs_WorkedOffClauses(Search); |
| prfs_SetWorkedOffClauses(Search,prfs_UsableClauses(Search)); |
| Search->woindex = prfs_UsableSharingIndex(Search); |
| prfs_SetUsableClauses(Search, Scan); |
| Search->usindex = Help; |
| |
| for (Scan=prfs_UsableClauses(Search); !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| clause_RemoveFlag(list_Car(Scan), WORKEDOFF); |
| for (Scan=prfs_WorkedOffClauses(Search);!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| clause_SetFlag(list_Car(Scan), WORKEDOFF); |
| } |
| |
| |
| PROOFSEARCH prfs_Create(void) |
| /************************************************************** |
| INPUT: None. |
| RETURNS: A new proof search object. The worked off and usable |
| indexes are created whilst the docproof index and the |
| sort theories are not created, since they are not |
| needed in general. |
| ***************************************************************/ |
| { |
| PROOFSEARCH Result; |
| |
| Result = memory_Malloc(sizeof(PROOFSEARCH_NODE)); |
| |
| Result->emptyclauses = list_Nil(); |
| Result->definitions = list_Nil(); |
| Result->usedemptyclauses = list_Nil(); |
| Result->woindex = sharing_IndexCreate(); |
| Result->wolist = list_Nil(); |
| Result->usindex = sharing_IndexCreate(); |
| Result->uslist = list_Nil(); |
| Result->finmonpreds = list_Nil(); |
| |
| Result->astatic = (SORTTHEORY)NULL; |
| Result->adynamic = (SORTTHEORY)NULL; |
| Result->dynamic = (SORTTHEORY)NULL; |
| |
| Result->precedence = symbol_CreatePrecedence(); |
| |
| Result->store = flag_CreateStore(); |
| flag_InitStoreByDefaults(Result->store); |
| |
| Result->dpindex = (SHARED_INDEX)NULL; |
| Result->dplist = list_Nil(); |
| |
| Result->stack = list_StackBottom(); |
| Result->validlevel = 0; |
| Result->lastbacktrack = 0; |
| Result->splitcounter = 0; |
| Result->keptclauses = 0; |
| Result->derivedclauses = 0; |
| Result->loops = 0; |
| Result->backtracked = 0; |
| Result->nontrivclausenumber = 0; |
| |
| return Result; |
| } |
| |
| |
| void prfs_CopyIndices(PROOFSEARCH Search, PROOFSEARCH SearchCopy) |
| /************************************************************** |
| INPUT: A proof search object and a clean proof search object. |
| RETURNS: Nothing. |
| EFFECT: Copies the indices from Search to SearchCopy. |
| CAUTION: Splitstack and theories are not copied! |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| /* If a DocProof index is required but not yet allocated in SearchCopy, |
| do it now */ |
| if (prfs_DocProofSharingIndex(Search) != NULL && |
| prfs_DocProofSharingIndex(SearchCopy) == NULL) |
| prfs_AddDocProofSharingIndex(SearchCopy); |
| |
| /* Copy usable, worked-off and docproof index */ |
| for (Scan = prfs_UsableClauses(Search); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| prfs_InsertUsableClause(SearchCopy, clause_Copy((CLAUSE) list_Car(Scan))); |
| |
| for (Scan = prfs_WorkedOffClauses(Search); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| prfs_InsertWorkedOffClause(SearchCopy, clause_Copy((CLAUSE) list_Car(Scan))); |
| |
| for (Scan = prfs_DocProofClauses(Search); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| prfs_InsertDocProofClause(SearchCopy, clause_Copy((CLAUSE) list_Car(Scan))); |
| } |
| |
| |
| void prfs_InsertWorkedOffClause(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| MEMORY: The clause is assumed to be unshared. |
| EFFECT: The clause is inserted into the worked off sharing index |
| and list of <Search>. The unshared literals are deleted. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsClause(Clause,prfs_Store(Search), prfs_Precedence(Search))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_InsertWorkedOffClause: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| clause_SetFlag(Clause,WORKEDOFF); |
| prfs_SetWorkedOffClauses(Search,list_Cons(Clause, prfs_WorkedOffClauses(Search))); |
| clause_InsertIntoSharing(Clause, prfs_WorkedOffSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| prfs_InsertInSortTheories(Search, Clause); |
| } |
| |
| |
| void prfs_InsertUsableClause(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| MEMORY: The clause is assumed to be unshared. |
| EFFECT: The clause is inserted into the usable sharing index |
| and list of <Search> sorted with respect to their weight. |
| The unshared literals are deleted. |
| ***************************************************************/ |
| { |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, prfs_Store(Search), prfs_Precedence(Search)) || |
| clause_GetFlag(Clause, WORKEDOFF)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_InsertUsableClause: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| /* The invariant that no two clauses have the same clause number cannot */ |
| /* be guaranteed as long as e.g. several directly subsequent reductions */ |
| /* are applied to a clause that eventually gets a greater split level. */ |
| #endif |
| |
| prfs_SetUsableClauses(Search,clause_InsertWeighed(Clause, |
| prfs_UsableClauses(Search), |
| prfs_Store(Search), |
| prfs_Precedence(Search))); |
| clause_InsertIntoSharing(Clause, prfs_UsableSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| } |
| |
| |
| void prfs_InsertDocProofClause(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| MEMORY: The clause is assumed to be unshared. |
| EFFECT: The clause is inserted into the proof documentation sharing index. |
| The unshared literals are deleted. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, prfs_Store(Search), prfs_Precedence(Search))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_InsertDocProofClause: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (prfs_DocProofSharingIndex(Search) == (SHARED_INDEX)NULL) |
| clause_Delete(Clause); |
| else { |
| prfs_SetDocProofClauses(Search,list_Cons(Clause, prfs_DocProofClauses(Search))); |
| clause_InsertIntoSharing(Clause, prfs_DocProofSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| } |
| } |
| |
| |
| void prfs_MoveUsableWorkedOff(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: The clause is inserted into the worked off sharing index |
| and list and it is deleted from the usable index and list. |
| In particular, the WorkedOff flag is set and if <Clause> is a |
| declaration clause, it is inserted into the respective sort theories. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsClause(Clause,prfs_Store(Search), prfs_Precedence(Search)) || |
| clause_GetFlag(Clause, WORKEDOFF)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_MoveUsableWorkedOff: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_SetUsableClauses(Search,list_PointerDeleteElement(prfs_UsableClauses(Search),Clause)); |
| clause_SetFlag(Clause,WORKEDOFF); |
| clause_MoveSharedClause(Clause, prfs_UsableSharingIndex(Search), |
| prfs_WorkedOffSharingIndex(Search), prfs_Store(Search), |
| prfs_Precedence(Search)); |
| prfs_SetWorkedOffClauses(Search,list_Cons(Clause, prfs_WorkedOffClauses(Search))); |
| prfs_InsertInSortTheories(Search, Clause); |
| } |
| |
| |
| void prfs_MoveWorkedOffDocProof(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: The clause is inserted into the doc proof sharing index |
| and list of <Search> and it is deleted from the worked off |
| index and list. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, prfs_Store(Search), prfs_Precedence(Search)) || |
| !clause_GetFlag(Clause, WORKEDOFF)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_MoveWorkedOffDocProof: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_DeleteFromSortTheories(Search, Clause); |
| prfs_SetWorkedOffClauses(Search,list_PointerDeleteElement(prfs_WorkedOffClauses(Search),Clause)); |
| clause_RemoveFlag(Clause,WORKEDOFF); |
| |
| if (prfs_DocProofSharingIndex(Search) == (SHARED_INDEX)NULL) |
| clause_DeleteFromSharing(Clause,prfs_WorkedOffSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| else { |
| clause_MoveSharedClause(Clause, prfs_WorkedOffSharingIndex(Search), |
| prfs_DocProofSharingIndex(Search),prfs_Store(Search), |
| prfs_Precedence(Search)); |
| prfs_SetDocProofClauses(Search,list_Cons(Clause, prfs_DocProofClauses(Search))); |
| } |
| } |
| |
| |
| void prfs_MoveUsableDocProof(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: The clause is inserted into the doc proof sharing index |
| and list of <Search> and it is deleted from the usable |
| index and list. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, prfs_Store(Search), prfs_Precedence(Search)) || |
| clause_GetFlag(Clause, WORKEDOFF)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_MoveUsableDocProof: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_SetUsableClauses(Search,list_PointerDeleteElement(prfs_UsableClauses(Search),Clause)); |
| |
| if (prfs_DocProofSharingIndex(Search) == (SHARED_INDEX)NULL) |
| clause_DeleteFromSharing(Clause, prfs_UsableSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| else { |
| clause_MoveSharedClause(Clause, prfs_UsableSharingIndex(Search), |
| prfs_DocProofSharingIndex(Search),prfs_Store(Search), |
| prfs_Precedence(Search)); |
| prfs_SetDocProofClauses(Search,list_Cons(Clause, prfs_DocProofClauses(Search))); |
| } |
| } |
| |
| |
| void prfs_MoveInvalidClausesDocProof(PROOFSEARCH Search) |
| /************************************************************** |
| INPUT: A proof search object. |
| RETURNS: Nothing. |
| EFFECT: All clauses that have a split level higher than the |
| current split level of <Search> are moved to the |
| proof documentation index. If it does not exist, i.e., |
| no proof documentation required, the clauses are |
| deleted. |
| ***************************************************************/ |
| { |
| LIST scan, invalid; |
| CLAUSE clause; |
| |
| invalid = list_Nil(); |
| for (scan = prfs_WorkedOffClauses(Search); !list_Empty(scan); |
| scan = list_Cdr(scan)) { |
| clause = (CLAUSE)list_Car(scan); |
| if (!prfs_IsClauseValid(clause, prfs_ValidLevel(Search))) |
| invalid = list_Cons(clause,invalid); |
| } |
| /* WARNING: The following move operation changes the worked off */ |
| /* set of the proof search object destructively. */ |
| /* So it's impossible to move those function calls into the */ |
| /* loop above. */ |
| for ( ; !list_Empty(invalid); invalid = list_Pop(invalid)) |
| prfs_MoveWorkedOffDocProof(Search,list_Car(invalid)); |
| |
| invalid = list_Nil(); |
| for (scan = prfs_UsableClauses(Search); !list_Empty(scan); |
| scan = list_Cdr(scan)) { |
| clause = (CLAUSE)list_Car(scan); |
| if (!prfs_IsClauseValid(clause, prfs_ValidLevel(Search))) |
| invalid = list_Cons(clause,invalid); |
| } |
| /* WARNING: The following move operation changes the usable */ |
| /* set of the proof search object destructively. */ |
| /* So it's impossible to move those function calls into the */ |
| /* loop above. */ |
| for ( ; !list_Empty(invalid); invalid = list_Pop(invalid)) |
| prfs_MoveUsableDocProof(Search,list_Car(invalid)); |
| } |
| |
| |
| void prfs_ExtractWorkedOff(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: The clause is removed from the worked off index and |
| list and returned as an unshared clause. |
| Sort theories are updated accordingly. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause) || !clause_GetFlag(Clause, WORKEDOFF)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_ExtractWorkedOff: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_DeleteFromSortTheories(Search, Clause); |
| clause_RemoveFlag(Clause,WORKEDOFF); |
| prfs_SetWorkedOffClauses(Search,list_PointerDeleteElement(prfs_WorkedOffClauses(Search),Clause)); |
| clause_MakeUnshared(Clause,prfs_WorkedOffSharingIndex(Search)); |
| } |
| |
| |
| void prfs_ExtractUsable(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: The clause is removed from the usable off index and |
| list and returned as an unshared clause. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause) || clause_GetFlag(Clause, WORKEDOFF)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_ExtractUsable: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_SetUsableClauses(Search,list_PointerDeleteElement(prfs_UsableClauses(Search),Clause)); |
| clause_MakeUnshared(Clause,prfs_UsableSharingIndex(Search)); |
| } |
| |
| |
| void prfs_ExtractDocProof(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: The clause is removed from the docproof off index and |
| list and returned as an unshared clause. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_ExtractDocProof: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_SetDocProofClauses(Search,list_PointerDeleteElement(prfs_DocProofClauses(Search),Clause)); |
| clause_MakeUnshared(Clause,prfs_DocProofSharingIndex(Search)); |
| } |
| |
| |
| void prfs_DeleteWorkedOff(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: The clause is deleted from the worked off index and list. |
| Sort theories are updated accordingly. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, prfs_Store(Search), prfs_Precedence(Search)) || |
| !clause_GetFlag(Clause, WORKEDOFF)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_DeleteWorkedOff: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_DeleteFromSortTheories(Search, Clause); |
| prfs_SetWorkedOffClauses(Search,list_PointerDeleteElement(prfs_WorkedOffClauses(Search),Clause)); |
| clause_DeleteFromSharing(Clause, prfs_WorkedOffSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| } |
| |
| |
| void prfs_DeleteUsable(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and a clause. |
| RETURNS: Nothing. |
| EFFECT: The clause is deleted from the usable index and list. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, prfs_Store(Search), prfs_Precedence(Search)) || |
| clause_GetFlag(Clause, WORKEDOFF)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_DeleteUsable: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_SetUsableClauses(Search,list_PointerDeleteElement(prfs_UsableClauses(Search),Clause)); |
| clause_DeleteFromSharing(Clause,prfs_UsableSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| } |
| |
| |
| void prfs_PrintSplit(SPLIT Split) |
| /************************************************************** |
| INPUT: A split. |
| RETURNS: Nothing. |
| EFFECT: Prints the information kept in the split structure. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| printf("\n Split: %d %ld", prfs_SplitSplitLevel(Split), (long)Split); |
| fputs("\n Father: ", stdout); |
| if (prfs_SplitFatherClause(Split) != (CLAUSE)NULL) |
| clause_Print(prfs_SplitFatherClause(Split)); |
| else |
| fputs("No father, unnecessary split.", stdout); |
| |
| fputs("\n Split is ", stdout); |
| if (prfs_SplitIsUnused(Split)) |
| puts("unused."); |
| else |
| puts("used."); |
| fputs(" Blocked clauses:", stdout); |
| for (Scan=prfs_SplitBlockedClauses(Split);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| putchar('\n'); |
| putchar(' '); |
| clause_Print(list_Car(Scan)); |
| } |
| fputs("\n Deleted clauses:", stdout); |
| for (Scan=prfs_SplitDeletedClauses(Split);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| putchar('\n'); |
| putchar(' '); |
| clause_Print(list_Car(Scan)); |
| } |
| } |
| |
| |
| void prfs_PrintSplitStack(PROOFSEARCH PS) |
| /************************************************************** |
| INPUT: A proof search object. |
| RETURNS: Nothing. |
| EFFECT: Prints almost all the information kept in the |
| split stack structure. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| fputs("\n Splitstack:", stdout); |
| |
| for (Scan = prfs_SplitStack(PS); !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| prfs_PrintSplit(list_Car(Scan)); |
| fputs("\n---------------------", stdout); |
| } |
| } |
| |
| |
| void prfs_Print(PROOFSEARCH Search) |
| /************************************************************** |
| INPUT: A proof search object. |
| RETURNS: void. |
| EFFECT: The proof search object is printed to stdout. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| #ifdef CHECK |
| if (!prfs_Check(Search)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_Print: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| printf("\n\n Proofsearch: Current Level: %d Last Backtrack Level: %d Splits: %d Loops: %d Backtracked: %d", |
| prfs_ValidLevel(Search),prfs_LastBacktrackLevel(Search),prfs_SplitCounter(Search), |
| prfs_Loops(Search),prfs_BacktrackedClauses(Search)); |
| if (prfs_NonTrivClauseNumber(Search)>0) |
| printf("\n Clause %d implies a non-trivial domain.", prfs_NonTrivClauseNumber(Search)); |
| else |
| fputs("\n Potentially trivial domain.", stdout); |
| fputs("\n Empty Clauses:", stdout); |
| for (Scan=prfs_EmptyClauses(Search);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| fputs("\n ", stdout); |
| clause_Print(list_Car(Scan)); |
| } |
| fputs("\n Definitions:", stdout); |
| for (Scan=prfs_Definitions(Search);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| putchar('\n'); |
| putchar(' '); |
| term_Print(list_Car(Scan)); |
| } |
| fputs("\n Worked Off Clauses:", stdout); |
| for (Scan=prfs_WorkedOffClauses(Search);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| putchar('\n'); |
| putchar(' '); |
| clause_Print(list_Car(Scan)); |
| } |
| fputs("\n Usable Clauses:", stdout); |
| for (Scan=prfs_UsableClauses(Search);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| putchar('\n'); |
| putchar(' '); |
| clause_Print(list_Car(Scan)); |
| } |
| fputs("\n Finite predicates:", stdout); |
| for (Scan=prfs_GetFinMonPreds(Search);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| fputs("\n ", stdout); |
| symbol_Print((SYMBOL)list_PairFirst(list_Car(Scan))); |
| fputs(": ", stdout); |
| term_TermListPrintPrefix(list_PairSecond(list_Car(Scan))); |
| } |
| prfs_PrintSplitStack(Search); |
| fputs("\n Static Sort Theory:", stdout); |
| sort_TheoryPrint(prfs_StaticSortTheory(Search)); |
| fputs("\n Dynamic Sort Theory:", stdout); |
| sort_TheoryPrint(prfs_DynamicSortTheory(Search)); |
| fputs("\n Approximated Dynamic Sort Theory:", stdout); |
| sort_TheoryPrint(prfs_ApproximatedDynamicSortTheory(Search)); |
| putchar('\n'); |
| } |
| |
| |
| CLAUSE prfs_DoSplitting(PROOFSEARCH PS, CLAUSE SplitClause, LIST Literals) |
| /************************************************************** |
| INPUT: An proof search object, an unshared clause to be splitted |
| where 'Literals' is the list of literals to keep (in their |
| order in the SplitClause). |
| RETURNS: A pointer to the (stack-, not sharing-) inserted splitted clause. |
| MEMORY: The blocked parts and the actparts literals are created |
| unshared, memory for the two (more for HornSplits) new |
| clausenodes is allocated. |
| EFFECT: A new SPLIT object is created on the split stack of the proof |
| search object. The clause for the right branch will get clause |
| number 0 to make it distinguishable from the negation clauses, |
| which get clause number -1. |
| All newly created clauses are influenced by some flags of the |
| internal flag store of the proof search object. |
| For example the maximal literals are influenced by |
| the weight of function symbols, which is defined by the |
| flag "flag_FUNCWEIGHT". |
| ***************************************************************/ |
| { |
| |
| SPLIT NewSplit; |
| CLAUSE NewClause, BlockedClause; |
| LITERAL NextLit,NewLit; |
| int i,j,lengthBlocked,lengthNew,lc,la,ls,nc,na,ns; |
| |
| #ifdef CHECK |
| if (list_Empty(Literals) || |
| !clause_IsClause(SplitClause, prfs_Store(PS), prfs_Precedence(PS))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_DoSplitting: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| prfs_DecSplitCounter(PS); |
| NewSplit = prfs_SplitCreate(PS); |
| |
| prfs_SplitSetFatherClause(NewSplit, SplitClause); |
| |
| lengthNew = list_Length(Literals); |
| lengthBlocked = clause_Length(SplitClause) - lengthNew; |
| |
| NewClause = clause_CreateBody(lengthNew); /* The left clause */ |
| BlockedClause = clause_CreateBody(lengthBlocked); /* The right clause */ |
| clause_DecreaseCounter(); /* reset internally increased counter! */ |
| clause_SetNumber(BlockedClause, 0); |
| /* To detect forgotten setting at insertion! */ |
| |
| lc = clause_LastConstraintLitIndex(SplitClause); |
| la = clause_LastAntecedentLitIndex(SplitClause); |
| ls = clause_LastSuccedentLitIndex(SplitClause); |
| |
| nc = na = ns = 0; |
| |
| j = clause_FirstLitIndex(); |
| |
| for (i = clause_FirstLitIndex(); i <= ls; i++) { |
| NextLit = clause_GetLiteral(SplitClause, i); |
| |
| NewLit = clause_LiteralCopy(NextLit); |
| |
| if ((lengthNew > 0) && /* To avoid access of Nirvana. */ |
| list_PointerMember(Literals, NextLit)) { |
| /* NewLit is literal for the NewClause. */ |
| |
| lengthNew--; |
| clause_SetLiteral(NewClause, j++, NewLit); |
| clause_LiteralSetOwningClause(NewLit, NewClause); |
| clause_AddParentClause(NewClause, clause_Number(SplitClause)); |
| clause_AddParentLiteral(NewClause, i); |
| if (i <= lc) |
| nc++; |
| else if (i <= la) |
| na++; |
| else |
| ns++; |
| |
| } else { /* NewLit is literal for the BlockedClause. */ |
| |
| clause_SetLiteral(BlockedClause, (i-j), NewLit); |
| clause_LiteralSetOwningClause(NewLit, BlockedClause); |
| clause_AddParentClause(BlockedClause, clause_Number(SplitClause)); |
| clause_AddParentLiteral(BlockedClause, i); |
| } |
| } /* end of 'for all literals'. */ |
| |
| clause_SetNumOfConsLits(NewClause, nc); |
| clause_SetNumOfConsLits(BlockedClause, |
| (clause_NumOfConsLits(SplitClause) - nc)); |
| clause_SetNumOfAnteLits(NewClause, na); |
| clause_SetNumOfAnteLits(BlockedClause, |
| (clause_NumOfAnteLits(SplitClause) - na)); |
| clause_SetNumOfSuccLits(NewClause, ns); |
| clause_SetNumOfSuccLits(BlockedClause, |
| (clause_NumOfSuccLits(SplitClause) - ns)); |
| |
| clause_ReInit(BlockedClause, prfs_Store(PS), prfs_Precedence(PS)); |
| clause_UpdateSplitDataFromNewSplitting(BlockedClause, SplitClause, |
| prfs_SplitSplitLevel(NewSplit)); |
| clause_SetFromSplitting(BlockedClause); |
| clause_SetParentLiterals(BlockedClause, |
| list_NReverse(clause_ParentLiterals(BlockedClause))); |
| |
| clause_SetDepth(BlockedClause, clause_Depth(SplitClause)+1); |
| |
| prfs_SplitAddBlockedClause(NewSplit, BlockedClause); |
| prfs_SplitSetDeletedClauses(NewSplit, list_Nil()); |
| |
| |
| prfs_SplitStackPush(PS, NewSplit); |
| |
| clause_ReInit(NewClause, prfs_Store(PS), prfs_Precedence(PS)); |
| clause_UpdateSplitDataFromNewSplitting(NewClause, SplitClause, |
| prfs_SplitSplitLevel(NewSplit)); |
| clause_SetFromSplitting(NewClause); |
| |
| clause_SetParentLiterals(NewClause, |
| list_NReverse(clause_ParentLiterals(NewClause))); |
| |
| clause_SetDepth(NewClause, clause_Depth(SplitClause)+1); |
| clause_RemoveFlag(NewClause, WORKEDOFF); |
| |
| if (clause_IsGround(NewClause)) { |
| /* Keep Clauses made from NewClause for refutation case! */ |
| CLAUSE UnitClause; |
| LIST AtomList; |
| |
| la = clause_LastAntecedentLitIndex(NewClause); |
| ls = clause_LastSuccedentLitIndex(NewClause); |
| |
| Literals = clause_ParentLiterals(NewClause); |
| |
| for (i = clause_FirstLitIndex(); i <= ls; i++) { |
| |
| NextLit = clause_GetLiteral(NewClause, i); |
| AtomList = list_List(term_Copy(clause_LiteralAtom(NextLit))); |
| |
| if (i <= la) |
| UnitClause = clause_Create(list_Nil(), list_Nil(), AtomList, |
| prfs_Store(PS), prfs_Precedence(PS)); |
| else |
| UnitClause = clause_Create(list_Nil(), AtomList, list_Nil(), |
| prfs_Store(PS), prfs_Precedence(PS)); |
| |
| clause_SetNumber(UnitClause, -1); |
| /* To detect forgotten setting at reinsertion! */ |
| clause_DecreaseCounter(); |
| /* Reset internally increased counter! */ |
| |
| list_Delete(AtomList); |
| |
| clause_SetFromSplitting(UnitClause); |
| clause_UpdateSplitDataFromNewSplitting(UnitClause, SplitClause, |
| prfs_SplitSplitLevel(NewSplit)); |
| clause_AddParentClause(UnitClause, clause_Number(NewClause)); |
| clause_AddParentLiteral(UnitClause, i); |
| clause_AddParentClause(UnitClause, clause_Number(SplitClause)); |
| clause_AddParentLiteral(UnitClause, (int)list_Car(Literals)); |
| Literals = list_Cdr(Literals); |
| prfs_SplitAddBlockedClause(NewSplit, UnitClause); |
| } |
| } |
| /* fputs("\n\nSPLITTING DONE!",stdout); |
| fputs("\nAus : ",stdout); clause_Print(SplitClause); fflush(stdout); |
| fputs("\nDer erste Teil: ",stdout); clause_Print(NewClause); fflush(stdout); |
| fputs("\nDer zweite Teil: ",stdout); |
| clause_Print(BlockedClause); fflush(stdout); |
| puts("\nDaher als BlockedClauses:"); |
| clause_ListPrint(prfs_SplitBlockedClauses(NewSplit)); fflush(stdout); |
| */ |
| return NewClause; |
| } |
| |
| |
| static LIST prfs_GetSplitLiterals(PROOFSEARCH PS, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause and a proofsearch object |
| RETURNS: A list of literals building the bigger part of a |
| variable-disjunct literal partition if one exists, |
| an empty list, else. |
| MEMORY: Allocates memory for the literal list. |
| ***************************************************************/ |
| { |
| LITERAL NextLit; |
| int i, length, OldLength; |
| LIST LitList, VarOcc, NextOcc; |
| BOOL Change; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, prfs_Store(PS), prfs_Precedence(PS))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In prfs_GetSplitLiterals: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| LitList = list_Nil(); |
| |
| if (prfs_SplitCounter(PS) != 0) { |
| |
| if (clause_HasSuccLits(Clause)) { |
| if (clause_HasGroundSuccLit(Clause)) { |
| |
| NextLit = clause_GetGroundSuccLit(Clause); |
| LitList = list_Cons(NextLit, LitList); |
| |
| for (i = clause_LastAntecedentLitIndex(Clause);i >= clause_FirstLitIndex();i--) { |
| NextLit = clause_GetLiteral(Clause, i); |
| if (term_IsGround(clause_LiteralAtom(NextLit))) |
| LitList = list_Cons(NextLit, LitList); |
| } |
| return LitList; |
| } |
| |
| /* Clause has no ground succedent literals, but > 1 non-ground */ |
| NextLit = clause_GetLiteral(Clause, clause_LastSuccedentLitIndex(Clause)); |
| VarOcc = term_VariableSymbols(clause_LiteralAtom(NextLit)); |
| LitList = list_List(NextLit); |
| length = clause_Length(Clause); |
| Change = TRUE; |
| |
| while (Change) { |
| Change = FALSE; |
| |
| for (i=clause_LastSuccedentLitIndex(Clause)-1; i>=clause_FirstLitIndex(); i--) { |
| |
| NextLit = clause_GetLiteral(Clause, i); |
| |
| if (!list_PointerMember(LitList, NextLit)) { |
| NextOcc = term_VariableSymbols(clause_LiteralAtom(NextLit)); |
| if (list_HasIntersection(VarOcc, NextOcc)) { |
| OldLength = list_Length(VarOcc); |
| VarOcc = list_NPointerUnion(VarOcc, NextOcc); |
| LitList = list_Cons(NextLit, LitList); |
| if (OldLength != list_Length(VarOcc)) |
| Change = TRUE; |
| } |
| else |
| list_Delete(NextOcc); |
| } |
| } |
| } |
| if (list_Length(LitList) == length) { |
| list_Delete(LitList); |
| LitList = list_Nil(); |
| } |
| Change = TRUE; /* Check whether not all succedent literals are used */ |
| for (i = clause_FirstSuccedentLitIndex(Clause); i < length && Change; i++) |
| if (!list_PointerMember(LitList,clause_GetLiteral(Clause, i))) |
| Change = FALSE; |
| if (Change) { |
| list_Delete(LitList); |
| LitList = list_Nil(); |
| } |
| list_Delete(VarOcc); |
| } |
| } |
| return LitList; |
| } |
| |
| |
| CLAUSE prfs_PerformSplitting(PROOFSEARCH Search, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A proof search object and an unshared clause. |
| EFFECT: If <Clause> can be split it is splitted, the first |
| part of the split is returned and the |
| splitted clause is kept in the split stack. |
| Otherwise <Clause> remains unchanged and NULL is returned. |
| RETURNS: NULL if <Clause> is not splittable, the first split part otherwise. |
| ***************************************************************/ |
| { |
| CLAUSE Result; |
| |
| Result = (CLAUSE)NULL; |
| |
| if (clause_HasSolvedConstraint(Clause)) { |
| LIST LitList; |
| |
| LitList = prfs_GetSplitLiterals(Search, Clause); |
| |
| if (!list_Empty(LitList)) { |
| Result = prfs_DoSplitting(Search, Clause, LitList); |
| list_Delete(LitList); |
| } |
| } |
| |
| return Result; |
| } |
| |
| |
| void prfs_InstallFiniteMonadicPredicates(PROOFSEARCH Search, LIST Clauses, |
| LIST Predicates) |
| /************************************************************** |
| INPUT: A proof search object a list of clauses and a list |
| of monadic predicates. |
| RETURNS: Nothing. |
| EFFECT: The argument terms for <Predicates> that occur in |
| positive unit clauses are extracted from <Clauses> |
| and installed in <Search> as an assoc list. |
| ***************************************************************/ |
| { |
| LIST Pair, Scan, Result; |
| CLAUSE Clause; |
| TERM Atom; |
| |
| Result = list_Nil(); |
| |
| for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| Clause = (CLAUSE)list_Car(Scan); |
| if (clause_Length(Clause) == 1 && |
| clause_NumOfSuccLits(Clause) == 1) { |
| Atom = clause_GetLiteralAtom(Clause,clause_FirstSuccedentLitIndex(Clause)); |
| if (list_PointerMember(Predicates, (POINTER)term_TopSymbol(Atom))) { |
| Pair = list_AssocListPair(Result, (POINTER)term_TopSymbol(Atom)); |
| if (Pair != list_PairNull()) |
| list_PairRplacSecond(Pair, list_Cons(term_Copy(term_FirstArgument(Atom)),list_PairSecond(Pair))); |
| else |
| Result = list_AssocCons(Result, (POINTER)term_TopSymbol(Atom), |
| list_List(term_Copy(term_FirstArgument(Atom)))); |
| } |
| } |
| } |
| |
| prfs_DeleteFinMonPreds(Search); |
| prfs_SetFinMonPreds(Search, Result); |
| } |
| |
| |
| NAT prfs_GetNumberOfInstances(PROOFSEARCH Search, LITERAL Literal, BOOL Usables) |
| /************************************************************** |
| INPUT: A proof search object, a literal, and a boolean flag. |
| RETURNS: The number of instances of the literal's atom. |
| EFFECT: |
| ***************************************************************/ |
| { |
| TERM Atom; |
| NAT NrOfInstances; |
| SHARED_INDEX WOIndex, UsIndex; |
| |
| Atom = clause_LiteralAtom(Literal); |
| WOIndex = prfs_WorkedOffSharingIndex(Search); |
| UsIndex = prfs_UsableSharingIndex(Search); |
| NrOfInstances = sharing_GetNumberOfInstances(Atom, WOIndex); |
| if (Usables) |
| NrOfInstances += sharing_GetNumberOfInstances(Atom, UsIndex); |
| |
| if (fol_IsEquality(Atom)) { |
| /* Exchange the subterms of the equation, and count the instances, too */ |
| Atom = term_Create(fol_Equality(), list_Reverse(term_ArgumentList(Atom))); |
| |
| NrOfInstances += sharing_GetNumberOfInstances(Atom, WOIndex); |
| if (Usables) |
| NrOfInstances += sharing_GetNumberOfInstances(Atom, UsIndex); |
| |
| list_Delete(term_ArgumentList(Atom)); |
| term_Free(Atom); |
| |
| /* If equation is oriented, consider instances of the greater side, too */ |
| Atom = clause_LiteralAtom(Literal); |
| if (clause_LiteralIsOrientedEquality(Literal)) { |
| NrOfInstances += sharing_GetNumberOfInstances(term_FirstArgument(Atom), |
| WOIndex); |
| if (Usables) |
| NrOfInstances += sharing_GetNumberOfInstances(term_FirstArgument(Atom), |
| UsIndex); |
| } |
| } |
| |
| return NrOfInstances; |
| } |