Google Git
Sign in
fuchsia / third_party / github.com / llvm / llvm-test-suite / refs/tags/llvmorg-10.0.0-rc1 / . / MultiSource / Applications / SPASS / foldfg.c
blob: cf021212c5692a62a1f86cb939007ff972c7e198 [file] [log] [blame]
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * 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);
}