/**************************************************************/ /* ********************************************************** */ /* * * */ /* * TERMS * */ /* * * */ /* * $Module: TERM * */ /* * * */ /* * Copyright (C) 1996, 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$ */ #ifndef _TERM_ #define _TERM_ /**************************************************************/ /* Includes */ /**************************************************************/ #include "symbol.h" #include "stack.h" /**************************************************************/ /* Structures */ /**************************************************************/ /* In CHECK mode you can block the stamp for all terms, so no other function can use the macro term_IncStamp(), which must be used for initialization at the beginning of a new traversal */ typedef struct term { SYMBOL symbol; union { LIST termlist; struct term* term; } super; LIST args; NAT stamp; NAT size; } *TERM, TERM_NODE; /* Data Structures and Macros for Marking of variables, used in */ /* all functions extracting variables from terms. */ extern NAT term_MARK; extern POINTER term_BIND[symbol__MAXVARIABLES][2]; #ifdef CHECK extern BOOL term_BINDPHASE; static __inline__ void term_StartBinding(void) { term_BINDPHASE=TRUE; } static __inline__ void term_StopBinding(void) { term_BINDPHASE=FALSE; } static __inline__ BOOL term_InBindingPhase(void) { return term_BINDPHASE; } #else static __inline__ void term_StartBinding(void) { } static __inline__ void term_StopBinding(void) { } #endif static __inline__ NAT term_NullMark(void) { return 0; } static __inline__ NAT term_BindingMark(SYMBOL Var) { return (NAT) term_BIND[symbol_VarIndex(Var)][0]; } static __inline__ void term_SetBindingMark(SYMBOL Var, NAT Mark) { term_BIND[symbol_VarIndex(Var)][0] = (POINTER) Mark; } static __inline__ POINTER term_BindingValue(SYMBOL Var) { return term_BIND[symbol_VarIndex(Var)][1]; } static __inline__ void term_SetBindingValue(SYMBOL Var, POINTER Value) { term_BIND[symbol_VarIndex(Var)][1] = Value; } static __inline__ void term_CreateBinding(SYMBOL Var, NAT Mark) { term_SetBindingMark(Var, Mark); } static __inline__ void term_ClearBinding(SYMBOL Var) { term_SetBindingMark(Var, term_NullMark()); } static __inline__ void term_CreateValueBinding(SYMBOL Var, NAT Mark, POINTER Value) { term_SetBindingMark(Var, Mark); term_SetBindingValue(Var, Value); } static __inline__ BOOL term_VarIsMarked(SYMBOL Var, NAT Mark) { return term_BindingMark(Var) >= Mark; } static __inline__ NAT term_ActMark(void) { NAT MarkVar; if (term_MARK == NAT_MAX) { int i; for (i = 0; i < symbol_MaxVars(); i++) term_BIND[i][0] = (POINTER) term_NullMark(); term_MARK = 1; } MarkVar = term_MARK++; return MarkVar; } static __inline__ void term_NewMark(void) { if (term_MARK == NAT_MAX) { int i; for (i = 0; i < symbol_MaxVars(); i++) term_BIND[i][0] = (POINTER) term_NullMark(); term_MARK = 1; } term_MARK++; } static __inline__ NAT term_OldMark(void) { return term_MARK - 1; } /**************************************************************/ /* Macros */ /**************************************************************/ static __inline__ TERM term_Null(void) { return (TERM)NULL; } static __inline__ SYMBOL term_TopSymbol(TERM T) { return T->symbol; } static __inline__ void term_RplacTop(TERM T, SYMBOL S) { T->symbol = S; } static __inline__ LIST term_SupertermList(TERM T) { return T->super.termlist; } static __inline__ void term_RplacSupertermList(TERM T, LIST L) { T->super.termlist = L; } static __inline__ LIST term_AtomsLiterals(TERM T) { return T->super.termlist; } static __inline__ TERM term_Superterm(TERM T) { return T->super.term; } static __inline__ void term_RplacSuperterm(TERM T1, TERM T2) { T1->super.term = T2; } static __inline__ BOOL term_IsVariable(TERM T) { return symbol_IsVariable(term_TopSymbol(T)); } static __inline__ BOOL term_IsStandardVariable(TERM T) { return symbol_IsStandardVariable(term_TopSymbol(T)); } static __inline__ BOOL term_IsIndexVariable(TERM T) { return symbol_IsIndexVariable(term_TopSymbol(T)); } static __inline__ LIST term_ArgumentList(TERM T) { return T->args; } static __inline__ void term_RplacArgumentList(TERM T, LIST A) { T->args = A; } static __inline__ BOOL term_IsComplex(TERM T) { return term_ArgumentList(T) != NULL; } static __inline__ BOOL term_IsConstant(TERM T) { return !term_IsComplex(T) && !term_IsVariable(T); } static __inline__ BOOL term_IsAtom(TERM T) { return symbol_IsPredicate(term_TopSymbol(T)); } static __inline__ BOOL term_IsDeclaration(TERM Term) /************************************************************** INPUT: A term. RETURNS: TRUE, if the term is a monadic atom, FALSE otherwise. ***************************************************************/ { return (term_IsAtom(Term) && symbol_IsBaseSort(term_TopSymbol(Term))); } static __inline__ TERM term_FirstArgument(TERM T) { return (TERM) list_First(T->args); } static __inline__ void term_RplacFirstArgument(TERM T1, TERM T2) { list_Rplaca(T1->args, T2); } static __inline__ TERM term_SecondArgument(TERM T) { return (TERM) list_Second(T->args); } static __inline__ void term_RplacSecondArgument(TERM T1, TERM T2) { list_RplacSecond(T1->args, T2); } static __inline__ void term_Free(TERM T) { memory_Free((char*) T, sizeof(TERM_NODE)); } static __inline__ BOOL term_EqualTopSymbols(TERM T, TERM S) { return symbol_Equal(term_TopSymbol(T), term_TopSymbol(S)); } static __inline__ void term_EqualitySwap(TERM T) { TERM Aux; Aux = term_FirstArgument(T); list_Rplaca(term_ArgumentList(T), (POINTER) term_SecondArgument(T)); list_Rplaca(list_Cdr(term_ArgumentList(T)), (POINTER) Aux); } /**************************************************************/ /* Macros and Variables for the term's stamp */ /**************************************************************/ /* Maximum number of modules that use the term module's stamp */ #define term_MAXSTAMPUSERS 20 extern NAT term_STAMP; extern BOOL term_STAMPBLOCKED; static __inline__ NAT term_Stamp(void) { return term_STAMP; } static __inline__ BOOL term_StampBlocked(void) { return term_STAMPBLOCKED; } #ifdef CHECK /* In CHECK mode 'term_StartStamp' is a real function defined in */ /* 'term.c'. */ static __inline__ void term_StopStamp(void) { term_STAMPBLOCKED = FALSE; } #else /* Attention: */ /* You should check for Overflow before calling this function !!!!! */ /* Use "term_StampOverflow" to do this. */ /* If an overflow occurred, you have to reset the stamp of all terms */ /* you're using. */ static __inline__ void term_StartStamp(void) { term_STAMP++; } static __inline__ void term_StopStamp(void) { } #endif static __inline__ NAT term_TermStamp(TERM T) { return T->stamp; } static __inline__ void term_SetTermStamp(TERM T) { T->stamp = term_STAMP; } static __inline__ NAT term_Size(TERM T) { return T->size; } static __inline__ void term_SetSize(TERM T, NAT s) { T->size = s; } static __inline__ BOOL term_AlreadyVisited(TERM T) { return T->stamp == term_STAMP; } static __inline__ BOOL term_HasTermStamp(TERM T) { return T->stamp == term_STAMP; } static __inline__ void term_ResetTermStamp(TERM T) { T->stamp = 0; } static __inline__ BOOL term_StampAlreadyReset(TERM T) { return T->stamp == 0; } /**************************************************************/ /* Functions on Term Creation And Deletion */ /**************************************************************/ void term_Init(void); TERM term_Create(SYMBOL, LIST); TERM term_CreateAddFather(SYMBOL, LIST); TERM term_CreateStandardVariable(void); void term_Delete(TERM); void term_DeleteIterative(TERM); /**************************************************************/ /* Term Comparisons */ /**************************************************************/ BOOL term_Equal(TERM, TERM); BOOL term_EqualIterative(TERM, TERM); /* Unused */ BOOL term_VariableEqual(TERM, TERM); BOOL term_IsGround(TERM); BOOL term_IsTerm(TERM); BOOL term_IsTermList(LIST); BOOL term_AllArgsAreVar(TERM); int term_CompareBySymbolOccurences(TERM, TERM); int term_CompareAbstract(TERM, TERM); BOOL term_CompareAbstractLEQ(TERM, TERM); /**************************************************************/ /* Low Level Term Functions */ /**************************************************************/ TERM term_Copy(TERM); TERM term_CopyIterative(TERM); /* Unused */ TERM term_CopyWithEmptyArgListNode(TERM, LIST, LIST*); void term_PrintWithEmptyArgListNode(TERM); BOOL term_ReplaceSubtermBy(TERM, TERM, TERM); void term_ReplaceVariable(TERM, SYMBOL, TERM); void term_ExchangeVariable(TERM, SYMBOL, SYMBOL); BOOL term_SubstituteVariable(SYMBOL, TERM, TERM*); NAT term_ComputeSize(TERM); void term_InstallSize(TERM); NAT term_Depth(TERM); BOOL term_ContainsSymbol(TERM, SYMBOL); BOOL term_Sharing(TERM); void term_AddFatherLinks(TERM); BOOL term_FatherLinksEstablished(TERM); TERM term_TopLevelTerm(TERM); BOOL term_HasPointerSubterm(TERM, TERM); BOOL term_HasSubterm(TERM, TERM); BOOL term_HasProperSuperterm(TERM, TERM); TERM term_FindSubterm(TERM, SYMBOL); LIST term_FindAllAtoms(TERM, SYMBOL); BOOL term_CheckTerm(TERM); NAT term_RootDistance(TERM); BOOL term_RootDistanceSmaller(TERM,TERM); static __inline__ LIST term_CopyTermList(LIST List) /************************************************************** INPUT: A list of TERMs. RETURNS: A deep copy of the list, i.e. the terms are copied, too. ***************************************************************/ { return list_CopyWithElement(List, (POINTER (*)(POINTER))term_Copy); } static __inline__ void term_CopyTermsInList(LIST List) /************************************************************** INPUT: A list of TERMs. EFFECT: Replaces every term in the list with its copy. ***************************************************************/ { list_NMapCar(List, (POINTER (*)(POINTER)) term_Copy); } static __inline__ void term_DeleteTermList(LIST List) /************************************************************** INPUT: A list of TERMs. RETURNS: Nothing. EFFECT: The list is freed together with its elements. ***************************************************************/ { list_DeleteWithElement(List, (void (*)(POINTER))term_Delete); } static __inline__ BOOL term_ListContainsTerm(LIST List, TERM Term) /************************************************************** INPUT: A list of TERMs. RETURNS: TRUE, if contains , FALSE otherwise. Terms are compared with respect to the term_Equal function. ***************************************************************/ { return list_Member(List, Term, (BOOL (*)(POINTER,POINTER))term_Equal); } static __inline__ LIST term_DeleteDuplicatesFromList(LIST List) /************************************************************** INPUT: A list of TERMs. RETURNS: The list where duplicate terms are removed. EFFECT: Terms are compared with respect to the term_Equal function. The duplicate terms are not deleted. ***************************************************************/ { return list_DeleteDuplicates(List, (BOOL (*)(POINTER, POINTER))term_Equal); } static __inline__ LIST term_DestroyDuplicatesInList(LIST Terms) /************************************************************** INPUT: A list of terms. RETURNS: The list where all duplicate terms are removed. EFFECTS: The terms are compared with respect to the term_Equal function. The duplicate terms are deleted, too. ***************************************************************/ { return list_DeleteDuplicatesFree(Terms, (BOOL (*)(POINTER,POINTER))term_Equal, (void (*)(POINTER))term_Delete); } /**************************************************************/ /* Term Input and Output Functions */ /**************************************************************/ void term_Print(TERM); void term_PrettyPrint(TERM); void term_FPrint(FILE*, TERM); void term_TermListPrint(LIST); void term_TermListFPrint(FILE*, LIST); void term_PrintPrefix(TERM); void term_FPrintPrefix(FILE*, TERM); void term_TermListPrintPrefix(LIST); void term_TermListFPrintPrefix(FILE*, LIST); void term_FPrintOtterPrefix(FILE*, TERM); void term_TermListFPrintOtterPrefix(FILE*, LIST); void term_FPrintPosition(FILE*,TERM,TERM); static __inline__ void term_PrintPosition(TERM TopTerm, TERM Subterm) { term_FPrintPosition(stdout, TopTerm, Subterm); } /**************************************************************/ /* High Level Term Functions */ /**************************************************************/ void term_ToCoVariables(TERM); NAT term_Bytes(TERM); void term_MarkVariables(TERM, NAT); void term_CountSymbols(TERM); LIST term_ListOfVariables(TERM); LIST term_VariableSymbols(TERM); LIST term_ListOfAtoms(TERM,SYMBOL); LIST term_ListOfConstants(TERM); LIST term_ListOfFunctions(TERM); NAT term_NumberOfVarOccs(TERM); NAT term_NumberOfSymbolOccurrences(TERM, SYMBOL); BOOL term_ContainsFunctions(TERM); BOOL term_ContainsVariable(TERM,SYMBOL); SYMBOL term_MaxVar(TERM); void term_StartMinRenaming(void); void term_StartMaxRenaming(SYMBOL); TERM term_Rename(TERM); SYMBOL term_GetRenamedVarSymbol(SYMBOL); LIST term_RenamePseudoLinear(TERM, SYMBOL); /**************************************************************/ /* Stamp Functions */ /**************************************************************/ /* Currently only in CHECK mode */ #ifdef CHECK void term_StartStamp(void); #endif void term_SetTermSubtermStamp(TERM T); NAT term_GetStampID(void); BOOL term_StampOverflow(NAT); #endif