diff options
Diffstat (limited to 'test/spass/search.c')
| -rw-r--r-- | test/spass/search.c | 1271 |
1 files changed, 1271 insertions, 0 deletions
diff --git a/test/spass/search.c b/test/spass/search.c new file mode 100644 index 0000000..5833ada --- /dev/null +++ b/test/spass/search.c @@ -0,0 +1,1271 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * 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: 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 "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; +} |