diff options
Diffstat (limited to 'test/spass/defs.c')
| -rw-r--r-- | test/spass/defs.c | 1359 |
1 files changed, 1359 insertions, 0 deletions
diff --git a/test/spass/defs.c b/test/spass/defs.c new file mode 100644 index 0000000..0b6268b --- /dev/null +++ b/test/spass/defs.c @@ -0,0 +1,1359 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * DEFINITIONS * */ +/* * * */ +/* * $Module: DEFS * */ +/* * * */ +/* * Copyright (C) 1998, 1999, 2000, 2001 * */ +/* * MPI fuer Informatik * */ +/* * * */ +/* * This program is free software; you can redistribute * */ +/* * it and/or modify it under the terms of the GNU * */ +/* * General Public License as published by the Free * */ +/* * Software Foundation; either version 2 of the License, * */ +/* * or (at your option) any later version. * */ +/* * * */ +/* * This program is distributed in the hope that it will * */ +/* * be useful, but WITHOUT ANY WARRANTY; without even * */ +/* * the implied warranty of MERCHANTABILITY or FITNESS * */ +/* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ +/* * License for more details. * */ +/* * * */ +/* * You should have received a copy of the GNU General * */ +/* * Public License along with this program; if not, write * */ +/* * to the Free Software Foundation, Inc., 59 Temple * */ +/* * Place, Suite 330, Boston, MA 02111-1307 USA * */ +/* * * */ +/* * * */ +/* $Revision: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + +#include "cnf.h" +#include "defs.h" +#include "foldfg.h" + +static void def_DeleteFromClauses(DEF); +static void def_DeleteFromTerm(DEF); + +DEF def_CreateFromClauses(TERM ExpTerm, TERM PredTerm, LIST Clauses, LIST Lits, + BOOL Con) +/********************************************************** + INPUT: Two terms, a list of clausenumbers, a list of literal indices and + a boolean saying whether all clauses derived by expanding the + predicate should be conclauses. + RETURNS: A definition consisting of the 2 terms as expansion term and + predicate term and the list of parent clause numbers and a list + of the indices of the defined predicate in the parent clauses. + ToProve and label are set to NULL. +********************************************************/ +{ + DEF result; + +#ifdef CHECK + if (!term_IsTerm(ExpTerm) || !term_IsTerm(PredTerm)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_CreateFromClause: Illegal input."); + misc_FinishErrorReport(); + } + if (list_Empty(Clauses)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_CreateFromClause: No parent clause given."); + misc_FinishErrorReport(); + } +#endif + + result = (DEF) memory_Malloc(sizeof(DEF_NODE)); + result->expansion = ExpTerm; + result->predicate = PredTerm; + result->toprove = (TERM) NULL; + result->parentclauses = list_PairCreate(Clauses, Lits); + result->label = (const char*) NULL; + result->conjecture = Con; + + return result; +} + +DEF def_CreateFromTerm(TERM ExpTerm, TERM PredTerm, TERM ToProve, const char* Label) +/********************************************************** + INPUT: 3 terms and a term label. + RETURNS: A definition consisting of the 3 terms as expansion term, + predicate term and term to prove before applying the + definition and the label of the parent term. + The list of clausenumbers is set to NULL. +********************************************************/ +{ + DEF result; + +#ifdef CHECK + if (!term_IsTerm(ExpTerm) || !term_IsTerm(PredTerm)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_CreateFromTerm: Illegal input."); + misc_FinishErrorReport(); + } + if (Label == NULL) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_CreateFromTerm: No parent clause given."); + misc_FinishErrorReport(); + } +#endif + + result = (DEF) memory_Malloc(sizeof(DEF_NODE)); + result->expansion = ExpTerm; + result->predicate = PredTerm; + result->toprove = ToProve; + result->parentclauses = list_PairCreate(list_Nil(), list_Nil()); + result->label = Label; + result->conjecture = FALSE; + + return result; +} + +static void def_DeleteFromClauses(DEF D) +/********************************************************** + INPUT: A definition derived from clauses. + EFFECT: The definition is deleted, INCLUDING THE TERMS AND + THE LIST OF CLAUSE NUMBERS. +********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(def_Expansion(D)) || !term_IsTerm(def_Predicate(D))) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_DeleteFormClauses: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + /* ToProve and Label are NULL */ + term_Delete(def_Expansion(D)); + term_Delete(def_Predicate(D)); + list_Delete(def_ClauseNumberList(D)); + list_Delete(def_ClauseLitsList(D)); + list_PairFree(D->parentclauses); + + memory_Free(D, sizeof(DEF_NODE)); +} + +static void def_DeleteFromTerm(DEF D) +/********************************************************** + INPUT: A definition derived from a term. + EFFECT: The definition is deleted, INCLUDING THE TERMS. + THE LABEL IS NOT FREED. +********************************************************/ +{ +#ifdef CHECK + if (!term_IsTerm(def_Expansion(D)) || !term_IsTerm(def_Predicate(D))) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_DeleteFromTerm: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + /* List of clausenumbers is NULL */ + term_Delete(def_Expansion(D)); + term_Delete(def_Predicate(D)); + if (def_ToProve(D) != (TERM) NULL) + term_Delete(def_ToProve(D)); + list_PairFree(D->parentclauses); + memory_Free(D, sizeof(DEF_NODE)); +} + +void def_Delete(DEF D) +/********************************************************** + INPUT: A definition derived from a term. + EFFECT: The definition is deleted. + CAUTION: All elements of the definition except of the label are freed. +********************************************************/ +{ + if (!list_Empty(def_ClauseNumberList(D))) + def_DeleteFromClauses(D); + else + def_DeleteFromTerm(D); +} + +int def_PredicateOccurrences(TERM Term, SYMBOL P) +/**************************************************** + INPUT: A term and a predicate symbol. + RETURNS: The number of occurrences of the predicate symbol in Term +**************************************************/ +{ + /* Quantifiers */ + if (fol_IsQuantifier(term_TopSymbol(Term))) + return def_PredicateOccurrences(term_SecondArgument(Term), P); + + /* Junctors and NOT */ + if (fol_IsJunctor(term_TopSymbol(Term)) || + symbol_Equal(term_TopSymbol(Term),fol_Not())){ + LIST scan; + int count; + count = 0; + for (scan=term_ArgumentList(Term); !list_Empty(scan); scan=list_Cdr(scan)) { + count += def_PredicateOccurrences((TERM) list_Car(scan), P); + /* Only the cases count==1 and count>1 are important */ + if (count > 1) + return count; + } + return count; + } + + if (symbol_Equal(term_TopSymbol(Term), P)) + return 1; + return 0; +} + +LIST def_ExtractDefsFromTerm(TERM Term, const char* Label) +/************************************************************** + INPUT: A term and its label. + RETURNS: A list of definitions found in the term. + NOTE: The Term is not changed, the definitions contain copies. +***************************************************************/ +{ + TERM andterm; + BOOL found; + int pol; + LIST univars, termlist, defslist, scan; + + /* First check if there is a top level and() so that the Term may + contain several definitions */ + + andterm = Term; + found = FALSE; + pol = 1; + univars = list_Nil(); + + /* Traverse top down universal quantifiers */ + while (!found) { + if ((symbol_Equal(term_TopSymbol(andterm), fol_All()) && (pol == 1)) + || (symbol_Equal(term_TopSymbol(andterm), fol_Exist()) && (pol == -1))) { + univars = list_Nconc(univars, list_Copy(fol_QuantifierVariables(andterm))); + andterm = term_SecondArgument(andterm); + } + else { + if (symbol_Equal(term_TopSymbol(andterm), fol_Not())) { + pol = -pol; + andterm = term_FirstArgument(andterm); + } + else + found = TRUE; + } + } + + termlist = list_Nil(); + /* Check if conjunction was found */ + if ((symbol_Equal(term_TopSymbol(andterm), fol_And()) && (pol == 1)) + || (symbol_Equal(term_TopSymbol(andterm), fol_Or()) && (pol == -1))) { + LIST l; + /* Flatten nested and/or */ + /* Make copy of relevant subterm */ + andterm = cnf_Flatten(term_Copy(andterm), term_TopSymbol(andterm)); + for (l=term_ArgumentList(andterm); !list_Empty(l); l=list_Cdr(l)) { + TERM newterm; + newterm = fol_CreateQuantifierAddFather(fol_All(), term_CopyTermList(univars), + list_List(list_Car(l))); + termlist = list_Cons(newterm, termlist); + } + /* Arguments are used in new terms */ + list_Delete(term_ArgumentList(andterm)); + term_Free(andterm); + } + else + termlist = list_List(term_Copy(Term)); + + list_Delete(univars); + + /* Now we have a list of terms that may contain definitions */ + defslist = list_Nil(); + for (scan=termlist; !list_Empty(scan); scan=list_Cdr(scan)) { + TERM cand; + TERM foundpred, toprove; + + /* Candidate from list */ + cand = (TERM) list_Car(scan); + term_AddFatherLinks(cand); + + if (cnf_ContainsDefinition(cand, &foundpred)) { + DEF def; +#ifdef CHECK + if (!fol_CheckFormula(cand)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_ExtractDefsFromTerm: Illegal term cand"); + misc_FinishErrorReport(); + } +#endif + cand = cnf_DefConvert(cand, foundpred, &toprove); +#ifdef CHECK + if (!fol_CheckFormula(cand)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_ExtractDefsFromTerm: Illegal term cand"); + misc_FinishErrorReport(); + } +#endif + def = def_CreateFromTerm(term_Copy(term_SecondArgument(term_Superterm(foundpred))), + term_Copy(foundpred), toprove, Label); + + if (def_PredicateOccurrences(cand, term_TopSymbol(foundpred)) > 1) + def_RemoveAttribute(def, PREDOCCURONCE); + else + def_AddAttribute(def, PREDOCCURONCE); + if (symbol_Equal(term_TopSymbol(foundpred), fol_Equality())) + def_AddAttribute(def, ISEQUALITY); + else + def_RemoveAttribute(def, ISEQUALITY); + + defslist = list_Cons(def, defslist); + } + term_Delete(cand); + } + + list_Delete(termlist); + return defslist; +} + +void def_ExtractDefsFromClauselist(PROOFSEARCH Search, LIST Clauselist) +/************************************************************** + INPUT: A proofsearch object and a list of clauses + RETURNS: Nothing. + EFFECT: The definitions found in the clauselist object are stored in + the proofsearch object. + NOTE: The clause list is not changed. + The old list of definitions in the proofsearch object is + overwritten. +***************************************************************/ +{ + LIST scan, defslist; + FLAGSTORE FlagStore; + PRECEDENCE Precedence; + + defslist = list_Nil(); + FlagStore = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + for (scan=Clauselist; !list_Empty(scan); scan=list_Cdr(scan)) { + CLAUSE Clause; + NAT index; + LIST pair; + + Clause = (CLAUSE) list_Car(scan); + /* Check if clause contains a predicate that may be part of a definition */ + if (clause_ContainsPotPredDef(Clause, FlagStore, Precedence, &index, &pair)) { + LIST l, compl, compllits; + BOOL done; + + compl = compllits = list_Nil(); + done = FALSE; + + /* Search for complement clauses */ + for (l=Clauselist; !list_Empty(l) && !done; l=list_Cdr(l)) { + int predindex; + if (clause_IsPartOfDefinition((CLAUSE) list_Car(l), + clause_GetLiteralTerm(Clause, index), + &predindex, pair)) { + compl = list_Cons(list_Car(l), compl); + compllits = list_Cons((POINTER) predindex, compllits); + + if (list_Empty(list_PairFirst(pair)) && + list_Empty(list_PairSecond(pair))) + done = TRUE; + } + } + + /* All complements found ? */ + if (done) { + LIST l2, clausenumbers, args; + DEF def; + NAT i; + TERM defterm, predterm; + BOOL con; + + clausenumbers = list_Nil(); + con = clause_GetFlag(Clause, CONCLAUSE); + + for (l2=compl; !list_Empty(l2); l2=list_Cdr(l2)) { + clausenumbers = list_Cons((POINTER) clause_Number((CLAUSE) list_Car(l2)), + clausenumbers); + if (clause_GetFlag((CLAUSE) list_Car(l2), CONCLAUSE)) + con = TRUE; + } + clausenumbers = list_Cons((POINTER) clause_Number(Clause), + clausenumbers); + compllits = list_Cons((POINTER) index, compllits); + + /* Build definition term */ + predterm = term_Copy(clause_GetLiteralTerm(Clause, index)); + args = list_Nil(); + for (i = 0; i < clause_Length(Clause); i++) + if (i != index) + args = list_Cons(term_Copy(clause_GetLiteralTerm(Clause, i)), args); + defterm = term_CreateAddFather(fol_Or(), args); + /* The expansion is negative here, so it must be inverted */ + defterm = term_Create(fol_Not(), list_List(defterm)); + defterm = cnf_NegationNormalFormula(defterm); + def = def_CreateFromClauses(defterm, predterm, clausenumbers, compllits, con); + defslist = list_Cons(def, defslist); + if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) { + fputs("\nNew definition found :", stdout); + def_Print(def); + } + } + else { + list_Delete(compllits); + list_Delete(list_PairSecond(pair)); + list_Delete(list_PairFirst(pair)); + } + list_Delete(compl); + list_PairFree(pair); + } + } + + if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) { + if (!list_Empty(defslist)) { + fputs("\nFound definitions :\n", stdout); + for (scan = defslist; !list_Empty(scan); scan = list_Cdr(scan)) { + def_Print((DEF) list_Car(scan)); + fputs("\n---\n", stdout); + } + } + } + + for (scan=defslist; !list_Empty(scan); scan=list_Cdr(scan)) + symbol_AddProperty(term_TopSymbol(def_Predicate((DEF) list_Car(scan))), ISDEF); + + prfs_SetDefinitions(Search, list_Nconc(prfs_Definitions(Search), defslist)); +} + +TERM def_ApplyDefToTermOnce(DEF Def, TERM Term, FLAGSTORE FlagStore, + PRECEDENCE Precedence, BOOL* Complete) +/************************************************************** + INPUT: A DEF structure, a term and a boolean that is set + to TRUE if no occurrences of the defined predicate + remain in the term. A flag store and a precedence. + RETURNS: A term where all occurrences of the definitions + predicate are expanded if possible. + NOTE: The Term is not changed. +***************************************************************/ +{ + TERM newtarget, oldtarget, targetpredicate, totoplevel, toprove; + LIST targettermvars, varsfortoplevel; + BOOL applicable; + + oldtarget = Term; + *Complete = TRUE; + + while (TRUE) { + newtarget = term_Copy(oldtarget); + term_AddFatherLinks(newtarget); + targettermvars = varsfortoplevel = list_Nil(); + + if (cnf_ContainsPredicate(newtarget, term_TopSymbol(def_Predicate(Def)), + &targetpredicate, &totoplevel, &targettermvars, + &varsfortoplevel)) { + *Complete = FALSE; + applicable = FALSE; + /* Check if definition is not always applicable */ + if (term_Equal(def_ToProve(Def), term_Null())) { + applicable = TRUE; + newtarget = cnf_ApplyDefinitionOnce(def_Predicate(Def), term_Copy(def_Expansion(Def)), + newtarget, targetpredicate, FlagStore); + if (oldtarget != Term) + term_Delete(oldtarget); + oldtarget = newtarget; + list_Delete(targettermvars); + list_Delete(varsfortoplevel); + } + else { + toprove = term_Copy(def_ToProve(Def)); + newtarget = cnf_DefTargetConvert(newtarget, totoplevel, toprove, + term_ArgumentList(def_Predicate(Def)), + term_ArgumentList(targetpredicate), + targettermvars, varsfortoplevel, + FlagStore, Precedence, + &applicable); + list_Delete(targettermvars); + list_Delete(varsfortoplevel); + if (applicable) { + newtarget = cnf_ApplyDefinitionOnce(def_Predicate(Def), term_Copy(def_Expansion(Def)), + newtarget, targetpredicate, FlagStore); + if (oldtarget != Term) + term_Delete(oldtarget); + oldtarget = newtarget; + } + else { + /* Predicate still exists but cannot be expanded */ + term_Delete(newtarget); + if (oldtarget == Term) + return NULL; + else { + oldtarget = cnf_ObviousSimplifications(oldtarget); + return oldtarget; + } + } + } + } + else { + *Complete = TRUE; + /* Predicate does no longer exist */ + term_Delete(newtarget); + /* No expansion possible */ + if (oldtarget == Term) + return NULL; + else { + oldtarget = cnf_ObviousSimplifications(oldtarget); + return oldtarget; + } + } + } + return NULL; /* Unreachable */ +} + +TERM def_ApplyDefToTermExhaustive(PROOFSEARCH Search, TERM Term) +/************************************************************** + INPUT: A proofsearch object and a term. + RETURNS: An expanded term. + NOTE: All occurences of defined predicates are expanded in the term, + until no further changes are possible. + CAUTION: If cyclic definitions exist, this will crash. +***************************************************************/ +{ + TERM oldterm, newterm; + BOOL done, complete; + FLAGSTORE FlagStore; + PRECEDENCE Precedence; + + done = FALSE; + oldterm = Term; + FlagStore = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + while (!done) { + LIST l; + done = TRUE; + /* Apply all definitions to term until no more changes occur */ + for (l=prfs_Definitions(Search); !list_Empty(l); l=list_Cdr(l)) { + newterm = def_ApplyDefToTermOnce((DEF) list_Car(l), oldterm, + FlagStore, Precedence, &complete); + if (newterm != NULL) { + if (oldterm != Term) + term_Delete(oldterm); + oldterm = newterm; + done = FALSE; + } + } + } + if (oldterm == Term) + return NULL; + else + return oldterm; +} + +LIST def_ApplyDefToClauseOnce(DEF Def, CLAUSE Clause, + FLAGSTORE FlagStore, PRECEDENCE Precedence) +/************************************************************** + INPUT: A DEF structure, a clause, a flag store and a + precedence. + RETURNS: A list of new clauses. + NOTE: The clause is not changed. + All occurences of the defined predicate are expanded + in the clause and in the derived clauses. +***************************************************************/ +{ + LIST result, l; + + result = list_List(Clause); + + for (l = result; !list_Empty(l); l = list_Cdr(l)) { + if (clause_ContainsSymbol((CLAUSE) list_Car(l), + term_TopSymbol(def_Predicate(Def)))) { + result = list_Nconc(result, + cnf_ApplyDefinitionToClause((CLAUSE) list_Car(l), + def_Predicate(Def), + def_Expansion(Def), + FlagStore, Precedence)); + /* Remove temporary clause */ + if ((CLAUSE) list_Car(l) != Clause) + clause_Delete((CLAUSE) list_Car(l)); + list_Rplaca(l, NULL); + } + } + result = list_PointerDeleteElement(result, NULL); + + /* Make sure the original clause is no longer in the list */ + if (!list_Empty(result)) + if (list_First(result) == Clause) + result = list_Pop(result); + + for (l = result; !list_Empty(l); l=list_Cdr(l)) { + CLAUSE c; + c = (CLAUSE) list_Car(l); + if (def_Conjecture(Def)) + clause_SetFlag((CLAUSE) list_Car(l), CONCLAUSE); + clause_SetFromDefApplication(c); + clause_SetParentClauses(c, list_Cons((POINTER) clause_Number(Clause), + list_Copy(def_ClauseNumberList(Def)))); + /* Parent literal is not available, as the predicate may occur several + times in the target clause */ + clause_SetParentLiterals(c, list_Cons((POINTER) 0, + list_Copy(def_ClauseLitsList(Def)))); + } + return result; +} + +LIST def_ApplyDefToClauseExhaustive(PROOFSEARCH Search, CLAUSE Clause) +/************************************************************** + INPUT: A proofsearch object and a clause. + RETURNS: A list of derived clauses. + NOTE: All occurences of defined predicates are expanded in the clause. + until no further changes are possible. + CAUTION: If cyclic definitions exist, this will crash. +***************************************************************/ +{ + LIST newclauses, scan, result; + CLAUSE orig; + FLAGSTORE FlagStore; + PRECEDENCE Precedence; + + orig = clause_Copy(Clause); + newclauses = list_List(orig); + result = list_Nil(); + FlagStore = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + while (!list_Empty(newclauses)) { + /* Check all clauses */ + LIST l, nextlist; + + /* List of clauses derived from newclauses by expanding predicates */ + nextlist = list_Nil(); + + for (l=newclauses; !list_Empty(l); l=list_Cdr(l)) { + LIST clauses; + CLAUSE c; + + c = (CLAUSE) list_Car(l); + + /* Apply all definitions to the clause */ + + /* List of clauses derived from one clause in newclauses by */ + /* expanding all possible predicates */ + clauses = list_Nil(); + + for (scan=prfs_Definitions(Search); !list_Empty(scan); scan=list_Cdr(scan)) + clauses = list_Nconc(clauses, def_ApplyDefToClauseOnce((DEF) list_Car(scan), c, FlagStore, Precedence)); + + /* If expansions were made delete old clause */ + if (!list_Empty(clauses)) { + /* DOCPROOF ? */ + if (c != Clause) { + if (flag_GetFlagValue(FlagStore, flag_DOCPROOF)) { + prfs_InsertDocProofClause(Search, c); + } + else + clause_Delete(c); + } + nextlist = list_Nconc(nextlist, clauses); + } + else { + /* No more expansions possible for this clause */ + /* If it is not the original clause, add it to the result list */ + if (c != Clause) + result = list_Cons(c, result); + } + } + list_Delete(newclauses); + newclauses = nextlist; + } + + return result; +} + + +void def_Print(DEF D) +/************************************************************** + INPUT: A DEF structure. + RETURNS: None. + EFFECT: Prints the definition to stdout. +***************************************************************/ +{ + LIST scan, scan2; + fputs("\n\nAtom: ", stdout); + fol_PrettyPrint(def_Predicate(D)); + fputs("\nExpansion: \n", stdout); + fol_PrettyPrint(def_Expansion(D)); + if (!list_Empty(def_ClauseNumberList(D))) { + fputs("\nParent clauses: ", stdout); + for (scan = def_ClauseNumberList(D), scan2 = def_ClauseLitsList(D); + !list_Empty(scan); scan = list_Cdr(scan), scan2 = list_Cdr(scan2)) + printf("%d.%d ", (NAT) list_Car(scan), (NAT) list_Car(scan2)); + if (D->conjecture) + fputs("\nDerived from conjecture clauses.", stdout); + else + fputs("\nNot derived from conjecture clauses.", stdout); + } + else { + fputs("\nLabel: ", stdout); + fputs(def_Label(D), stdout); + puts("\nGuard:"); + if (def_ToProve(D) != NULL) + fol_PrettyPrint(def_ToProve(D)); + else + fputs("Nothing.", stdout); + } + + fputs("\nAttributes: ", stdout); + if (def_HasAttribute(D, ISEQUALITY) || def_HasAttribute(D, PREDOCCURONCE)) { + if (def_HasAttribute(D, ISEQUALITY)) + fputs(" Equality ", stdout); + if (def_HasAttribute(D, PREDOCCURONCE)) + fputs(" No Multiple Occurrences ", stdout); + } + else { + fputs(" None ", stdout); + } +} + +LIST def_ApplyDefToClauselist(PROOFSEARCH Search, DEF Def, + LIST Clauselist, BOOL Destructive) +/************************************************************** + INPUT: A proofsearch object, a DEF structure, a list of unshared clauses + and a boolean saying whether the parent clause of an expansion + should be deleted. + RETURNS: None. + EFFECT: For each occurrence of the defined predicate in a clause in the list, + a new clause with expanded predicate is added to the list. +***************************************************************/ +{ + LIST l, newclauses, allnew; + FLAGSTORE FlagStore; + PRECEDENCE Precedence; + + allnew = list_Nil(); + FlagStore = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + for (l = Clauselist; !list_Empty(l); l = list_Cdr(l)) { + newclauses = def_ApplyDefToClauseOnce(Def, (CLAUSE) list_Car(l), + FlagStore, Precedence); + /* Expansions were possible, delete the original clause */ + if (Destructive && !list_Empty(newclauses)) { + if (flag_GetFlagValue(FlagStore, flag_DOCPROOF)) + prfs_InsertDocProofClause(Search, (CLAUSE) list_Car(l)); + else + clause_Delete((CLAUSE) list_Car(l)); + list_Rplaca(l, NULL); + } + allnew = list_Nconc(allnew, newclauses); + } + if (Destructive) + Clauselist = list_PointerDeleteElement(Clauselist, NULL); + + + if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) { + if (!list_Empty(allnew)) { + fputs("\nNew clauses after applying definitions : \n", stdout); + clause_ListPrint(allnew); + } + } + + Clauselist = list_Nconc(Clauselist, allnew); + return Clauselist; +} + +LIST def_ApplyDefToTermlist(DEF Def, LIST Termlist, + FLAGSTORE FlagStore, PRECEDENCE Precedence, + BOOL* Complete, BOOL Destructive) +/************************************************************** + INPUT: A DEF structure and a list of pairs (label, term), + a flag store, a precedence and a pointer to a + boolean. + If Destructive is TRUE the father of an expanded + term is deleted. + RETURNS: The changed list of terms. + EFFECT: For each occurrence of the defined predicate in a + term in the list, a new term with expanded predicate + is added to the list. + If every occurrence of the predicate could be + expanded, Complete is set to TRUE. +***************************************************************/ +{ + LIST l, newterms; + + newterms = list_Nil(); + + *Complete = TRUE; + for (l=Termlist; !list_Empty(l); l=list_Cdr(l)) { + TERM newterm; + TERM oldterm; + BOOL complete; + oldterm = list_PairSecond(list_Car(l)); + newterm = def_ApplyDefToTermOnce(Def, oldterm, FlagStore, + Precedence, &complete); + if (!complete) + *Complete = FALSE; + /* destructive part of function */ + if (newterm != NULL) { + newterms = list_Cons(list_PairCreate(NULL, newterm),newterms); + if (Destructive) { + /* Delete oldterm from Termlist */ + term_Delete(list_PairSecond(list_Car(l))); + if (list_PairFirst(list_Car(l)) != NULL) + string_StringFree(list_PairFirst(list_Car(l))); + + list_PairFree(list_Car(l)); + list_Rplaca(l, NULL); + } + } + } + Termlist = list_PointerDeleteElement(Termlist, NULL); + + if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) { + if (!list_Empty(newterms)) { + fputs("\n\nNew terms after applying definitions : \n", stdout); + for (l=newterms; !list_Empty(l); l=list_Cdr(l)) { + fputs("\n", stdout); + fol_PrettyPrint(list_PairSecond(list_Car(l))); + } + } + } + + Termlist = list_Nconc(Termlist, newterms); + return Termlist; +} + +void def_ExtractDefsFromTermlist(PROOFSEARCH Search, LIST Axioms, LIST Conj) +/************************************************************** + INPUT: A proofsearch object and 2 lists of pairs label/term. + RETURNS: None. + EFFECT: Add all found definitions to the proofsearch object. + The old list of definitions in the proofsearch object is + overwritten. +***************************************************************/ +{ + LIST l, deflist; + FLAGSTORE FlagStore; + + deflist = list_Nil(); + FlagStore = prfs_Store(Search); + + for (l=Axioms; !list_Empty(l); l=list_Cdr(l)) { + fol_NormalizeVars(list_PairSecond(list_Car(l))); /* Is needed for proper variable match ! */ + deflist = list_Nconc(deflist, + def_ExtractDefsFromTerm(list_PairSecond(list_Car(l)), + list_PairFirst(list_Car(l)))); + } + for (l=Conj; !list_Empty(l); l=list_Cdr(l)) { + fol_NormalizeVars(list_PairSecond(list_Car(l))); /* Is needed for proper variable match ! */ + deflist = list_Nconc(deflist, + def_ExtractDefsFromTerm(list_PairSecond(list_Car(l)), + list_PairFirst(list_Car(l)))); + } + for (l=deflist; !list_Empty(l); l=list_Cdr(l)) + symbol_AddProperty(term_TopSymbol(def_Predicate(list_Car(l))), ISDEF); + + prfs_SetDefinitions(Search, list_Nconc(prfs_Definitions(Search), deflist)); + + if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) { + if (!list_Empty(deflist)) { + fputs("\nFound definitions :\n", stdout); + for (l = prfs_Definitions(Search); !list_Empty(l); l = list_Cdr(l)) { + def_Print(list_Car(l)); + fputs("\n---\n", stdout); + } + } + } +} + +LIST def_FlattenWithOneDefinition(PROOFSEARCH Search, DEF Def) +/************************************************************** + INPUT: A proofsearch object and one definition. + RETURNS: The list of new definitions. + EFFECT: For every occurrence of the defined predicate among the other + definitions an expansion is attempted. + A new definition is only created if the result of the expansion is + again a definition. + The proofsearch object is not changed. +***************************************************************/ +{ + LIST newdefinitions; + FLAGSTORE FlagStore; + PRECEDENCE Precedence; + + newdefinitions = list_Nil(); + FlagStore = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + if (def_ToProve(Def) == NULL) { + LIST definitions, l; + + definitions = prfs_Definitions(Search); + + for (l = definitions; !list_Empty(l); l=list_Cdr(l)) { + DEF d; + + d = (DEF) list_Car(l); + if (d != Def) { + /* Expansion possible */ + if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) { + /* Resulting term is still a definition */ + if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) { + TERM newexpansion; + BOOL complete; + DEF newdef; + newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d), + FlagStore, Precedence, + &complete); + + newdef = def_CreateFromTerm(newexpansion, + term_Copy(def_Predicate(d)), + term_Copy(def_ToProve(d)), def_Label(d)); + newdefinitions = list_Cons(newdef, newdefinitions); + } + } + } + + } + } + return newdefinitions; +} + + +void def_FlattenWithOneDefinitionDestructive(PROOFSEARCH Search, DEF Def) +/************************************************************** + INPUT: A proofsearch object and one definition. + RETURNS: None. + EFFECT: If the definition is always applicable, every occurrence of the + defined predicate among the other definitions is expanded in place. + If the resulting term is no longer a definition, it is deleted from + the proofsearch object. + Def is deleted. + CAUTION: This function changes the list entries in the list of definitions + in the proofsearch object, so do not call it from a loop over + all definitions. +***************************************************************/ +{ + FLAGSTORE FlagStore; + PRECEDENCE Precedence; + + FlagStore = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + if (def_ToProve(Def) == NULL) { + LIST definitions, l; + + definitions = prfs_Definitions(Search); + for (l = definitions; !list_Empty(l); l = list_Cdr(l)) { + DEF d; + + d = (DEF) list_Car(l); + if (d != Def) { + /* Expansion possible */ + if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) { + /* Resulting term is still a definition */ + if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) { + TERM newexpansion; + BOOL complete; + + newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d), FlagStore, Precedence, &complete); + term_Delete(def_Expansion(d)); + def_RplacExp(d, newexpansion); + } + else { + symbol_RemoveProperty(term_TopSymbol(def_Predicate(d)), ISDEF); + def_Delete(d); + list_Rplaca(l, NULL); + } + } + } + else { + /* Remove given definition */ + list_Rplaca(l, NULL); + } + } + symbol_RemoveProperty(term_TopSymbol(def_Predicate(Def)), ISDEF); + def_Delete(Def); + definitions = list_PointerDeleteElement(definitions, NULL); + prfs_SetDefinitions(Search, definitions); + } +} + +void def_FlattenWithOneDefinitionSemiDestructive(PROOFSEARCH Search, DEF Def) +/************************************************************** + INPUT: A proofsearch object and one definition. + RETURNS: Nothing. + EFFECT: If the definition can be applied to another definition + in the search object, that definition is destructively changed. + If the resulting term is no longer a definition, it is deleted to + prevent cycles. + The applied definition Def is NOT deleted. + CAUTION: After calling this function some entries of the definitions list + in the proofsearch object may be NULL. +***************************************************************/ +{ + FLAGSTORE FlagStore; + PRECEDENCE Precedence; + + FlagStore = prfs_Store(Search); + Precedence = prfs_Precedence(Search); + + if (def_ToProve(Def) == NULL) { + LIST definitions, l; + + definitions = prfs_Definitions(Search); + for (l = definitions; !list_Empty(l); l=list_Cdr(l)) { + DEF d; + + d = (DEF) list_Car(l); + if (d != Def) { + /* Expansion possible */ + if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) { + /* Resulting term is still a definition */ + if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) { + TERM newexpansion; + BOOL complete; + + newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d), + FlagStore, Precedence, + &complete); + term_Delete(def_Expansion(d)); + def_RplacExp(d, newexpansion); + } + else { + symbol_RemoveProperty(term_TopSymbol(def_Predicate(d)), ISDEF); + def_Delete(d); + list_Rplaca(l, NULL); + } + } + } + } + } +} + +void def_FlattenDefinitionsDestructive(PROOFSEARCH Search) +/************************************************************** + INPUT: A proofsearch object. + RETURNS: None. + EFFECT: For every definition that is always applicable try to + expand the predicate in other + definitions if possible. +***************************************************************/ +{ + LIST l; + + for (l = prfs_Definitions(Search); !list_Empty(l); l=list_Cdr(l)) { + DEF d; + + d = (DEF) list_Car(l); + fol_PrettyPrintDFG(def_Predicate(d)); + if (d != NULL) + def_FlattenWithOneDefinitionSemiDestructive(Search, d); + } + prfs_SetDefinitions(Search, list_PointerDeleteElement(prfs_Definitions(Search), NULL)); +} + +LIST def_GetTermsForProof(TERM Term, TERM SubTerm, int Polarity) +/************************************************************** + INPUT: Two formulas, <Term> and <SubTerm> which must be subformula + of <Term>,an int which is the polarity of <SubTerm> in its + superterm and a list of variables <Variables>. + RETURN: A list of formulas that are used to prove the guard of Atom. + COMMENT: Helpfunction of def_FindProofFor Guard. + CAUTION: Father links must be set. Free variables may exist in terms of + return list. + Terms are copied. +***************************************************************/ +{ + TERM SuperTerm, AddToList; + SYMBOL Top; + LIST Scan1, NewList; + + term_AddFatherLinks(Term); + +#ifdef CHECK + if (!fol_CheckFormula(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_GetTermsForProof: Illegal input Term."); + misc_FinishErrorReport(); + } +#endif + + if (Term == SubTerm) + return list_Nil(); + + SuperTerm = term_Superterm(SubTerm); + Top = term_TopSymbol(SuperTerm); + NewList = list_Nil(); + AddToList = term_Null(); + + if (symbol_Equal(Top, fol_Not())) + return def_GetTermsForProof(Term, SuperTerm, -1*Polarity); + + if (symbol_Equal(Top, fol_Or()) && Polarity == 1) { + /* Get and store AddToList */ + for (Scan1 = term_ArgumentList(SuperTerm); !list_Empty(Scan1); Scan1 = list_Cdr(Scan1)) { + if (!term_HasPointerSubterm(list_Car(Scan1), SubTerm)) + NewList = list_Cons(term_Create(fol_Not(),list_List(term_Copy(list_Car(Scan1)))), NewList); + /* NewList's elements have the form not(term) */ + } + if (list_Length(NewList) == 1) { + AddToList = list_Car(NewList); + list_Delete(NewList); + } + else { + AddToList = term_Create(fol_And(), NewList); + } + return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity)); + } + if (symbol_Equal(Top, fol_And()) && Polarity == -1) { + /* Get and store AddToList */ + if (list_Length(term_ArgumentList(SuperTerm)) == 2) { + if (!term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm)) { + AddToList = term_Copy(term_FirstArgument(SuperTerm)); + } + else { + AddToList = term_Copy(term_SecondArgument(SuperTerm)); + } + } + else if (list_Length(term_ArgumentList(SuperTerm)) > 2) { + for (Scan1 = term_ArgumentList(SuperTerm); !list_Empty(Scan1); Scan1 = list_Cdr(Scan1)) { + if (!term_HasPointerSubterm(list_Car(Scan1), SubTerm)) + NewList = list_Cons(term_Copy(list_Car(Scan1)), NewList); + } + AddToList = term_Create(fol_And(), NewList); + } + else { /* Only one argument */ + AddToList = term_Copy(term_FirstArgument(SuperTerm)); + } + return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity)); + } + if (symbol_Equal(Top, fol_Implies())) { + if (term_HasPointerSubterm(term_SecondArgument(SuperTerm), SubTerm) && Polarity == 1) { + AddToList = term_Copy(term_FirstArgument(SuperTerm)); + return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity)); + } + if (term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm) && Polarity == -1) { + AddToList = term_Copy(term_SecondArgument(SuperTerm)); + AddToList = term_Create(fol_Not(), list_List(AddToList)); + return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, -1*Polarity)); + } + } + if (symbol_Equal(Top, fol_Implied())) { /* symmetric to fol_Implies */ + if (term_HasPointerSubterm(term_SecondArgument(SuperTerm), SubTerm) && Polarity == -1) { + AddToList = term_Copy(term_FirstArgument(SuperTerm)); + AddToList = term_Create(fol_Not(), list_List(AddToList)); + return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, -1*Polarity)); + } + if (term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm) && Polarity == 1) { + AddToList = term_Copy(term_SecondArgument(SuperTerm)); + return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity)); + } + } + if (fol_IsQuantifier(Top)) + return def_GetTermsForProof(Term, SuperTerm, Polarity); + + /* In all other cases, SubTerm is the top level term in which Atom occurs disjunctively */ + + return list_Nil(); +} + +BOOL def_FindProofForGuard(TERM Term, TERM Atom, TERM Guard, FLAGSTORE FlagStore, PRECEDENCE Precedence) +/************************************************************************** + INPUT: A formula Term, an atom Atom, a term Guard a flag store and a + precedence. + RETURNS: True iff a proof can be found for Guard in Term. +***************************************************************************/ +{ + BOOL LocallyTrue; + TERM ToProve, Conjecture; + LIST ArgList, FreeVars; + + ArgList = list_Nil(); + FreeVars = list_Nil(); + ToProve = term_Null(); + Conjecture = term_Copy(Term); + +#ifdef CHECK + if (!fol_CheckFormula(Term)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_FindProofForGuard: No correct formula term."); + misc_FinishErrorReport(); + } + if (!term_HasPointerSubterm(Term, Atom)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_FindProofForGuard: Illegal input."); + misc_FinishErrorReport(); + } +#endif + + ArgList = def_GetTermsForProof(Term, Atom, 1); + + if (!list_Empty(ArgList)) { + ToProve = term_Create(fol_And(), ArgList); + FreeVars = list_Nconc(fol_FreeVariables(ToProve), fol_FreeVariables(Guard)); + FreeVars = term_DeleteDuplicatesFromList(FreeVars); + term_CopyTermsInList(FreeVars); + + ArgList = list_List(term_Copy(Guard)); + ArgList = list_Cons(ToProve, ArgList); + ToProve = term_Create(fol_Implies(), ArgList); + ToProve = fol_CreateQuantifier(fol_All(), FreeVars, list_List(ToProve)); + + /* Now ToProve has the form <forall[]: A implies Guard> */ + /* puts("\n*ToProve: "); fol_PrettyPrintDFG(ToProve); */ + +#ifdef CHECK + if (!fol_CheckFormula(ToProve)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_FindProofForGuard: No correct formula ToProve."); + misc_FinishErrorReport(); + } +#endif + + LocallyTrue = cnf_HaveProof(list_Nil(), ToProve, FlagStore, Precedence); + term_Delete(ToProve); + term_Delete(Conjecture); + if (LocallyTrue) + return TRUE; + } + else { /* empty list */ + term_DeleteTermList(ArgList); + term_Delete(Conjecture); + } + + return FALSE; +} + +LIST def_ApplyDefinitionToTermList(LIST Defs, LIST Terms, + FLAGSTORE Flags, PRECEDENCE Precedence) +/************************************************************************** + INPUT: A list of definitions <Defs> and a list of pairs (Label.Formula), + the maximal number <Applics> of expansions, a flag store and a + precedence. + RETURNS: The possibly destructively changed list <Terms>. + EFFECT: In all formulas of Terms any definition of Defs is applied exactly + once if possible. + The terms are changed destructively if the expanded def_predicate + is not an equality. +**************************************************************************/ +{ + TERM ActTerm; /* Actual term in Terms */ + TERM DefPredicate; /* Actual definition predicate out of Defs */ + TERM Expansion; /* Expansion term of the definition */ + TERM Target; /* Target predicate to be replaced */ + LIST TargetList, Scan1, Scan2, Scan3; + BOOL Apply; + int Applics; + + Apply = TRUE; + TargetList = list_Nil(); + Applics = flag_GetFlagValue(Flags, flag_APPLYDEFS); + + while (Apply && Applics != 0) { + Apply = FALSE; + + for (Scan1=Defs; !list_Empty(Scan1) && Applics != 0; Scan1=list_Cdr(Scan1)) { + DefPredicate = term_Copy(def_Predicate(list_Car(Scan1))); + + /* puts("\n----\nDefPred:"); fol_PrettyPrintDFG(DefPredicate);*/ + + for (Scan2=Terms; !list_Empty(Scan2) && Applics != 0; Scan2=list_Cdr(Scan2)) { + ActTerm = list_PairSecond(list_Car(Scan2)); + TargetList = term_FindAllAtoms(ActTerm, term_TopSymbol(DefPredicate)); + term_AddFatherLinks(ActTerm); + + /* puts("\nActTerm:"); fol_PrettyPrintDFG(ActTerm);*/ + + for (Scan3=TargetList; !list_Empty(Scan3) && Applics != 0; Scan3=list_Cdr(Scan3)) { + Target = list_Car(Scan3); + cont_StartBinding(); + + /* puts("\nTarget:"); fol_PrettyPrintDFG(Target);*/ + + if (unify_Match(cont_LeftContext(), DefPredicate, Target)) { + cont_BackTrack(); + Expansion = term_Copy(def_Expansion(list_Car(Scan1))); + fol_NormalizeVarsStartingAt(ActTerm, term_MaxVar(Expansion)); + unify_Match(cont_LeftContext(), DefPredicate, Target); + + if (fol_ApplyContextToTerm(cont_LeftContext(), Expansion)) { /* Matcher applied on Expansion */ + if (!def_HasGuard(list_Car(Scan1))) { + Applics--; + Apply = TRUE; + /* puts("\n*no Guard!");*/ + term_RplacTop(Target, term_TopSymbol(Expansion)); + term_DeleteTermList(term_ArgumentList(Target)); + term_RplacArgumentList(Target, term_ArgumentList(Expansion)); + term_RplacArgumentList(Expansion, list_Nil()); + term_AddFatherLinks(ActTerm); +#ifdef CHECK + if (!fol_CheckFormula(ActTerm)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_ApplyDefinitionToTermList:"); + misc_ErrorReport(" No correct formula ActTerm."); + misc_FinishErrorReport(); + } +#endif + if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { + puts("\nApplied definition for"); + fol_PrettyPrintDFG(def_Predicate(list_Car(Scan1))); + puts("\nNew formula:"); + fol_PrettyPrintDFG(ActTerm); + } + } + else { /* check guard */ + TERM Guard; + Guard = term_Copy(def_ToProve(list_Car(Scan1))); + if (fol_ApplyContextToTerm(cont_LeftContext(), Guard)) { + cont_BackTrack(); + if (def_FindProofForGuard(ActTerm, Target,Guard, + Flags, Precedence)) { + Applics--; + Apply = TRUE; + term_RplacTop(Target, term_TopSymbol(Expansion)); + term_DeleteTermList(term_ArgumentList(Target)); + term_RplacArgumentList(Target, term_ArgumentList(Expansion)); + term_RplacArgumentList(Expansion, list_Nil()); + term_AddFatherLinks(ActTerm); +#ifdef CHECK + if (!fol_CheckFormula(ActTerm)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In def_ApplyDefinitionToTermList:"); + misc_ErrorReport(" No correct formula ActTerm"); + misc_FinishErrorReport(); + } +#endif + if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { + puts("\nApplied definition for"); + fol_PrettyPrintDFG(def_Predicate(list_Car(Scan1))); + puts("\nNew formula:"); + fol_PrettyPrintDFG(ActTerm); + } + } + } + term_Delete(Guard); + } + } + term_Delete(Expansion); + } + cont_BackTrack(); + } + list_Delete(TargetList); + } + term_Delete(DefPredicate); + } + } + return Terms; +} |