diff options
Diffstat (limited to 'test/spass/term.c')
| -rw-r--r-- | test/spass/term.c | 2551 |
1 files changed, 2551 insertions, 0 deletions
diff --git a/test/spass/term.c b/test/spass/term.c new file mode 100644 index 0000000..2bc38e4 --- /dev/null +++ b/test/spass/term.c @@ -0,0 +1,2551 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * 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: 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 "term.h" + +/**************************************************************/ +/* Global variables */ +/**************************************************************/ + +NAT term_MARK; +POINTER term_BIND[symbol__MAXVARIABLES][2]; +#ifdef CHECK +BOOL term_BINDPHASE; +#endif + +NAT term_STAMP; +BOOL term_STAMPBLOCKED; +static BOOL term_STAMPOVERFLOW[term_MAXSTAMPUSERS]; +static NAT term_STAMPUSERS; + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * TERM CREATION FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +void term_Init(void) +/********************************************************** + INPUT: None. + RETURNS: None. + CAUTION: The term module is initialized. +***********************************************************/ +{ + int i; + + term_MARK = 1; + + term_STAMP = 0; + term_STAMPBLOCKED = FALSE; + for (i = 0; i < term_MAXSTAMPUSERS; i++) + term_STAMPOVERFLOW[i] = FALSE; + term_STAMPUSERS = 0; +#ifdef CHECK + term_BINDPHASE = FALSE; +#endif +} + + +TERM term_Create(SYMBOL Symbol, LIST List) +/********************************************************** + INPUT: A symbol and a list of arguments. + RETURNS: A term consisting of the top symbol 'Symbol' and + the arguments stored in 'List'. + CAUTION: None. +********************************************************/ +{ + TERM Result; + +#ifdef CHECK + if (!symbol_IsSymbol(Symbol) || !term_IsTermList(List)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_Create: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Result = (TERM)memory_Malloc(sizeof(TERM_NODE)); + Result->symbol = Symbol; + Result->args = List; + Result->super.termlist = list_Nil(); + Result->stamp = 0; + Result->size = 0; + return Result; +} + +TERM term_CreateAddFather(SYMBOL Symbol, LIST List) +/********************************************************** + INPUT: A symbol and a list of arguments. + RETURNS: A term consisting of the top symbol 'Symbol' and + the arguments stored in 'List'. + In contrast to term_Create the superterm members are set for the arguments. + CAUTION: None. +********************************************************/ +{ + TERM Result; + LIST l; + Result = term_Create(Symbol, List); + for (l=term_ArgumentList(Result); !list_Empty(l); l = list_Cdr(l)) + term_RplacSuperterm((TERM) list_Car(l), Result); + return Result; +} + +TERM term_CreateStandardVariable(void) +/********************************************************** + RETURNS: Returns a term with a new variable as top symbol. +***********************************************************/ +{ + return term_Create(symbol_CreateStandardVariable(), list_Nil()); +} + + +void term_Delete(TERM Term) +/********************************************************** + INPUT: A term. + SUMMARY: Deletes the term and frees the storage. + CAUTION: The arguments of Term are also deleted. +********************************************************/ +{ + if (term_IsComplex(Term)) { + LIST Scan; + for (Scan = term_ArgumentList(Term); + list_Exist(Scan); + Scan = list_Cdr(Scan)) + term_Delete(list_Car(Scan)); + list_Delete(term_ArgumentList(Term)); + } + term_Free(Term); +} + + +void term_DeleteIterative(TERM Term) +/********************************************************** + INPUT: A term. + SUMMARY: Deletes the term and frees the storage. + CAUTION: The arguments of Term are also deleted. +********************************************************/ +{ + if (term_IsComplex(Term)) { + LIST Stack, Aux; + Stack = list_StackBottom(); + do { + if (term_IsComplex(Term)) + Stack = list_Push(term_ArgumentList(Term),Stack); + term_Free(Term); + while (!list_StackEmpty(Stack) && list_Empty(list_Top(Stack))) + Stack = list_Pop(Stack); + if (!list_StackEmpty(Stack)) { + Aux = list_Top(Stack); + Term = (TERM)list_Car(Aux); + list_RplacTop(Stack, list_Cdr(Aux)); + list_Free(Aux); + } + } while (!list_StackEmpty(Stack)); + } + else + term_Free(Term); +} + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * PRIMITIVE TERM FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +BOOL term_Equal(TERM Term1, TERM Term2) +/********************************************************* + INPUT: Two terms. + RETURNS: The boolean value TRUE if the terms are equal. + CAUTION: EQUAL FUNCTION- OR PREDICATE SYMBOLS SHARE THE + SAME ARITY. THIS IS NOT VALID FOR JUNCTORS! +**********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Term1) || !term_IsTerm(Term2)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_Equal: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + /* if (term_IsIndexVariable(Term1)) + puts("\nterm_Equal: Left index variable."); + else if (term_IsIndexVariable(Term2)) + puts("\nterm_Equal: Right index variable."); + + fflush(stdout); */ + + if (Term1 == Term2) /* pointers are equal */ + return TRUE; + else if (!term_EqualTopSymbols(Term1, Term2)) + return FALSE; + else if (term_ArgumentList(Term1)) { + LIST Scan1, Scan2; + for (Scan1=term_ArgumentList(Term1), Scan2=term_ArgumentList(Term2); + list_Exist(Scan1) && list_Exist(Scan2); + Scan1=list_Cdr(Scan1), Scan2=list_Cdr(Scan2)) + if (!term_Equal(list_Car(Scan1),list_Car(Scan2))) + return FALSE; + return (list_Empty(Scan1) ? list_Empty(Scan2) : FALSE); + } else + return TRUE; +} + + +BOOL term_EqualIterative(TERM Term1, TERM Term2) +/********************************************************* + INPUT: Two terms. + RETURNS: The boolean value TRUE if the terms are equal. + CAUTION: Notice that there may be symbols with arbitrary arity +*******************************************************/ +{ + LIST Stack1,Stack2; + +#ifdef CHECK + if (!term_IsTerm(Term1) || !term_IsTerm(Term2)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_EqualIterative: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Stack1 = Stack2 = list_StackBottom(); + do { + if (term_EqualTopSymbols(Term1,Term2) && + term_IsComplex(Term1) && term_IsComplex(Term2)) { + Stack1 = list_Push(term_ArgumentList(Term1),Stack1); + Stack2 = list_Push(term_ArgumentList(Term2),Stack2); + } + if (!term_EqualTopSymbols(Term1,Term2) || + term_IsComplex(Term1) != term_IsComplex(Term2)) { + Stack1 = list_StackFree(Stack1); + Stack2 = list_StackFree(Stack2); + return FALSE; + } + while (!list_StackEmpty(Stack1) && list_Empty(list_Top(Stack1))) + if (!list_StackEmpty(Stack2) && list_Empty(list_Top(Stack2))) { + Stack1 = list_Pop(Stack1); + Stack2 = list_Pop(Stack2); + } + else { + Stack1 = list_StackFree(Stack1); + Stack2 = list_StackFree(Stack2); + return FALSE; + } + if (!list_StackEmpty(Stack1)) { + if (!list_Empty(list_Top(Stack2))) { + Term1 = (TERM)list_Car(list_Top(Stack1)); + list_RplacTop(Stack1, list_Cdr(list_Top(Stack1))); + Term2 = (TERM)list_Car(list_Top(Stack2)); + list_RplacTop(Stack2, list_Cdr(list_Top(Stack2))); + } + else { + Stack1 = list_StackFree(Stack1); + Stack2 = list_StackFree(Stack2); + return FALSE; + } + } + } while (!list_StackEmpty(Stack1)); + return TRUE; +} + + +BOOL term_VariableEqual(TERM Variable1, TERM Variable2) +/********************************************************* + INPUT: Two Variables. + RETURNS: The boolean value TRUE, if the variables are + equal. +**********************************************************/ +{ + return term_EqualTopSymbols(Variable1, Variable2); +} + + +BOOL term_IsGround(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: A boolean value which is TRUE, if 'Term' is a + ground term, i.e. does not contain variables. +********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_IsGround: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (term_IsComplex(Term)) { + LIST Stack; + Stack = list_StackBottom(); + do { + if (term_IsComplex(Term)) + Stack = list_Push(term_ArgumentList(Term),Stack); + else + if (term_IsVariable(Term)) { + Stack = list_StackFree(Stack); + return FALSE; + } + while (!list_StackEmpty(Stack) && list_Empty(list_Top(Stack))) + Stack = list_Pop(Stack); + if (!list_StackEmpty(Stack)) { + Term = (TERM)list_Car(list_Top(Stack)); + list_RplacTop(Stack, list_Cdr(list_Top(Stack))); + } + } while (!list_StackEmpty(Stack)); + return TRUE; + } else + return !term_IsVariable(Term); +} + + +BOOL term_IsTerm(TERM Term) +/********************************************************* + INPUT: A term. + RETURNS: TRUE, if 'Term' is not NULL + and has a symbol as its top symbol. +**********************************************************/ +{ + return (Term != (TERM)NULL && symbol_IsSymbol(term_TopSymbol(Term))); +} + + +BOOL term_IsTermList(LIST TermList) +/********************************************************* + INPUT: A term. + RETURNS: TRUE iff <TermList> is a list of terms. +*******************************************************/ +{ + for ( ; !list_Empty(TermList); TermList=list_Cdr(TermList)) + if (!(term_IsTerm((TERM)list_Car(TermList)))) + return FALSE; + + return TRUE; +} + + +BOOL term_AllArgsAreVar(TERM Term) +/********************************************************* + INPUT: A term. + RETURNS: The boolean value TRUE, if all arguments of the + term are variables. +*******************************************************/ +{ + LIST Scan; + for (Scan = term_ArgumentList(Term); + !list_Empty(Scan); Scan = list_Cdr(Scan)) + if (!term_IsVariable(list_Car(Scan))) + return FALSE; + return TRUE; +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * LOW LEVEL FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +TERM term_Copy(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: A copy of 'Term' where the stamp field is copied, too. + SUMMARY: Copies "Term" and returns a pointer to the copy. +*********************************************************/ +{ + TERM Result; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_Copy: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (term_IsComplex(Term)) { + LIST Scan, ArgumentList; + for (Scan = ArgumentList = list_Copy(term_ArgumentList(Term)); + list_Exist(Scan); + Scan = list_Cdr(Scan)) + list_Rplaca(Scan, term_Copy(list_Car(Scan))); + Result = term_Create(term_TopSymbol(Term), ArgumentList); + } else + Result = term_Create(term_TopSymbol(Term), list_Nil()); + + Result->stamp = Term->stamp; + Result->size = Term->size; + + return Result; +} + + +TERM term_CopyIterative(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: A copy of <Term>. + SUMMARY: Copies <Term> and returns a pointer to the copy. +*********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_CopyIterative: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (term_IsComplex(Term)) { + LIST TopStack, ArgumentStack, ActStack; + TopStack = list_Push((POINTER)term_TopSymbol(Term), + list_StackBottom()); + ArgumentStack = list_Push(list_Copy(term_ArgumentList(Term)), + list_StackBottom()); + ActStack = list_Push(list_Top(ArgumentStack), + list_StackBottom()); + + while (!list_StackEmpty(TopStack)) { + if (list_Empty(list_Top(ActStack))) { + Term = term_Create((SYMBOL)list_Top(TopStack), + (LIST)list_Top(ArgumentStack)); + TopStack = list_Pop(TopStack); + ArgumentStack = list_Pop(ArgumentStack); + ActStack = list_Pop(ActStack); + if (!list_StackEmpty(TopStack)) { + list_Rplaca(list_Top(ActStack), Term); + list_RplacTop(ActStack, list_Cdr(list_Top(ActStack))); + } + } + else { + Term = (TERM)list_Car(list_Top(ActStack)); + if (term_IsComplex(Term)) { + TopStack = list_Push((POINTER)term_TopSymbol(Term), TopStack); + ArgumentStack = list_Push(list_Copy(term_ArgumentList(Term)), + ArgumentStack); + ActStack = list_Push(list_Top(ArgumentStack), ActStack); + } + else { + list_Rplaca(list_Top(ActStack), + term_Create(term_TopSymbol(Term), list_Nil())); + list_RplacTop(ActStack, list_Cdr(list_Top(ActStack))); + } + } + } + return Term; + } + else + return term_Create(term_TopSymbol(Term), list_Nil()); +} + + +TERM term_CopyWithEmptyArgListNode(TERM Term, LIST ArgListNode, + LIST* ListNodeCopyPt) +/********************************************************** + INPUT: A term and a pointer to an argument list node of + this term. + RETURNS: A copy of 'Term' with a NULL as list_Car(ListNodeCopy). + SUMMARY: Copies "Term" and returns a pointer to the copy. +*********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_CopyWithEmptyArgListNode: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (term_IsComplex(Term)) { + LIST Scan, ArgumentList, HelpScan; + TERM Result; + + HelpScan = term_ArgumentList(Term); + ArgumentList = list_Copy(HelpScan); + + for (Scan = ArgumentList; + list_Exist(Scan); + Scan = list_Cdr(Scan),HelpScan = list_Cdr(HelpScan)) + if (HelpScan != ArgListNode) + list_Rplaca(Scan, + term_CopyWithEmptyArgListNode(list_Car(Scan), + ArgListNode, + ListNodeCopyPt)); + else{ + list_Rplaca(Scan, (TERM)NULL); + *ListNodeCopyPt = Scan; + } + + Result = (TERM)memory_Malloc(sizeof(TERM_NODE)); + Result->symbol = term_TopSymbol(Term); + Result->args = ArgumentList; + Result->super.termlist = list_Nil(); + + return Result; + + } else + return term_Create(term_TopSymbol(Term), list_Nil()); +} + + +void term_PrintWithEmptyArgListNode(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: none. + SUMMARY: Prints any term to stdout, especially terms with empty + argument list nodes. + CAUTION: Uses the other term_Output functions. +*************************************************************/ +{ + if (Term == (TERM)NULL) + fputs("(NULL)", stdout); + + else if (term_IsComplex(Term)) { + putchar('('); + symbol_Print(term_TopSymbol(Term)); + putchar(' '); + list_Apply((void (*)(POINTER)) term_PrintWithEmptyArgListNode, + term_ArgumentList(Term)); + putchar(')'); + + } else if (term_IsVariable(Term)) { + + symbol_Print(term_TopSymbol(Term)); + + } else { + + /* term_IsConstant(Term) */ + putchar('('); + symbol_Print(term_TopSymbol(Term)); + putchar(')'); + } +} + + +BOOL term_ReplaceSubtermBy(TERM Atom, TERM TermS, TERM TermT) +/************************************************************** + INPUT: Three terms. + RETURNS: None. + EFFECT: Replaces all occurrences of TermS in Atom by TermT. + Top level is NOT considered! +*************************************************************/ +{ + LIST ArgListNode; + BOOL Replaced; + int B_Stack; + +#ifdef CHECK + if (!term_IsTerm(Atom) || !term_IsTerm(TermS) || + !term_IsTerm(TermT) || term_Equal(Atom, TermS)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ReplaceSubtermBy: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + /*fputs("\nWe look for: ",stdout);term_Print(TermS); + fputs("\nin: ",stdout);term_Print(Atom); + */ + + Replaced = FALSE; + TermS = term_Copy(TermS); + + if (!term_Equal(Atom, TermS) && !list_Empty(term_ArgumentList(Atom))) { + + B_Stack = stack_Bottom(); + stack_Push(term_ArgumentList(Atom)); + + while (!stack_Empty(B_Stack)) { + ArgListNode = stack_Top(); + Atom = (TERM)list_Car(ArgListNode); + stack_RplacTop(list_Cdr(ArgListNode)); + + if (term_Equal(Atom, TermS)) { + Replaced = TRUE; + list_Rplaca(ArgListNode, term_Copy(TermT)); + term_Delete(Atom); + } + else + if (term_IsComplex(Atom)) + stack_Push(term_ArgumentList(Atom)); + + while (!stack_Empty(B_Stack) && list_Empty(stack_Top())) + stack_Pop(); + } + } + term_Delete(TermS); + return Replaced; +} + + +void term_ReplaceVariable(TERM Term, SYMBOL Symbol, TERM Repl) +/************************************************************** + INPUT: A term, a variable symbol and a replacement term. + RETURNS: void + EFFECT: All variables with <Symbol> in <Term> are replaced + with copies of <Repl> + CAUTION: Destructive +***************************************************************/ +{ + LIST Scan; + +#ifdef CHECK + if (!term_IsTerm(Term) || !term_IsTerm(Repl) || !symbol_IsVariable(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ReplaceVariable: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (symbol_Equal(term_TopSymbol(Term), Symbol)) { + term_RplacTop(Term,term_TopSymbol(Repl)); + term_RplacArgumentList(Term,term_CopyTermList(term_ArgumentList(Repl))); + } + else + for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) + term_ReplaceVariable(list_Car(Scan),Symbol,Repl); +} + +void term_ExchangeVariable(TERM Term, SYMBOL Old, SYMBOL New) +/************************************************************** + INPUT: A term, and two variable symbols. + RETURNS: void + EFFECT: All variables <Old> in <Term> are replaced with <New> + CAUTION: Destructive +***************************************************************/ +{ + LIST Scan; + +#ifdef CHECK + if (!term_IsTerm(Term) || !symbol_IsVariable(Old) || !symbol_IsVariable(New)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ExchangeVariable: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (symbol_Equal(term_TopSymbol(Term), Old)) + term_RplacTop(Term,New); + else + for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) + term_ExchangeVariable(list_Car(Scan),Old,New); +} + + +BOOL term_SubstituteVariable(SYMBOL Symbol, TERM Repl, TERM* Term) +/****************************************************** + INPUT: A Symbol which has to be found in the Term, + a term which is the replacement for the + 'Symbol', and a term in which the substitu- + tions take place. + RETURNS: A boolean value which is TRUE, if any sub- + stitutions were made. + SUMMARY: term_Substitute works recursively and repl. + every occurence of 'Symbol' in 'Term' by + 'Repl'. + CAUTION: FUNCTION IS DESTRUCTIVE ON 'Term'. REPLACE- + MENT IS COPIED EACH TIME A SUB. TAKES PLACE +*******************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(*Term) || !term_IsTerm(Repl) || !symbol_IsSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_SubstituteVariable: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (symbol_Equal(term_TopSymbol(*Term), Symbol)) { + + TERM New; + New = term_Copy(Repl); + (*Term)->symbol = Repl->symbol; + (*Term)->args = term_ArgumentList(New); + + /* Free Top-Node of New, as the symbol has been written */ + /* into the node pointed to by `Term'. */ + memory_Free(New, sizeof(TERM_NODE)); + return TRUE; + + } else { + + BOOL Result; + LIST List; + + Result = FALSE; + for (List = term_ArgumentList(*Term); + list_Exist(List); List = list_Cdr(List)) + if (term_SubstituteVariable(Symbol, Repl, (TERM*) &(List->car))) + Result = TRUE; + return Result; + } +} + + +static int term_CompareByConstants(TERM Left, TERM Right) +/************************************************************** + INPUT: Two terms. + RETURNS: 1 if left term < right term + 0 if left term = right term + -1 if left term > right term + EFFECT: The terms are compared by their multisets of + constants. The frequency of elements in the + multisets is a multiset itself. The frequencies + are sorted and the resulting sorted multisets + compared. +***************************************************************/ +{ + LIST lconsts, rconsts; + int result; + + /* Get multiset of constants. */ + + lconsts = term_ListOfConstants(Left); + rconsts = term_ListOfConstants(Right); + + result = list_CompareMultisetsByElementDistribution(lconsts, rconsts); + + list_Delete(lconsts); + list_Delete(rconsts); + + return result; +} + +static int term_CompareByFunctions(TERM Left, TERM Right) +/************************************************************** + INPUT: Two terms. + RETURNS: 1 if left term < right term + 0 if left term = right term + -1 if left term > right term + EFFECT: The terms are compared by their multisets of + functions. The frequency of elements in the + multisets is a multiset itself. The frequencies + are sorted and the resulting sorted multisets + compared. +***************************************************************/ +{ + LIST lfuns, rfuns; + int result; + + /* Get multiset of functions. */ + + lfuns = term_ListOfFunctions(Left); + rfuns = term_ListOfFunctions(Right); + + result = list_CompareMultisetsByElementDistribution(lfuns, rfuns); + + list_Delete(lfuns); + list_Delete(rfuns); + + return result; +} + +static int term_CompareByVariables(TERM Left, TERM Right) +/************************************************************** + INPUT: Two terms. + RETURNS: 1 if left term < right term + 0 if left term = right term + -1 if left term > right term + EFFECT: The terms are compared by their multisets of + variables. The frequency of elements in the + multisets is a multiset itself. The frequencies + are sorted and the resulting sorted multisets + compared. +***************************************************************/ +{ + LIST lvars, rvars; + int result; + + /* Get multiset of variables. */ + + lvars = term_ListOfVariables(Left); + rvars = term_ListOfVariables(Right); + + result = list_CompareMultisetsByElementDistribution(lvars, rvars); + + list_Delete(lvars); + list_Delete(rvars); + + return result; +} + +LIST term_ListOfConstants(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: A list of constants. + EFFECT: Creates a list of constants used in a term. If no + constants are used in a term, it returns an empty + list. +***************************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ListOfConstants: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (symbol_IsConstant(term_TopSymbol(Term))) + return list_List((POINTER) term_TopSymbol(Term)); + else { + LIST result; + LIST scan; + + result = list_Nil(); + for (scan = term_ArgumentList(Term); + !list_Empty(scan); + scan = list_Cdr(scan)) { + /* Append to the smaller list for efficiency. + A subterm's list of constants will usually + be smaller than the intermediate result. + */ + result = list_Nconc(term_ListOfConstants((TERM) list_Car(scan)), result); + } + + return result; + } +} + +LIST term_ListOfFunctions(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: A list of functions. + EFFECT: Creates a list of functions used in a term. If no + functions are used in a term, it returns an empty + list. +***************************************************************/ +{ + LIST result; + LIST scan; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ListOfFunctions: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + result = list_Nil(); + + /* If the term starts with a function, add the function symbol + to the result. + */ + if (symbol_IsFunction(term_TopSymbol(Term))) { + result = list_Nconc(result, list_List((POINTER) term_TopSymbol(Term))); + } + + /* A function can utilize other functions, so + traverse the argument list for further + functions. + */ + for (scan = term_ArgumentList(Term); + !list_Empty(scan); + scan = list_Cdr(scan)) { + /* Append to the smaller list for efficiency. + A subterm's list of functions will usually + be smaller than the intermediate result. + */ + result = list_Nconc(term_ListOfFunctions((TERM) list_Car(scan)), result); + } + + return result; +} + +void term_CountSymbols(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: None. + EFFECT: Counts the non-variable symbols in the term, and + increases their counts accordingly. +***************************************************************/ +{ + LIST scan; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_CountSymbols: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + /* If the term starts with a function, increase the count for + the function symbol. + */ + if (symbol_IsFunction(term_TopSymbol(Term))) { + SYMBOL S; + + S = term_TopSymbol(Term); + symbol_SetCount(S, symbol_GetCount(S) + 1); + } + + /* A function can utilize other functions, so + traverse the argument list for further + function symbols. + */ + for (scan = term_ArgumentList(Term); + !list_Empty(scan); + scan = list_Cdr(scan)) { + term_CountSymbols((TERM) list_Car(scan)); + } +} + +static int term_CompareByArity(TERM Left, TERM Right) +/************************************************************** + INPUT: Two terms. + RETURNS: 1 if left term < right term + 0 if left term = right term + -1 if left term > right term + EFFECT: Terms are compared top down, left to right with + respect to the arity of their signature symbols, + where variables in addition are defined to be smaller + than constants. +***************************************************************/ +{ + NAT lval, rval; + SYMBOL lsymb, rsymb; + LIST largs, rargs; + int result; + + result = 0; + + /* Compare top symbols first */ + lsymb = term_TopSymbol(Left); + rsymb = term_TopSymbol(Right); + + if (symbol_IsVariable(lsymb)) { + if (symbol_IsVariable(rsymb)) + return 0; + else + return 1; + } + else + if (symbol_IsVariable(rsymb)) + return -1; + + lval = symbol_Arity(lsymb); + rval = symbol_Arity(rsymb); + + if (lval > rval) + return -1; + + if (lval < rval) + return 1; + + /* If top symbol arities are equal, compare subterms left to right */ + largs = term_ArgumentList(Left); + rargs = term_ArgumentList(Right); + + while(!list_Empty(largs)) { + result = term_CompareByArity(list_Car(largs), list_Car(rargs)); + if (result != 0) + break; + + largs = list_Cdr(largs); + rargs = list_Cdr(rargs); + } + + return result; +} + +int term_CompareBySymbolOccurences(TERM Left, TERM Right) +/************************************************************** + INPUT: Two terms. + RETURNS: 1 if left term < right term + 0 if left term = right term + -1 if left term > right term + EFFECT: Terms are compared top down, left to right with + respect to the frequency of their symbols. +***************************************************************/ +{ + unsigned long lval, rval; + SYMBOL lsymb, rsymb; + LIST largs, rargs; + int result; + + result = 0; + + /* Compare top symbols first */ + lsymb = term_TopSymbol(Left); + rsymb = term_TopSymbol(Right); + + if (symbol_IsFunction(lsymb)) { + if (symbol_IsFunction(rsymb)) { + + lval = symbol_GetCount(lsymb); + rval = symbol_GetCount(rsymb); + + if (lval > rval) + return -1; + + if (lval < rval) + return 1; + + /* If top symbol arities are equal, compare subterms left to right */ + largs = term_ArgumentList(Left); + rargs = term_ArgumentList(Right); + + while(!list_Empty(largs)) { + result = term_CompareBySymbolOccurences(list_Car(largs), + list_Car(rargs)); + if (result != 0) + break; + + largs = list_Cdr(largs); + rargs = list_Cdr(rargs); + } + } + else { + return -1; + } + } + else { + if (symbol_IsFunction(rsymb)) { + return 1; + } + } + + return result; +} + +int term_CompareAbstract(TERM Left, TERM Right) +/************************************************************** + INPUT: Two terms. + RETURNS: 1 if left term < right term + 0 if left term = right term + -1 if left term > right term + EFFECT: Compares two terms using an internal array of term + comparison functions. As soon as a term is found to + compare greater than the other, the result of the + comparison is returned. If all term comparison + functions yield an "equal", then 0 is returned. +***************************************************************/ +{ + int result; + int i; + int functions; + + typedef int (*TERM_COMPARE_FUNCTION) (TERM, TERM); + + static const TERM_COMPARE_FUNCTION term_compare_functions [] = { + term_CompareByArity, + term_CompareBySymbolOccurences, + term_CompareByConstants, + term_CompareByVariables, + term_CompareByFunctions + }; + +#ifdef CHECK + if (!(term_IsTerm(Left) && term_IsTerm(Right))) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_CompareAbstract: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + result = 0; + functions = sizeof(term_compare_functions)/sizeof(TERM_COMPARE_FUNCTION); + + for (i = 0; i < functions; i++) { + result = term_compare_functions[i](Left, Right); + + if ( result != 0) { + return result; + } + } + + return result; +} + +BOOL term_CompareAbstractLEQ(TERM Left, TERM Right) +/************************************************************** + INPUT: Two terms. + RETURNS: TRUE if left term <= right term, FALSE otherwise. + EFFECT: Terms are compared top down, left to right with + respect to the arity of their signature symbols, + where variables in addition are defined to be smaller + than constants. +***************************************************************/ +{ + return (term_CompareAbstract(Left, Right) >= 0); +} + + +NAT term_ComputeSize(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: The number of symbols in the term. + EFFECT: None +***************************************************************/ +{ + NAT Weight; + LIST Scan; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ComputeSize: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Weight = 1; + for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) + Weight += term_ComputeSize((TERM)list_Car(Scan)); + return Weight; +} + +NAT term_RootDistance(TERM Term) +/************************************************************** + INPUT: A term with establised father links. + RETURNS: The distance from <Term> to its root father term. + EFFECT: None +***************************************************************/ +{ + NAT Distance; + + Distance = 0; + + while (term_Superterm(Term) != (TERM)NULL) { + Distance++; + Term = term_Superterm(Term); + } + + return Distance; +} + +BOOL term_RootDistanceSmaller(TERM Term1, TERM Term2) +/************************************************************** + INPUT: Two terms with establised father links. + RETURNS: TRUE iff root distance of <Term1> is smaller than + root distance of <Term2> + EFFECT: None +***************************************************************/ +{ + return (term_RootDistance(Term1)<term_RootDistance(Term2)); +} + +void term_InstallSize(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: None + EFFECT: Sets for every subterm the size. +***************************************************************/ +{ + NAT Weight; + LIST Scan; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_InstallSize: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Weight = 1; + for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) { + term_InstallSize((TERM)list_Car(Scan)); + Weight += term_Size((TERM)list_Car(Scan)); + }; + term_SetSize(Term, Weight); +} + +NAT term_Depth(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: The depth of the term. + EFFECT: None +***************************************************************/ +{ + NAT Depth,Help; + LIST Scan; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_Depth: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Depth = 0; + for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) { + Help = term_Depth(list_Car(Scan)); + if (Help > Depth) + Depth = Help; + } + return (Depth+1); +} + +BOOL term_ContainsSymbol(TERM Term, SYMBOL Symbol) +/************************************************************** + INPUT: A term and a symbol. + RETURNS: TRUE, if the symbol occurs somewhere in the term, + FALSE otherwise. +***************************************************************/ +{ + int Stack; + +#ifdef CHECK + if (!term_IsTerm(Term) || !symbol_IsSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ContainsSymbol: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Stack = stack_Bottom(); + + do { + if (term_TopSymbol(Term) == Symbol) { + stack_SetBottom(Stack); /* Clean up the stack */ + return TRUE; + } + else + if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + + if (!stack_Empty(Stack)) { + Term = list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(Stack)); + + return FALSE; +} + +TERM term_FindSubterm(TERM Term, SYMBOL Symbol) +/************************************************************** + INPUT: A term and a symbol. + RETURNS: If the symbol occurs in the Term the subterm is returned. + NULL otherwise. +***************************************************************/ +{ + int stack; + +#ifdef CHECK + if (!term_IsTerm(Term) || !symbol_IsSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_FindSubterm: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + stack = stack_Bottom(); + + do { + if (term_TopSymbol(Term) == Symbol) { + stack_SetBottom(stack); /* Clean up the stack */ + return Term; + } else if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + + while (!stack_Empty(stack) && list_Empty(stack_Top())) + stack_Pop(); + + if (!stack_Empty(stack)) { + Term = list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(stack)); + + return NULL; +} + +static int term_SharingList(TERM Term, LIST List) +/************************************************************** + INPUT: A term and a list cell. + RETURNS: The number of times <List> occurs in <Term> + EFFECT: None +***************************************************************/ +{ + LIST Scan; + int n; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_SharingList: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + n = 0; + + for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) { + if (Scan == List) + n++; + n += term_SharingList(list_Car(Scan), List); + } + + return n; +} + + +static int term_SharingTerm(TERM Term, TERM CompareTerm) +/************************************************************** + INPUT: A term and a compare term + RETURNS: The number of occurrences of <CompareTerm> in <Term> + EFFECT: None +***************************************************************/ +{ + LIST Scan; + int n; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_SharingTerm: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + n = 0; + + if (Term == CompareTerm) + n = 1; + + for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) + n += term_SharingTerm(list_Car(Scan),CompareTerm); + + return n; +} + + +BOOL term_Sharing(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: TRUE iff the term shares list cells or subterms. + EFFECT: None +***************************************************************/ +{ + LIST Scan; + int stack; + TERM ActTerm; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_Sharing: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + stack = stack_Bottom(); + stack_Push(Term); + + while (!stack_Empty(stack)) { + ActTerm = (TERM)stack_Top(); + stack_Pop(); + + if (term_SharingTerm(Term,ActTerm)>1) + return TRUE; + + if (term_IsComplex(Term)) { + for (Scan = term_ArgumentList(ActTerm); + !list_Empty(Scan); + Scan=list_Cdr(Scan)) + if (term_SharingList(Term, Scan) > 1) + return TRUE; + else + stack_Push(list_Car(Scan)); + } + } + + return FALSE; +} + + +void term_AddFatherLinks(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: void. + EFFECT: The super term links of Term are cleared and then all + its subterms are set. +***************************************************************/ +{ + LIST Scan; + TERM ActTerm; + + term_RplacSuperterm(Term,(TERM)NULL); + + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + ActTerm = (TERM)list_Car(Scan); + term_AddFatherLinks(ActTerm); + term_RplacSuperterm(ActTerm,Term); + } + +} + +BOOL term_FatherLinksEstablished(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: TRUE iff all father links in Term are established. + EFFECT: None. +***************************************************************/ +{ + LIST Scan; + + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + if (Term != term_Superterm(list_Car(Scan)) || !term_FatherLinksEstablished(list_Car(Scan))) + return FALSE; + + return TRUE; +} + +TERM term_TopLevelTerm(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: The top level father of the term. + EFFECT: The father links have to be established! +***************************************************************/ +{ + while (term_Superterm(Term)) + Term = term_Superterm(Term); + return Term; +} + + +BOOL term_HasPointerSubterm(TERM Term, TERM Subterm) +/************************************************************** + INPUT: Two terms. + RETURNS: TRUE, if <Term> has <Subterm> as a subterm. + CAUTION: Only term pointers are compared, term_Equal isn't used. +***************************************************************/ +{ + if (Term == Subterm) + return TRUE; + else { + LIST scan = term_ArgumentList(Term); + + while (!list_Empty(scan)) { + if (term_HasPointerSubterm((TERM) list_Car(scan), Subterm)) + return TRUE; + scan = list_Cdr(scan); + } + } + + return FALSE; +} + +BOOL term_HasSubterm(TERM Term, TERM Subterm) +/************************************************************** + INPUT: Two terms. + RETURNS: TRUE, if <Term> has <Subterm> as a subterm. + CAUTION: term_Equal is used. +***************************************************************/ +{ + if (term_Equal(Term,Subterm)) + return TRUE; + else { + LIST Scan; + Scan = term_ArgumentList(Term); + + while (!list_Empty(Scan)) { + if (term_HasSubterm((TERM) list_Car(Scan), Subterm)) + return TRUE; + Scan = list_Cdr(Scan); + } + } + + return FALSE; +} + +BOOL term_HasProperSuperterm(TERM Term, TERM Super) +/********************************************************** + INPUT : Two terms. + RETURNS : TRUE iff Super can be reached from Term by following + the superterm member of the TERM structure. + CAUTION : not reflexive +**********************************************************/ +{ + if (Term == Super) + return FALSE; + while (Term != (TERM) NULL) { + if (Term == Super) /* Pointer equality ! */ + return TRUE; + else + Term = term_Superterm(Term); + } + return FALSE; +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * TERM OUTPUT FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +void term_Print(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: none. + SUMMARY: Prints the term to stdout. + CAUTION: Uses the other term output functions. +***************************************************************/ +{ + if (term_IsComplex(Term)) { + putchar('('); + symbol_Print(term_TopSymbol(Term)); + putchar(' '); + term_TermListPrint(term_ArgumentList(Term)); + putchar(')'); + + } else if (term_IsVariable(Term)) { + + symbol_Print(term_TopSymbol(Term)); + + } else { + + /* term_IsConstant(Term) */ + putchar('('); + symbol_Print(term_TopSymbol(Term)); + putchar(')'); + } +} + +static void term_PrettyPrintIntern(TERM Term, int Depth) +/************************************************************** + INPUT: A term and a depth parameter for indentation. + RETURNS: none. + SUMMARY: Prints the term hopefully more pretty to stdout. +***************************************************************/ +{ + int i; + LIST scan; + + + for (i=0; i < Depth; i++) + fputs(" ", stdout); + if (symbol_IsJunctor(term_TopSymbol(Term))) { + if (term_IsComplex(Term)) { + symbol_Print(term_TopSymbol(Term)); + putchar('('); + fputs("\n", stdout); + for (scan=term_ArgumentList(Term); !list_Empty(scan); scan= list_Cdr(scan)) { + term_PrettyPrintIntern((TERM) list_Car(scan), Depth+1); + if (!list_Empty(list_Cdr(scan))) + fputs(",\n", stdout); + } + putchar(')'); + } + else { + if (term_IsVariable(Term)) { + symbol_Print(term_TopSymbol(Term)); + } + else { + putchar('('); + symbol_Print(term_TopSymbol(Term)); + putchar(')'); + } + } + } + else { + term_PrintPrefix(Term); + } +} + +void term_PrettyPrint(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: none. + SUMMARY: Prints the term hopefully more pretty to stdout. +***************************************************************/ +{ + term_PrettyPrintIntern(Term, 0); +} + + +void term_FPrint(FILE* File,TERM Term) +/************************************************************** + INPUT: A file and a term. + RETURNS: none. + SUMMARY: Prints the term to the file. + CAUTION: Uses the other term output functions. +***************************************************************/ +{ + if (term_IsComplex(Term)) { + putc('(', File); + symbol_FPrint(File,term_TopSymbol(Term)); + putc(' ', File); + term_TermListFPrint(File,term_ArgumentList(Term)); + putc(')', File); + + } else if (term_IsVariable(Term)) { + + symbol_FPrint(File,term_TopSymbol(Term)); + + } else { + + /* term_IsConstant(Term) */ + putc('(', File); + symbol_FPrint(File,term_TopSymbol(Term)); + putc(')', File); + } +} + + +void term_TermListPrint(LIST List) +/************************************************************** + INPUT: A list of terms. + RETURNS: None. +***************************************************************/ +{ + for (; !list_Empty(List); List=list_Cdr(List)) { + term_Print(list_Car(List)); fflush(stdout); + if (!list_Empty(list_Cdr(List))) + putchar(' '); + } +} + + +void term_TermListFPrint(FILE* File, LIST List) +/************************************************************** + INPUT: A list of terms. + RETURNS: None. +***************************************************************/ +{ + for (; !list_Empty(List); List=list_Cdr(List)) { + term_FPrint(File,list_Car(List)); + if (!list_Empty(list_Cdr(List))) + putc(' ', File); + } +} + + +void term_PrintPrefix(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: none. + SUMMARY: Prints the term in prefix notation to stdout. + CAUTION: Uses the other term output functions. +***************************************************************/ +{ + if (term_IsComplex(Term)) { + symbol_Print(term_TopSymbol(Term)); + putchar('('); + term_TermListPrintPrefix(term_ArgumentList(Term)); + putchar(')'); + + } else + symbol_Print(term_TopSymbol(Term)); +} + + +void term_FPrintPrefix(FILE* File, TERM Term) +/************************************************************** + INPUT: A file and a term. + RETURNS: none. + SUMMARY: Prints the term in prefix notation to the file. + CAUTION: Uses the other term output functions. +***************************************************************/ +{ + if (term_IsComplex(Term)) { + symbol_FPrint(File,term_TopSymbol(Term)); + putc('(', File); + term_TermListFPrintPrefix(File,term_ArgumentList(Term)); + putc(')', File); + + } else + symbol_FPrint(File,term_TopSymbol(Term)); +} + + +void term_TermListPrintPrefix(LIST List) +/************************************************************** + INPUT: A list of terms. + RETURNS: None. +***************************************************************/ +{ + for (; !list_Empty(List); List=list_Cdr(List)) { + term_PrintPrefix(list_Car(List)); + if (!list_Empty(list_Cdr(List))) + putchar(','); + } +} + + +void term_TermListFPrintPrefix(FILE* File, LIST List) +/************************************************************** + INPUT: A list of terms. + RETURNS: None. +***************************************************************/ +{ + for (; !list_Empty(List); List=list_Cdr(List)) { + term_FPrintPrefix(File,list_Car(List)); + if (!list_Empty(list_Cdr(List))) + putc(',', File); + } +} + + + +void term_FPrintOtterPrefix(FILE* File, TERM Term) +/************************************************************** + INPUT: A file and a term. + RETURNS: none. + SUMMARY: Prints the term in prefix notation to the file. + CAUTION: Uses the other term_Output functions. +***************************************************************/ +{ + if (term_IsComplex(Term)) { + symbol_FPrintOtter(File, term_TopSymbol(Term)); + putc('(', File); + term_TermListFPrintOtterPrefix(File, term_ArgumentList(Term)); + putc(')', File); + } else + symbol_FPrintOtter(File, term_TopSymbol(Term)); +} + + +void term_TermListFPrintOtterPrefix(FILE* File, LIST List) +/************************************************************** + INPUT: A list of terms. + RETURNS: None. +***************************************************************/ +{ + for (; !list_Empty(List); List=list_Cdr(List)) { + term_FPrintOtterPrefix(File,list_Car(List)); + if (!list_Empty(list_Cdr(List))) + putc(',', File); + } +} + + +void term_FPrintPosition(FILE* File, TERM TopTerm, TERM Subterm) +/************************************************************** + INPUT: An output file and two terms where <Subterm> is a subterm + of <TopTerm>. + RETURNS: Nothing. + SUMMARY: The position of <Subterm> relative to <TopTerm> is + printed to the output file. A simple top-down search + is done, so the superterm pointers are not needed. + Note that we compare terms with respect to pointers! + If <Subterm> isn't a subterm of <TopTerm> at all, + this causes an error message followed by a core dump. +***************************************************************/ +{ + NAT pos; + LIST Scan; + + if (TopTerm == Subterm) + return; + + for (Scan = term_ArgumentList(TopTerm), pos = 1; !list_Empty(Scan); + Scan = list_Cdr(Scan), pos++) { + if (term_HasPointerSubterm(list_Car(Scan), Subterm)) { + fprintf(File, "%u", pos); + if (Subterm != list_Car(Scan)) { + putc('.', File); + term_FPrintPosition(File, list_Car(Scan), Subterm); + } + return; + } + } + misc_StartErrorReport(); + misc_ErrorReport("\n In term_FPrintPosition: Term isn't subterm of the other one."); + misc_FinishErrorReport(); +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * HIGH LEVEL FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +NAT term_Bytes(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: The number of bytes occupied by the term. + EFFECT: None +***************************************************************/ +{ + NAT Bytes; + LIST Scan; + + Bytes = sizeof(TERM_NODE) + list_Bytes(term_ArgumentList(Term)); + for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) + Bytes += term_Bytes((TERM)list_Car(Scan)); + return Bytes; +} + + +LIST term_ListOfVariables(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: The list of variables occurring in the term. + Note that there may be many terms with same variable symbol. +***************************************************************/ +{ + LIST Stack, Variables; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ListOfVariables: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Variables = list_Nil(); + Stack = list_StackBottom(); + do { + if (term_IsComplex(Term)) + Stack = list_Push(term_ArgumentList(Term),Stack); + else + if (term_IsVariable(Term)) + Variables = list_Cons(Term, Variables); + while (!list_StackEmpty(Stack) && list_Empty(list_Top(Stack))) + Stack = list_Pop(Stack); + if (!list_StackEmpty(Stack)) { + Term = (TERM)list_Car(list_Top(Stack)); + list_RplacTop(Stack, list_Cdr(list_Top(Stack))); + } + } while (!list_StackEmpty(Stack)); + return Variables; +} + + +void term_MarkVariables(TERM Term, NAT Mark) +/************************************************************** + INPUT: A term. + RETURNS: Nothing. + EFFECT: All variables from <Term> are marked with <Mark>. + CAUTION: The term module must be in a binding phase (started with + term_StartBinding)! +***************************************************************/ +{ + int Stack; + +#ifdef CHECK + if (!term_InBindingPhase()) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_MarkVariables:"); + misc_ErrorReport(" Called while not in binding phase."); + misc_FinishErrorReport(); + } +#endif + + Stack = stack_Bottom(); + do { + if (term_IsComplex(Term)) { + stack_Push(term_ArgumentList(Term)); + } + else if (term_IsVariable(Term)) + term_CreateBinding(term_TopSymbol(Term), Mark); + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + if (!stack_Empty(Stack)) { + Term = (TERM)list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(Stack)); +} + + +LIST term_VariableSymbols(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: The list of variable symbols occurring in the term. +***************************************************************/ +{ + LIST Variables; + int Stack; + SYMBOL Top; + NAT ActMark; + +#ifdef CHECK + if (!term_IsTerm(Term) || term_InBindingPhase()) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_VariableSymbols: Illegal input or context."); + misc_FinishErrorReport(); + } +#endif + + term_StartBinding(); + + Variables = list_Nil(); + Stack = stack_Bottom(); + ActMark = term_ActMark(); + do { + if (term_IsComplex(Term)) { + stack_Push(term_ArgumentList(Term)); + } + else { + Top = term_TopSymbol(Term); + if (symbol_IsVariable(Top) && !term_VarIsMarked(Top, ActMark)) { + Variables = list_Cons((POINTER)Top, Variables); + term_CreateBinding(Top, ActMark); + } + } + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + if (!stack_Empty(Stack)) { + Term = (TERM)list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(Stack)); + + term_StopBinding(); + + return Variables; +} + + +NAT term_NumberOfVarOccs(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: The list of variable symbols occurring in the term. +***************************************************************/ +{ + NAT Result; + int Stack; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_NumberOfVarOccs: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Result = 0; + Stack = stack_Bottom(); + do { + if (term_IsComplex(Term)) { + stack_Push(term_ArgumentList(Term)); + } + else { + if (symbol_IsVariable(term_TopSymbol(Term))) + Result++; + } + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + if (!stack_Empty(Stack)) { + Term = (TERM)list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(Stack)); + + return Result; +} + +NAT term_NumberOfSymbolOccurrences(TERM Term, SYMBOL Symbol) +/************************************************************** + INPUT: A term and a symbol. + RETURNS: The number of occurrences of <Symbol> in <Term> +***************************************************************/ +{ + NAT Result; + LIST Scan; + +#ifdef CHECK + if (!term_IsTerm(Term) || !symbol_IsSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_NumberOfSymbolOccurrences: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Result = 0; + + if (symbol_Equal(term_TopSymbol(Term),Symbol)) + Result++; + + for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) + Result += term_NumberOfSymbolOccurrences(list_Car(Scan), Symbol); + + return Result; +} + + +BOOL term_ContainsFunctions(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: TRUE iff the term contains a function symbol +***************************************************************/ +{ + int Stack; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ContainsFunctions: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Stack = stack_Bottom(); + do { + if (term_IsComplex(Term)) { + if (symbol_IsFunction(term_TopSymbol(Term)) && !symbol_IsConstant(term_TopSymbol(Term))) { + stack_SetBottom(Stack); + return TRUE; + } + stack_Push(term_ArgumentList(Term)); + } + + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + if (!stack_Empty(Stack)) { + Term = (TERM)list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(Stack)); + + return FALSE; +} + +BOOL term_ContainsVariable(TERM Term, SYMBOL Var) +/************************************************************** + INPUT: A term and a variable symbol. + RETURNS: TRUE iff the term contains the variable symbol +***************************************************************/ +{ + int Stack; + +#ifdef CHECK + if (!term_IsTerm(Term) || !symbol_IsSymbol(Var)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_ContainsVariable: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Stack = stack_Bottom(); + do { + if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + else + if (symbol_Equal(term_TopSymbol(Term),Var)) { + stack_SetBottom(Stack); + return TRUE; + } + + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + if (!stack_Empty(Stack)) { + Term = (TERM)list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(Stack)); + + return FALSE; +} + +SYMBOL term_MaxVar(TERM Term) +/********************************************************* + INPUT: A term. + RETURNS: The maximal variable in <Term>, NULL otherwise +********************************************************/ +{ + LIST Scan; + int Stack; + SYMBOL Result; + +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_MaxVar: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + Result = (SYMBOL)NULL; + Stack = stack_Bottom(); + + if (term_IsStandardVariable(Term)) { + if (term_TopSymbol(Term)>Result) + Result = term_TopSymbol(Term); + } + else + if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + + while (!stack_Empty(Stack)) { + Scan = stack_Top(); + Term = (TERM)list_Car(Scan); + stack_RplacTop(list_Cdr(Scan)); + + if (term_IsStandardVariable(Term)) { + if (term_TopSymbol(Term)>Result) + Result = term_TopSymbol(Term); + } + else + if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + } + + return Result; +} + + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * Renaming * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +void term_StartMinRenaming(void) +/************************************************************** + INPUT: None + EFFECT: Initializes the term and symbol modules for min co var renaming +***************************************************************/ +{ + symbol_ResetStandardVarCounter(); + term_NewMark(); +} + + +void term_StartMaxRenaming(SYMBOL MaxVar) +/************************************************************** + INPUT: A variable symbol. + EFFECT: Initializes the term and symbol modules for renaming above <MaxVar> +***************************************************************/ +{ + symbol_SetStandardVarCounter(MaxVar); + term_NewMark(); +} + + +TERM term_Rename(TERM Term) +/************************************************************** + INPUT: A Term. + RETURNS: The destructively renamed term. + EFFECT: All co variables are destructively renamed in <TERM> +***************************************************************/ +{ + int Stack; + SYMBOL Top; + NAT ActMark; + TERM ActTerm; + +#ifdef CHECK + if (!term_IsTerm(Term) || term_InBindingPhase()) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_Rename: Illegal input or context."); + misc_FinishErrorReport(); + } +#endif + + term_StartBinding(); + + Stack = stack_Bottom(); + ActMark = term_OldMark(); + ActTerm = Term; + do { + if (term_IsComplex(ActTerm)) { + stack_Push(term_ArgumentList(ActTerm)); + } + else { + Top = term_TopSymbol(ActTerm); + if (symbol_IsVariable(Top)) { + if (!term_VarIsMarked(Top, ActMark)) + term_CreateValueBinding(Top, ActMark, (POINTER)symbol_CreateStandardVariable()); + term_RplacTop(ActTerm,(SYMBOL)term_BindingValue(Top)); + } + } + + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + if (!stack_Empty(Stack)) { + ActTerm = (TERM)list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(Stack)); + + term_StopBinding(); + + return Term; +} + +SYMBOL term_GetRenamedVarSymbol(SYMBOL Var) +/************************************************************** + INPUT: A variable symbol. + RETURNS: The renamed variable for symbol for <var> with respect + to the current renaming. If it does not exist, <var> + itself is returned. + EFFECT: None. +***************************************************************/ +{ + NAT ActMark; + +#ifdef CHECK + if (!symbol_IsStandardVariable(Var)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_GetRenamedVarSymbol: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + ActMark = term_OldMark(); + + if (term_VarIsMarked(Var, ActMark)) + return (SYMBOL)term_BindingValue(Var); + + return Var; +} + + +static LIST term_MakePseudoLinear(TERM Term, NAT Depth, NAT Mark) +/************************************************************** + INPUT: A Term and a variable and the current depth. + RETURNS: A list of pairs (<oldvar>,<newvar>) + EFFECT: The term is destructively made pseudo_linear. +***************************************************************/ +{ + LIST Result,Scan; + SYMBOL Top; + + Result = list_Nil(); + + if (term_IsComplex(Term)) + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + Result = list_Nconc(term_MakePseudoLinear(list_Car(Scan),Depth+1,Mark), + Result); + else { + Top = term_TopSymbol(Term); + if (symbol_IsVariable(Top)) { + if (term_VarIsMarked(Top, Mark)) { + if (Depth != (NAT)term_BindingValue(Top)) + term_RplacTop(Term,symbol_CreateStandardVariable()); + Result = list_Cons(list_PairCreate((POINTER)Top, + (POINTER)term_TopSymbol(Term)), + Result); + } + else { + term_CreateValueBinding(Top, Mark, (POINTER)Depth); + } + } + } + + return Result; +} + + +LIST term_RenamePseudoLinear(TERM Term, SYMBOL Var) +/************************************************************** + INPUT: A Term and a variable. + RETURNS: A list of pairs (<oldvar>,<newvar>) + EFFECT: The term is destructively renamed. +***************************************************************/ +{ + NAT Mark; + LIST Result; + +#ifdef CHECK + if (!term_IsTerm(Term) || !symbol_IsVariable(Var) || term_InBindingPhase()) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_RenamePseudoLinear: Illegal input or context."); + misc_FinishErrorReport(); + } +#endif + + term_StartBinding(); + symbol_SetStandardVarCounter(Var); + + term_NewMark(); + Mark = term_ActMark(); + Result = term_MakePseudoLinear(Term,0,Mark); + + term_StopBinding(); + + return Result; +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * STAMP FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +NAT term_GetStampID(void) +/************************************************************** + INPUT: None + RETURNS: An identifier that must be used for some stamp functions + EFFECT: Each module using the term stamp has to request an + identifier that is needed for function term_StampOverflow + The purpose of this identifier is to synchronize + different modules in case of an overflow of the variable + term_STAMP. +***************************************************************/ +{ + if (term_STAMPUSERS >= term_MAXSTAMPUSERS) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n In term_GetStampID: no more free stamp IDs."); + misc_UserErrorReport("\n You have to increase the constant term_MAXSTAMPUSERS."); + misc_FinishUserErrorReport(); + } + + return term_STAMPUSERS++; +} + + +BOOL term_StampOverflow(NAT ID) +/************************************************************** + INPUT: The identifier of the calling module as returned by + the function term_GetStampID. + RETURNS: True if an overflow of the variable term_STAMP occurred + for the module with the identifier ID. + CAUTION: If an overflow occurred for a module you can test that + only once!!! After the first test the overflow flag + is cleared for that module. +***************************************************************/ +{ + BOOL Result = FALSE; + NAT i; + +#ifdef CHECK + if (ID >= term_MAXSTAMPUSERS) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_StampOverflow: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + if (term_STAMP == NAT_MAX) { + term_STAMP = 0; + /* set overflow flag for all other modules */ + for (i = 0; i < term_MAXSTAMPUSERS; i++) + term_STAMPOVERFLOW[i] = TRUE; + term_STAMPOVERFLOW[ID] = FALSE; + Result = TRUE; + } else if (term_STAMPOVERFLOW[ID]) { + term_STAMPOVERFLOW[ID] = FALSE; + Result = TRUE; + } + return Result; +} + +void term_SetTermSubtermStamp(TERM Term) +/************************************************************** + INPUT: A term. + RETURNS: void. + EFFECT: Sets the current stamp to <Term> and its subterms. +***************************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_SetTermSubtermStamp: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + term_SetTermStamp(Term); + list_Apply((void (*)(POINTER)) term_SetTermSubtermStamp, + term_ArgumentList(Term)); +} + +LIST term_ListOfAtoms(TERM Term, SYMBOL Predicate) +/************************************************************** + INPUT: A term and a predicate symbol. + RETURNS: A list of pointers to all atoms in Term with + predicate symbol <Predicate>. +***************************************************************/ +{ + if (symbol_Equal(term_TopSymbol(Term), Predicate)) + return list_List(Term); + else { + LIST Result, List; + + Result = list_Nil(); + for (List = term_ArgumentList(Term); !list_Empty(List); List = list_Cdr(List)) + Result = list_Nconc(Result, term_ListOfAtoms(list_Car(List), Predicate)); + return Result; + } +} + +/* Currently only in CHECK mode */ +#ifdef CHECK + +void term_StartStamp(void) +/************************************************************** + INPUT: None + RETURNS: Nothing + EFFECT: The stamp is prepared for a new term traversal. +***************************************************************/ +{ + if (term_STAMPBLOCKED) { + /* Error: the Stamp is already used */ + misc_StartErrorReport(); + misc_ErrorReport("\n In term_StartStamp: Illegal context, term stamp is already used."); + misc_FinishErrorReport(); + } + else { + term_STAMP++; + term_STAMPBLOCKED = TRUE; + } +} + +#endif + +LIST term_FindAllAtoms(TERM Term, SYMBOL Predicate) +/********************************************************************** + INPUT: A term Term and a symbol Predicate. + RETURN: A list of all atoms of Term with Symbol as top symbol. +***********************************************************************/ +{ + int stack; + LIST Result; + +#ifdef CHECK + if (!term_IsTerm(Term) || !symbol_IsPredicate(Predicate)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In term_FindAllPredicates: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + stack = stack_Bottom(); + Result = list_Nil(); + + do { + if (term_TopSymbol(Term) == Predicate) { + Result = list_Cons(Term, Result); + } else if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + + while (!stack_Empty(stack) && list_Empty(stack_Top())) + stack_Pop(); + + if (!stack_Empty(stack)) { + Term = list_Car(stack_Top()); + stack_RplacTop(list_Cdr(stack_Top())); + } + } while (!stack_Empty(stack)); + + return Result; +} + +BOOL term_CheckTermIntern(TERM Term, BOOL Links) +/************************************************************************** + INPUT: A term and a boolean. + RETURN: True iff 1) the arity of each top symbol is equal to the number + of arguments of symbol's term. + and 2) either all father links are set correctly iff Links is TRUE + or none is set iff Links is FALSE. + COMMENT: Intern function of term_CheckTerm. +***************************************************************************/ +{ + LIST Scan; + SYMBOL Top; + + if (!term_IsTerm(Term)) + return FALSE; + + Top = term_TopSymbol(Term); + if (symbol_IsSignature(Top) && + symbol_Arity(Top) != -1 && + symbol_Arity(Top) != (int)list_Length(term_ArgumentList(Term))) + return FALSE; + + if (symbol_IsVariable(Top) && !list_Empty(term_ArgumentList(Term))) + return FALSE; + + if (Links) { + for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) { + if (term_Superterm(list_Car(Scan)) != Term || + !term_CheckTermIntern(list_Car(Scan), Links)) + return FALSE; + } + } + else { + for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) { + if (term_Superterm(list_Car(Scan)) != term_Null() || + !term_CheckTermIntern(list_Car(Scan), Links)) + return FALSE; + } + } + return TRUE; +} + +BOOL term_CheckTerm(TERM Term) +/******************************************************************************** + INPUT : A term Term. + RETURN: TRUE iff eihter all or no father links are set AND + the length of any argument list matches the arity of the respective symbol +*********************************************************************************/ +{ + if (term_IsComplex(Term) && + term_Superterm(term_FirstArgument(Term)) != term_Null()) + /* check father links as well */ + return term_CheckTermIntern(Term, TRUE); + else + return term_CheckTermIntern(Term, FALSE); +} |