diff options
Diffstat (limited to 'test/spass/sharing.c')
| -rw-r--r-- | test/spass/sharing.c | 1143 |
1 files changed, 1143 insertions, 0 deletions
diff --git a/test/spass/sharing.c b/test/spass/sharing.c new file mode 100644 index 00000000..47f8b501 --- /dev/null +++ b/test/spass/sharing.c @@ -0,0 +1,1143 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * STRUCTURE SHARING * */ +/* * * */ +/* * $Module: SHARING * */ +/* * * */ +/* * Copyright (C) 1996, 1997, 1998, 1999, 2000 * */ +/* * MPI fuer Informatik * */ +/* * * */ +/* * This program is free software; you can redistribute * */ +/* * it and/or modify it under the terms of the GNU * */ +/* * General Public License as published by the Free * */ +/* * Software Foundation; either version 2 of the License, * */ +/* * or (at your option) any later version. * */ +/* * * */ +/* * This program is distributed in the hope that it will * */ +/* * be useful, but WITHOUT ANY WARRANTY; without even * */ +/* * the implied warranty of MERCHANTABILITY or FITNESS * */ +/* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ +/* * License for more details. * */ +/* * * */ +/* * You should have received a copy of the GNU General * */ +/* * Public License along with this program; if not, write * */ +/* * to the Free Software Foundation, Inc., 59 Temple * */ +/* * Place, Suite 330, Boston, MA 02111-1307 USA * */ +/* * * */ +/* * * */ +/* $Revision: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + +#include "sharing.h" + +/**************************************************************/ +/* Static Variables */ +/**************************************************************/ + +#ifdef CHECK +static BOOL sharing_DATABLOCKED; +#endif + +static LIST sharing_DATALIST = (LIST) NULL; + +#define sharing_STACKSIZE 500 +static LIST sharing_STACK[sharing_STACKSIZE]; +static LIST* sharing_STACKPOINTER = sharing_STACK; + +/**************************************************************/ +/* Prototypes for static functions used only in this module */ +/**************************************************************/ + +static BOOL sharing_IsNoMoreUsed(TERM); +static LIST sharing_InternGetDataList(TERM); + +static TERM sharing_InsertIntoSharing(TERM, SHARED_INDEX); +static void sharing_DeleteFromSharing(TERM, SHARED_INDEX); + +static void sharing_ResetTermStamp(TERM); + +static void sharing_PrintWithSuperterms(TERM); + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * PRIMITIVE SHARING FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +SHARED_INDEX sharing_IndexCreate(void) +/********************************************************** + INPUT: None. + RETURNS: A shared index, consisting of an Index, a Consttable + and a Vartable. + EFFECTS: Initializes the shared Index for the sharing_Vartable and the + sharing_Consttable with NULL-Pointers and an empty st_index. +**********************************************************/ +{ + SHARED_INDEX Result; + int i; + + Result = (SHARED_INDEX)memory_Malloc(sizeof(SHARED_INDEX_NODE)); + sharing_SetIndex(Result, st_IndexCreate()); + + for (i=0; (i < symbol_MaxVars()); i++) + sharing_SetVartableEntry(Result, i, NULL); + + for (i=0; (i < symbol_MaxConsts()); i++) + sharing_SetConsttableEntry(Result, i, NULL); + + sharing_SetStampID(Result, term_GetStampID()); + return Result; +} + + +void sharing_IndexDelete(SHARED_INDEX ShIndex) +/********************************************************** + INPUT: A shared Index. + RETURNS: None. + EFFECTS: Deletes the Index and frees the memory for the + structure including the Const- and Vartable. +**********************************************************/ +{ + st_IndexDelete(sharing_Index(ShIndex)); + + memory_Free(ShIndex, sizeof(SHARED_INDEX_NODE)); +} + + +void sharing_PushOnStack(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: None. + EFFECTS: Creates a Stack of Pointers to the + term and all of its subterms in their order in + the arglist (thus ordered by depth). + top of the stack is bottom term +**********************************************************/ +{ + LIST ArgList; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_PushOnStack: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + stack_Push(Term); + + ArgList = term_ArgumentList(Term); + + while (!list_Empty(ArgList)){ + sharing_PushOnStack(list_Car(ArgList)); + ArgList = list_Cdr(ArgList); + } +} + + +void sharing_PushReverseOnStack(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: None. + EFFECTS: Creates a Stack of Pointers to the + term and all of its subterms, except variables in their order in + the arglist (thus ordered by depth). + top of the stack is top term +**********************************************************/ +{ + LIST ArgList; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_PushReverseOnStack: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if (!term_IsVariable(Term)) { + + ArgList = term_ArgumentList(Term); + + while (!list_Empty(ArgList)){ + sharing_PushReverseOnStack(list_Car(ArgList)); + ArgList = list_Cdr(ArgList); + } + + stack_Push(Term); + } +} + +void sharing_PushReverseOnStackExcept(TERM Term, LIST DontTermList) +/********************************************************** + INPUT: A term and an exception list. + RETURNS: None. + EFFECTS: Creates a Stack of Pointers to the + term and all of its subterms that are not contained + or below the terms in DontTermList in their order in + the arglist (thus ordered by depth). + top of the stack is top term +**********************************************************/ +{ + LIST ArgList; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_PushReverseOnStack: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if (!term_IsVariable(Term) && !term_ListContainsTerm(DontTermList, Term)) { + ArgList = term_ArgumentList(Term); + + while (!list_Empty(ArgList)){ + sharing_PushReverseOnStackExcept(list_Car(ArgList), DontTermList); + ArgList = list_Cdr(ArgList); + } + + stack_Push(Term); + } +} + +void sharing_PushOnStackNoStamps(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: None. + EFFECTS: Creates a Stack of Pointers to the + term and all of its subterms that are not stamped + or below stamped terms. + top of the stack is top term. +**********************************************************/ +{ + LIST ArgList; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_PushReverseOnStackNoStamps: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if (!term_IsVariable(Term) && !term_HasTermStamp(Term)) { + + stack_Push(Term); + + ArgList = term_ArgumentList(Term); + + while (!list_Empty(ArgList)){ + sharing_PushOnStackNoStamps(list_Car(ArgList)); + ArgList = list_Cdr(ArgList); + } + } +} + + +void sharing_PushListOnStack(LIST TermList) +/********************************************************** + INPUT: A list of terms. + RETURNS: None. + EFFECTS: Creates a Stack of Pointers to the + terms in <TermList> and all of subterms in their order in + the arglist (thus ordered by depth). +**********************************************************/ +{ + while (!list_Empty(TermList)) { + sharing_PushOnStack(list_Car(TermList)); + TermList = list_Cdr(TermList); + } +} + + +void sharing_PushListReverseOnStack(LIST TermList) +/********************************************************** + INPUT: A list of terms. + RETURNS: None. + EFFECTS: Puts all terms in Termlist and their superterms + in their order in the arglist (thus ordered by depth) + on the stack. + On top of the stack are subterms. +**********************************************************/ +{ + while (!list_Empty(TermList)) { + sharing_PushReverseOnStack(list_Car(TermList)); + TermList = list_Cdr(TermList); + } +} + +void sharing_PushListReverseOnStackExcept(LIST TermList, LIST DontPushList) +/********************************************************** + INPUT: Two lists of terms. + RETURNS: None. + EFFECTS: Puts all terms in Termlist except those contained in + DontPushList and their superterms + in their order in the arglist (thus ordered by depth) + on the stack. + On top of the stack are subterms. +**********************************************************/ +{ + while (!list_Empty(TermList)) { + sharing_PushReverseOnStackExcept(list_Car(TermList), DontPushList); + TermList = list_Cdr(TermList); + } +} + +void sharing_PushListOnStackNoStamps(LIST TermList) +/********************************************************** + INPUT: A list of terms. + RETURNS: None. + EFFECTS: Puts all terms in Termlist on the stack. + On top of the stack are subterms. +**********************************************************/ +{ + while (!list_Empty(TermList)) { + sharing_PushOnStackNoStamps(list_Car(TermList)); + TermList = list_Cdr(TermList); + } +} + + +static BOOL sharing_IsNoMoreUsed(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: TRUE, if the Term has no superterms, + FALSE, else. +**********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_IsNoMoreUsed: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + return (list_Empty(term_SupertermList(Term))); +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * FUNCTIONS FOR INSERTION AND DELETION * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * 1) FUNCTIONS FOR INSERTION * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +TERM sharing_Insert(POINTER Data, TERM Atom, SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A data element, it's unshared atom and a SharedIndex. + RETURNS: The shared term inserted into the SharedIndex. + CAUTION: The superterm slot of <Atom> is destructively used! + MEMORY: The term 'Atom' still exists, memory needed for + the shared version is allocated. +**********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Atom) || (!sharing_IsNoMoreUsed(Atom))){ + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_Insert: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + Atom = sharing_InsertIntoSharing(Atom, SharedIndex); + + term_RplacSupertermList(Atom, list_Cons(Data, term_SupertermList(Atom))); + + return(Atom); +} + + +static TERM sharing_InsertIntoSharing(TERM Term, SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A term and a shared index. + RETURNS: A copy of 'Term' which is inserted into the Sharing + and the "SharedIndex". + MEMORY: The unshared version isn't freed, needed memory + is allocated. +**********************************************************/ +{ + int B_Stack; + TERM InsTerm; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_InsertIntoSharing: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + B_Stack = stack_Bottom(); + sharing_PushOnStack(Term); + InsTerm = stack_Top(); /* not necessary initialization ... */ + + while (! stack_Empty(B_Stack)){ + InsTerm = stack_PopResult(); + + if (term_IsVariable(InsTerm)){ + if (!sharing_IsSharedVar(InsTerm, SharedIndex)) { + + sharing_SetVartableEntry(SharedIndex, sharing_VariableIndex(InsTerm), + term_Create(term_TopSymbol(InsTerm), + list_Nil())); + + st_EntryCreate(sharing_Index(SharedIndex), + sharing_VartableEntry(SharedIndex, + sharing_VariableIndex(InsTerm)), + sharing_VartableEntry(SharedIndex, + sharing_VariableIndex(InsTerm)), + cont_LeftContext()); + } + + /* The NULL-Pointer in the Vartable is replaced by a copy of the */ + /* InsTerm, which is referenced by the InsTerms SharedTermCopy. */ + /* A complex T still has to be insert. into its Args superlists. */ + /* The unshared Term isn't yet in the 'SharedIndex' and thus is */ + /* inserted, too. */ + + + sharing_RememberSharedTermCopy(InsTerm, + sharing_VartableEntry(SharedIndex, sharing_VariableIndex(InsTerm))); + + }else if (term_IsConstant(InsTerm)){ + if (!sharing_IsSharedConst(InsTerm, SharedIndex)) { + sharing_SetConsttableEntry(SharedIndex, sharing_ConstantIndex(InsTerm), + term_Create(term_TopSymbol(InsTerm), + list_Nil())); + + st_EntryCreate(sharing_Index(SharedIndex), + sharing_ConsttableEntry(SharedIndex, sharing_ConstantIndex(InsTerm)), + sharing_ConsttableEntry(SharedIndex, sharing_ConstantIndex(InsTerm)), + cont_LeftContext()); + } + + /* The NULL-Pointer in the Consttable is replaced by a copy of the */ + /* InsTerm, which is referenced by the InsTerms SharedTermCopy. */ + /* A complex T still has to be insert. into its Args superlists. */ + /* The unshared Term isn't yet in the 'SharedIndex' and thus is */ + /* inserted, too. */ + + sharing_RememberSharedTermCopy(InsTerm, + sharing_ConsttableEntry(SharedIndex, sharing_ConstantIndex(InsTerm))); + + }else{ /* term_IsComplex(InsTerm) */ + /* -> owns subterms which now have copies in Sharing. */ + + TERM SharedDuplicate; + LIST HelpList; + BOOL DuplCandHasSameArgs; + + SharedDuplicate = (TERM)NULL; + HelpList = + term_SupertermList(sharing_SharedTermCopy(term_FirstArgument(InsTerm))); + if (list_Empty(HelpList)){ + SharedDuplicate = term_Create(term_TopSymbol(InsTerm), list_Nil()); + DuplCandHasSameArgs = FALSE; + } + else{ + DuplCandHasSameArgs = FALSE; + while (!DuplCandHasSameArgs && !list_Empty(HelpList)){ + SharedDuplicate = (TERM) list_First(HelpList); + + if (term_TopSymbol(SharedDuplicate) == term_TopSymbol(InsTerm)){ + LIST OrigHelpArgList, DuplHelpArgList; + + OrigHelpArgList = term_ArgumentList(InsTerm); + DuplHelpArgList = term_ArgumentList(SharedDuplicate); + while (!list_Empty(OrigHelpArgList) && + (DuplCandHasSameArgs = + (sharing_SharedTermCopy(list_First(OrigHelpArgList)) == + list_First(DuplHelpArgList)))){ + DuplHelpArgList = list_Cdr(DuplHelpArgList); + OrigHelpArgList = list_Cdr(OrigHelpArgList); + } + } + HelpList = list_Cdr(HelpList); + } + if (!DuplCandHasSameArgs) + SharedDuplicate = term_Create(term_TopSymbol(InsTerm), list_Nil()); + } /* end of else fuer Behandlung von InsTerm mit shared FirstArg. */ + + if (!DuplCandHasSameArgs){ + /* Falls neue Kopie gemacht wurde, wird diese hier "eingeshared": */ + + for (HelpList = term_ArgumentList(InsTerm); !list_Empty(HelpList); + HelpList = list_Cdr(HelpList)){ + TERM SharedArg; + + SharedArg = sharing_SharedTermCopy((TERM)list_First(HelpList)); + + term_RplacArgumentList(SharedDuplicate, + list_Cons(SharedArg, + term_ArgumentList(SharedDuplicate))); + + term_RplacSupertermList(SharedArg, + list_Cons(SharedDuplicate, + term_SupertermList(SharedArg))); + } + term_RplacArgumentList(SharedDuplicate, + list_NReverse(term_ArgumentList(SharedDuplicate))); + + /* Now a newly generated term can be inserted into the 'SharedIndex' ! */ + + st_EntryCreate(sharing_Index(SharedIndex), + SharedDuplicate, + SharedDuplicate, + cont_LeftContext()); + + } + sharing_RememberSharedTermCopy(InsTerm, + SharedDuplicate); + } + } + + return(sharing_SharedTermCopy(InsTerm)); +} + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * 2) FUNCTIONS FOR DELETION * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +void sharing_Delete(POINTER Data, TERM Atom, SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A data element, its atom and an index. + RETURNS: Nothing. + MEMORY: Destructive, deletes 'Atom' from Sharing and frees + memory that's no more needed. +***********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Atom)){ + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_Delete: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + term_RplacSupertermList(Atom, + list_PointerDeleteElement(term_SupertermList(Atom), Data)); + + if (sharing_IsNoMoreUsed(Atom)) + sharing_DeleteFromSharing(Atom, SharedIndex); + +} + + +static void sharing_DeleteFromSharing(TERM Term, SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A term and a SharedIndex + RETURNS: Nothing + MEMORY: 'Term' is removed from the Sharing, only correct + if 'Term' is unshared in sharing (real subterms + may be shared, off course). +***********************************************************/ +{ + BOOL IsIndexed; +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_DeleteFromSharing: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + IsIndexed = st_EntryDelete(sharing_Index(SharedIndex), Term, Term, cont_LeftContext()); + +#ifdef CHECK + if (!IsIndexed) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_DeleteFromSharing: Input not indexed.\n"); + misc_FinishErrorReport(); + } +#endif + + if (term_IsComplex(Term)){ + LIST Args; + + Args = term_ArgumentList(Term); + + while (!list_Empty(Args)){ + TERM NextArg; + LIST Help; + + /* This block frees the terms arglists memory. */ + Help = Args; + NextArg = (TERM) list_First(Args); + Args = list_Cdr(Args); + list_Free(Help); + + term_RplacSupertermList(NextArg, + list_PointerDeleteOneElement(term_SupertermList(NextArg), Term)); + if (sharing_IsNoMoreUsed(NextArg)) + sharing_DeleteFromSharing(NextArg, SharedIndex); + } + + } else if (term_IsConstant(Term)) { + sharing_SetConsttableEntry(SharedIndex, sharing_ConstantIndex(Term), NULL); + } else { + sharing_SetVartableEntry(SharedIndex, sharing_VariableIndex(Term), NULL); + } + list_Delete(term_SupertermList(Term)); + term_Free(Term); +} + + +/**************************************************************/ +/* Functions to access unshared data via the shared term. */ +/**************************************************************/ + +LIST sharing_GetDataList(TERM Term, SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A shared term and the shared index it belongs to. + RETURNS: The list of data connected to all superterms of Term, + e.g. the list of all literals containing Term. + EFFECT: Allocates memory for the returned list. + CAUTION: Works recursive! +**********************************************************/ +{ + LIST Result = list_Nil(); +#ifdef CHECK + if (!term_IsTerm(Term) || (SharedIndex == NULL)){ + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_GetDataList: Illegal input.\n"); + misc_FinishErrorReport(); + } + /* What if the term doesn't belong to this shared index ?????? */ + +#endif + + if (term_StampOverflow(sharing_StampID(SharedIndex))) + sharing_ResetAllTermStamps(SharedIndex); + + term_StartStamp(); + + Result = sharing_InternGetDataList(Term); + + term_StopStamp(); + + return Result; +} + + +static LIST sharing_InternGetDataList(TERM Term) +/********************************************************** + INPUT: A shared term. + RETURNS: The list of data connected to all superterms of Term + EFFECT: Allocates memory for the returned list. +********************************************************/ +{ + if (term_IsAtom(Term)) + /* We are at top level of the superterm "tree", */ + /* so the recursion stops here */ + return list_Copy(term_AtomsLiterals(Term)); + else{ + LIST SuperList; + LIST DataList = list_Nil(); + + for (SuperList = term_SupertermList(Term); !list_Empty(SuperList); + SuperList = list_Cdr(SuperList)) { + TERM superterm = (TERM) list_Car(SuperList); + if (!term_AlreadyVisited(superterm)) { + DataList = list_Nconc(sharing_InternGetDataList(superterm), DataList); + term_SetTermStamp(superterm); + } + } + return DataList; + } +} + + +void sharing_StartDataIterator(TERM Term, SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A shared term and the shared index it belongs to. + RETURNS: Nothing. + EFFECT: Prepares the data iterator for Term. + After this call you can access single data items + for Term with function sharing_GetNextData. +********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Term) || (SharedIndex == NULL)){ + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_StartDataIterator: Illegal input.\n"); + misc_FinishErrorReport(); + } + if (sharing_DATABLOCKED) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_StartDataIterator: Data iterator already used.\n"); + misc_FinishErrorReport(); + } + sharing_DATABLOCKED = TRUE; +#endif + + if (term_StampOverflow(sharing_StampID(SharedIndex))) + sharing_ResetAllTermStamps(SharedIndex); + term_StartStamp(); + + /* Init stack */ + sharing_STACKPOINTER = sharing_STACK; /* Pop all items */ + while (!term_IsAtom(Term)) { + /* Push superterm list on stack */ + *(sharing_STACKPOINTER++) = term_SupertermList(Term); + Term = list_Car(term_SupertermList(Term)); + } + + sharing_DATALIST = term_AtomsLiterals(Term); +} + + +POINTER sharing_GetNextData(void) +/********************************************************** + INPUT: None + RETURNS: A single data item connected to the term specified + in the previous call of sharing_StartDataIterator. + NULL is returned, if all data items were accessed before. + EFFECT: In contrast to function sharing_GetDataList + no memory is allocated. +********************************************************/ +{ + POINTER Result = NULL; + LIST superlist; + +#ifdef CHECK + if (!sharing_DATABLOCKED) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_GetNextData: Iterator wasn't started.\n"); + misc_FinishErrorReport(); + } +#endif + + if (!list_Empty(sharing_DATALIST)) { + Result = list_Car(sharing_DATALIST); + sharing_DATALIST = list_Cdr(sharing_DATALIST); + } else { + superlist = NULL; + while ((sharing_STACKPOINTER > sharing_STACK) && /* stack not empty */ + list_Empty(superlist)) { + /* change between backtracking and expansion */ + do { /* Backtracking */ + superlist = *(--sharing_STACKPOINTER); /* PopResult */ + term_SetTermStamp(list_Car(superlist)); + do + superlist = list_Cdr(superlist); + while (!list_Empty(superlist) && + term_AlreadyVisited(list_Car(superlist))); + } while ((sharing_STACKPOINTER>sharing_STACK) && list_Empty(superlist)); + while (!list_Empty(superlist) && + !term_IsAtom(list_Car(superlist))) { /* Expansion */ + *(sharing_STACKPOINTER++) = superlist; + superlist = term_SupertermList(list_Car(superlist)); + /* Search next unvisited term */ + while (!list_Empty(superlist) && + term_AlreadyVisited(list_Car(superlist))) + superlist = list_Cdr(superlist); + } + } + if (!list_Empty(superlist)) { + *(sharing_STACKPOINTER++) = superlist; + sharing_DATALIST = term_AtomsLiterals(list_Car(superlist)); + Result = list_Car(sharing_DATALIST); + sharing_DATALIST = list_Cdr(sharing_DATALIST); + } + } /* else */ + return Result; +} + + +void sharing_StopDataIterator(void) +/********************************************************** + INPUT: None. + RETURNS: Nothing. + EFFECT: The data iterator is stopped for the term you specified + in the corresponding call of sharing_StartDataIterator. +********************************************************/ +{ +#ifdef CHECK + if (!sharing_DATABLOCKED) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_StopDataIterator: Iterator wasn't started.\n"); + misc_FinishErrorReport(); + } + sharing_DATABLOCKED = FALSE; +#endif + sharing_DATALIST = list_Nil(); + term_StopStamp(); +} + + +LIST sharing_NAtomDataList(TERM Atom) +/********************************************************** + INPUT: A shared term. + RETURNS: A List of data connected with 'Term' or superterms. + EFFECT: No memory Allocation + CAUTION: THE RETURNED LIST MUST NOT CHANGE +**********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Atom) || !term_IsAtom(Atom)){ + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_NAtomDataList: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + return(term_AtomsLiterals(Atom)); +} + + +LIST sharing_GetAllSuperTerms(SHARED_INDEX Index) +/********************************************************** + INPUT: A shared Index. + RETURNS: A List of all Data in the shared Index. + EFFECT: The term stamp is used. +**********************************************************/ +{ + int i; + LIST Result = list_Nil(); + TERM term; + + if (term_StampOverflow(sharing_StampID(Index))) + sharing_ResetAllTermStamps(Index); + term_StartStamp(); + + for (i = 0; i < symbol_MaxVars(); i++) { + term = sharing_VartableEntry(Index,i); + if (term != NULL) + Result = list_Nconc(sharing_InternGetDataList(term), Result); + } + + for (i = 0; i < symbol_MaxConsts(); i++) { + term = sharing_ConsttableEntry(Index,i); + if (term != NULL) + Result = list_Nconc(sharing_InternGetDataList(term), Result); + } + + term_StopStamp(); + + return Result; +} + + +void sharing_ResetAllTermStamps(SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A shared index. + RETURNS: Nothing. + EFFECT: The stamps of all terms in the shared index are reset. +**********************************************************/ +{ + TERM term; + int i; + + /* Reset stamp for all variables and their superterms */ + for (i = 0; i < symbol_MaxVars(); i++) { + term = sharing_VartableEntry(SharedIndex, i); + if (term != NULL) + sharing_ResetTermStamp(term); + } + + /* Reset stamp for all constants and their superterms */ + for (i = 0; i < symbol_MaxConsts(); i++){ + term = sharing_ConsttableEntry(SharedIndex, i); + if (term != NULL) + sharing_ResetTermStamp(term); + } +} + + +static void sharing_ResetTermStamp(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: Nothing. + EFFECT: The stamps of Term and all its superterms are reset. +**********************************************************/ +{ + LIST SuperList; + TERM SuperTerm; + + if (!term_IsAtom(Term)) { + for (SuperList = term_SupertermList(Term); !list_Empty(SuperList); + SuperList = list_Cdr(SuperList)) { + SuperTerm = (TERM) list_Car(SuperList); + if (!term_StampAlreadyReset(SuperTerm)) { + sharing_ResetTermStamp(SuperTerm); + term_ResetTermStamp(SuperTerm); + } + } + } +} + + +NAT sharing_GetNumberOfOccurances(TERM Term) +/************************************************************** + INPUT: A shared (!) term. + RETURNS: How many literals contain <Term>. + Note that literals containing <Term> <n> times are counted + <n> times. +***************************************************************/ +{ + if (term_IsAtom(Term)) + /* Stop recursion */ + return list_Length(term_AtomsLiterals(Term)); + else { + LIST Scan; + NAT Result; + + Result = 0; + for (Scan = term_SupertermList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) + Result += sharing_GetNumberOfOccurances(list_Car(Scan)); + + return Result; + } +} + + +NAT sharing_GetNumberOfInstances(TERM Term, SHARED_INDEX Index) +/************************************************************** + INPUT: A (!) shared term and a shared index. The term has to be + part of the index. + RETURNS: How many literals within the index contain an instance of <Term>. + Note that literals containing <n> instances of <Term> + are counted <n> times. +***************************************************************/ +{ + NAT Result; + TERM Instance; + + Result = 0; + Instance = st_ExistInstance(cont_LeftContext(), sharing_Index(Index), Term); + while (Instance != NULL) { + Result += sharing_GetNumberOfOccurances(Instance); + Instance = st_NextCandidate(); + } + return Result; +} + + +/**************************************************************/ +/* Output functions for the sharing structure. */ +/**************************************************************/ + +void sharing_PrintVartable(SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A shared index. + RETURNS: Nothing. + EFFECT: Prints the Vartable entries to stdout +**********************************************************/ +{ + int i; + + for (i = 0; i < symbol_MaxVars(); i++){ + if (sharing_VartableEntry(SharedIndex, i) != NULL){ + printf("\n X%d : ", i); + + term_Print(sharing_VartableEntry(SharedIndex, i)); + } + } +} + + +void sharing_PrintConsttable(SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A shared index. + RETURNS: Nothing. + EFFECT: Prints the Consttable entries to stdout +**********************************************************/ +{ + int i; + + for (i = 0; i < symbol_MaxConsts(); i++){ + if (sharing_ConsttableEntry(SharedIndex, i) != NULL){ + printf("\n c%d : ", i); + + term_Print(sharing_ConsttableEntry(SharedIndex, i)); + } + } +} + + +void sharing_PrintSharingConstterms1(SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A shared index. + RETURNS: Nothing. + EFFECT: Prints all terms from the Consttable and their + direct superterms to stdout +**********************************************************/ +{ + TERM term; + int i; + + for (i = 0; i < symbol_MaxConsts(); i++) { + term = sharing_ConsttableEntry(SharedIndex, i); + if (term != NULL){ + printf("\n c%d : ", i); + term_Print(term); + puts(" has the direct superterms : "); + term_TermListPrint(term_SupertermList(term)); + } + } +} + + +void sharing_PrintSharingVarterms1(SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A shared index. + RETURNS: Nothing. + EFFECT: Prints all terms from the Vartable and their + superterms to stdout +**********************************************************/ +{ + TERM term; + int i; + + for (i = 0; i < symbol_MaxVars(); i++) { + term = sharing_VartableEntry(SharedIndex, i); + if (term != NULL){ + printf("\n x%d : ", i); + term_Print(term); + puts(" has the direct superterms : "); + term_TermListPrint(term_SupertermList(term)); + } + } +} + + +static void sharing_PrintWithSuperterms(TERM Term) +/********************************************************** + INPUT: A Term + RETURNS: Nothing. + EFFECT: Prints all Superterms of 'Term' from the sharing + to stdout. +**********************************************************/ +{ + + LIST HelpList; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sharing_PrintWithSuperterms: Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if (term_IsAtom(Term)) { + term_Print(Term); + putchar('\n'); + } + else{ + term_Print(Term); + HelpList = term_SupertermList(Term); + if (!list_Empty(HelpList)){ + putchar('['); + term_TermListPrint(HelpList); + puts("]"); + while (!list_Empty(HelpList)){ + sharing_PrintWithSuperterms(list_Car(HelpList)); + HelpList = list_Cdr(HelpList); + } + } + } +} + + +void sharing_PrintSharing(SHARED_INDEX SharedIndex) +/********************************************************** + INPUT: A shared Index. + EFFECT: Prints the sharing to standard.out. +**********************************************************/ +{ + int i; + + for (i = 0; i < symbol_MaxConsts(); i++){ + if (sharing_ConsttableEntry(SharedIndex, i) != NULL){ + sharing_PrintWithSuperterms(sharing_ConsttableEntry(SharedIndex, i)); + puts("\n"); + } + } + puts("------------------------"); + for (i = 0; i < symbol_MaxVars(); i++){ + if (sharing_VartableEntry(SharedIndex, i) != NULL){ + sharing_PrintWithSuperterms(sharing_VartableEntry(SharedIndex, i)); + puts("\n"); + } + } +} + + +void sharing_PrintSameLevelTerms(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: Nothing. + EFFECT: Prints all terms, that share any of 'Term's args to + standard.out. +**********************************************************/ +{ + LIST HelpList; + + HelpList = term_ArgumentList(Term); + + while (!list_Empty(HelpList)){ + if (!list_Empty(term_SupertermList(list_First(HelpList)))) + term_TermListPrint(term_SupertermList(list_First(HelpList))); + + HelpList = list_Cdr(HelpList); + } +} + +void sharing_PrintStack(void) +/********************************************************** + INPUT: None. + RETURNS: Nothing. + EFFECT: Prints the internal sharing stack for iterative + queries. Only for debugging purposes. +**********************************************************/ +{ + TERM term; + LIST* ptr = sharing_STACKPOINTER; + + while (ptr > sharing_STACK) { + ptr--; + term = list_Car(*ptr); + term_Print(term); + putchar('\n'); + } +} + + |