| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * FIRST ORDER LOGIC SYMBOLS * */ |
| /* * * */ |
| /* * $Module: FOL DFG * */ |
| /* * * */ |
| /* * 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$ */ |
| |
| |
| #include "foldfg.h" |
| #include "flags.h" |
| |
| |
| SYMBOL fol_ALL; |
| SYMBOL fol_EXIST; |
| SYMBOL fol_AND; |
| SYMBOL fol_OR; |
| SYMBOL fol_NOT; |
| SYMBOL fol_IMPLIES; |
| SYMBOL fol_IMPLIED; |
| SYMBOL fol_EQUIV; |
| SYMBOL fol_VARLIST; |
| SYMBOL fol_EQUALITY; |
| SYMBOL fol_TRUE; |
| SYMBOL fol_FALSE; |
| |
| LIST fol_SYMBOLS; |
| |
| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * FUNCTIONS * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| void fol_Init(BOOL All, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A boolean value determining whether only 'equality' or |
| all fol symbols are created, and a precedence. |
| RETURNS: Nothing. |
| SUMMARY: Initializes the Fol Module. |
| EFFECTS: If <All> then all fol-symbols are created, |
| only 'equality' otherwise. |
| The precedence of the first order logic symbols is set |
| in <Precedence>. |
| CAUTION: MUST BE CALLED BEFORE ANY OTHER fol-FUNCTION. |
| ***************************************************************/ |
| { |
| if (All) { |
| |
| fol_ALL = symbol_CreateJunctor("forall", 2, symbol_STATLEX, Precedence); |
| fol_EXIST = symbol_CreateJunctor("exists", 2, symbol_STATLEX, Precedence); |
| fol_AND = symbol_CreateJunctor("and", symbol_ArbitraryArity(), |
| symbol_STATLEX, Precedence); |
| fol_OR = symbol_CreateJunctor("or", symbol_ArbitraryArity(), |
| symbol_STATLEX, Precedence); |
| fol_NOT = symbol_CreateJunctor("not", 1, symbol_STATLEX, Precedence); |
| fol_IMPLIES = symbol_CreateJunctor("implies", 2, symbol_STATLEX, Precedence); |
| fol_IMPLIED = symbol_CreateJunctor("implied", 2, symbol_STATLEX, Precedence); |
| fol_EQUIV = symbol_CreateJunctor("equiv", 2, symbol_STATLEX, Precedence); |
| fol_VARLIST = symbol_CreateJunctor("", symbol_ArbitraryArity(), |
| symbol_STATLEX, Precedence); |
| fol_EQUALITY = symbol_CreatePredicate("equal", 2, symbol_STATLEX, Precedence); |
| fol_TRUE = symbol_CreatePredicate("true", 0, symbol_STATLEX, Precedence); |
| fol_FALSE = symbol_CreatePredicate("false", 0, symbol_STATLEX, Precedence); |
| |
| fol_SYMBOLS = |
| list_Cons((POINTER)fol_ALL, list_Cons((POINTER)fol_EXIST, |
| list_Cons((POINTER)fol_AND, list_Cons((POINTER)fol_OR, |
| list_Cons((POINTER)fol_NOT, |
| list_Cons((POINTER)fol_IMPLIES, list_Cons((POINTER)fol_IMPLIED, |
| list_Cons((POINTER)fol_EQUIV, list_Cons((POINTER)fol_VARLIST, |
| list_Cons((POINTER)fol_EQUALITY, list_Cons((POINTER)fol_TRUE, |
| list_List((POINTER)fol_FALSE)))))))))))); |
| } |
| else { |
| fol_EQUALITY = symbol_CreatePredicate("equal", 2, symbol_STATLEX, Precedence); |
| fol_NOT = symbol_CreateJunctor("not", 1, symbol_STATLEX, Precedence); |
| fol_SYMBOLS = list_Cons((POINTER)fol_NOT, list_List((POINTER)fol_EQUALITY)); |
| } |
| } |
| |
| |
| SYMBOL fol_IsStringPredefined(const char* String) |
| /************************************************************** |
| INPUT: A string. |
| RETURNS: The symbol iff String is a predefined fol string, |
| symbol NULL otherwise |
| ***************************************************************/ |
| { |
| LIST Scan; |
| for (Scan=fol_SYMBOLS; !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| if (string_Equal(String, symbol_Name((SYMBOL)list_Car(Scan)))) |
| return (SYMBOL)list_Car(Scan); |
| return symbol_Null(); |
| } |
| |
| |
| TERM fol_CreateQuantifier(SYMBOL Quantifier, LIST VarList, LIST Arguments) |
| /************************************************************** |
| INPUT: A symbol (which MUST be a fol quantifier), |
| a list of variables that will be bound, and |
| a list of arguments. |
| RETURNS: A quantified term. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!fol_IsQuantifier(Quantifier)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_CreateQuantifier: Symbol isn't FOL quantifier.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| return term_Create(Quantifier, list_Cons(term_Create(fol_Varlist(), VarList), |
| Arguments)); |
| } |
| |
| |
| TERM fol_CreateQuantifierAddFather(SYMBOL Quantifier, LIST VarList, LIST Arguments) |
| /************************************************************** |
| INPUT: A symbol (which MUST be a fol quantifier), |
| a list of variables that will be bound, and |
| a list of arguments. |
| In contrast to fol_CreateQuantifier the superterm members |
| are set for the arguments. |
| RETURNS: A quantified term. |
| ***************************************************************/ |
| { |
| return term_CreateAddFather(Quantifier, |
| list_Cons(term_CreateAddFather(fol_Varlist(), |
| VarList), |
| Arguments)); |
| } |
| |
| |
| TERM fol_ComplementaryTerm(TERM Term) |
| /************************************************************** |
| INPUT: A formula. |
| RETURNS: The (copied) complementary (in sign) formula of <Term> |
| ***************************************************************/ |
| { |
| if (symbol_Equal(term_TopSymbol(Term), fol_Not())) |
| return term_Copy((TERM)list_First(term_ArgumentList(Term))); |
| else |
| return term_Create(fol_Not(), list_List(term_Copy(Term))); |
| } |
| |
| |
| LIST fol_GetNonFOLPredicates(void) |
| /************************************************************** |
| INPUT: None. |
| RETURNS: The list of all predicate symbols except the predefined |
| FOL symbols. |
| ***************************************************************/ |
| { |
| LIST Result; |
| |
| Result = symbol_GetAllPredicates(); |
| Result = list_DeleteElementIf(Result, (BOOL (*)(POINTER))fol_IsPredefinedPred); |
| return Result; |
| } |
| |
| |
| LIST fol_GetAssignments(TERM Term) |
| /************************************************************** |
| INPUT: A formula. |
| RETURNS: All assignemnts that occur inside the formula, i.e., |
| equations of the form "x=t" where "x" does not |
| occur in "t". |
| ***************************************************************/ |
| { |
| if (term_IsAtom(Term)) { |
| if (fol_IsAssignment(Term)) |
| return list_List(Term); |
| } |
| else |
| if (term_IsComplex(Term)) { |
| LIST Scan,Result; |
| Result = list_Nil(); |
| for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| Result = list_Nconc(fol_GetAssignments(list_Car(Scan)),Result); |
| return Result; |
| } |
| |
| return list_Nil(); |
| |
| } |
| |
| static void fol_NormalizeVarsIntern(TERM Formula) |
| /************************************************************** |
| INPUT: A sentence. |
| RETURNS: void. |
| EFFECT: The quantifier variables of the formula are |
| normalized, i.e., no two different quantifiers |
| bind the same variable. |
| CAUTION: Desctructive. |
| ***************************************************************/ |
| { |
| SYMBOL Top; |
| LIST Scan1; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Formula)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_NormalizeVarsIntern: Formula is corrupted.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Top = term_TopSymbol(Formula); |
| |
| if (term_IsComplex(Formula)) { |
| if (fol_IsQuantifier(Top)) { |
| SYMBOL Var; |
| LIST OldVars,Scan2; |
| OldVars = list_Nil(); |
| for (Scan1=fol_QuantifierVariables(Formula);!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) { |
| Var = term_TopSymbol(list_Car(Scan1)); |
| OldVars = list_Nconc(OldVars,list_List((POINTER)term_BindingValue(Var))); |
| term_CreateValueBinding(Var, term_OldMark(), (POINTER)symbol_CreateStandardVariable()); |
| } |
| fol_NormalizeVarsIntern(term_SecondArgument(Formula)); |
| for (Scan1=fol_QuantifierVariables(Formula),Scan2=OldVars; |
| !list_Empty(Scan1); |
| Scan1=list_Cdr(Scan1),Scan2=list_Cdr(Scan2)) { |
| Var = term_TopSymbol(list_Car(Scan1)); |
| term_RplacTop(list_Car(Scan1),(SYMBOL)term_BindingValue(Var)); |
| term_CreateValueBinding(Var, term_OldMark(), list_Car(Scan2)); |
| } |
| list_Delete(OldVars); |
| } |
| else |
| for (Scan1=term_ArgumentList(Formula);!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) |
| fol_NormalizeVarsIntern(list_Car(Scan1)); |
| } |
| else |
| if (symbol_IsVariable(Top)) |
| term_RplacTop(Formula,(SYMBOL)term_BindingValue(Top)); |
| |
| return; |
| } |
| |
| |
| void fol_NormalizeVars(TERM Formula) |
| /************************************************************** |
| INPUT: A sentence. |
| RETURNS: void. |
| EFFECT: The quantifier variables of the formula are |
| normalized, i.e., no two different quantifiers |
| bind the same variable. |
| CAUTION: Destructive. |
| ***************************************************************/ |
| { |
| symbol_ResetStandardVarCounter(); |
| term_NewMark(); |
| fol_NormalizeVarsIntern(Formula); |
| } |
| |
| |
| void fol_NormalizeVarsStartingAt(TERM Formula, SYMBOL S) |
| /************************************************************** |
| INPUT: A sentence. |
| RETURNS: void. |
| EFFECT: The quantifier variables of the formula are |
| normalized, i.e., no two different quantifiers |
| bind the same variable. |
| CAUTION: Destructive. |
| ***************************************************************/ |
| { |
| SYMBOL old = symbol_STANDARDVARCOUNTER; |
| symbol_SetStandardVarCounter(S); |
| term_NewMark(); |
| fol_NormalizeVarsIntern(Formula); |
| symbol_SetStandardVarCounter(old); |
| } |
| |
| |
| void fol_RemoveImplied(TERM Formula) |
| /********************************************************* |
| INPUT: A formula. |
| RETURNS: void. |
| EFFECT: All occurrences of "implied" are replaced by "implies" |
| CAUTION: Destructive. |
| *******************************************************/ |
| { |
| if (!fol_IsLiteral(Formula)) { |
| if (fol_IsQuantifier(term_TopSymbol(Formula))) |
| fol_RemoveImplied(term_SecondArgument(Formula)); |
| else { |
| LIST Scan; |
| if (symbol_Equal(term_TopSymbol(Formula),fol_Implied())) { |
| term_RplacTop(Formula,fol_Implies()); |
| term_RplacArgumentList(Formula,list_NReverse(term_ArgumentList(Formula))); |
| } |
| for (Scan=term_ArgumentList(Formula);!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| fol_RemoveImplied(list_Car(Scan)); |
| } |
| } |
| } |
| |
| |
| BOOL fol_VarOccursFreely(TERM Var,TERM Term) |
| /************************************************************** |
| INPUT: A variable and a term. |
| RETURNS: TRUE iff <Var> occurs freely in <Term> |
| ***************************************************************/ |
| { |
| LIST Scan; |
| int Stack; |
| SYMBOL Top; |
| BOOL Hit; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Term) || !term_IsVariable(Var)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_VarOccursFreely: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Stack = stack_Bottom(); |
| |
| do { |
| Top = term_TopSymbol(Term); |
| if (term_IsComplex(Term)) { |
| if (fol_IsQuantifier(Top)) { |
| Hit = TRUE; |
| for (Scan=fol_QuantifierVariables(Term);!list_Empty(Scan)&&Hit;Scan=list_Cdr(Scan)) |
| if (symbol_Equal(term_TopSymbol(list_Car(Scan)),term_TopSymbol(Var))) |
| Hit = FALSE; |
| if (Hit) |
| stack_Push(list_Cdr(term_ArgumentList(Term))); |
| } |
| else |
| stack_Push(term_ArgumentList(Term)); |
| } |
| else { |
| if (symbol_IsVariable(Top) && symbol_Equal(Top,term_TopSymbol(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; |
| } |
| |
| |
| LIST fol_FreeVariables(TERM Term) |
| /************************************************************** |
| INPUT: A term where we assume that no variable is bound by more than |
| one quantifier in <Term> !!!!! |
| RETURNS: The list of variables occurring in the term. Variables are |
| not (!) copied. |
| Note that there may be many terms with same variable symbol. |
| All Variable terms are newly created. |
| ***************************************************************/ |
| { |
| LIST Variables,Scan; |
| int Stack; |
| SYMBOL Top; |
| NAT BoundMark,FreeMark; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Term) || term_InBindingPhase()) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_FreeVariables: Illegal input or context.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_StartBinding(); |
| |
| Variables = list_Nil(); |
| Stack = stack_Bottom(); |
| BoundMark = term_ActMark(); |
| FreeMark = term_ActMark(); |
| |
| do { |
| Top = term_TopSymbol(Term); |
| if (term_IsComplex(Term)) { |
| if (fol_IsQuantifier(Top)) { |
| for (Scan=fol_QuantifierVariables(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| if (!term_VarIsMarked(term_TopSymbol(list_Car(Scan)), FreeMark)) |
| term_CreateBinding(term_TopSymbol(list_Car(Scan)), BoundMark); |
| stack_Push(term_ArgumentList(Term)); /* Mark has to be removed ! */ |
| stack_Push(list_Cdr(term_ArgumentList(Term))); |
| } |
| else |
| if (symbol_Equal(Top,fol_Varlist())) { |
| for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| if (!term_VarIsMarked(term_TopSymbol(list_Car(Scan)), FreeMark)) |
| term_CreateBinding(term_TopSymbol(list_Car(Scan)), 0); /* Mark has to be removed ! */ |
| stack_RplacTop(list_Cdr(stack_Top())); /* Second Argument is Quantifier Arg */ |
| } |
| else |
| stack_Push(term_ArgumentList(Term)); |
| } |
| else { |
| if (symbol_IsVariable(Top) && !term_VarIsMarked(Top, FreeMark) |
| && !term_VarIsMarked(Top, BoundMark)) { |
| Variables = list_Cons(Term, Variables); |
| term_CreateBinding(Top, FreeMark); |
| } |
| } |
| 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; |
| } |
| |
| LIST fol_BoundVariables(TERM Term) |
| /************************************************************** |
| INPUT: A term |
| RETURNS: The list of bound variables occurring in the term. |
| ***************************************************************/ |
| { |
| int stack; |
| LIST result; |
| |
| stack = stack_Bottom(); |
| result = list_Nil(); |
| |
| do { |
| if (fol_IsQuantifier(term_TopSymbol(Term))) { |
| result = list_Nconc(result, list_Copy(fol_QuantifierVariables(Term))); |
| stack_Push(list_Cdr(term_ArgumentList(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)); |
| result = term_DeleteDuplicatesFromList(result); |
| return result; |
| } |
| |
| |
| void fol_Free(void) |
| /************************************************************** |
| INPUT: None. |
| RETURNS: void. |
| EFFECT: The memory used by the fol modul is freed. |
| ***************************************************************/ |
| { |
| list_Delete(fol_SYMBOLS); |
| } |
| |
| |
| BOOL fol_FormulaIsClause(TERM Formula) |
| /************************************************************** |
| INPUT: A formula. |
| RETURNS: TRUE, if <Formula> is a clause, FALSE otherwise. |
| ***************************************************************/ |
| { |
| LIST LitList; |
| |
| if (term_TopSymbol(Formula) == fol_ALL) |
| Formula = term_SecondArgument(Formula); |
| |
| if (term_TopSymbol(Formula) != fol_OR) |
| return FALSE; |
| |
| LitList = term_ArgumentList(Formula); |
| |
| while (!list_Empty(LitList)) { |
| if (!fol_IsLiteral(list_Car(LitList))) |
| return FALSE; |
| LitList = list_Cdr(LitList); |
| } |
| |
| return TRUE; |
| } |
| |
| |
| void fol_FPrintOtterOptions(FILE* File, BOOL Equality, |
| FLAG_TDFG2OTTEROPTIONSTYPE Options) |
| /************************************************************** |
| INPUT: A file, a boolean flag and an Flag determining printed options. |
| RETURNS: Nothing. |
| SUMMARY: Prints Otter Options to <File>. |
| If <Equality> then appropriate paramodulation options |
| are possibly added. |
| ***************************************************************/ |
| { |
| switch (Options) { |
| case flag_TDFG2OTTEROPTIONSPROOFCHECK: |
| fputs("\nset(process_input).", File); |
| fputs("\nset(binary_res).", File); |
| fputs("\nset(factor).", File); |
| /*fputs("\nassign(pick_given_ratio, 4).", File);*/ |
| fputs("\nclear(print_kept).", File); |
| fputs("\nassign(max_seconds, 20).", File); |
| if (Equality) { |
| fputs("\nclear(print_new_demod).", File); |
| fputs("\nclear(print_back_demod).", File); |
| fputs("\nclear(print_back_sub).", File); |
| /*fputs("\nset(knuth_bendix).", File);*/ |
| fputs("\nset(para_from).", File); |
| fputs("\nset(para_into).", File); |
| fputs("\nset(para_from_vars).", File); |
| fputs("\nset(back_demod).", File); |
| } /* No break: add auto */ |
| case flag_TDFG2OTTEROPTIONSAUTO: |
| fputs("\nset(auto).", File); |
| break; |
| case flag_TDFG2OTTEROPTIONSAUTO2: |
| fputs("\nset(auto2).", File); |
| break; |
| case flag_TDFG2OTTEROPTIONSOFF: |
| /* print nothing */ |
| break; |
| default: |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_FPrintOtterOptions: Illegal parameter value %d.", |
| Options); |
| misc_FinishErrorReport(); |
| } |
| |
| fputs("\n\n",File); |
| } |
| |
| static void fol_FPrintOtterFormula(FILE* File, TERM Formula) |
| /************************************************************** |
| INPUT: A file and a formula. |
| RETURNS: Nothing. |
| SUMMARY: Prints the formula in Otter format to <File>. |
| ***************************************************************/ |
| { |
| SYMBOL Top; |
| |
| Top = term_TopSymbol(Formula); |
| |
| if (symbol_IsPredicate(Top)) { |
| if (symbol_Equal(Top, fol_Equality())) { |
| term_FPrintOtterPrefix(File,term_FirstArgument(Formula)); |
| fputs(" = ", File); |
| term_FPrintOtterPrefix(File,term_SecondArgument(Formula)); |
| } |
| else |
| term_FPrintOtterPrefix(File,Formula); |
| } |
| else { |
| if (fol_IsQuantifier(Top)) { |
| LIST Scan; |
| for (Scan=fol_QuantifierVariables(Formula);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| if (symbol_Equal(Top,fol_All())) |
| fputs("all ", File); |
| else |
| fputs("exists ", File); |
| term_FPrintOtterPrefix(File, list_Car(Scan)); |
| fputs(" (", File); |
| } |
| fol_FPrintOtterFormula(File, term_SecondArgument(Formula)); |
| for (Scan=fol_QuantifierVariables(Formula);!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| fputs(")", File); |
| } |
| else |
| if (symbol_Equal(Top,fol_Not())) { |
| fputs("- (", File); |
| fol_FPrintOtterFormula(File, term_FirstArgument(Formula)); |
| fputs(")", File); |
| } |
| else |
| if (symbol_Equal(Top, fol_And()) || symbol_Equal(Top, fol_Or()) || |
| symbol_Equal(Top, fol_Equiv()) || symbol_Equal(Top, fol_Implies()) ) { |
| LIST Scan; |
| fputs("(", File); |
| for (Scan=term_ArgumentList(Formula);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| if (fol_IsLiteral(list_Car(Scan))) |
| fol_FPrintOtterFormula(File, list_Car(Scan)); |
| else { |
| fputs("(", File); |
| fol_FPrintOtterFormula(File, list_Car(Scan)); |
| fputs(")", File); |
| } |
| if (!list_Empty(list_Cdr(Scan))) { |
| if (symbol_Equal(Top, fol_And())) |
| fputs(" & ", File); |
| if (symbol_Equal(Top, fol_Or())) |
| fputs(" | ", File); |
| if (symbol_Equal(Top, fol_Equiv())) |
| fputs(" <-> ", File); |
| if (symbol_Equal(Top, fol_Implies())) |
| fputs(" -> ", File); |
| } |
| } |
| fputs(")", File); |
| } |
| } |
| } |
| |
| void fol_FPrintOtter(FILE* File, LIST Formulae, FLAG_TDFG2OTTEROPTIONSTYPE Option) |
| /************************************************************** |
| INPUT: A file, a list of pairs (label.formula) and an option flag. |
| RETURNS: Nothing. |
| SUMMARY: Prints a the respective formulae in Otter format to <File>. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| BOOL Equality; |
| TERM Formula; |
| |
| Equality = FALSE; |
| |
| for (Scan=Formulae;!list_Empty(Scan) && !Equality; Scan=list_Cdr(Scan)) { |
| Formula = (TERM)list_PairSecond(list_Car(Scan)); |
| Equality = term_ContainsSymbol(Formula, fol_Equality()); |
| } |
| |
| fol_FPrintOtterOptions(File, Equality, Option); |
| |
| if (!list_Empty(Formulae)) { |
| fputs("formula_list(usable).\n", File); |
| if (Equality) |
| fputs("all x (x=x).\n", File); |
| for (Scan=Formulae;!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| if (list_PairFirst(list_Car(Scan)) != NULL) |
| fprintf(File,"\n%% %s \n",(char *)list_PairFirst(list_Car(Scan))); |
| fol_FPrintOtterFormula(File,list_PairSecond(list_Car(Scan))); |
| fputs(".\n\n", File); |
| } |
| fputs("end_of_list.\n\n", File); |
| } |
| } |
| |
| |
| void fol_FPrintDFGSignature(FILE* File) |
| /************************************************************** |
| INPUT: A file stream. |
| RETURNS: Nothing. |
| SUMMARY: Prints all signature symbols in DFG format to the |
| file stream. |
| ***************************************************************/ |
| |
| { |
| NAT i; |
| SYMBOL symbol; |
| LIST functions, predicates; |
| |
| functions = symbol_GetAllFunctions(); |
| predicates = fol_GetNonFOLPredicates(); |
| |
| /* First print the function symbols */ |
| if (!list_Empty(functions)) { |
| fputs(" functions[", File); |
| i = 0; |
| do { |
| symbol = (SYMBOL) list_Top(functions); |
| fprintf(File, "(%s, %d)", symbol_Name(symbol), symbol_Arity(symbol)); |
| functions = list_Pop(functions); |
| if (!list_Empty(functions)) |
| fputs(", ", File); |
| if (i < 15) |
| i++; |
| else { |
| i = 0; |
| fputs("\n\t", File); |
| } |
| |
| } while (!list_Empty(functions)); |
| fputs("].\n", File); |
| } |
| |
| /* Now print the predicate symbols */ |
| if (!list_Empty(predicates)) { |
| i = 0; |
| fputs(" predicates[", File); |
| do { |
| symbol = (SYMBOL) list_Top(predicates); |
| fprintf(File, "(%s, %d)", symbol_Name(symbol), symbol_Arity(symbol)); |
| predicates = list_Pop(predicates); |
| if (!list_Empty(predicates)) |
| fputs(", ", File); |
| if (i < 15) |
| i++; |
| else { |
| i = 0; |
| fputs("\n\t", File); |
| } |
| } while (!list_Empty(predicates)); |
| fputs("].\n", File); |
| } |
| list_Delete(predicates); |
| list_Delete(functions); |
| } |
| |
| |
| static void fol_TermListFPrintDFG(FILE* File, LIST List) |
| /************************************************************** |
| INPUT: A list of terms. |
| RETURNS: Nothing. |
| ***************************************************************/ |
| { |
| for (; !list_Empty(List); List=list_Cdr(List)) { |
| fol_FPrintDFG(File,list_Car(List)); |
| if (!list_Empty(list_Cdr(List))) |
| putc(',', File); |
| } |
| } |
| |
| |
| void fol_FPrintDFG(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 fol_Output functions. |
| ***************************************************************/ |
| { |
| if (term_IsComplex(Term)) { |
| if (fol_IsQuantifier(term_TopSymbol(Term))) { |
| symbol_FPrint(File,term_TopSymbol(Term)); |
| fputs("([", File); |
| fol_TermListFPrintDFG(File,fol_QuantifierVariables(Term)); |
| fputs("],", File); |
| fol_FPrintDFG(File, term_SecondArgument(Term)); |
| putc(')', File); |
| } |
| else { |
| symbol_FPrint(File,term_TopSymbol(Term)); |
| putc('(', File); |
| fol_TermListFPrintDFG(File,term_ArgumentList(Term)); |
| putc(')', File); |
| } |
| } |
| else |
| symbol_FPrint(File,term_TopSymbol(Term)); |
| } |
| |
| void fol_PrintDFG(TERM Term) |
| { |
| fol_FPrintDFG(stdout,Term); |
| } |
| |
| |
| void fol_PrintPrecedence(PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A precedence. |
| RETURNS: void |
| EFFECT: Prints the current precedence to stdout, |
| fol symbols are excluded. |
| ***************************************************************/ |
| { |
| if (symbol_SignatureExists()) { |
| LIST Symbols, Scan; |
| SYMBOL Symbol; |
| int Index; |
| SIGNATURE S; |
| |
| Symbols = list_Nil(); |
| for (Index = 1; Index < symbol_ACTINDEX; Index++) { |
| S = symbol_Signature(Index); |
| if (S != NULL) { |
| Symbol = S->info; |
| if ((symbol_IsPredicate(Symbol) || symbol_IsFunction(Symbol)) && |
| !fol_IsPredefinedPred(Symbol)) |
| Symbols = list_Cons((POINTER)Symbol, Symbols); |
| } |
| } |
| Symbols = symbol_SortByPrecedence(Symbols, Precedence); |
| for (Scan = Symbols; !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| S = symbol_Signature(symbol_Index((SYMBOL)list_Car(Scan))); |
| fputs(S->name, stdout); |
| if (!list_Empty(list_Cdr(Scan))) |
| fputs(" > ", stdout); |
| } |
| list_Delete(Symbols); |
| } |
| } |
| |
| void fol_FPrintPrecedence(FILE *File, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A file to print to, and a precedence. |
| RETURNS: Nothing. |
| EFFECT: Prints the current precedence as a setting |
| command in DFG syntax to <File>. |
| fol symbols are excluded. |
| ***************************************************************/ |
| { |
| if (symbol_SignatureExists()) { |
| LIST Symbols, Scan; |
| SYMBOL Symbol; |
| int Index; |
| SIGNATURE S; |
| |
| Symbols = list_Nil(); |
| for (Index = 1; Index < symbol_ACTINDEX; Index++) { |
| S = symbol_Signature(Index); |
| if (S != NULL) { |
| Symbol = S->info; |
| if ((symbol_IsPredicate(Symbol) || symbol_IsFunction(Symbol)) && |
| !fol_IsPredefinedPred(Symbol)) |
| Symbols = list_Cons((POINTER)Symbol, Symbols); |
| } |
| } |
| Symbols = symbol_SortByPrecedence(Symbols, Precedence); |
| Index = 0; |
| fputs("set_precedence(", File); |
| for (Scan = Symbols; !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| S = symbol_Signature(symbol_Index((SYMBOL)list_Car(Scan))); |
| putc('(', File); |
| fputs(S->name, File); |
| putc(',', File); |
| fprintf(File, "%d", S->weight); |
| putc(',', File); |
| putc((symbol_HasProperty((SYMBOL)list_Car(Scan),ORDRIGHT) ? 'r' : |
| (symbol_HasProperty((SYMBOL)list_Car(Scan),ORDMUL) ? 'm' : 'l')), |
| File); |
| putc(')', File); |
| if (!list_Empty(list_Cdr(Scan))) |
| putc(',', File); |
| |
| if (Index > 15) { |
| Index = 0; |
| fputs("\n\t", File); |
| } |
| else |
| Index++; |
| } |
| fputs(").", File); |
| list_Delete(Symbols); |
| } |
| } |
| |
| |
| static void fol_FPrintFormulaList(FILE* File, LIST Formulas, const char* Name) |
| /************************************************************** |
| INPUT: A file, a list of formulas, a name. |
| EFFECTS: Print a list formulas in DFG format, with given list name. |
| **************************************************************/ |
| { |
| LIST scan; |
| |
| fputs("list_of_formulae(", File); |
| fputs(Name, File); |
| fputs(").\n", File); |
| for (scan = Formulas; !list_Empty(scan); scan= list_Cdr(scan)) { |
| fputs("\tformula(", File); |
| fol_FPrintDFG(File, list_Car(scan)); |
| fputs(").\n", File); |
| } |
| fputs("end_of_list.\n\n", File); |
| } |
| |
| |
| void fol_FPrintDFGProblem(FILE* File, const char* Name, const char* Author, |
| const char* Status, const char* Description, |
| LIST Axioms, LIST Conjectures) |
| /************************************************************** |
| INPUT: A file, two lists of formulas, ??? EK |
| EFFECTS: Prints a complete DFG file containing these lists. |
| **************************************************************/ |
| { |
| fputs("begin_problem(Unknown).\n\n", File); |
| |
| fputs("list_of_descriptions.\n", File); |
| fprintf(File,"name(%s).\n",Name); |
| fprintf(File,"author(%s).\n",Author); |
| fprintf(File,"status(%s).\n",Status); |
| fprintf(File,"description(%s).\n",Description); |
| fputs("end_of_list.\n\n", File); |
| |
| fputs("list_of_symbols.\n", File); |
| fol_FPrintDFGSignature(File); |
| fputs("end_of_list.\n\n", File); |
| |
| fol_FPrintFormulaList(File, Axioms, "axioms"); |
| fol_FPrintFormulaList(File, Conjectures, "conjectures"); |
| |
| fputs("end_problem.\n", File); |
| } |
| |
| |
| BOOL fol_AssocEquation(TERM Term, SYMBOL *Result) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: TRUE if the term is an equation defining associativity |
| for some function symbol. |
| EFFECT: If the <Term> is an assoc equation, then <*Result> is |
| assigned the assoc symbol. |
| ***************************************************************/ |
| { |
| |
| if (fol_IsEquality(Term)) { |
| SYMBOL Top; |
| TERM Left,Right; |
| Left = term_FirstArgument(Term); |
| Right= term_SecondArgument(Term); |
| Top = term_TopSymbol(Left); |
| if (symbol_IsFunction(Top) && symbol_Arity(Top) == 2 && |
| symbol_Equal(Top,term_TopSymbol(Right))) { |
| SYMBOL v1,v2,v3; |
| if (term_IsVariable(term_FirstArgument(Left))) |
| v1 = term_TopSymbol(term_FirstArgument(Left)); |
| else |
| if (term_IsVariable(term_FirstArgument(Right))) { |
| Term = Right; |
| Right = Left; |
| Left = Term; |
| v1 = term_TopSymbol(term_FirstArgument(Left)); |
| } |
| else |
| return FALSE; |
| if (symbol_Equal(term_TopSymbol(term_SecondArgument(Left)),Top) && |
| symbol_IsVariable((v2=term_TopSymbol(term_FirstArgument(term_SecondArgument(Left)))))&& |
| symbol_IsVariable((v3=term_TopSymbol(term_SecondArgument(term_SecondArgument(Left)))))&& |
| symbol_Equal(term_TopSymbol(term_FirstArgument(Right)),Top) && |
| symbol_Equal(v1,term_TopSymbol(term_FirstArgument(term_FirstArgument(Right)))) && |
| symbol_Equal(v2,term_TopSymbol(term_SecondArgument(term_FirstArgument(Right)))) && |
| symbol_Equal(v3,term_TopSymbol(term_SecondArgument(Right)))) { |
| *Result = Top; |
| return TRUE; |
| } |
| } |
| } |
| |
| return FALSE; |
| } |
| |
| |
| BOOL fol_DistributiveEquation(TERM Term, SYMBOL* Addition, |
| SYMBOL* Multiplication) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: TRUE if the term is an equation defining distributivity |
| for two function symbols, FALSE otherwise. |
| EFFECT: If the function returns TRUE, < Addition> and |
| <Multiplication> return the respective symbols. |
| ***************************************************************/ |
| { |
| TERM left, right, help, v1, v2, v3; |
| |
| if (!fol_IsEquality(Term)) |
| return FALSE; |
| |
| left = term_FirstArgument(Term); |
| right = term_SecondArgument(Term); |
| |
| if (term_EqualTopSymbols(left, right) || |
| !symbol_IsFunction(term_TopSymbol(left)) || |
| !symbol_IsFunction(term_TopSymbol(right)) || |
| symbol_Arity(term_TopSymbol(left)) != 2 || |
| symbol_Arity(term_TopSymbol(right)) != 2) |
| return FALSE; |
| |
| if (term_IsVariable(term_FirstArgument(left))) |
| v1 = term_FirstArgument(left); |
| else if (term_IsVariable(term_FirstArgument(right))) { |
| help = right; /* Exchange left and right terms */ |
| right = left; |
| left = help; |
| v1 = term_FirstArgument(left); |
| } else |
| return FALSE; |
| |
| if (!term_EqualTopSymbols(left, term_FirstArgument(right)) || |
| !term_EqualTopSymbols(left, term_SecondArgument(right)) || |
| !term_EqualTopSymbols(term_SecondArgument(left), right)) |
| return FALSE; |
| |
| v2 = term_FirstArgument(term_SecondArgument(left)); |
| v3 = term_SecondArgument(term_SecondArgument(left)); |
| |
| if (term_IsVariable(v2) && term_IsVariable(v3) && |
| term_EqualTopSymbols(term_FirstArgument(term_FirstArgument(right)), v1) && |
| term_EqualTopSymbols(term_SecondArgument(term_FirstArgument(right)), v2) && |
| term_EqualTopSymbols(term_FirstArgument(term_SecondArgument(right)), v1) && |
| term_EqualTopSymbols(term_SecondArgument(term_SecondArgument(right)), v3)) { |
| *Addition = term_TopSymbol(right); |
| *Multiplication = term_TopSymbol(left); |
| return TRUE; |
| } |
| |
| return FALSE; |
| } |
| |
| |
| static LIST fol_InstancesIntern(TERM Formula, TERM ToMatch, NAT Symbols) |
| /************************************************************** |
| INPUT: A formula in which all instances of <ToMatch> are searched. |
| The number of symbols of <ToMatch>. |
| RETURNS: The list of found instances. |
| CAUTION: Bound variables must be different, for otherwise the |
| used matching produces wrong results!! |
| ***************************************************************/ |
| { |
| NAT HitSymbols; |
| LIST Result; |
| int Stack; |
| |
| Stack = stack_Bottom(); |
| Result = list_Nil(); |
| |
| do { |
| HitSymbols = term_Size(Formula); /* First check number of symbols of current formula */ |
| |
| if (HitSymbols >= Symbols && (Formula != ToMatch)) { |
| cont_StartBinding(); |
| if (unify_MatchFlexible(cont_LeftContext(), ToMatch, Formula)) |
| Result = list_Cons(Formula, Result); |
| else |
| if (!symbol_IsPredicate(term_TopSymbol(Formula))) { |
| if (fol_IsQuantifier(term_TopSymbol(Formula))) |
| stack_Push(list_Cdr(term_ArgumentList(Formula))); |
| else |
| stack_Push(term_ArgumentList(Formula)); |
| } |
| cont_BackTrack(); |
| } |
| |
| while (!stack_Empty(Stack) && list_Empty(stack_Top())) |
| stack_Pop(); |
| if (!stack_Empty(Stack)) { |
| Formula = (TERM)list_Car(stack_Top()); |
| stack_RplacTop(list_Cdr(stack_Top())); |
| } |
| } while (!stack_Empty(Stack)); |
| |
| return Result; |
| } |
| |
| |
| LIST fol_Instances(TERM Formula, TERM ToMatch) |
| /************************************************************** |
| INPUT: A formula in which all instances of <ToMatch> are searched. |
| RETURNS: The list of found occurrences matched by <ToMatch>. |
| The formula <ToMatch> is not included! |
| ***************************************************************/ |
| { |
| NAT Symbols; |
| |
| Symbols = term_ComputeSize(ToMatch); /* We use the number of symbols as a filter */ |
| term_InstallSize(Formula); |
| |
| return fol_InstancesIntern(Formula, ToMatch, Symbols); |
| } |
| |
| |
| static LIST fol_GeneralizationsIntern(TERM Formula, TERM MatchedBy, NAT Symbols) |
| /************************************************************** |
| INPUT: A formula in which all instances of <ToMatch> are searched. |
| The number of symbols of <ToMatch>. |
| RETURNS: The list of found instances. |
| CAUTION: Bound variables must be different, for otherwise the |
| used matching produces wrong results!! |
| ***************************************************************/ |
| { |
| NAT HitSymbols; |
| LIST Result; |
| int Stack; |
| |
| Stack = stack_Bottom(); |
| Result = list_Nil(); |
| |
| do { |
| if (Formula != MatchedBy) { |
| HitSymbols = term_Size(Formula); /* First check number of symbols of current formula */ |
| if (HitSymbols <= Symbols) { |
| cont_StartBinding(); |
| if (unify_MatchFlexible(cont_LeftContext(), Formula, MatchedBy)) |
| Result = list_Cons(Formula, Result); |
| else |
| if (!symbol_IsPredicate(term_TopSymbol(Formula))) { |
| if (fol_IsQuantifier(term_TopSymbol(Formula))) |
| stack_Push(list_Cdr(term_ArgumentList(Formula))); |
| else |
| stack_Push(term_ArgumentList(Formula)); |
| } |
| cont_BackTrack(); |
| } |
| else |
| if (!symbol_IsPredicate(term_TopSymbol(Formula))) { |
| if (fol_IsQuantifier(term_TopSymbol(Formula))) |
| stack_Push(list_Cdr(term_ArgumentList(Formula))); |
| else |
| stack_Push(term_ArgumentList(Formula)); |
| } |
| } |
| |
| while (!stack_Empty(Stack) && list_Empty(stack_Top())) |
| stack_Pop(); |
| if (!stack_Empty(Stack)) { |
| Formula = (TERM)list_Car(stack_Top()); |
| stack_RplacTop(list_Cdr(stack_Top())); |
| } |
| } while (!stack_Empty(Stack)); |
| |
| return Result; |
| } |
| |
| |
| LIST fol_Generalizations(TERM Formula, TERM MatchedBy) |
| /************************************************************** |
| INPUT: A formula in which all first-order generalizations of <MatchedBy> are searched. |
| RETURNS: The list of found occurrences that are more general than <MatchedBy>. |
| The formula <MatchedBy> is not included! |
| ***************************************************************/ |
| { |
| NAT Symbols; |
| |
| Symbols = term_ComputeSize(MatchedBy); /* We use the number of symbols as a filter */ |
| term_InstallSize(Formula); |
| |
| return fol_GeneralizationsIntern(Formula, MatchedBy, Symbols); |
| } |
| |
| |
| TERM fol_MostGeneralFormula(LIST Formulas) |
| /************************************************************** |
| INPUT: A list of formulas. |
| RETURNS: A most general formula out of the list, i.e., if |
| some formula is returned, there is no formula in the |
| list that is more general than that formula. |
| ***************************************************************/ |
| { |
| TERM Result, Candidate; |
| LIST Scan; |
| |
| #ifdef CHECK |
| if (list_Empty(Formulas)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_MostGeneralFormula: Called with empty list.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Car(Formulas); |
| |
| for (Scan=list_Cdr(Formulas);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| Candidate = (TERM)list_Car(Scan); |
| cont_StartBinding(); |
| if (unify_MatchFlexible(cont_LeftContext(), Candidate, Result)) |
| Result = Candidate; |
| cont_BackTrack(); |
| } |
| |
| return Result; |
| } |
| |
| |
| void fol_ReplaceVariable(TERM Term, SYMBOL Symbol, TERM Repl) |
| /************************************************************** |
| INPUT: A term, a variable symbol and a replacement term. |
| RETURNS: void |
| EFFECT: All free 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 fol_ReplaceVariable: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (fol_IsQuantifier(term_TopSymbol(Term))) { |
| for (Scan=term_ArgumentList(term_FirstArgument(Term)); !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| if (symbol_Equal(term_TopSymbol(list_Car(Scan)), Symbol)) /* var is bound */ |
| return; |
| fol_ReplaceVariable(term_SecondArgument(Term), Symbol, Repl); |
| } |
| |
| 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)) |
| fol_ReplaceVariable(list_Car(Scan),Symbol,Repl); |
| } |
| |
| |
| static void fol_PrettyPrintInternDFG(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; |
| SYMBOL Top; |
| |
| Top = term_TopSymbol(Term); |
| if (!symbol_Equal(Top,fol_Varlist())) { |
| for (i = 0; i < Depth; i++) |
| fputs(" ", stdout); |
| if (fol_IsLiteral(Term)) |
| term_PrintPrefix(Term); |
| else { |
| if (symbol_IsJunctor(Top)) { |
| if (term_IsComplex(Term)) { |
| symbol_Print(Top); |
| putchar('('); |
| if (!fol_IsQuantifier(Top)) |
| putchar('\n'); |
| for (scan=term_ArgumentList(Term); !list_Empty(scan); scan= list_Cdr(scan)) { |
| fol_PrettyPrintInternDFG((TERM) list_Car(scan), Depth+1); |
| if (!list_Empty(list_Cdr(scan))) |
| fputs(",\n", stdout); |
| } |
| putchar(')'); |
| } |
| else { |
| if (term_IsVariable(Term)) { |
| symbol_Print(Top); |
| } |
| else { |
| putchar('('); |
| symbol_Print(Top); |
| putchar(')'); |
| } |
| } |
| } |
| else { |
| term_PrintPrefix(Term); |
| } |
| } |
| } |
| else { |
| putchar('['); |
| term_TermListPrintPrefix(term_ArgumentList(Term)); |
| putchar(']'); |
| } |
| } |
| |
| |
| void fol_PrettyPrintDFG(TERM Term) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: none. |
| SUMMARY: Prints the term hopefully more pretty to stdout. |
| ***************************************************************/ |
| { |
| fol_PrettyPrintInternDFG(Term, 0); |
| } |
| |
| |
| TERM fol_CheckFatherLinksIntern(TERM Term) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: A subterm whose superterm pointer is not set correctly, |
| else NULL. |
| SUMMARY: Checks if all superterm links except of those from quantifier |
| variables are set correctly. |
| ***************************************************************/ |
| { |
| LIST l; |
| if (fol_IsQuantifier(term_TopSymbol(Term))) |
| return fol_CheckFatherLinksIntern(term_SecondArgument(Term)); |
| if (term_IsComplex(Term)) { |
| for (l=term_ArgumentList(Term); !list_Empty(l); l=list_Cdr(l)) { |
| TERM result; |
| if (term_Superterm((TERM) list_Car(l)) != Term) |
| return (TERM) list_Car(l); |
| result = fol_CheckFatherLinksIntern((TERM) list_Car(l)); |
| if (result != NULL) |
| return result; |
| } |
| } |
| return NULL; |
| } |
| |
| |
| void fol_CheckFatherLinks(TERM Term) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: none. |
| SUMMARY: Checks if all superterm links except of those from |
| quantifier variables are set correctly. |
| ***************************************************************/ |
| { |
| TERM Result; |
| |
| Result = fol_CheckFatherLinksIntern(Term); |
| #ifdef CHECK |
| if (Result != NULL || term_Superterm(Term) != NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_CheckFatherLinks:"); |
| misc_ErrorReport(" Found a term where the father links"); |
| misc_ErrorReport(" are not correctly set."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| } |
| |
| |
| static void fol_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)) { |
| if (fol_IsQuantifier(term_TopSymbol(Term))) { |
| symbol_Print(term_TopSymbol(Term)); |
| fputs("([", stdout); |
| for (scan=fol_QuantifierVariables(Term); !list_Empty(scan); scan=list_Cdr(scan)) { |
| symbol_Print(term_TopSymbol((TERM) list_Car(scan))); |
| if (!list_Empty(list_Cdr(scan))) |
| putchar(','); |
| } |
| fputs("],\n", stdout); |
| fol_PrettyPrintIntern(term_SecondArgument(Term), Depth+1); |
| } |
| else { |
| symbol_Print(term_TopSymbol(Term)); |
| fputs("(\n", stdout); |
| for (scan=term_ArgumentList(Term); !list_Empty(scan); scan= list_Cdr(scan)) { |
| fol_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 fol_PrettyPrint(TERM Term) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: none. |
| SUMMARY: Prints the term hopefully more pretty to stdout. |
| ***************************************************************/ |
| { |
| fol_PrettyPrintIntern(Term, 0); |
| } |
| |
| |
| LIST fol_GetSubstEquations(TERM Term) |
| /************************************************************** |
| INPUT: A Term. |
| RETURNS: The list of all equations of the form x=t or t=x in <Term> |
| where x is a variable and t is a term not containing x. |
| ***************************************************************/ |
| { |
| LIST Result; |
| LIST Scan; |
| |
| Result = list_Nil(); |
| |
| if (fol_IsQuantifier(term_TopSymbol(Term))) |
| return fol_GetSubstEquations(term_SecondArgument(Term)); |
| if (fol_IsEquality(Term)) { |
| if (term_IsVariable(term_SecondArgument(Term))) { |
| if (!term_ContainsSymbol(term_FirstArgument(Term), term_TopSymbol(term_SecondArgument(Term)))) |
| Result = list_Cons(Term, Result); |
| } |
| else { |
| if (term_IsVariable(term_FirstArgument(Term))) |
| if (!term_ContainsSymbol(term_SecondArgument(Term), term_TopSymbol(term_FirstArgument(Term)))) |
| Result = list_Cons(Term, Result); |
| } |
| } |
| if (symbol_IsPredicate(term_TopSymbol(Term))) |
| return Result; |
| else |
| for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| Result = list_Nconc(Result, fol_GetSubstEquations(list_Car(Scan))); |
| |
| return Result; |
| } |
| |
| |
| TERM fol_GetBindingQuantifier(TERM Term, SYMBOL Symbol) |
| /************************************************************** |
| INPUT: A symbol and a term containing the symbol. |
| RETURNS: The Quantifier binding the symbol. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Term) || !symbol_IsSymbol(Symbol)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_GetBindingQuantifier: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (fol_IsQuantifier(term_TopSymbol(Term))) { |
| for ( Scan = fol_QuantifierVariables(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| if (symbol_Equal(Symbol, term_TopSymbol(list_Car(Scan)))) { |
| return Term; |
| } |
| } |
| |
| return fol_GetBindingQuantifier(term_Superterm(Term), Symbol); |
| } |
| |
| |
| int fol_TermPolarity(TERM SubTerm, TERM Term) |
| /************************************************************** |
| INPUT: Two terms, SubTerm subterm of Term. |
| It is assumed that the superterm links in <Term> |
| are established. |
| RETURNS: The polarity of SubTerm in Term. |
| ***************************************************************/ |
| { |
| TERM SuperTerm; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(SubTerm) || !term_IsTerm(Term) || !term_FatherLinksEstablished(Term)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_TermPolarity: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (SubTerm == Term) |
| return 1; |
| |
| SuperTerm = term_Superterm(SubTerm); |
| |
| if (SuperTerm) { |
| SYMBOL Top; |
| Top = term_TopSymbol(SuperTerm); |
| |
| if (symbol_Equal(Top,fol_AND) || symbol_Equal(Top,fol_OR) || fol_IsQuantifier(Top)) |
| return fol_TermPolarity(SuperTerm, Term); |
| |
| if (symbol_Equal(Top,fol_NOT)) |
| return (-fol_TermPolarity(SuperTerm, Term)); |
| |
| if (symbol_Equal(Top,fol_EQUIV)) |
| return 0; |
| |
| if (symbol_Equal(Top, fol_IMPLIES)) { |
| if (SubTerm == term_FirstArgument(SuperTerm)) |
| return (-fol_TermPolarity(SuperTerm, Term)); |
| else |
| return fol_TermPolarity(SuperTerm, Term); |
| } |
| if (symbol_Equal(Top, fol_IMPLIED)) { |
| if (SubTerm == term_SecondArgument(SuperTerm)) |
| return (-fol_TermPolarity(SuperTerm, Term)); |
| else |
| return fol_TermPolarity(SuperTerm, Term); |
| } |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_TermPolarity: Unknown first-order operator.\n"); |
| misc_FinishErrorReport(); |
| } |
| |
| return 1; |
| } |
| |
| |
| static int fol_PolarCheckCount(TERM Nowterm, TERM SuperTerm, int Nowpolar) |
| /************************************************************** |
| INPUT: Two terms, Nowterm and its superterm, and the polarity of |
| Nowterm. |
| RETURNS: The polarity of SuperTerm according to Nowterm. |
| COMMENT: Helpfunction for fol_PolarCheck. |
| ***************************************************************/ |
| { |
| SYMBOL Top; |
| Top = term_TopSymbol(SuperTerm); |
| |
| if (Nowterm == SuperTerm) |
| return Nowpolar; |
| |
| if (symbol_Equal(Top, fol_OR) || symbol_Equal(Top, fol_AND) || fol_IsQuantifier(Top) || |
| (symbol_Equal(Top, fol_IMPLIES) && Nowterm == term_SecondArgument(SuperTerm)) || |
| (symbol_Equal(Top, fol_IMPLIED) && Nowterm == term_FirstArgument(SuperTerm))) |
| return Nowpolar; |
| |
| if (symbol_Equal(term_TopSymbol(SuperTerm), fol_EQUIV)) |
| return 0; |
| |
| return -Nowpolar; |
| } |
| |
| |
| static BOOL fol_PolarCheckAllquantor(TERM Subterm, TERM Term, int SubtermPolar) |
| /************************************************************** |
| INPUT: Two terms, Subterm subterm of Term, and polarity of Subterm. |
| RETURNS: TRUE iff Subterm occurs in Term disjunctively. |
| COMMENT: Help function for fol_PolarCheck. Dual case to Exist quantor. |
| ***************************************************************/ |
| { |
| TERM SuperTerm; |
| SYMBOL Top; |
| int SubPolar; |
| |
| if (Subterm == Term) |
| return TRUE; |
| |
| SuperTerm = term_Superterm(Subterm); |
| |
| if (SuperTerm == Term) /* Ugly, but it does not make sense to introduce a further function */ |
| return TRUE; |
| |
| Top = term_TopSymbol(SuperTerm); |
| SubPolar = fol_PolarCheckCount(Subterm, SuperTerm, SubtermPolar); |
| |
| /* To be clarified: can the below condition generalized to universal quantifiers? */ |
| |
| if (symbol_Equal(Top,fol_NOT) || |
| (symbol_Equal(Top, fol_OR) && SubPolar == 1) || |
| (symbol_Equal(Top, fol_AND) && SubPolar == -1) || |
| (symbol_Equal(Top,fol_IMPLIES) && SubPolar == 1) || |
| (symbol_Equal(Top,fol_IMPLIED) && SubPolar == 1)) |
| return fol_PolarCheckAllquantor(SuperTerm, Term, SubPolar); |
| |
| return FALSE; |
| } |
| |
| |
| static BOOL fol_PolarCheckExquantor(TERM Subterm, TERM Term, int SubtermPolar) |
| /************************************************************** |
| INPUT: Two terms, Subterm subterm of Term, and polarity of Subterm. |
| RETURNS: TRUE iff Subterm occurs in Term conjunctively. |
| COMMENT: Help function for fol_PolarCheck. Dual case to Allquantor. |
| ***************************************************************/ |
| { |
| TERM SuperTerm; |
| SYMBOL Top; |
| int SubPolar; |
| |
| if (Subterm == Term) |
| return TRUE; |
| |
| SuperTerm = term_Superterm(Subterm); |
| |
| if (SuperTerm == Term) /* Ugly, but it does not make sense to introduce a further function */ |
| return TRUE; |
| |
| Top = term_TopSymbol(SuperTerm); |
| SubPolar = fol_PolarCheckCount(Subterm, SuperTerm, SubtermPolar); |
| |
| /* To be clarified: can the below condition generalized to existential quantifiers? */ |
| |
| if (symbol_Equal(Top,fol_NOT) || |
| (symbol_Equal(Top, fol_OR) && SubPolar == -1) || |
| (symbol_Equal(Top, fol_AND) && SubPolar == 1) || |
| (symbol_Equal(Top,fol_IMPLIES) && SubPolar == -1) || |
| (symbol_Equal(Top,fol_IMPLIED) && SubPolar == -1)) |
| return fol_PolarCheckExquantor(SuperTerm, Term, SubPolar); |
| |
| return FALSE; |
| } |
| |
| BOOL fol_PolarCheck(TERM Subterm, TERM Term) |
| /************************************************************** |
| INPUT: Two terms, <Subterm> is of the form x=t, where x or t variable. |
| <Subterm> is a subterm of <Term> and the top symbol of |
| <Term> must be the binding quantifier of x or t. |
| RETURNS: BOOL if check is ok. |
| ***************************************************************/ |
| { |
| int SubtermPolar; |
| SYMBOL Top; |
| |
| SubtermPolar = fol_TermPolarity(Subterm, Term); |
| Top = term_TopSymbol(Term); |
| |
| if (SubtermPolar == -1 && symbol_Equal(Top, fol_ALL)) |
| return fol_PolarCheckAllquantor(Subterm, Term, SubtermPolar); |
| |
| if (SubtermPolar == 1 && symbol_Equal(Top, fol_EXIST)) |
| return fol_PolarCheckExquantor(Subterm, Term, SubtermPolar); |
| |
| return FALSE; |
| } |
| |
| |
| void fol_PopQuantifier(TERM Term) |
| /************************************************************** |
| INPUT: A term whose top symbol is a quantifier. |
| RETURNS: Nothing. |
| EFFECT: Removes the quantifier. |
| If supertermlinks were set, they are updated. |
| ***************************************************************/ |
| { |
| TERM SubTerm; |
| LIST Scan; |
| |
| #ifdef CHECK |
| if (!fol_IsQuantifier(term_TopSymbol(Term))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_PopQuantifier: Top symbol of term isn't a quantifier.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_Delete(term_FirstArgument(Term)); |
| SubTerm = term_SecondArgument(Term); |
| list_Delete(term_ArgumentList(Term)); |
| term_RplacTop(Term,term_TopSymbol(SubTerm)); |
| term_RplacArgumentList(Term,term_ArgumentList(SubTerm)); |
| for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| if (term_Superterm(list_Car(Scan))) |
| term_RplacSuperterm(list_Car(Scan),Term); |
| term_Free(SubTerm); |
| } |
| |
| |
| void fol_DeleteQuantifierVariable(TERM Quant,SYMBOL Var) |
| /**************************************************************** |
| INPUT: A term starting with a quantifier and a variable symbol. |
| RETURNS: Nothing. |
| EFFECT: The variable is deleted from the list of variables |
| bound by the quantor of <Quant> |
| *****************************************************************/ |
| { |
| LIST Scan; |
| |
| for (Scan=fol_QuantifierVariables(Quant);!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| if (symbol_Equal(term_TopSymbol(list_Car(Scan)), Var)) { |
| term_Delete((TERM)list_Car(Scan)); |
| list_Rplaca(Scan, (POINTER)NULL); |
| } |
| term_RplacArgumentList(term_FirstArgument(Quant), |
| list_PointerDeleteElement(fol_QuantifierVariables(Quant),(POINTER)NULL)); |
| if (list_Empty(fol_QuantifierVariables(Quant))) |
| fol_PopQuantifier(Quant); |
| } |
| |
| |
| |
| void fol_SetTrue(TERM Term) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: Nothing. |
| EFFECT: Replaces Term destructively by fol_True(). |
| ***************************************************************/ |
| { |
| term_DeleteTermList(term_ArgumentList(Term)); |
| term_RplacArgumentList(Term, list_Nil()); |
| term_RplacTop(Term, fol_True()); |
| } |
| |
| void fol_SetFalse(TERM Term) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: Nothing. |
| EFFECT: Replaces Term destructively by fol_False(). |
| ***************************************************************/ |
| { |
| term_DeleteTermList(term_ArgumentList(Term)); |
| term_RplacArgumentList(Term, list_Nil()); |
| term_RplacTop(Term, fol_False()); |
| } |
| |
| |
| static void fol_ReplaceByArgCon(TERM Term) |
| /************************************************************** |
| INPUT: A term of the form f(...)=f(...), where f is a function. |
| RETURNS: True. |
| EFFECT: Substitutes Term by <and(t1=s1, t2=s2, ..., tn=sn)>, |
| where ti and si are the arguments of both f's in Term. |
| ***************************************************************/ |
| { |
| LIST Scan, Bscan, List, Hlist; |
| TERM Func1, Func2, NewTerm; |
| |
| Func1 = term_FirstArgument(Term); |
| Func2 = term_SecondArgument(Term); |
| List = term_ArgumentList(Term); |
| Scan = list_Nil(); |
| term_RplacArgumentList(Term, list_Nil()); |
| term_RplacTop(Term, fol_And()); |
| |
| for (Scan = term_ArgumentList(Func1),Bscan = term_ArgumentList(Func2); |
| !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| Hlist = list_Nil(); |
| Hlist = list_Cons(list_Car(Bscan), Hlist); |
| Hlist = list_Cons(list_Car(Scan), Hlist); |
| NewTerm = term_Create(fol_Equality(), Hlist); |
| term_RplacArgumentList(Term, list_Cons(NewTerm, term_ArgumentList(Term))); |
| Bscan = list_Cdr(Bscan); |
| } |
| |
| list_Delete(term_ArgumentList(Func1)); |
| list_Delete(term_ArgumentList(Func2)); |
| term_RplacArgumentList(Func1, list_Nil()); |
| term_RplacArgumentList(Func2, list_Nil()); |
| term_Delete(Func1); |
| term_Delete(Func2); |
| list_Delete(List); |
| } |
| |
| |
| BOOL fol_PropagateFreeness(TERM Term) |
| /************************************************************** |
| INPUT: A term and a list of functions. |
| RETURNS: True iff a subterm of the form f(...)=f(...) occurs in the term, |
| where f has property FREELY and GENERATED. |
| EFFECT: Substitutes all occurences of f=f by <and(t1=s1,...tn=sn)>,where |
| ti and si are the arguments of each f in f=f. |
| ***************************************************************/ |
| { |
| BOOL Free; |
| LIST Scan; |
| TERM Argum1, Argum2; |
| |
| Free = FALSE; |
| |
| if (fol_IsQuantifier(term_TopSymbol(Term))) |
| return fol_PropagateFreeness(term_SecondArgument(Term)); |
| |
| if (!term_IsAtom(Term)) { |
| for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| if (fol_PropagateFreeness(list_Car(Scan))) |
| Free = TRUE; |
| } |
| else |
| if (fol_IsEquality(Term)) { |
| Argum1 = term_FirstArgument(Term); |
| Argum2 = term_SecondArgument(Term); |
| if (symbol_Equal(term_TopSymbol(Argum1), term_TopSymbol(Argum2)) && |
| symbol_HasProperty(term_TopSymbol(Argum1), FREELY) && |
| symbol_HasProperty(term_TopSymbol(Argum1), GENERATED)) { |
| fol_ReplaceByArgCon(Term); |
| return TRUE; |
| } |
| } |
| |
| return Free; |
| } |
| |
| |
| static BOOL fol_PropagateWitnessIntern(TERM Equation, SYMBOL Variable) |
| /************************************************************** |
| INPUT: A Term which is an equation where <Variable> is one |
| of the equation's arguments that does not occur in the |
| other argument. Father links must exist. |
| RETURNS: True in case of witness propagation. |
| EFFECT: Checks whether subterm the equation is part of |
| is of the form described in fol_PropagateWitness and |
| substitutes in case of a hit. |
| ***************************************************************/ |
| { |
| TERM SuperTerm, BindQuantor, Predicat; |
| SYMBOL SuperTop; |
| |
| SuperTerm = term_Superterm(Equation); |
| |
| if (SuperTerm == term_Null()) |
| return FALSE; |
| |
| SuperTop = term_TopSymbol(SuperTerm); |
| BindQuantor = term_Superterm(SuperTerm); |
| |
| if (BindQuantor == term_Null()) |
| return FALSE; |
| |
| if (!fol_IsQuantifier(term_TopSymbol(BindQuantor)) || |
| list_Length(term_ArgumentList(SuperTerm)) != 2) |
| return FALSE; |
| |
| if (Equation == term_SecondArgument(SuperTerm)) |
| Predicat = term_FirstArgument(SuperTerm); |
| else |
| Predicat = term_SecondArgument(SuperTerm); |
| |
| if (symbol_Equal(term_TopSymbol(BindQuantor), fol_All()) && |
| symbol_Equal(SuperTop, fol_Or()) && |
| symbol_Equal(term_TopSymbol(Predicat), fol_Not()) && |
| symbol_HasProperty(term_TopSymbol(term_FirstArgument(Predicat)), FREELY) && |
| symbol_HasProperty(term_TopSymbol(term_FirstArgument(Predicat)), GENERATED) && |
| symbol_Equal(term_TopSymbol(term_FirstArgument(term_FirstArgument(Predicat))), Variable)) { |
| fol_SetFalse(BindQuantor); |
| return TRUE; |
| } |
| if (!symbol_HasProperty(term_TopSymbol(Predicat), FREELY) || |
| !symbol_HasProperty(term_TopSymbol(Predicat), GENERATED) || |
| !symbol_Equal(Variable, term_TopSymbol(term_FirstArgument(Predicat)))) |
| return FALSE; |
| |
| if (symbol_Equal(term_TopSymbol(BindQuantor), fol_All())) { |
| if (symbol_Equal(SuperTop, fol_Implies()) && |
| term_SecondArgument(SuperTerm) == Equation) { |
| fol_SetFalse(BindQuantor); |
| return TRUE; |
| } |
| if (symbol_Equal(SuperTop, fol_Implied()) && |
| term_FirstArgument(SuperTerm) == Equation) { |
| fol_SetFalse(BindQuantor); |
| return TRUE; |
| } |
| } |
| else /* Exquantor */ |
| if (symbol_Equal(SuperTop, fol_And())) { |
| fol_SetTrue(BindQuantor); |
| return TRUE; |
| } |
| |
| return FALSE; |
| } |
| |
| |
| BOOL fol_PropagateWitness(TERM Term) |
| /************************************************************** |
| INPUT: A Term. |
| RETURNS: True in case of witness propagation. |
| EFFECT: Substitutes any subterm of Term of the form |
| forall([x],implies(P(x),x=t)) |
| forall([x],implied(x=t,P(x))) |
| forall([x],or(notP(x),x=t)) by FALSE and |
| exists([x],and(P(x),x=t)) by TRUE, where |
| P has property FREELY and GENERATED, x doesn't occur in t. |
| ***************************************************************/ |
| { |
| BOOL Hit; |
| LIST Scan; |
| |
| Hit = FALSE; |
| |
| if (fol_IsQuantifier(term_TopSymbol(Term))) |
| return fol_PropagateWitness(term_SecondArgument(Term)); |
| if (fol_IsEquality(Term)) { |
| if (term_IsVariable(term_SecondArgument(Term))) { |
| if (!term_ContainsSymbol(term_FirstArgument(Term), term_TopSymbol(term_SecondArgument(Term)))) |
| Hit = fol_PropagateWitnessIntern(Term,term_TopSymbol(term_SecondArgument(Term))); |
| } |
| else { |
| if (term_IsVariable(term_FirstArgument(Term))) |
| if (!term_ContainsSymbol(term_SecondArgument(Term), term_TopSymbol(term_FirstArgument(Term)))) |
| Hit = fol_PropagateWitnessIntern(Term,term_TopSymbol(term_FirstArgument(Term))); |
| } |
| } |
| if (symbol_IsPredicate(term_TopSymbol(Term))) |
| return FALSE; |
| |
| for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| if (fol_PropagateWitness(list_Car(Scan))) |
| Hit = TRUE; |
| |
| return Hit; |
| } |
| |
| BOOL fol_PropagateTautologies(TERM Term) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: True iff function replaced a subterm. |
| EFFECT: Replaces all occurences of t=t, or(A,not(A)) by TRUE |
| and and(A,not(A)) by FALSE. |
| ***************************************************************/ |
| { |
| BOOL Hit; |
| LIST Scan, Bscan, ArgumentList; |
| SYMBOL Top; |
| |
| Top = term_TopSymbol(Term); |
| Hit = FALSE; |
| ArgumentList = term_ArgumentList(Term); |
| |
| if (fol_IsQuantifier(Top)) |
| return fol_PropagateTautologies(term_SecondArgument(Term)); |
| |
| if (fol_IsEquality(Term)) { |
| if (term_Equal(term_FirstArgument(Term), term_SecondArgument(Term))) { |
| fol_SetTrue(Term); |
| return TRUE; |
| } |
| } |
| |
| if (symbol_Equal(Top, fol_Or()) || symbol_Equal(Top, fol_And())) { |
| for (Scan = ArgumentList; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| if (symbol_Equal(term_TopSymbol(list_Car(Scan)), fol_Not())) { |
| for (Bscan = ArgumentList; !list_Empty(Bscan); Bscan = list_Cdr(Bscan)) { |
| if (list_Car(Scan) != list_Car(Bscan) && |
| fol_AlphaEqual(term_FirstArgument(list_Car(Scan)), list_Car(Bscan))) { |
| if (symbol_Equal(Top, fol_Or())) |
| fol_SetTrue(Term); |
| else |
| fol_SetFalse(Term); |
| return TRUE; |
| } |
| } |
| } |
| } |
| |
| if (!term_IsAtom(Term)) |
| for (Scan = ArgumentList; !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| if (fol_PropagateTautologies(list_Car(Scan))) |
| Hit = TRUE; |
| } |
| |
| return Hit; |
| } |
| |
| |
| static BOOL fol_AlphaEqualIntern(TERM Term1, TERM Term2, NAT Mark) |
| /************************************************************** |
| INPUT: Two terms which represent formulae and a binding mark. |
| RETURNS: True iff Term2 is equal to Term1 with respect to the |
| renaming of bound variables. |
| ***************************************************************/ |
| { |
| LIST Scan, Bscan; |
| SYMBOL Top1, Top2; |
| |
| Top1 = term_TopSymbol(Term1); |
| Top2 = term_TopSymbol(Term2); |
| |
| if (symbol_IsVariable(Top1) && symbol_IsVariable(Top2)) { |
| if (term_VarIsMarked(Top2, Mark)) |
| return symbol_Equal(Top1, (SYMBOL)term_BindingValue(Top2)); |
| else |
| return symbol_Equal(Top1, Top2); |
| } |
| |
| if (!symbol_Equal(Top1, Top2)) |
| return FALSE; |
| |
| if (fol_IsQuantifier(Top1)) { |
| if (list_Length(fol_QuantifierVariables(Term1)) != list_Length(fol_QuantifierVariables(Term2))) |
| return FALSE; |
| for (Scan = fol_QuantifierVariables(Term1), Bscan = fol_QuantifierVariables(Term2); |
| !list_Empty(Scan); |
| Scan = list_Cdr(Scan), Bscan = list_Cdr(Bscan)) |
| term_CreateValueBinding(term_TopSymbol(list_Car(Bscan)), Mark, |
| (POINTER)term_TopSymbol(list_Car(Scan))); |
| |
| if (!fol_AlphaEqualIntern(term_SecondArgument(Term1), term_SecondArgument(Term2), Mark)) |
| return FALSE; |
| for (Scan = fol_QuantifierVariables(Term1), Bscan = fol_QuantifierVariables(Term2); |
| !list_Empty(Scan); |
| Scan = list_Cdr(Scan), Bscan = list_Cdr(Bscan)) |
| term_SetBindingMark(term_TopSymbol(list_Car(Bscan)), term_NullMark()); |
| } |
| else { |
| if (list_Length(term_ArgumentList(Term1)) != list_Length(term_ArgumentList(Term2))) |
| return FALSE; |
| |
| for (Scan = term_ArgumentList(Term1), Bscan = term_ArgumentList(Term2); |
| !list_Empty(Scan); Scan = list_Cdr(Scan), Bscan = list_Cdr(Bscan)) |
| if (!fol_AlphaEqualIntern(list_Car(Scan), list_Car(Bscan), Mark)) |
| return FALSE; |
| } |
| return TRUE; |
| } |
| |
| |
| BOOL fol_AlphaEqual(TERM Term1, TERM Term2) |
| /************************************************************** |
| INPUT: Two terms of the form Qx(<rest>). All variables that occur in |
| Term1 and Term2 must be bound by only one quantifier! |
| RETURNS: TRUE iff Term2 is bound renaming of Term1. |
| ***************************************************************/ |
| { |
| BOOL Hit; |
| |
| #ifdef CHECK |
| if (Term1 == term_Null() || Term2 == term_Null()) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_AlphaEqual: Corrupted term as parameter.\n"); |
| misc_FinishErrorReport(); |
| } |
| if (fol_VarBoundTwice(Term1) || fol_VarBoundTwice(Term2)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_AlphaEqual: Variables are bound more than once.\n"); |
| misc_FinishErrorReport(); |
| } |
| if (term_InBindingPhase()) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_AlphaEqual: Term context is in binding phase.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_StartBinding(); |
| |
| Hit = fol_AlphaEqualIntern(Term1, Term2, term_ActMark()); |
| |
| term_StopBinding(); |
| |
| return Hit; |
| } |
| |
| |
| static BOOL fol_VarBoundTwiceIntern(TERM Term, NAT Mark) |
| /************************************************************** |
| INPUT: A term, possibly a NULL Term and a valid binding mark. |
| RETURNS: TRUE iff a variable in <Term> is bound by more than one quantifier. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| if (Term == term_Null()) |
| return FALSE; |
| |
| if (term_IsAtom(Term)) |
| return FALSE; |
| |
| if (!fol_IsQuantifier(term_TopSymbol(Term))) { |
| for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| if (fol_VarBoundTwiceIntern(list_Car(Scan), Mark)) |
| return TRUE; |
| } |
| else { |
| for (Scan = fol_QuantifierVariables(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| if (!term_VarIsMarked(term_TopSymbol(list_Car(Scan)), Mark)) |
| term_SetBindingMark(term_TopSymbol(list_Car(Scan)), Mark); |
| else |
| return TRUE; |
| } |
| if (fol_VarBoundTwiceIntern(term_SecondArgument(Term), Mark)) |
| return TRUE; |
| for (Scan = fol_QuantifierVariables(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| term_SetBindingMark(term_TopSymbol(list_Car(Scan)), term_NullMark()); |
| } |
| return FALSE; |
| } |
| |
| |
| BOOL fol_VarBoundTwice(TERM Term) |
| /************************************************************** |
| INPUT: A term. |
| RETURNS: TRUE iff a variable in term is bound by more than one quantifier. |
| ***************************************************************/ |
| { |
| BOOL Hit; |
| |
| #ifdef CHECK |
| if (term_InBindingPhase()) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n\n Context in fol_VarBoundTwice: term in binding phase\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_StartBinding(); |
| |
| Hit = fol_VarBoundTwiceIntern(Term, (NAT)term_ActMark()); |
| |
| term_StopBinding(); |
| |
| return Hit; |
| } |
| |
| |
| NAT fol_Depth(TERM Term) |
| /************************************************************** |
| INPUT: A formula. |
| RETURNS: The depth of the formula up to predicate level. |
| ***************************************************************/ |
| { |
| NAT Depth,Help; |
| LIST Scan; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Term)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_Depth: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Depth = 0; |
| |
| if (symbol_IsPredicate(term_TopSymbol(Term))) |
| return 1; |
| |
| if (fol_IsQuantifier(term_TopSymbol(Term))) |
| return (fol_Depth(term_SecondArgument(Term)) + 1); |
| |
| for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) { |
| Help = fol_Depth(list_Car(Scan)); |
| if (Help > Depth) |
| Depth = Help; |
| } |
| |
| return (Depth+1); |
| } |
| |
| |
| static void fol_ApplyContextToTermIntern(CONTEXT Context, TERM Term) |
| /******************************************************************** |
| INPUT: A context (Context) and a term (Term). |
| RETURN: void. |
| EFFECT: Term is destructively changed modulo Context. |
| *********************************************************************/ |
| { |
| LIST Scan; |
| |
| if (fol_IsQuantifier(term_TopSymbol(Term))) { |
| fol_ApplyContextToTermIntern(Context, term_SecondArgument(Term)); |
| } |
| else if (symbol_IsVariable(term_TopSymbol(Term))) { |
| if (cont_VarIsBound(Context, term_TopSymbol(Term))) |
| Term = cont_ApplyBindingsModuloMatching(Context, Term, TRUE); |
| } |
| else { |
| for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| fol_ApplyContextToTermIntern(Context, list_Car(Scan)); |
| } |
| } |
| |
| |
| static BOOL fol_CheckApplyContextToTerm(CONTEXT Context, TERM Term) |
| /************************************************************* |
| INPUT: A Context and a term. |
| RETURN: TRUE iff Context can be applied to Term. |
| COMMENT: Intern funktion of fol_ApplyContextToTerm. |
| **************************************************************/ |
| { |
| LIST Scan; |
| BOOL Apply; |
| |
| Apply = TRUE; |
| |
| if (fol_IsQuantifier(term_TopSymbol(Term))) { |
| for (Scan=fol_QuantifierVariables(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| if (cont_VarIsBound(Context, term_TopSymbol(list_Car(Scan)))) |
| return FALSE; |
| for (Scan=term_ArgumentList(term_SecondArgument(Term)); !list_Empty(Scan); Scan=list_Cdr(Scan)) { |
| if (!fol_CheckApplyContextToTerm(Context, list_Car(Scan))) |
| Apply = FALSE; |
| } |
| } |
| else { |
| for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| if (!fol_CheckApplyContextToTerm(Context, list_Car(Scan))) |
| Apply = FALSE; |
| } |
| return Apply; |
| } |
| |
| |
| BOOL fol_ApplyContextToTerm(CONTEXT Context, TERM Term) |
| /*************************************************************** |
| INPUT: A context (Context) and a term (Term). |
| RETURN: TRUE iff context could be applied on Term. |
| EFFECT: Term is destructively changed modulo Context iff possible. |
| ****************************************************************/ |
| { |
| if (fol_CheckApplyContextToTerm(Context, Term)) { |
| fol_ApplyContextToTermIntern(Context, Term); |
| return TRUE; |
| } |
| |
| return FALSE; |
| } |
| |
| |
| BOOL fol_SignatureMatchFormula(TERM Formula, TERM Instance, BOOL Variant) |
| /******************************************************************** |
| INPUT : Two formulas and a flag. |
| It is assumed that the symbol context is clean. |
| RETURN: TRUE iff <Formula> can be matched to <Instance> by matching |
| variables as well as signature symbols. If <Variant> is TRUE |
| variables must be matched to variables. |
| EFFECT: The symbol matches are stored in the symbol context. |
| *********************************************************************/ |
| { |
| int Stack; |
| SYMBOL FormulaTop, InstanceTop; |
| NAT ActMark; |
| TERM ActFormula, ActInstance; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Formula) || term_InBindingPhase() || |
| !term_IsTerm(Instance) || !symbol_ContextIsClean()) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_SignatureMatchFormula: Illegal input or context."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_StartBinding(); |
| |
| Stack = stack_Bottom(); |
| term_NewMark(); |
| ActMark = term_OldMark(); |
| ActFormula = Formula; |
| ActInstance = Instance; |
| |
| do { |
| FormulaTop = term_TopSymbol(ActFormula); |
| InstanceTop = term_TopSymbol(ActInstance); |
| |
| if (!symbol_IsVariable(FormulaTop)) { |
| if (!symbol_ContextIsBound(FormulaTop)) { |
| if (!symbol_IsJunctor(FormulaTop) && !symbol_IsJunctor(InstanceTop) && |
| !fol_IsPredefinedPred(FormulaTop) && !fol_IsPredefinedPred(InstanceTop)) |
| symbol_ContextSetValue(FormulaTop, InstanceTop); /* Symbols are ALWAYS bound !*/ |
| else { |
| if (!symbol_Equal(FormulaTop, InstanceTop)) { |
| term_StopBinding(); |
| return FALSE; |
| } |
| } |
| } |
| else { |
| if (symbol_ContextIsBound(FormulaTop) && |
| !symbol_Equal(symbol_ContextGetValue(FormulaTop),InstanceTop)) { |
| term_StopBinding(); |
| return FALSE; |
| } |
| } |
| } |
| |
| if (list_Length(term_ArgumentList(ActFormula)) != list_Length(term_ArgumentList(ActInstance))) { |
| term_StopBinding(); |
| return FALSE; |
| } |
| |
| if (term_IsComplex(ActFormula)) { |
| stack_Push(term_ArgumentList(ActInstance)); |
| stack_Push(term_ArgumentList(ActFormula)); |
| } |
| else { |
| if (symbol_IsVariable(FormulaTop)) { |
| if (!term_VarIsMarked(FormulaTop, ActMark)) { |
| if (!Variant || symbol_IsVariable(InstanceTop)) |
| term_CreateValueBinding(FormulaTop, ActMark, (POINTER)InstanceTop); |
| else { |
| term_StopBinding(); |
| return FALSE; |
| } |
| } |
| else { |
| if (!symbol_Equal((SYMBOL)term_BindingValue(FormulaTop), InstanceTop)) { |
| term_StopBinding(); |
| return FALSE; |
| } |
| } |
| } |
| } |
| |
| while (!stack_Empty(Stack) && list_Empty(stack_Top())) { |
| stack_Pop(); |
| stack_Pop(); |
| } |
| if (!stack_Empty(Stack)) { |
| ActFormula = (TERM)list_Car(stack_Top()); |
| ActInstance = (TERM)list_Car(stack_NthTop(1)); |
| stack_RplacTop(list_Cdr(stack_Top())); |
| stack_RplacNthTop(1,list_Cdr(stack_NthTop(1))); |
| } |
| } while (!stack_Empty(Stack)); |
| |
| term_StopBinding(); |
| |
| return TRUE; |
| } |
| |
| |
| BOOL fol_SignatureMatch(TERM Term, TERM Instance, LIST* Bindings, BOOL Variant) |
| /***************************************************************** |
| INPUT : Two formulas, a binding list and a boolean flag. |
| RETURN: TRUE iff <Term> can be matched to <Instance> by matching |
| variables as well as signature symbols. If <Variant> is TRUE |
| variables must be matched to variables. Signature symbol |
| matchings have to be injective. |
| EFFECT: The symbol matches are stored in the symbol context. |
| ******************************************************************/ |
| { |
| int Stack; |
| SYMBOL TermTop, InstanceTop; |
| NAT ActMark; |
| TERM ActTerm, ActInstance; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Term) || !term_IsTerm(Instance)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In fol_SignatureMatch: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Stack = stack_Bottom(); |
| ActMark = term_OldMark(); |
| ActTerm = Term; |
| ActInstance = Instance; |
| |
| do { |
| TermTop = term_TopSymbol(ActTerm); |
| InstanceTop = term_TopSymbol(ActInstance); |
| |
| if (!symbol_IsVariable(TermTop)) { |
| if (!symbol_ContextIsBound(TermTop)) { |
| if (!symbol_IsJunctor(TermTop) && !symbol_IsJunctor(InstanceTop) && |
| !fol_IsPredefinedPred(TermTop) && !fol_IsPredefinedPred(InstanceTop) && |
| !symbol_ContextIsMapped(InstanceTop)) { |
| symbol_ContextSetValue(TermTop, InstanceTop); /* Symbols are ALWAYS bound !*/ |
| *Bindings = list_Cons((POINTER)TermTop,*Bindings); |
| } |
| else { |
| if (!symbol_Equal(TermTop, InstanceTop)) { |
| return FALSE; |
| } |
| } |
| } |
| else { |
| if (symbol_ContextIsBound(TermTop) && |
| !symbol_Equal(symbol_ContextGetValue(TermTop),InstanceTop)) { |
| return FALSE; |
| } |
| } |
| } |
| |
| if (list_Length(term_ArgumentList(ActTerm)) != list_Length(term_ArgumentList(ActInstance))) { |
| return FALSE; |
| } |
| |
| if (term_IsComplex(ActTerm)) { |
| stack_Push(term_ArgumentList(ActInstance)); |
| stack_Push(term_ArgumentList(ActTerm)); |
| } |
| else { |
| if (symbol_IsVariable(TermTop)) { |
| if (!term_VarIsMarked(TermTop, ActMark)) { |
| if (!Variant || symbol_IsVariable(InstanceTop)) { |
| term_CreateValueBinding(TermTop, ActMark, (POINTER)InstanceTop); |
| *Bindings = list_Cons((POINTER)TermTop,*Bindings); |
| } |
| else |
| return FALSE; |
| } |
| else { |
| if (!symbol_Equal((SYMBOL)term_BindingValue(TermTop), InstanceTop)) { |
| return FALSE; |
| } |
| } |
| } |
| } |
| |
| while (!stack_Empty(Stack) && list_Empty(stack_Top())) { |
| stack_Pop(); |
| stack_Pop(); |
| } |
| if (!stack_Empty(Stack)) { |
| ActTerm = (TERM)list_Car(stack_Top()); |
| ActInstance = (TERM)list_Car(stack_NthTop(1)); |
| stack_RplacTop(list_Cdr(stack_Top())); |
| stack_RplacNthTop(1,list_Cdr(stack_NthTop(1))); |
| } |
| } while (!stack_Empty(Stack)); |
| |
| return TRUE; |
| } |
| |
| |
| BOOL fol_CheckFormula(TERM Formula) |
| /******************************************************************* |
| INPUT : A term Formula. |
| RETURN: TRUE iff no free variables occure in Formula |
| and father links are properly set |
| and argument list lengths match arities |
| ********************************************************************/ |
| { |
| LIST FreeVars; |
| |
| FreeVars = fol_FreeVariables(Formula); |
| |
| if (!list_Empty(FreeVars)) { |
| list_Delete(FreeVars); |
| return FALSE; |
| } |
| |
| return term_CheckTerm(Formula); |
| } |