/**************************************************************/ /* ********************************************************** */ /* * * */ /* * CNF TRANSLATOR * */ /* * * */ /* * $Module: CNF * */ /* * * */ /* * 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 "cnf.h" #include "rules-inf.h" #include "rules-red.h" static TERM cnf_AntiPrenexPath(TERM, TERM); static TERM cnf_ApplyDefinitionInternOnce(TERM, TERM, TERM, TERM, BOOL*); static SYMBOL cnf_GetDualSymbol(SYMBOL symbol); static TERM cnf_IsDefinition(TERM); static void cnf_OptimizedSkolemFormula(PROOFSEARCH, TERM, char*, BOOL, TERM, LIST*, LIST*, BOOL, HASH, int); static int cnf_PredicateOccurrences(TERM, SYMBOL); static void cnf_RplacVar(TERM, LIST, LIST); static LIST cnf_SatUnit(PROOFSEARCH, LIST); static LIST cnf_SkolemFunctionFormula(TERM, LIST, LIST, PRECEDENCE); /* For every variable the depth in the current term, required for */ /* strong skolemization */ static int* cnf_VARIABLEDEPTHARRAY; /* Holds a copy of the ProofSearch--Object built by cnf_Flotter */ /* during cnf_QueryFlotter */ static PROOFSEARCH cnf_SEARCHCOPY; /* Proofsearch--Object for the function cnf_HaveProof. We need this */ /* to reduce the number of term stamps required. */ static PROOFSEARCH cnf_HAVEPROOFPS; void cnf_Init(FLAGSTORE Flags) /*************************************************************** INPUT: A flag store. RETURNS: None. SUMMARY: Initializes the CNF Module. EFFECTS: Initializes global variables. CAUTION: MUST BE CALLED BEFORE ANY OTHER CNF-FUNCTION. ***************************************************************/ { /* If strong skolemization is performed, allocate array for variable depth */ if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) cnf_VARIABLEDEPTHARRAY = (int*) memory_Malloc(sizeof(int[symbol__MAXSTANDARDVAR + 1])); else cnf_VARIABLEDEPTHARRAY = NULL; cnf_SEARCHCOPY = prfs_Create(); cnf_HAVEPROOFPS = prfs_Create(); } void cnf_Free(FLAGSTORE Flags) /************************************************************** INPUT: A flag store. RETURNS: None. SUMMARY: Frees the CNF Module. ***************************************************************/ { /* If strong skolemization is performed, free array for variable depth */ if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) { memory_Free(cnf_VARIABLEDEPTHARRAY, sizeof(int) * (symbol__NOOFSTANDARDVAR + 1)); cnf_VARIABLEDEPTHARRAY = NULL; } prfs_Delete(cnf_SEARCHCOPY); cnf_SEARCHCOPY = NULL; prfs_Delete(cnf_HAVEPROOFPS); cnf_HAVEPROOFPS = NULL; } static int cnf_GetFormulaPolarity(TERM term, TERM subterm) /********************************************************** INPUT: Two terms term and subterm where subterm is a subterm of term. RETURNS: The polarity of subterm in term. ********************************************************/ { LIST scan; TERM term1; int polterm1,bottom; bottom = vec_ActMax(); vec_Push((POINTER) 1); vec_Push(term); do { term1 = (TERM)vec_PopResult(); polterm1 = (int)vec_PopResult(); if (term1 == subterm) { vec_SetMax(bottom); return polterm1; }else if (symbol_Equal(term_TopSymbol(term1),fol_Not())) { vec_Push((POINTER) (- polterm1)); vec_Push(list_Car(term_ArgumentList(term1))); } if (symbol_Equal(term_TopSymbol(term1),fol_Exist()) || symbol_Equal(term_TopSymbol(term1),fol_All())) { vec_Push((POINTER)polterm1); vec_Push(list_Second(term_ArgumentList(term1))); } else if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) { vec_Push((POINTER) (- polterm1)); vec_Push(list_Car(term_ArgumentList(term1))); vec_Push((POINTER) polterm1); vec_Push(list_Second(term_ArgumentList(term1))); } else if (symbol_Equal(term_TopSymbol(term1),fol_Equiv())) { vec_Push(0); vec_Push(list_Car(term_ArgumentList(term1))); vec_Push(0); vec_Push(list_Second(term_ArgumentList(term1))); } else if (symbol_Equal(term_TopSymbol(term1),fol_And()) || symbol_Equal(term_TopSymbol(term1),fol_Or())) { for (scan = term_ArgumentList(term1); !list_Empty(scan); scan = list_Cdr(scan)) { vec_Push((POINTER) polterm1); vec_Push(list_Car(scan)); } } } while (bottom != vec_ActMax()); vec_SetMax(bottom); misc_StartErrorReport(); misc_ErrorReport("\n In cnf_GetFormulaPolarity: Wrong arguments !\n"); misc_FinishErrorReport(); return -2; } static BOOL cnf_ContainsDefinitionIntern(TERM TopDef, TERM Def, int Polarity, TERM* FoundPred) /********************************************************** INPUT: A term TopDef which is the top level term of the recursion. A term Def which is searched for a definition. A pointer to a term into which the predicate of the definition is stored if it is found. RETURNS: TRUE if Def contains a definition that can be converted to standard form. ********************************************************/ { /* AND / OR */ /* In these cases Def cannot be converted to standard form */ if ((symbol_Equal(term_TopSymbol(Def),fol_And()) && (Polarity == 1)) || (symbol_Equal(term_TopSymbol(Def),fol_Or()) && (Polarity == -1))) return FALSE; if (symbol_Equal(term_TopSymbol(Def), fol_And()) || symbol_Equal(term_TopSymbol(Def),fol_Or())) { /* Polarity is ok */ LIST l; for (l=term_ArgumentList(Def); !list_Empty(l); l=list_Cdr(l)) if (cnf_ContainsDefinitionIntern(TopDef, list_Car(l), Polarity, FoundPred)) return TRUE; return FALSE; } /* Quantifiers */ if (fol_IsQuantifier(term_TopSymbol(Def))) return cnf_ContainsDefinitionIntern(TopDef, term_SecondArgument(Def), Polarity, FoundPred); /* Negation */ if (symbol_Equal(term_TopSymbol(Def),fol_Not())) return cnf_ContainsDefinitionIntern(TopDef, term_FirstArgument(Def), -Polarity, FoundPred); /* Implication */ if (symbol_Equal(term_TopSymbol(Def),fol_Implies())) { if (Polarity==1) { if (cnf_ContainsDefinitionIntern(TopDef, term_FirstArgument(Def), -Polarity, FoundPred)) return TRUE; return cnf_ContainsDefinitionIntern(TopDef, term_SecondArgument(Def), Polarity, FoundPred); } return FALSE; } /* Equivalence */ if (symbol_Equal(term_TopSymbol(Def),fol_Equiv()) && (Polarity==1)) { /* Check if equivalence itself is in correct form */ TERM defpredicate; defpredicate = cnf_IsDefinition(Def); if (defpredicate != (TERM) NULL) { LIST predicate_vars, l, defpath; BOOL allquantifierfound; TERM super; int pol; /* Check if predicate occurs several times in TopDef */ /* if (cnf_PredicateOccurrences(TopDef, term_TopSymbol(defpredicate)) > 1) {} puts("\n Predicate occurs more than once."); return FALSE; */ /* Now make sure that the variables of the predicate are */ /* all--quantified and not in the scope of an exist quantifier */ /* predicate_vars = list_Copy(term_ArgumentList(defpredicate)); */ predicate_vars = term_ListOfVariables(defpredicate); predicate_vars = term_DeleteDuplicatesFromList(predicate_vars); /* So far (going bottom--up) no all-quantifier was found for */ /* a variable of the predicates' arguments */ allquantifierfound = FALSE; /* Build defpath here by going bottom up */ /* At first, list of superterms on path is top down */ defpath = list_Nil(); super = Def; while (super != (TERM) NULL) { defpath = list_Cons(super, defpath); super = term_Superterm(super); } /* No go top down and add polarities */ pol = 1; for (l=defpath; !list_Empty(l); l=list_Cdr(l)) { list_Rplaca(l, list_PairCreate((TERM) list_Car(l), (LIST) pol)); if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Not())) pol = -pol; else { if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Implies()) && (term_FirstArgument((TERM) list_Car(l)) == (TERM) list_Car(list_Cdr(l)))) pol = -pol; else if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Equiv())) pol = 0; } } /* is now a list of pairs (term, polarity) */ for (l=defpath; !list_Empty(l) && !list_Empty(predicate_vars); l=list_Cdr(l)) { LIST pair; TERM t; int p; /* Pair Term t / Polarity p */ pair = (LIST) list_Car(l); t = (TERM) list_PairFirst(pair); p = (int) list_PairSecond(pair); if (fol_IsQuantifier(term_TopSymbol(t))) { /* Variables of the predicate that are universally quantified are no problem */ if ((symbol_Equal(term_TopSymbol(t), fol_All()) && (p==1)) || (symbol_Equal(term_TopSymbol(t), fol_Exist()) && (p==-1))) { LIST scan; allquantifierfound = TRUE; for (scan=fol_QuantifierVariables(t); !list_Empty(scan); scan=list_Cdr(scan)) predicate_vars = list_DeleteElement(predicate_vars,(TERM) list_Car(scan), (BOOL (*)(POINTER,POINTER))term_Equal); } else { /* Check if allquantified variables of the predicate are in scope of an exist--quantifier */ /* We already found an all quantified variable */ if (allquantifierfound) { list_Delete(predicate_vars); list_DeletePairList(defpath); return FALSE; } else { LIST scan; /* Check if a variable of the predicate is exist--quantified */ for (scan=fol_QuantifierVariables(t); !list_Empty(scan); scan=list_Cdr(scan)) { if (term_ListContainsTerm(predicate_vars, list_Car(scan))) { list_Delete(predicate_vars); list_DeletePairList(defpath); return FALSE; } } } } } } #ifdef CHECK if (!list_Empty(predicate_vars)) { list_Delete(predicate_vars); misc_StartErrorReport(); misc_ErrorReport("\n In cnf_ContainsDefinitionIntern: Definition has free variables.\n"); misc_FinishErrorReport(); } #endif list_DeletePairList(defpath); *FoundPred = defpredicate; return TRUE; } } return FALSE; } BOOL cnf_ContainsDefinition(TERM Def, TERM* FoundPred) /********************************************************** INPUT: A term Def which is searched for a definition of a predicate. A pointer to a term into which the predicate of the definition is stored if it is found. RETURNS: TRUE if Def contains a definition that can be converted to standard form. ***********************************************************/ { BOOL result; #ifdef CHECK fol_CheckFatherLinks(Def); #endif result = cnf_ContainsDefinitionIntern(Def, Def, 1, FoundPred); #ifdef CHECK fol_CheckFatherLinks(Def); #endif return result; } static TERM cnf_IsDefinition(TERM Def) /********************************************************** INPUT: A term Def. RETURNS: The Def term where the arguments of the equivalence are exchanged iff the first one is not a predicate. **********************************************************/ { LIST l,freevars, predicatevars; #ifdef CHECK if (Def == NULL) { misc_StartErrorReport(); misc_ErrorReport("\n In cnf_IsDefinition: Empty formula.\n"); misc_FinishErrorReport(); } if (!symbol_Equal(term_TopSymbol(Def),fol_Equiv())) { misc_StartErrorReport(); misc_ErrorReport("\n In cnf_IsDefinition: Formula is no equivalence.\n"); misc_FinishErrorReport(); } #endif /* If the predicate is the second argument of the equivalence, exchange them */ if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def)))) { TERM arg1; arg1 = term_FirstArgument(Def); term_RplacFirstArgument(Def, term_SecondArgument(Def)); term_RplacSecondArgument(Def, arg1); } /* Check if the first argument is a predicate */ if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def)))) return NULL; /* Check if first argument is a predicate and not fol_Equality */ /* if (!symbol_IsPredicate(term_TopSymbol(term_FirstArgument(Def))) || symbol_Equal(term_TopSymbol(term_FirstArgument(Def)), fol_Equality()))) { return NULL; }*/ /* The free variables of the non-predicate term must occur in the predicate term */ freevars = fol_FreeVariables(term_SecondArgument(Def)); freevars = term_DeleteDuplicatesFromList(freevars); predicatevars = term_ListOfVariables(term_FirstArgument(Def)); predicatevars = term_DeleteDuplicatesFromList(predicatevars); for (l=predicatevars; !list_Empty(l); l=list_Cdr(l)) freevars = list_DeleteElement(freevars, list_Car(l), (BOOL (*)(POINTER,POINTER))term_Equal); if (!list_Empty(freevars)) { list_Delete(freevars); list_Delete(predicatevars); return NULL; } list_Delete(predicatevars); return term_FirstArgument(Def); } static BOOL cnf_ContainsPredicateIntern(TERM Target, SYMBOL Predicate, int Polarity, TERM* TargetPredicate, TERM* ToTopLevel, LIST* TargetVars, LIST* VarsForTopLevel) /********************************************************** INPUT: A term (sub--) Target A symbol Predicate which is searched in the target term. The polarity of the subterm. A pointer to the term TargetPredicate into which the found predicate term is stored. A pointer to the list TargetVars into which the variables found in the predicates' arguments are stored. A pointer to a list VarsForTopLevel into which all variables are stored that are all--quantified and can be moved to top level. RETURNS: TRUE if Formula contains the predicate for which a definition was found. ********************************************************/ { /* AND / OR */ /* In these cases the predicate (if it exists) can not be moved to a higher level */ if ((symbol_Equal(term_TopSymbol(Target),fol_And()) && Polarity == 1) || (symbol_Equal(term_TopSymbol(Target),fol_Or()) && Polarity == -1) || (symbol_Equal(term_TopSymbol(Target),fol_Implies()) && Polarity != 1) || symbol_Equal(term_TopSymbol(Target), fol_Equiv())) { TERM s; LIST l; /* Try to find Predicate in Target */ s = term_FindSubterm(Target, Predicate); if (s == NULL) return FALSE; /* Store variables found in the predicates arguments */ for (l=term_ArgumentList(s); !list_Empty(l); l = list_Cdr(l)) *TargetVars = list_Nconc(fol_FreeVariables((TERM) list_Car(l)), *TargetVars); *TargetVars = term_DeleteDuplicatesFromList(*TargetVars); /* Keep found predicate */ *TargetPredicate = s; *ToTopLevel = Target; return TRUE; } /* AND / OR continued */ if (symbol_Equal(term_TopSymbol(Target),fol_And()) || symbol_Equal(term_TopSymbol(Target),fol_Or())) { /* The polarity is ok here */ LIST l; for (l=term_ArgumentList(Target); !list_Empty(l); l = list_Cdr(l)) if (cnf_ContainsPredicateIntern((TERM) list_Car(l), Predicate, Polarity, TargetPredicate, ToTopLevel, TargetVars, VarsForTopLevel)) return TRUE; return FALSE; } /* Quantifiers */ if (fol_IsQuantifier(term_TopSymbol(Target))) { if (cnf_ContainsPredicateIntern(term_SecondArgument(Target), Predicate, Polarity, TargetPredicate, ToTopLevel, TargetVars, VarsForTopLevel)) { /* Quantifiers for free variables of the predicate should be moved to top level to make the proof easier */ if ((symbol_Equal(term_TopSymbol(Target), fol_All()) && Polarity == 1) || (symbol_Equal(term_TopSymbol(Target), fol_Exist()) && Polarity == -1)) { LIST l; /* Check for all variables found in the predicates arguments */ for (l = *TargetVars; !list_Empty(l); l=list_Cdr(l)) { if (term_ListContainsTerm(fol_QuantifierVariables(Target),list_Car(l))) *VarsForTopLevel = list_Cons(list_Car(l), *VarsForTopLevel); } } return TRUE; } return FALSE; } /* Negation */ if (symbol_Equal(term_TopSymbol(Target),fol_Not())) return cnf_ContainsPredicateIntern(term_FirstArgument(Target), Predicate, -Polarity, TargetPredicate, ToTopLevel, TargetVars, VarsForTopLevel); /* Implication */ if (symbol_Equal(term_TopSymbol(Target),fol_Implies())) { /* In this case the predicate (if it exists) can be moved to a higher level */ if (cnf_ContainsPredicateIntern(term_FirstArgument(Target), Predicate, -Polarity, TargetPredicate, ToTopLevel, TargetVars, VarsForTopLevel)) return TRUE; return cnf_ContainsPredicateIntern(term_SecondArgument(Target), Predicate, Polarity, TargetPredicate, ToTopLevel, TargetVars, VarsForTopLevel); } /* Found the predicate */ if (symbol_Equal(term_TopSymbol(Target), Predicate)) { LIST l; for (l = term_ArgumentList(Target); !list_Empty(l); l = list_Cdr(l)) *TargetVars = list_Nconc(fol_FreeVariables((TERM) list_Car(l)), *TargetVars); *TargetVars = term_DeleteDuplicatesFromList(*TargetVars); *TargetPredicate = Target; *ToTopLevel = Target; return TRUE; } /* In all other cases the predicate was not found */ return FALSE; } BOOL cnf_ContainsPredicate(TERM Target, SYMBOL Predicate, TERM* TargetPredicate, TERM* ToTopLevel, LIST* TargetVars, LIST* VarsForTopLevel) /********************************************************** INPUT: A term Target without implications. A symbol Predicate which is searched in the target term. A pointer to the predicate found in TargetTerm is recorded. A pointer to the term TargetPredicate into which the found predicate term is stored. A pointer to the list TargetVars into which the variables found in the predicates' arguments are stored. A pointer to a list VarsForTopLevel into which all variables are stored that are all--quantified and can be moved to top level. RETURNS: TRUE if Formula contains the predicate for which a definition was found. ********************************************************/ { BOOL result; #ifdef CHECK fol_CheckFatherLinks(Target); #endif result = cnf_ContainsPredicateIntern(Target, Predicate, 1, TargetPredicate, ToTopLevel, TargetVars, VarsForTopLevel); #ifdef CHECK fol_CheckFatherLinks(Target); #endif return result; } static int cnf_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 cnf_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 += cnf_PredicateOccurrences(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; } static TERM cnf_NegationNormalFormulaPath(TERM Term, TERM PredicateTerm) /********************************************************** INPUT: A term and a predicate term which is a subterm of term RETURNS: The negation normal form of the term along the path. CAUTION: The term is destructively changed. This works only if the superterm member of Term and its subterms are set. ********************************************************/ { TERM subterm, termL, term1; LIST scan; SYMBOL symbol; BOOL set; term1 = Term; while (term1 != NULL) { set = FALSE; if (symbol_Equal(term_TopSymbol(term1),fol_Not())) { subterm = term_FirstArgument(term1); if (symbol_Equal(term_TopSymbol(subterm),fol_Not())) { LIST l; term_RplacTop(term1,term_TopSymbol(term_FirstArgument(subterm))); list_Delete(term_ArgumentList(term1)); term_RplacArgumentList(term1,term_ArgumentList(term_FirstArgument(subterm))); term_Free(term_FirstArgument(subterm)); list_Delete(term_ArgumentList(subterm)); term_Free(subterm); /* Set superterm member to new superterm */ for (l=term_ArgumentList(term1); !list_Empty(l); l=list_Cdr(l)) term_RplacSuperterm(list_Car(l), term1); /* term1 weiter betrachten */ set = TRUE; } else { if (fol_IsQuantifier(term_TopSymbol(subterm))) { LIST l; symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm)); termL = term_CreateAddFather(fol_Not(), list_List(term_SecondArgument(subterm))); list_RplacSecond(term_ArgumentList(subterm), termL); term_RplacSuperterm(termL, subterm); term_RplacTop(term1,symbol); list_Delete(term_ArgumentList(term1)); term_RplacArgumentList(term1, term_ArgumentList(subterm)); for (l=term_ArgumentList(term1); !list_Empty(l); l = list_Cdr(l)) term_RplacSuperterm(list_Car(l), term1); term_RplacArgumentList(subterm, list_Nil()); term_Delete(subterm); term1 = termL; /* Next term to check is not(subterm) */ set = TRUE; } else { if (symbol_Equal(term_TopSymbol(subterm),fol_Or()) || (symbol_Equal(term_TopSymbol(subterm),fol_And()))) { LIST l; symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm)); for (scan = term_ArgumentList(subterm); !list_Empty(scan); scan = list_Cdr(scan)) { TERM new; termL = list_Car(scan); new = term_CreateAddFather(fol_Not(),list_List(termL)); list_Rplaca(scan, new); term_RplacSuperterm(new, subterm); } term_RplacTop(term1,symbol); list_Delete(term_ArgumentList(term1)); term_RplacArgumentList(term1,term_ArgumentList(subterm)); for (l = term_ArgumentList(term1); !list_Empty(l); l=list_Cdr(l)) term_RplacSuperterm(list_Car(l), term1); term_RplacArgumentList(subterm, list_Nil()); term_Delete(subterm); } } } } if (!set) { if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) if (term_HasProperSuperterm(PredicateTerm, list_Car(scan))) { term1 = list_Car(scan); set = TRUE; break; } if (!set) term1 = NULL; } } return Term; } TERM cnf_ApplyDefinitionOnce(TERM Predicate, TERM Formula, TERM TargetTerm, TERM TargetPredicate, FLAGSTORE Flags) /********************************************************* INPUT: A term Predicate which is a predicate found in a definition. A term Formula which is a term equivalent to the predicate. A term TargetTerm in which one occurrence of the predicate may be replaced by the Formula. A term TargetPredicate which is the subterm of the TargetTerm to be replaced. A flag store. RETURNS: The changed TargetTerm. *************************************************************/ { SYMBOL maxvar, maxvar_temp; LIST bound, scan; BOOL success; /* Init varcounter */ maxvar = term_MaxVar(TargetTerm); maxvar_temp = term_MaxVar(Formula); if (maxvar_temp > maxvar) maxvar = maxvar_temp; symbol_SetStandardVarCounter(maxvar); /* Find bound variables in formula for renaming them */ bound = fol_BoundVariables(Formula); for (scan=bound; !list_Empty(scan); scan=list_Cdr(scan)) { /* Bound variable in definition is already used in term */ if (term_ContainsSymbol(TargetTerm, term_TopSymbol(list_Car(scan)))) term_ExchangeVariable(Formula, term_TopSymbol(list_Car(scan)), symbol_CreateStandardVariable()); } list_Delete(bound); TargetTerm = cnf_ApplyDefinitionInternOnce(Predicate, Formula, TargetTerm, TargetPredicate,&success); if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { if (success) { fputs("\nTarget after applying def:\n", stdout); fol_PrettyPrint(TargetTerm); puts("\n"); } } return TargetTerm; } static TERM cnf_ApplyDefinitionInternOnce(TERM Predicate, TERM Formula, TERM TargetTerm, TERM TargetPredicate, BOOL* Success) /********************************************************** INPUT: A term Predicate which is equivalence to Formula and Term RETURNS: The term in which all occurrences of P(..) are replaced by Formula modulo the proper bindings CAUTION: Term is destructively changed! ***********************************************************/ { /* Quantifiers */ if (fol_IsQuantifier(term_TopSymbol(TargetTerm))) { term_RplacSecondArgument(TargetTerm, cnf_ApplyDefinitionInternOnce(Predicate, Formula, term_SecondArgument(TargetTerm), TargetPredicate, Success)); term_RplacSuperterm(term_SecondArgument(TargetTerm), TargetTerm); return TargetTerm; } /* Junctors and NOT */ if (fol_IsJunctor(term_TopSymbol(TargetTerm)) || symbol_Equal(term_TopSymbol(TargetTerm),fol_Not())) { LIST scan; for (scan=term_ArgumentList(TargetTerm); !list_Empty(scan); scan=list_Cdr(scan)) { list_Rplaca(scan, cnf_ApplyDefinitionInternOnce(Predicate, Formula, list_Car(scan), TargetPredicate, Success)); term_RplacSuperterm((TERM) list_Car(scan), TargetTerm); } return TargetTerm; } if (symbol_Equal(term_TopSymbol(TargetTerm), term_TopSymbol(Predicate))) { if (TargetTerm == TargetPredicate) { TERM result; result = Formula; cnf_RplacVar(result, term_ArgumentList(Predicate), term_ArgumentList(TargetTerm)); term_AddFatherLinks(result); term_Delete(TargetTerm); *Success = TRUE; return result; } } return TargetTerm; } static TERM cnf_RemoveEquivImplFromFormula(TERM term) /********************************************************** INPUT: A term. RETURNS: The term with replaced implications and equivalences. CAUTION: The term is destructively changed. ********************************************************/ { TERM term1,termL,termR,termLneg,termRneg; LIST scan; int bottom,pol; bottom = vec_ActMax(); vec_Push(term); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) { term_RplacTop(term1, fol_Or()); list_Rplaca(term_ArgumentList(term1), term_Create(fol_Not(), list_List(list_Car(term_ArgumentList(term1))))); }else if (symbol_Equal(term_TopSymbol(term1),fol_Equiv())) { pol = cnf_GetFormulaPolarity(term,term1); termL = (TERM)list_Car(term_ArgumentList(term1)); termR = (TERM)list_Second(term_ArgumentList(term1)); termLneg = term_Create(fol_Not(),list_List(term_Copy(termL))); termRneg = term_Create(fol_Not(),list_List(term_Copy(termR))); if (pol == 1 || pol == 0) { term_RplacTop(term1, fol_And()); list_Rplaca(term_ArgumentList(term1), term_Create(fol_Or(),list_Cons(termLneg,list_List(termR)))); list_RplacSecond(term_ArgumentList(term1),term_Create(fol_Or(),list_Cons(termRneg,list_List(termL)))); }else if (pol == -1) { term_RplacTop(term1, fol_Or()); list_Rplaca(term_ArgumentList(term1), term_Create(fol_And(),list_Cons(termLneg,list_List(termRneg)))); list_RplacSecond(term_ArgumentList(term1), term_Create(fol_And(),list_Cons(termL,list_List(termR)))); } } if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); } vec_SetMax(bottom); return term; } static TERM cnf_MovePredicateVariablesUp(TERM Term, TERM TargetPredicateTerm, LIST VarsForTopLevel) /********************************************************** INPUT: A term and a predicate term which is a subterm of term an equivalence. RETURNS: The term where the free variables of the equivalence, which must be allquantified and not in the scope of an exist quantifier, are moved to toplevel. CAUTION: The term is destructively changed. ********************************************************/ { TERM term1; LIST scan; int bottom; bottom = vec_ActMax(); vec_Push(Term); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) { TERM arg; arg = (TERM) list_Car(scan); if (term_HasProperSuperterm(TargetPredicateTerm, arg)) { if (symbol_Equal(term_TopSymbol(arg), fol_All())) { LIST predicatevarscan, quantifiervars; quantifiervars = fol_QuantifierVariables(arg); for (predicatevarscan=VarsForTopLevel; !list_Empty(predicatevarscan); predicatevarscan = list_Cdr(predicatevarscan)) quantifiervars = list_DeleteElementFree(quantifiervars, (TERM) list_Car(predicatevarscan), (BOOL (*)(POINTER,POINTER))term_Equal, (void (*)(POINTER))term_Delete); if (!list_Empty(quantifiervars)) term_RplacArgumentList(term_FirstArgument(arg), quantifiervars); else { TERM subterm; subterm = term_SecondArgument(arg); term_Free(term_FirstArgument(arg)); list_Delete(term_ArgumentList(arg)); term_Free(arg); list_Rplaca(scan, subterm); term_RplacSuperterm(subterm, term1); } } vec_Push((TERM) list_Car(scan)); } } } for (scan=VarsForTopLevel; !list_Empty(scan); scan = list_Cdr(scan)) list_Rplaca(scan, term_Copy((TERM) list_Car(scan))); if (symbol_Equal(term_TopSymbol(Term), fol_All())) { LIST vars; vars = fol_QuantifierVariables(Term); vars = list_Nconc(vars, list_Copy(VarsForTopLevel)); vars = term_DestroyDuplicatesInList(vars); term_RplacArgumentList(term_FirstArgument(Term), vars); } else { TERM newtop; newtop = fol_CreateQuantifier(fol_All(), list_Copy(VarsForTopLevel), list_List(Term)); term_RplacSuperterm(Term, newtop); Term = newtop; } vec_SetMax(bottom); return Term; } static TERM cnf_RemoveImplFromFormulaPath(TERM Term, TERM PredicateTerm) /********************************************************** INPUT: A term and a predicate term which is a subterm of term RETURNS: The term where implications along the path to PredicateTerm are replaced. CAUTION: The term is destructively changed. This works only if the superterm member of Term and its subterms are set. ********************************************************/ { TERM term1; LIST scan; int bottom; bottom = vec_ActMax(); vec_Push(Term); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (term_HasProperSuperterm(PredicateTerm, term1)) { if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) { TERM newterm; term_RplacTop(term1, fol_Or()); newterm = term_CreateAddFather(fol_Not(), list_List(list_Car(term_ArgumentList(term1)))); list_Rplaca(term_ArgumentList(term1), newterm); term_RplacSuperterm(newterm, term1); } if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); } } vec_SetMax(bottom); return Term; } static SYMBOL cnf_GetDualSymbol(SYMBOL symbol) /******************************************************** INPUT: A predefined symbol. RETURNS: The dual symbol. ********************************************************/ { SYMBOL dual; dual = symbol; if (symbol_Equal(symbol,fol_All())) dual = fol_Exist(); else if (symbol_Equal(symbol,fol_Exist())) dual = fol_All(); else if (symbol_Equal(symbol,fol_Or())) dual = fol_And(); else if (symbol_Equal(symbol,fol_And())) dual = fol_Or(); return dual; } TERM cnf_NegationNormalFormula(TERM term) /******************************************************** INPUT: A term. RETURNS: The negation normal form of the term. CAUTION: The term is destructively changed. ********************************************************/ { TERM term1,subterm,termL; LIST scan; SYMBOL symbol; int bottom; bottom = vec_ActMax(); vec_Push(term); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (symbol_Equal(term_TopSymbol(term1),fol_Not())) { subterm = (TERM)list_Car(term_ArgumentList(term1)); if (symbol_Equal(term_TopSymbol(subterm),fol_Not())) { term_RplacTop(term1,term_TopSymbol(term_FirstArgument(subterm))); list_Delete(term_ArgumentList(term1)); term_RplacArgumentList(term1,term_ArgumentList(term_FirstArgument(subterm))); term_Free(term_FirstArgument(subterm)); list_Delete(term_ArgumentList(subterm)); term_Free(subterm); vec_Push(term1); }else if (fol_IsQuantifier(term_TopSymbol(subterm))) { symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm)); termL = term_Create(fol_Not(), list_List(term_SecondArgument(subterm))); list_RplacSecond(term_ArgumentList(subterm), termL); term_RplacTop(term1,symbol); list_Delete(term_ArgumentList(term1)); term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(subterm))); term_Delete(subterm); } else if (symbol_Equal(term_TopSymbol(subterm),fol_Or()) || symbol_Equal(term_TopSymbol(subterm),fol_And())) { symbol = (SYMBOL)cnf_GetDualSymbol(term_TopSymbol(subterm)); for (scan = term_ArgumentList(subterm); !list_Empty(scan); scan = list_Cdr(scan)) { termL = (TERM)list_Car(scan); list_Rplaca(scan, term_Create(fol_Not(),list_List(termL))); } term_RplacTop(term1,symbol); list_Delete(term_ArgumentList(term1)); term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(subterm))); term_Delete(subterm); } } if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); } vec_SetMax(bottom); return term; } static TERM cnf_QuantMakeOneVar(TERM term) /************************************************************** INPUT: A term. RETURNS: The term where all quantifiers quantify over only one variable. CAUTION: The term is destructively changed. ***************************************************************/ { TERM term1,termL; SYMBOL quantor; LIST scan,varlist; int bottom; bottom = vec_ActMax(); vec_Push(term); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (fol_IsQuantifier(term_TopSymbol(term1))) { quantor = term_TopSymbol(term1); if (list_Length(term_ArgumentList(term_FirstArgument(term1))) > 1) { varlist = list_Copy(list_Cdr(term_ArgumentList(term_FirstArgument(term1)))); for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan)) { termL = term_SecondArgument(term1); term_RplacSecondArgument(term1, fol_CreateQuantifier(quantor,list_List(list_Car(scan)),list_List(termL))); } for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan)) { term_RplacArgumentList(term_FirstArgument(term1), list_PointerDeleteElement(term_ArgumentList(term_FirstArgument(term1)),list_Car(scan))); } list_Delete(varlist); } } if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); } vec_SetMax(bottom); return term; } static LIST cnf_GetSymbolList(LIST varlist) /************************************************************** INPUT: A list of variables RETURNS: The list of the symbols of the variables. ***************************************************************/ { LIST scan,result; result = list_Nil(); for (scan=varlist;!list_Empty(scan);scan=list_Cdr(scan)) result = list_Cons((POINTER)term_TopSymbol((TERM)list_Car(scan)),result); return result; } static BOOL cnf_TopIsAnd(LIST termlist) /************************************************************** INPUT: A list of terms. RETURNS: True if one term in termlist is a conjunction. ***************************************************************/ { LIST scan; for (scan=termlist;!list_Empty(scan);scan=list_Cdr(scan)) if (term_TopSymbol(list_Car(scan)) == fol_And()) return TRUE; return FALSE; } static TERM cnf_MakeOneOr(TERM term) /************************************************************** INPUT: A term. RETURNS: Takes all arguments of an or together. CAUTION: The term is destructively changed. ***************************************************************/ { LIST scan; if (symbol_Equal(term_TopSymbol(term),fol_Or())) { TERM argterm; scan=term_ArgumentList(term); while (!list_Empty(scan)) { argterm = (TERM)list_Car(scan); cnf_MakeOneOr(argterm); if (symbol_Equal(term_TopSymbol(argterm),fol_Or())) { scan = list_Cdr(scan); term_RplacArgumentList(term, list_Nconc(term_ArgumentList(argterm),list_PointerDeleteElement(term_ArgumentList(term),argterm))); term_Free(argterm); } else scan = list_Cdr(scan); } } else if (!symbol_IsPredicate(term_TopSymbol(term))) for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan)) cnf_MakeOneOr(list_Car(scan)); return term; } static TERM cnf_MakeOneOrPredicate(TERM term) /************************************************************** INPUT: A term. RETURNS: Takes all predicates and negated predicates as arguments of an or together. CAUTION: The term is destructively changed. ***************************************************************/ { LIST scan,scan1,predlist; if (cnf_TopIsAnd(term_ArgumentList(term))) { for (scan1=term_ArgumentList(term); !(list_Empty(scan1) || symbol_Equal(term_TopSymbol(list_Car(scan1)),fol_And())); scan1=list_Cdr(scan1)); if (!list_Empty(scan1)) { predlist = list_Nil(); for (scan=scan1; !list_Empty(scan); scan=list_Cdr(scan)) { if (symbol_IsPredicate(term_TopSymbol(list_Car(scan))) || fol_IsNegativeLiteral(list_Car(scan))) { predlist = list_Cons(list_Car(scan),predlist); } } for (scan=predlist;!list_Empty(scan);scan=list_Cdr(scan)) term_RplacArgumentList(term, list_PointerDeleteElement(term_ArgumentList(term),list_Car(scan))); if (!list_Empty(predlist)) term_RplacArgumentList(term, list_Nconc(predlist,term_ArgumentList(term))); } } return term; } static TERM cnf_MakeOneOrTerm(TERM term) /************************************************************** INPUT: A term. RETURNS: Takes all predicates as arguments of an or together. CAUTION: The term is destructively changed. ***************************************************************/ { return cnf_MakeOneOrPredicate(cnf_MakeOneOr(term)); } static TERM cnf_MakeOneAnd(TERM term) /************************************************************** INPUT: A term. RETURNS: Takes all arguments of an and together. CAUTION: The term is destructively changed. ***************************************************************/ { LIST scan; if (symbol_Equal(term_TopSymbol(term),fol_And())) { TERM argterm; scan=term_ArgumentList(term); while (!list_Empty(scan)) { argterm = (TERM)list_Car(scan); cnf_MakeOneAnd(argterm); if (symbol_Equal(term_TopSymbol(argterm),fol_And())) { scan = list_Cdr(scan); term_RplacArgumentList(term, list_Nconc(term_ArgumentList(argterm),list_PointerDeleteElement(term_ArgumentList(term),argterm))); term_Free(argterm); } else scan = list_Cdr(scan); } } else if (!symbol_IsPredicate(term_TopSymbol(term))) for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan)) cnf_MakeOneAnd(list_Car(scan)); return term; } static TERM cnf_MakeOneAndPredicate(TERM term) /************************************************************** INPUT: A term. RETURNS: Takes all predicates as arguments of one or together. CAUTION: The term is destructively changed. ***************************************************************/ { LIST scan,scan1,predlist; for (scan1=term_ArgumentList(term); !(list_Empty(scan1) || symbol_Equal(term_TopSymbol(list_Car(scan1)),fol_Or())); scan1=list_Cdr(scan1)); if (!list_Empty(scan1)) { /* The car of scan1 points to a term with topsymbol 'or' */ predlist = list_Nil(); for (scan=scan1; !list_Empty(scan); scan=list_Cdr(scan)) { if (symbol_IsPredicate(term_TopSymbol(list_Car(scan))) && fol_IsNegativeLiteral(list_Car(scan))) { predlist = list_Cons(list_Car(scan),predlist); } } for (scan=predlist; !list_Empty(scan); scan=list_Cdr(scan)) term_RplacArgumentList(term, list_PointerDeleteElement(term_ArgumentList(term),list_Car(scan))); if (!list_Empty(predlist)) term_RplacArgumentList(term, list_Nconc(predlist,term_ArgumentList(term))); } return term; } static TERM cnf_MakeOneAndTerm(TERM term) /************************************************************** INPUT: A term. RETURNS: Takes all predicates as arguments of an or together. CAUTION: The term is destructively changed. ***************************************************************/ { return cnf_MakeOneAndPredicate(cnf_MakeOneAnd(term)); } LIST cnf_ComputeLiteralLists(TERM Term) /********************************************************** INPUT: A term in negation normal form without quantifiers. RETURNS: The list of all literal lists corresponding to the CNF of Term. ***********************************************************/ { LIST Scan, Scan1, Scan2, Help, Result, List1, List2, NewResult; SYMBOL Symbol; Symbol = term_TopSymbol(Term); Result = list_Nil(); if (symbol_Equal(Symbol,fol_Or())) { Result = cnf_ComputeLiteralLists(list_Car(term_ArgumentList(Term))); for (Scan=list_Cdr(term_ArgumentList(Term));!list_Empty(Scan);Scan=list_Cdr(Scan)) { Help = cnf_ComputeLiteralLists(list_Car(Scan)); NewResult = list_Nil(); for (Scan1=Help;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) for (Scan2=Result;!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) { List1 = list_Car(Scan1); List2 = list_Car(Scan2); if (!list_Empty(list_Cdr(Scan2))) List1 = term_CopyTermList(List1); if (!list_Empty(list_Cdr(Scan1))) List2 = term_CopyTermList(List2); NewResult = list_Cons(term_DestroyDuplicatesInList(list_Nconc(List1,List2)), NewResult); } list_Delete(Help); list_Delete(Result); Result = NewResult; } return Result; } if (symbol_Equal(Symbol,fol_And())) { Result = cnf_ComputeLiteralLists(list_Car(term_ArgumentList(Term))); for (Scan=list_Cdr(term_ArgumentList(Term));!list_Empty(Scan);Scan=list_Cdr(Scan)) { Result = list_Nconc(cnf_ComputeLiteralLists(list_Car(Scan)), Result); } return Result; } if (symbol_Equal(Symbol,fol_Not()) || symbol_IsPredicate(Symbol)) return list_List(list_List(term_Copy(Term))); misc_StartErrorReport(); misc_ErrorReport("\n In cnf_ComputeLiteralLists: Unexpected junctor in input Formula!\n"); misc_FinishErrorReport(); return Result; } static TERM cnf_DistributiveFormula(TERM Formula) /************************************************************** INPUT: A Formula in NNF which consists only of disjunctions and conjunctions. RETURNS: The Formula where the distributivity rule is exhaustively applied and all disjunctions and the top level conjunction are grouped. CAUTION: The Formula is destructively changed. ***************************************************************/ { TERM Result; LIST Scan, Lists; Lists = cnf_ComputeLiteralLists(Formula); for (Scan= Lists; !list_Empty(Scan); Scan=list_Cdr(Scan)) list_Rplaca(Scan,term_Create(fol_Or(), list_Car(Scan))); Result = term_Create(fol_And(), Lists); term_Delete(Formula); return Result; } void cnf_FPrintClause(TERM term, FILE* file) /************************************************************** INPUT: A term and a file pointer. RETURNS: Nothing. EFFECT: Print the term which contains only disjunctions to file. The disjunctions represent a clause. ***************************************************************/ { TERM term1; LIST scan; int bottom; bottom = vec_ActMax(); vec_Push(term); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (symbol_Equal(term_TopSymbol(term1),fol_Or())) { for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); }else term_FPrint(file,term1); } fputs(".\n", file); vec_SetMax(bottom); } void cnf_FPrint(TERM term, FILE* file) /************************************************************** INPUT: A term and a file pointer. RETURNS: Nothing. EFFECT: Print the term (in negation normal form) which contains only conjunctions of disjunctions to file. The conjunctions are interpreted to represent different clauses. ***************************************************************/ { TERM term1; LIST scan; int bottom; bottom = vec_ActMax(); vec_Push(term); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (symbol_Equal(term_TopSymbol(term1),fol_And())) { for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); }else if (symbol_Equal(term_TopSymbol(term1),fol_Or()) || symbol_IsPredicate(term_TopSymbol(term1)) || symbol_Equal(term_TopSymbol(term1),fol_Not())) cnf_FPrintClause(term1,file); } vec_SetMax(bottom); } void cnf_StdoutPrint(TERM term) /************************************************************** INPUT: A term. RETURNS: Nothing. EFFECT: Print the term (in negation normal form) which contains only conjunctions of disjunctions to standard out. The conjunctions are interpreted to represent different clauses. ***************************************************************/ { LIST termlist,scan,scan1; for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) { termlist = list_Nil(); if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) || fol_IsNegativeLiteral(list_Car(scan)))) termlist = term_ArgumentList(list_Car(scan)); if (!list_Empty(termlist)) { for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1)) term_Print(list_Car(scan1)); puts("."); }else{ term_Print(list_Car(scan)); puts("."); } } } void cnf_FilePrint(TERM term, FILE* file) /************************************************************** INPUT: A term and a file. RETURNS: Nothing. EFFECT: Print the term (in negation normal form) which contains only conjunctions of disjunctions to file. The conjunctions are interpreted to represent different clauses. ***************************************************************/ { LIST termlist,scan,scan1; for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) { termlist = list_Nil(); if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) || fol_IsNegativeLiteral(list_Car(scan)))) termlist = term_ArgumentList(list_Car(scan)); if (!list_Empty(termlist)) { for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1)) term_FPrint(file,list_Car(scan1)); fputs(".\n", file); }else{ term_FPrint(file,list_Car(scan)); fputs(".\n", file); } } } void cnf_FilePrintPrefix(TERM term, FILE* file) /************************************************************** INPUT: A term and a file pointer. RETURNS: Nothing. EFFECT: Prefix Print the term (in negation normal form) which contains only conjunctions of disjunctions to file. The conjunctions are interpreted to represent different clauses. ***************************************************************/ { LIST termlist,scan,scan1; for (scan=term_ArgumentList(term);!list_Empty(scan);scan=list_Cdr(scan)) { termlist = list_Nil(); if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) || fol_IsNegativeLiteral(list_Car(scan)))) termlist = term_ArgumentList(list_Car(scan)); if (!list_Empty(termlist)) { for (scan1=termlist;!list_Empty(scan1);scan1=list_Cdr(scan1)) { term_FPrintPrefix(file,list_Car(scan1)); if (!list_Empty(list_Cdr(scan1))) fputs(" | ", file); } fputs(".\n", file); } else { term_FPrintPrefix(file,list_Car(scan)); fputs(".\n", file); } } } static LIST cnf_SubsumeClauseList(LIST clauselist) /********************************************************** INPUT: A list of clauses. RETURNS: The list of clauses without subsumed clauses. CAUTION: The list is destructively changed. ***********************************************************/ { LIST scan,result; st_INDEX stindex; CLAUSE actclause; stindex = st_IndexCreate(); result = list_Nil(); for (scan = clauselist; !list_Empty(scan); scan=list_Cdr(scan)) res_InsertClauseIndex(list_Car(scan),stindex); for (scan=clauselist; !list_Empty(scan); scan=list_Cdr(scan)) { actclause = list_Car(scan); res_DeleteClauseIndex(actclause,stindex); if (!res_BackSubWithLength(actclause,stindex)) { res_InsertClauseIndex(actclause,stindex); result = list_Cons(actclause,result); } } if (list_Length(result) != list_Length(clauselist)) { for (scan = result; !list_Empty(scan); scan=list_Cdr(scan)) clauselist = list_PointerDeleteElement(clauselist,list_Car(scan)); if (!list_Empty(result)) clause_DeleteClauseList(clauselist); }else list_Delete(clauselist); st_IndexDelete(stindex); return result; } static LIST cnf_MakeClauseList(TERM term, BOOL Sorts, BOOL Conclause, FLAGSTORE Flags, PRECEDENCE Precedence) /************************************************************** INPUT: A term in cnf and two boolean values indicating whether sorts should be generated and whether the generated clauses are Conclauses, a flag store and a precedence. RETURNS: A list of clauses with respect to term. The terms in the new clauses are the copied subterms from term. EFFECT: The flag store and the precedence are not changed, but they're needed for creating clauses. ***************************************************************/ { LIST termlist,scan,clauselist,newclauselist,delclauselist,condlist; CLAUSE clause; int j; termlist = list_Nil(); clauselist = list_Nil(); if (fol_IsTrue(term)) return clauselist; if (fol_IsNegativeLiteral(term) || symbol_IsPredicate(term_TopSymbol(term))) { termlist = list_List(term_Copy(term)); clause = clause_CreateFromLiterals(termlist, Sorts, Conclause,TRUE, Flags, Precedence); clauselist = list_Nconc(clauselist,list_List(clause)); term_StartMinRenaming(); term_Rename(clause_GetLiteralTerm(clause,0)); list_Delete(termlist); return clauselist; } delclauselist = list_Nil(); term = cnf_MakeOneAndTerm(term); if (symbol_Equal(term_TopSymbol(term), fol_And())) { for (scan=term_ArgumentList(term); !list_Empty(scan); scan=list_Cdr(scan)) { list_Rplaca(scan, cnf_MakeOneOrTerm(list_Car(scan))); termlist = list_Nil(); if (!(symbol_IsPredicate(term_TopSymbol(list_Car(scan))) || fol_IsNegativeLiteral(list_Car(scan)))) { termlist = term_CopyTermList(term_ArgumentList(list_Car(scan))); termlist = term_DestroyDuplicatesInList(termlist); } else termlist = list_List(term_Copy(list_Car(scan))); if (!list_Empty(termlist)) { clause = clause_CreateFromLiterals(termlist, Sorts, Conclause, TRUE, Flags, Precedence); term_StartMinRenaming(); for (j = 0; j < clause_Length(clause); j++) term_Rename(clause_GetLiteralTerm(clause,j)); clauselist = list_Cons(clause,clauselist); list_Delete(termlist); } } } else { /* Here the term is a disjunction, i.e. there is only one clause */ term = cnf_MakeOneOrTerm(term); if (!(symbol_IsPredicate(term_TopSymbol(term)) || fol_IsNegativeLiteral(term))) { termlist = term_CopyTermList(term_ArgumentList(term)); termlist = term_DestroyDuplicatesInList(termlist); } else termlist = list_List(term_Copy(term)); if (!list_Empty(termlist)) { clause = clause_CreateFromLiterals(termlist, Sorts, Conclause, TRUE, Flags, Precedence); term_StartMinRenaming(); for (j = 0; j < clause_Length(clause); j++) term_Rename(clause_GetLiteralTerm(clause,j)); clauselist = list_Cons(clause,clauselist); list_Delete(termlist); } } for (scan=clauselist; !list_Empty(scan); scan=list_Cdr(scan)) { condlist = cond_CondFast(list_Car(scan)); if (!list_Empty(condlist)) clause_DeleteLiterals(list_Car(scan), condlist, Flags, Precedence); list_Delete(condlist); } clauselist = cnf_SubsumeClauseList(clauselist); newclauselist = list_Nil(); while (!list_Empty(clauselist)) { clause = res_SelectLightestClause(clauselist); newclauselist = list_Nconc(newclauselist,list_List(clause)); clauselist = list_PointerDeleteElement(clauselist,clause); } list_Delete(clauselist); for (scan=newclauselist; !list_Empty(scan); scan=list_Cdr(scan)) { if (res_HasTautology(list_Car(scan))) delclauselist = list_Cons(list_Car(scan),delclauselist); } for (scan=delclauselist; !list_Empty(scan); scan=list_Cdr(scan)) newclauselist = list_PointerDeleteElement(newclauselist,list_Car(scan)); clause_DeleteClauseList(delclauselist); return newclauselist; } TERM cnf_Flatten(TERM Term, SYMBOL Symbol) /************************************************************** INPUT: A and that is assumed to be associative. RETURNS: If the top symbol of is the is flattened as long as it contains further direct subterms starting with CAUTION: The term is destructively changed. ***************************************************************/ { LIST Scan1,Scan2; if (symbol_Equal(term_TopSymbol(Term), Symbol)) { TERM Argterm; Scan1 =term_ArgumentList(Term); while (!list_Empty(Scan1)) { Argterm = (TERM)list_Car(Scan1); Scan2 = list_Cdr(Scan1); if (symbol_Equal(term_TopSymbol(Argterm),Symbol)) { cnf_Flatten(Argterm,Symbol); list_NInsert(Scan1,list_Cdr(term_ArgumentList(Argterm))); /* Be efficient ... */ list_Rplaca(Scan1,list_Car(term_ArgumentList(Argterm))); list_Free(term_ArgumentList(Argterm)); term_Free(Argterm); } Scan1 = Scan2; } } return Term; } static TERM cnf_FlattenPath(TERM Term, TERM PredicateTerm) /************************************************************** INPUT: A and that is assumed to be associative, and a predicate term which is a subterm of term RETURNS: If the top symbol of is the is flattened as long as it contains further direct subterms starting with CAUTION: The term is destructively changed. ***************************************************************/ { TERM subterm; subterm = Term; while (symbol_Equal(term_TopSymbol(subterm), fol_All())) subterm = term_SecondArgument(subterm); if (symbol_Equal(term_TopSymbol(subterm), fol_Or())) { TERM Argterm; LIST scan1; scan1 = term_ArgumentList(subterm); while (!list_Empty(scan1)) { LIST scan2; Argterm = (TERM)list_Car(scan1); scan2 = list_Cdr(scan1); if (term_HasProperSuperterm(PredicateTerm, Argterm)) { if (symbol_Equal(term_TopSymbol(Argterm),fol_Or())) { LIST l; cnf_Flatten(Argterm,fol_Or()); for (l=term_ArgumentList(Argterm); !list_Empty(l); l=list_Cdr(l)) term_RplacSuperterm((TERM) list_Car(l), subterm); list_NInsert(scan1,list_Cdr(term_ArgumentList(Argterm))); /* Be efficient ... */ list_Rplaca(scan1,list_Car(term_ArgumentList(Argterm))); list_Free(term_ArgumentList(Argterm)); term_Free(Argterm); } } scan1 = scan2; } } return Term; } static void cnf_DistrQuantorNoVarSub(TERM Term) /************************************************************** INPUT: A formula in negation normal form starting with a universal (existential) quantifier and a disjunction (conjunction) as argument. EFFECT: The Quantor is distributed if possible. CAUTION: The term is destructively changed. ***************************************************************/ { LIST Variables,Subformulas,Scan1,Scan2,Rest; TERM Subterm,Var,NewForm; SYMBOL Subtop,Top; Top = term_TopSymbol(Term); Variables = list_Copy(fol_QuantifierVariables(Term)); Subterm = term_SecondArgument(Term); Subtop = term_TopSymbol(Subterm); Subterm = cnf_Flatten(Subterm,Subtop); for (Scan1=Variables;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) { Subformulas = list_Nil(); Var = (TERM)list_Car(Scan1); for (Scan2=term_ArgumentList(Subterm);!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) if (!fol_VarOccursFreely(Var,list_Car(Scan2))) Subformulas = list_Cons(list_Car(Scan2),Subformulas); if (!list_Empty(Subformulas)) { Rest = list_NPointerDifference(term_ArgumentList(Subterm),Subformulas); if (list_Empty(list_Cdr(Rest))) { /* One subformula */ if (symbol_Equal(Top,term_TopSymbol(list_Car(Rest)))) { /* Optimization: quantifier still exist */ NewForm = (TERM)list_Car(Rest); term_RplacArgumentList(term_FirstArgument(NewForm), list_Cons((POINTER)Var,fol_QuantifierVariables(NewForm))); list_Delete(Rest); } else NewForm = fol_CreateQuantifier(Top,list_List((POINTER)Var),Rest); } else NewForm = fol_CreateQuantifier(Top,list_List((POINTER)Var),list_List(term_Create(Subtop,Rest))); term_RplacArgumentList(Subterm,list_Cons(NewForm,Subformulas)); term_RplacArgumentList(term_FirstArgument(Term), list_PointerDeleteElement(fol_QuantifierVariables(Term),(POINTER)Var)); } } if (list_Empty(fol_QuantifierVariables(Term))) { /* All variables moved inside */ term_Free(term_FirstArgument(Term)); list_Delete(term_ArgumentList(Term)); term_RplacTop(Term,Subtop); term_RplacArgumentList(Term,term_ArgumentList(Subterm)); term_Free(Subterm); } list_Delete(Variables); } static TERM cnf_AntiPrenex(TERM Term) /************************************************************** INPUT: A formula in negation normal form. RETURNS: The term after application of anti-prenexing. Quantifiers are moved inside as long as possible. CAUTION: The term is destructively changed. ***************************************************************/ { LIST Scan; SYMBOL Top; Top = term_TopSymbol(Term); if (fol_IsQuantifier(Top)) { TERM Subterm,Actterm; SYMBOL DistrSymb,Subtop; /* The junctor the respective quantifier distributes over */ Subterm = term_SecondArgument(Term); Subtop = term_TopSymbol(Subterm); if (!symbol_IsPredicate(Subtop) && !symbol_Equal(Subtop,fol_Not())) { /* Formula in NNF: No Literals or Atoms */ if (symbol_Equal(Top,fol_All())) DistrSymb = fol_And(); else DistrSymb = fol_Or(); if (fol_IsQuantifier(Subtop)) { cnf_AntiPrenex(Subterm); Subtop = term_TopSymbol(Subterm); } if (symbol_Equal(Subtop,DistrSymb)) { LIST Variables; LIST NewVars; Variables = fol_QuantifierVariables(Term); Subterm = cnf_Flatten(Subterm,DistrSymb); for (Scan=term_ArgumentList(Subterm);!list_Empty(Scan);Scan=list_Cdr(Scan)) { Actterm = (TERM)list_Car(Scan); NewVars = list_NIntersect(fol_FreeVariables(Actterm),Variables, (BOOL (*)(POINTER,POINTER))term_Equal); if (!list_Empty(NewVars)) { if (symbol_Equal(Top,term_TopSymbol(Actterm))) { /* Quantor already there */ term_CopyTermsInList(NewVars); term_RplacArgumentList(term_FirstArgument(Actterm), list_Nconc(fol_QuantifierVariables(Actterm), NewVars)); } else { term_CopyTermsInList(NewVars); list_Rplaca(Scan,fol_CreateQuantifier(Top, NewVars, list_List(Actterm))); } } } term_Delete(term_FirstArgument(Term)); /* Delete old variable list */ list_Delete(term_ArgumentList(Term)); term_RplacTop(Term,DistrSymb); term_RplacArgumentList(Term,term_ArgumentList(Subterm)); term_Free(Subterm); for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) list_Rplaca(Scan,cnf_AntiPrenex(list_Car(Scan))); } else if (!fol_IsQuantifier(Subtop)) { cnf_DistrQuantorNoVarSub(Term); for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) cnf_AntiPrenex(list_Car(Scan)); } } } else if (!symbol_Equal(Top,fol_Not()) && !symbol_IsPredicate(Top)) for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) cnf_AntiPrenex(list_Car(Scan)); return Term; } static void cnf_DistrQuantorNoVarSubPath(TERM Term, TERM PredicateTerm) /************************************************************** INPUT: A formula in negation normal form starting with a universal (existential) quantifier and a disjunction (conjunction) as argument and a predicate term which is a subterm of term. CAUTION: The term is destructively changed. ***************************************************************/ { LIST Variables,Subformulas,Scan1,Scan2,Rest; TERM Subterm,Var,NewForm; SYMBOL Subtop,Top; /*fputs("\nAN0:\t",stdout);term_Print(Term);*/ Top = term_TopSymbol(Term); Variables = list_Copy(fol_QuantifierVariables(Term)); Subterm = term_SecondArgument(Term); Subtop = term_TopSymbol(Subterm); Subterm = cnf_Flatten(Subterm,Subtop); /*fputs("\nAN1:\t",stdout);term_Print(Subterm);*/ for (Scan1=Variables;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) { Subformulas = list_Nil(); Var = (TERM)list_Car(Scan1); /* Find subterms in which the variable does not occur freely */ for (Scan2=term_ArgumentList(Subterm);!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) if (!fol_VarOccursFreely(Var,list_Car(Scan2))) Subformulas = list_Cons(list_Car(Scan2),Subformulas); if (!list_Empty(Subformulas)) { /* Rest is the list of those subterms where the variable does occur freely */ Rest = list_NPointerDifference(term_ArgumentList(Subterm),Subformulas); if (list_Empty(list_Cdr(Rest))) { /* One subformula */ if (symbol_Equal(Top,term_TopSymbol(list_Car(Rest)))) { /* Optimization: quantifier still exist */ NewForm = (TERM)list_Car(Rest); /* Move one variable down */ term_RplacArgumentList(term_FirstArgument(NewForm), list_Cons((POINTER)Var,fol_QuantifierVariables(NewForm))); list_Delete(Rest); } else { NewForm = fol_CreateQuantifierAddFather(Top,list_List((POINTER)Var), Rest); } } else { TERM t; t = term_CreateAddFather(Subtop,Rest); NewForm = fol_CreateQuantifierAddFather(Top,list_List((POINTER)Var),list_List(t)); } if (term_HasProperSuperterm(PredicateTerm, NewForm)) NewForm = cnf_AntiPrenexPath(NewForm, PredicateTerm); term_RplacArgumentList(Subterm,list_Cons(NewForm,Subformulas)); term_RplacSuperterm(NewForm, Subterm); term_RplacArgumentList(term_FirstArgument(Term), list_PointerDeleteElement(fol_QuantifierVariables(Term),(POINTER)Var)); } } if (list_Empty(fol_QuantifierVariables(Term))) { /* All variables moved inside */ LIST l; term_Free(term_FirstArgument(Term)); list_Delete(term_ArgumentList(Term)); term_RplacTop(Term,Subtop); term_RplacArgumentList(Term,term_ArgumentList(Subterm)); term_Free(Subterm); for (l=term_ArgumentList(Term); !list_Empty(l); l=list_Cdr(l)) term_RplacSuperterm((TERM) list_Car(l), Term); } list_Delete(Variables); } static TERM cnf_AntiPrenexPath(TERM Term, TERM PredicateTerm) /************************************************************** INPUT: A formula in negation normal form and a predicate term which is a subterm of term. RETURNS: The term after application of anti-prenexing. Quantifiers are moved inside along the path as long as possible. CAUTION: The term is destructively changed. ***************************************************************/ { LIST Scan; SYMBOL Top; Top = term_TopSymbol(Term); if (fol_IsQuantifier(Top)) { TERM Subterm,Actterm; SYMBOL DistrSymb,Subtop; /* The junctor the respective quantifier distributes over */ Subterm = term_SecondArgument(Term); Subtop = term_TopSymbol(Subterm); if (!symbol_Equal(Subtop,fol_Not()) && !symbol_IsPredicate(Subtop)) { /* No Literals or Atoms */ if (symbol_Equal(Top,fol_All())) DistrSymb = fol_And(); else DistrSymb = fol_Or(); if (fol_IsQuantifier(Subtop)) { cnf_AntiPrenexPath(Subterm, PredicateTerm); Subtop = term_TopSymbol(Subterm); } if (symbol_Equal(Subtop,DistrSymb)) { LIST Variables; LIST NewVars; Variables = fol_QuantifierVariables(Term); Subterm = cnf_Flatten(Subterm,DistrSymb); term_AddFatherLinks(Subterm); /* for (l=term_ArgumentList(Subterm); !list_Empty(l); l=list_Cdr(l)) term_RplacSuperterm((TERM) list_Car(l), Subterm); */ for (Scan=term_ArgumentList(Subterm);!list_Empty(Scan);Scan=list_Cdr(Scan)) { Actterm = (TERM)list_Car(Scan); NewVars = list_NIntersect(fol_FreeVariables(Actterm),Variables, (BOOL (*)(POINTER,POINTER))term_Equal); if (!list_Empty(NewVars)) { if (symbol_Equal(Top,term_TopSymbol(Actterm))) { /* Quantor already there */ term_CopyTermsInList(NewVars); term_RplacArgumentList(term_FirstArgument(Actterm), list_Nconc(fol_QuantifierVariables(Actterm), NewVars)); } else { term_CopyTermsInList(NewVars); list_Rplaca(Scan,fol_CreateQuantifierAddFather(Top, NewVars, list_List(Actterm))); } } } term_Delete(term_FirstArgument(Term)); /* Delete old variable list */ list_Delete(term_ArgumentList(Term)); term_RplacTop(Term,DistrSymb); term_RplacArgumentList(Term,term_ArgumentList(Subterm)); term_Free(Subterm); term_AddFatherLinks(Term); for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) { term_RplacSuperterm((TERM) list_Car(Scan), Term); if (term_HasPointerSubterm((TERM) list_Car(Scan), PredicateTerm)) { puts("\ncheck1"); list_Rplaca(Scan,cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm)); term_RplacSuperterm((TERM) list_Car(Scan), Term); } } } else if (!fol_IsQuantifier(Subtop)) { cnf_DistrQuantorNoVarSubPath(Term, PredicateTerm); for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) { if (term_HasPointerSubterm(list_Car(Scan), PredicateTerm)) cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm); } } } } else if (!symbol_Equal(Top,fol_Not()) && !symbol_IsPredicate(Top)) for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) if (term_HasProperSuperterm(PredicateTerm, (TERM) list_Car(Scan))) cnf_AntiPrenexPath(list_Car(Scan), PredicateTerm); term_AddFatherLinks(Term); return Term; } static TERM cnf_RemoveTrivialOperators(TERM Term) /************************************************************** INPUT: A formula. RETURNS: The formula after removal of "or" and "and" with only one argument CAUTION: The term is destructively changed. ***************************************************************/ { SYMBOL Top; LIST Scan; Top = term_TopSymbol(Term); if (symbol_IsPredicate(Top)) return Term; if ((symbol_Equal(Top,fol_And()) || symbol_Equal(Top,fol_Or())) && list_Empty(list_Cdr(term_ArgumentList(Term)))) { TERM Result; Result = term_FirstArgument(Term); term_RplacSuperterm(Result, term_Superterm(Term)); list_Delete(term_ArgumentList(Term)); term_Free(Term); return cnf_RemoveTrivialOperators(Result); } for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) { list_Rplaca(Scan,cnf_RemoveTrivialOperators(list_Car(Scan))); term_RplacSuperterm((TERM) list_Car(Scan), Term); } return Term; } static TERM cnf_SimplifyQuantors(TERM Term) /************************************************************** INPUT: A formula. RETURNS: The formula after removal of bindings of variables that don't occur in the respective subformula and possible mergings of quantors CAUTION: The term is destructively changed. ***************************************************************/ { SYMBOL Top; LIST Scan; Top = term_TopSymbol(Term); if (symbol_IsPredicate(Top) || symbol_Equal(Top,fol_Varlist())) return Term; if (fol_IsQuantifier(Top)) { LIST Vars; TERM Var,Subterm,Aux; Vars = list_Nil(); Subterm = term_SecondArgument(Term); while (symbol_Equal(term_TopSymbol(Subterm),Top)) { term_RplacArgumentList(term_FirstArgument(Term), list_Nconc(fol_QuantifierVariables(Term),fol_QuantifierVariables(Subterm))); term_Free(term_FirstArgument(Subterm)); Aux = term_SecondArgument(Subterm); list_Delete(term_ArgumentList(Subterm)); term_Free(Subterm); list_Rplaca(list_Cdr(term_ArgumentList(Term)),Aux); Subterm = Aux; } for (Scan=fol_QuantifierVariables(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) { Var = (TERM)list_Car(Scan); if (!fol_VarOccursFreely(Var,Subterm)) Vars = list_Cons(Var,Vars); } if (!list_Empty(Vars)) { Subterm = term_FirstArgument(Term); term_RplacArgumentList(Subterm,list_NPointerDifference(term_ArgumentList(Subterm),Vars)); term_DeleteTermList(Vars); if (list_Empty(term_ArgumentList(Subterm))) { Subterm = term_SecondArgument(Term); term_Delete(term_FirstArgument(Term)); list_Delete(term_ArgumentList(Term)); term_Free(Term); return cnf_SimplifyQuantors(Subterm); } } } for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) list_Rplaca(Scan,cnf_SimplifyQuantors(list_Car(Scan))); return Term; } TERM cnf_RemoveTrivialAtoms(TERM Term) /************************************************************** INPUT: A formula. RETURNS: The formula where occurrences of the atoms "true" and "false" are propagated and eventually removed. CAUTION: The term is destructively changed. ***************************************************************/ { SYMBOL Top,Subtop; LIST Scan; TERM Result; BOOL Update; if (!term_IsComplex(Term)) return Term; Top = term_TopSymbol(Term); Update = FALSE; if (symbol_Equal(Top,fol_And())) { Scan = term_ArgumentList(Term); while (!list_Empty(Scan)) { Result = cnf_RemoveTrivialAtoms(list_Car(Scan)); Subtop = term_TopSymbol(Result); if (symbol_Equal(Subtop,fol_True())) Update = TRUE; else if (symbol_Equal(Subtop,fol_False())) { term_RplacTop(Term,fol_False()); term_DeleteTermList(term_ArgumentList(Term)); term_RplacArgumentList(Term,list_Nil()); return Term; } Scan = list_Cdr(Scan); } if (Update) { term_RplacArgumentList(Term,fol_DeleteTrueTermFromList(term_ArgumentList(Term))); if (list_Empty(term_ArgumentList(Term))) { term_RplacTop(Term,fol_True()); return Term; } } } else if (symbol_Equal(Top,fol_Or())) { Scan = term_ArgumentList(Term); while (!list_Empty(Scan)) { Result = cnf_RemoveTrivialAtoms(list_Car(Scan)); Subtop = term_TopSymbol(Result); if (symbol_Equal(Subtop,fol_False())) Update = TRUE; else if (symbol_Equal(Subtop,fol_True())) { term_RplacTop(Term,fol_True()); term_DeleteTermList(term_ArgumentList(Term)); term_RplacArgumentList(Term,list_Nil()); return Term; } Scan = list_Cdr(Scan); } if (Update) { term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term))); if (list_Empty(term_ArgumentList(Term))) { term_RplacTop(Term,fol_False()); return Term; } } } else if (fol_IsQuantifier(Top) || symbol_Equal(Top,fol_Not())) { if (fol_IsQuantifier(Top)) Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term)); else Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term)); Subtop = term_TopSymbol(Result); if ((symbol_Equal(Subtop,fol_False()) && symbol_Equal(Top,fol_Not())) || (symbol_Equal(Subtop,fol_True()) && fol_IsQuantifier(Top))) { term_RplacTop(Term,fol_True()); term_DeleteTermList(term_ArgumentList(Term)); term_RplacArgumentList(Term,list_Nil()); return Term; } else if ((symbol_Equal(Subtop,fol_True()) && symbol_Equal(Top,fol_Not())) || (symbol_Equal(Subtop,fol_False()) && fol_IsQuantifier(Top))) { term_RplacTop(Term,fol_False()); term_DeleteTermList(term_ArgumentList(Term)); term_RplacArgumentList(Term,list_Nil()); return Term; } } else if (symbol_Equal(Top,fol_Implies())) { Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term)); Subtop = term_TopSymbol(Result); if (symbol_Equal(Subtop,fol_False())) { term_RplacTop(Term,fol_True()); term_DeleteTermList(term_ArgumentList(Term)); term_RplacArgumentList(Term,list_Nil()); return Term; } else if (symbol_Equal(Subtop,fol_True())) { term_Delete(Result); Result = term_SecondArgument(Term); list_Delete(term_ArgumentList(Term)); term_RplacTop(Term,term_TopSymbol(Result)); term_RplacArgumentList(Term,term_ArgumentList(Result)); term_Free(Result); return cnf_RemoveTrivialAtoms(Term); } Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term)); Subtop = term_TopSymbol(Result); if (symbol_Equal(Subtop,fol_True())) { term_RplacTop(Term,fol_True()); term_DeleteTermList(term_ArgumentList(Term)); term_RplacArgumentList(Term,list_Nil()); return Term; } else if (symbol_Equal(Subtop,fol_False())) { term_RplacTop(Term,fol_Not()); term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term))); } } else if (symbol_Equal(Top,fol_Equiv())) { Result = cnf_RemoveTrivialAtoms(term_FirstArgument(Term)); Subtop = term_TopSymbol(Result); if (symbol_Equal(Subtop,fol_False())) { term_RplacTop(Term,fol_Not()); term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term))); if (list_Empty(term_ArgumentList(Term))) { term_RplacTop(Term, fol_True()); return Term; } return cnf_RemoveTrivialAtoms(Term); } else if (symbol_Equal(Subtop,fol_True())) { term_Delete(Result); Result = term_SecondArgument(Term); list_Delete(term_ArgumentList(Term)); term_RplacTop(Term,term_TopSymbol(Result)); term_RplacArgumentList(Term,term_ArgumentList(Result)); term_Free(Result); return cnf_RemoveTrivialAtoms(Term); } Result = cnf_RemoveTrivialAtoms(term_SecondArgument(Term)); Subtop = term_TopSymbol(Result); if (symbol_Equal(Subtop,fol_False())) { term_RplacTop(Term,fol_Not()); term_RplacArgumentList(Term,fol_DeleteFalseTermFromList(term_ArgumentList(Term))); } else if (symbol_Equal(Subtop,fol_True())) { term_Delete(Result); Result = term_FirstArgument(Term); list_Delete(term_ArgumentList(Term)); term_RplacTop(Term,term_TopSymbol(Result)); term_RplacArgumentList(Term,term_ArgumentList(Result)); term_Free(Result); } } return Term; } TERM cnf_ObviousSimplifications(TERM Term) /************************************************************** INPUT: A formula. RETURNS: The formula after performing the following simplifications: - remove "or" and "and" with only one argument - remove bindings of variables that don't occur in the respective subformula - merge quantors CAUTION: The term is destructively changed. ***************************************************************/ { Term = cnf_RemoveTrivialAtoms(Term); Term = cnf_RemoveTrivialOperators(Term); Term = cnf_SimplifyQuantors(Term); return Term; } /* EK: warum wird Term zurueckgegeben, wenn er destruktiv geaendert wird??? */ static TERM cnf_SkolemFormula(TERM Term, PRECEDENCE Precedence, LIST* Symblist) /************************************************************** INPUT: A formula in negation normal form, a precedence and pointer to a list used as return value. RETURNS: The skolemized term and the list of introduced Skolem functions. CAUTION: The term is destructively changed. The precedence of the new Skolem functions is set in . ***************************************************************/ { SYMBOL Top,SkolemSymbol; TERM Subterm,SkolemTerm; LIST Varlist,Scan; NAT Arity; Top = term_TopSymbol(Term); if (fol_IsQuantifier(term_TopSymbol(Term))) { if (symbol_Equal(Top,fol_All())) { 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)); term_Free(Subterm); return cnf_SkolemFormula(Term, Precedence, Symblist); } else { /* exist quantifier */ Varlist = fol_FreeVariables(Term); Arity = list_Length(Varlist); for (Scan=fol_QuantifierVariables(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) { SkolemSymbol = symbol_CreateSkolemFunction(Arity, Precedence); *Symblist = list_Cons((POINTER)SkolemSymbol, *Symblist); SkolemTerm = term_Create(SkolemSymbol,Varlist); /* Caution: Sharing of Varlist ! */ fol_ReplaceVariable(term_SecondArgument(Term),term_TopSymbol(list_Car(Scan)),SkolemTerm); term_Free(SkolemTerm); } list_Delete(Varlist); 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)); term_Free(Subterm); return cnf_SkolemFormula(Term, Precedence, Symblist); } } else if (symbol_Equal(Top,fol_And()) || symbol_Equal(Top,fol_Or())) for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) cnf_SkolemFormula(list_Car(Scan), Precedence, Symblist); return Term; } static TERM cnf_Cnf(TERM Term, PRECEDENCE Precedence, LIST* Symblist) /************************************************************** INPUT: A formula, a precedence and a pointer to a list of symbols used as return value. RETURNS: The term is transformed to conjunctive normal form. EFFECT: The term is destructively changed and not normalized. The precedence of new Skolem symbols is set in . ***************************************************************/ { /* Necessary because ren_Rename crashes if a e.g. and() has only one argument */ Term = cnf_ObviousSimplifications(Term); term_AddFatherLinks(Term); Term = ren_Rename(Term, Precedence, Symblist, FALSE, FALSE); Term = cnf_RemoveEquivImplFromFormula(Term); Term = cnf_NegationNormalFormula(Term); Term = cnf_SkolemFormula(cnf_AntiPrenex(Term), Precedence, Symblist); Term = cnf_DistributiveFormula(Term); return Term; } static LIST cnf_GetUsedTerms(CLAUSE C, PROOFSEARCH Search, HASH InputClauseToTermLabellist) /************************************************************** INPUT: RETURNS: ***************************************************************/ { LIST UsedTerms, Used2, Scan; UsedTerms = list_Copy(hsh_Get(InputClauseToTermLabellist, C)); UsedTerms = cnf_DeleteDuplicateLabelsFromList(UsedTerms); if (!list_Empty(UsedTerms)) return UsedTerms; for (Scan = clause_ParentClauses(C); !list_Empty(Scan); Scan = list_Cdr(Scan)) { CLAUSE P; int ClauseNumber; ClauseNumber = (int) list_Car(Scan); P = clause_GetNumberedCl(ClauseNumber, prfs_WorkedOffClauses(Search)); if (P == NULL) { P = clause_GetNumberedCl(ClauseNumber, prfs_UsableClauses(Search)); if (P == NULL) P = clause_GetNumberedCl(ClauseNumber, prfs_DocProofClauses(Search)); } Used2 = cnf_GetUsedTerms(P, Search, InputClauseToTermLabellist); UsedTerms = list_Nconc(UsedTerms, Used2); } return UsedTerms; } static BOOL cnf_HaveProofOptSkolem(PROOFSEARCH Search, TERM topterm, char* toplabel, TERM term2, LIST* UsedTerms, LIST* Symblist, HASH InputClauseToTermLabellist) /************************************************************** INPUT: RETURNS: ??? EK ***************************************************************/ { LIST ConClauses, EmptyClauses; LIST scan; BOOL found; LIST Usables; FLAGSTORE Flags; PRECEDENCE Precedence; Flags = prfs_Store(Search); Precedence = prfs_Precedence(Search); ConClauses = list_Nil(); found = FALSE; /* List of clauses from term2 */ term_AddFatherLinks(term2); term2 = cnf_Cnf(term2, Precedence, Symblist); Usables = cnf_MakeClauseList(term2, FALSE, FALSE, Flags, Precedence); term_Delete(term2); for (scan=Usables; !list_Empty(scan); scan = list_Cdr(scan)) { clause_SetFlag(list_Car(scan), CONCLAUSE); if (flag_GetFlagValue(Flags, flag_DOCPROOF)) { #ifdef CHECK hsh_Check(InputClauseToTermLabellist); #endif hsh_Put(InputClauseToTermLabellist, list_Car(scan), toplabel); #ifdef CHECK_CNF fputs("\nUsable : ", stdout); clause_Print(list_Car(scan)); printf(" Label %s", toplabel); #endif } } EmptyClauses = cnf_SatUnit(Search, Usables); if (!list_Empty(EmptyClauses)) { found = TRUE; #ifdef CHECK_CNF fputs("\nHaveProof : Empty Clause : ", stdout); clause_Print((CLAUSE) list_Car(EmptyClauses)); putchar('\n'); #endif if (flag_GetFlagValue(Flags, flag_DOCPROOF)) *UsedTerms = list_Nconc(*UsedTerms, cnf_GetUsedTerms((CLAUSE) list_Car(EmptyClauses), Search, InputClauseToTermLabellist)); EmptyClauses = list_PointerDeleteDuplicates(EmptyClauses); clause_DeleteClauseList(EmptyClauses); } /* Removing ConClauses from UsablesIndex */ ConClauses = list_Copy(prfs_UsableClauses(Search)); for (scan = ConClauses; !list_Empty(scan); scan = list_Cdr(scan)) if (flag_GetFlagValue(Flags, flag_DOCPROOF)) prfs_MoveUsableDocProof(Search, (CLAUSE) list_Car(scan)); else prfs_DeleteUsable(Search, (CLAUSE) list_Car(scan)); list_Delete(ConClauses); return found; } BOOL cnf_HaveProof(LIST TermList, TERM ToProve, FLAGSTORE InputFlags, PRECEDENCE InputPrecedence) /************************************************************** INPUT: A list of terms, a term to prove, a flag store and a precedence. The arguments are not changed. RETURNS: True if the termlist implies ToProve CAUTION: All terms are copied. ***************************************************************/ { PROOFSEARCH search; LIST scan, usables, symblist, emptyclauses; BOOL found; FLAGSTORE Flags; PRECEDENCE Precedence; /* Use global PROOFSEARCH object to avoid stamp overflow */ search = cnf_HAVEPROOFPS; usables = symblist = list_Nil(); /* Initialize search object's flag store */ Flags = prfs_Store(search); flag_CleanStore(Flags); flag_InitFlotterSubproofFlags(InputFlags, Flags); /* Initialize search object's precedence */ Precedence = prfs_Precedence(search); symbol_TransferPrecedence(InputPrecedence, Precedence); /* Build list of clauses from the termlist */ for (scan=TermList; !list_Empty(scan); scan=list_Cdr(scan)) { TERM t; t = term_Copy(list_Car(scan)); t = cnf_Cnf(t, Precedence, &symblist); usables = list_Nconc(cnf_MakeClauseList(t,FALSE,FALSE,Flags,Precedence), usables); term_Delete(t); } /* Build clauses from negated term to prove */ ToProve = term_Create(fol_Not(), list_List(term_Copy(ToProve))); term_AddFatherLinks(ToProve); ToProve = cnf_Cnf(ToProve, Precedence, &symblist); usables = list_Nconc(cnf_MakeClauseList(ToProve,FALSE,FALSE,Flags,Precedence), usables); term_Delete(ToProve); /* SatUnit requires the CONCLAUSE flag */ for (scan=usables;!list_Empty(scan); scan = list_Cdr(scan)) clause_SetFlag(list_Car(scan), CONCLAUSE); emptyclauses = cnf_SatUnit(search, usables); if (!list_Empty(emptyclauses)) { found = TRUE; emptyclauses = list_PointerDeleteDuplicates(emptyclauses); clause_DeleteClauseList(emptyclauses); } else found = FALSE; prfs_Clean(search); symbol_DeleteSymbolList(symblist); return found; } static void cnf_RplacVarsymbFunction(TERM term, SYMBOL varsymb, TERM function) /********************************************************** INPUT: A term, a variable symbol and a function. EFFECT: The variable with the symbol varsymb in the term is replaced by the function function. CAUTION: The term is destructively changed. ***********************************************************/ { int bottom; TERM term1; LIST scan; bottom = vec_ActMax(); vec_Push(term); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (symbol_Equal(term_TopSymbol(term1),varsymb)) { term_RplacTop(term1,term_TopSymbol(function)); term_RplacArgumentList(term1,term_CopyTermList(term_ArgumentList(function))); }else if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); } vec_SetMax(bottom); } static void cnf_RplacVar(TERM Term, LIST Varlist, LIST Termlist) /********************************************************** INPUT: A term,a variable symbol and a function. RETURNS: The variable with the symbol varsymb in the term is replaced by the function function. CAUTION: The term is destructively changed. ***********************************************************/ { int bottom; TERM term1; LIST scan,scan2; bottom = vec_ActMax(); vec_Push(Term); while (bottom != vec_ActMax()) { term1 = vec_PopResult(); if (symbol_IsVariable(term_TopSymbol(term1))) { BOOL done; done = FALSE; for (scan=Varlist, scan2=Termlist; !list_Empty(scan) && !done; scan = list_Cdr(scan), scan2 = list_Cdr(scan2)) { if (symbol_Equal(term_TopSymbol(term1),term_TopSymbol(list_Car(scan)))) { term_RplacTop(term1,term_TopSymbol((TERM) list_Car(scan2))); term_RplacArgumentList(term1, term_CopyTermList(term_ArgumentList(list_Car(scan2)))); done = TRUE; } } } else if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); } vec_SetMax(bottom); } static TERM cnf_MakeSkolemFunction(LIST varlist, PRECEDENCE Precedence) /************************************************************** INPUT: A list of variables and a precedence. RETURNS: The new term oskf... (oskc...) which is a function with varlist as arguments. EFFECT: The precedence of the new Skolem function is set in . ***************************************************************/ { TERM term; SYMBOL skolem; skolem = symbol_CreateSkolemFunction(list_Length(varlist), Precedence); term = term_Create(skolem, term_CopyTermList(varlist)); return term; } static void cnf_PopAllQuantifier(TERM term) /******************************************************** INPUT: A term whose top symbol is fol_all. RETURNS: Nothing. EFFECT: Removes the quantifier ********************************************************/ { TERM SubTerm; LIST VarList; #ifdef CHECK if (!symbol_Equal(term_TopSymbol(term), fol_All())) { misc_StartErrorReport(); misc_ErrorReport("\n In cnf_PopAllQuantifier: Top symbol is not fol_All !\n"); misc_FinishErrorReport(); } #endif VarList = term_ArgumentList(term_FirstArgument(term)); term_DeleteTermList(VarList); term_Free(term_FirstArgument(term)); SubTerm = term_SecondArgument(term); list_Delete(term_ArgumentList(term)); term_RplacTop(term,term_TopSymbol(SubTerm)); term_RplacArgumentList(term,term_ArgumentList(SubTerm)); term_Free(SubTerm); } static TERM cnf_QuantifyAndNegate(TERM term, LIST VarList, LIST FreeList) /**************************************************************** INPUT: A term, a list of variables to be exist-quantified, a list of variables to be all-quantified RETURNS: not(forall[FreeList](exists[VarList](term))) MEMORY: The term, the lists and their arguments are copied. ***************************************************************/ { TERM Result; TERM TermCopy; LIST VarListCopy; LIST FreeListCopy; TermCopy = term_Copy(term); VarListCopy = term_CopyTermList(VarList); Result = fol_CreateQuantifier(fol_Exist(),VarListCopy,list_List(TermCopy)); FreeListCopy = list_Nil(); FreeList = fol_FreeVariables(Result); if (!list_Empty(FreeList)) { FreeListCopy = term_CopyTermList(FreeList); list_Delete(FreeList); Result = fol_CreateQuantifier(fol_All(), FreeListCopy, list_List(Result)); } Result = term_Create(fol_Not(), list_List(Result)); return Result; } static TERM cnf_MoveProvedTermToTopLevel(TERM Term, TERM Term1, TERM Proved, LIST VarList, LIST FreeList, PRECEDENCE Precedence) /******************************************************************** INPUT: A top-level term, which must be a conjunction, a subterm of , a subterm of , a list of existence quantified variables , a list of free variables and a precedence. is of the form exists[...](t1 and t2 and ... and Proved and ..) RETURNS: A new term, where is removed from the arguments of . EFFECT: The precedence of new Skolem functions is set in *******************************************************************/ { TERM termR; TERM skolemfunction; SYMBOL varsymb; LIST scan; termR = term_SecondArgument(Term1); /* t1 and t2 and ... and Proved ... */ term_RplacArgumentList(termR, list_PointerDeleteElement(term_ArgumentList(termR), Proved)); if (list_Length(term_ArgumentList(termR)) < 2) { TERM termRL = term_FirstArgument(termR); /* t1 */ list_Delete(term_ArgumentList(termR)); term_RplacTop(termR, term_TopSymbol(termRL)); term_RplacArgumentList(termR,term_ArgumentList(termRL)); term_Free(termRL); } for (scan = VarList; scan != list_Nil(); scan = list_Cdr(scan)) { varsymb = term_TopSymbol(list_Car(scan)); skolemfunction = cnf_MakeSkolemFunction(FreeList, Precedence); cnf_RplacVarsymbFunction(termR,varsymb,skolemfunction); cnf_RplacVarsymbFunction(Proved,varsymb,skolemfunction); term_Delete(skolemfunction); } if (!list_Empty(FreeList)) { Proved = fol_CreateQuantifier(fol_All(), term_CopyTermList(FreeList), list_List(Proved)); if (list_Length(FreeList) > 1) Proved = cnf_QuantMakeOneVar(Proved); } term_Delete(term_FirstArgument(Term1)); /* Variables of "exists" */ list_Delete(term_ArgumentList(Term1)); term_RplacTop(Term1,term_TopSymbol(termR)); term_RplacArgumentList(Term1,term_ArgumentList(termR)); term_Free(termR); term_RplacArgumentList(Term, list_Cons(Proved, term_ArgumentList(Term))); return Proved; } static void cnf_Skolemize(TERM Term, LIST FreeList, PRECEDENCE Precedence) /******************************************************** INPUT: A existence quantified term, the list of free variables and a precedence. RETURNS: Nothing. EFFECT: The term is destructively changed, i.e. the existence quantifier is removed by skolemization. The precedence of new Skolem functions is set in . *********************************************************/ { LIST exlist; TERM subterm; LIST symblist; symblist = list_Nil(); exlist = cnf_GetSymbolList(term_ArgumentList(term_FirstArgument(Term))); 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)); term_Free(subterm); symblist = cnf_SkolemFunctionFormula(Term, FreeList, exlist, Precedence); list_Delete(exlist); list_Delete(symblist); } static LIST cnf_FreeVariablesBut(TERM Term, LIST Symbols) /******************************************************** INPUT: A term and a list of symbols RETURNS: A list of all free variable terms in Term whose symbols are not in Symbols *********************************************************/ { LIST follist, Scan; follist = fol_FreeVariables(Term); for (Scan = follist; !list_Empty(Scan); Scan = list_Cdr(Scan)) if (list_Member(Symbols, (POINTER)term_TopSymbol(list_Car(Scan)), (BOOL (*)(POINTER,POINTER))symbol_Equal)) list_Rplaca(Scan,NULL); follist = list_PointerDeleteElement(follist,NULL); return follist; } static void cnf_SkolemFunctionFormulaMapped(TERM term, LIST allist, LIST map) /************************************************************** INPUT: A term term and a list allist of variables and a list map of pairs (variable symbols, function symbol) RETURNS: None. CAUTION: The term is destructively changed. All variable symbols in map which appear in term are replaced by the skolem functions with respect to allist which contains the universally quantified variables. ***************************************************************/ { TERM term1; LIST scan,scan1; SYMBOL skolem, symbol; int bottom; bottom = vec_ActMax(); for (scan1=map; !list_Empty(scan1); scan1=list_Cdr(scan1)) { vec_Push(term); symbol = (SYMBOL) list_PairFirst((LIST) list_Car(scan1)); skolem = (SYMBOL) list_PairSecond((LIST) list_Car(scan1)); #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(flag_PSTRSKOLEM)) { fputs("\nVariable : ", stdout); symbol_Print(symbol); fputs("\nFunction : ", stdout); symbol_Print(skolem); } #endif while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (symbol_Equal(term_TopSymbol(term1),symbol)) { term_RplacTop(term1,skolem); list_Delete(term_ArgumentList(term1)); term_RplacArgumentList(term1,term_CopyTermList(allist)); } if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) { vec_Push(list_Car(scan)); } } } vec_SetMax(bottom); } static BOOL cnf_HasDeeperVariable(LIST List1, LIST List2) /****************************************************************** INPUT: Two lists of variable terms RETURNS: TRUE if a variable in the first list is deeper than all variables in the second list, FALSE otherwise. NOTE: If cnf_VARIABLEDEPTHARRAY is not allocated this will crash If new variables are introduced by strong skolemization, their depth is -1. *******************************************************************/ { LIST scan; int maxdepth1; /* Determine maximum depth of variables in List1 */ maxdepth1 = 0; for (scan=List1; !list_Empty(scan); scan=list_Cdr(scan)) { int i; i = cnf_VARIABLEDEPTHARRAY[term_TopSymbol((TERM) list_Car(scan))]; #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(flag_PSTRSKOLEM)) { fputs("\nFor variable ", stdout); symbol_Print(term_TopSymbol((TERM) list_Car(scan))); printf(" depth is %d.", i); } #endif if (i > maxdepth1) maxdepth1 = i; } /* Compare with depth of variables in List2 */ for (scan=List2; !list_Empty(scan); scan=list_Cdr(scan)) { int i; i = cnf_VARIABLEDEPTHARRAY[term_TopSymbol((TERM) list_Car(scan))]; #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(flag_PSTRSKOLEM)) { fputs("\nFor variable ", stdout); symbol_Print(term_TopSymbol((TERM) list_Car(scan))); printf(" depth is %d.", i); } #endif if (i >= maxdepth1) return FALSE; } return TRUE; } static void cnf_StrongSkolemization(PROOFSEARCH Search, TERM Topterm, char* Toplabel, BOOL TopAnd, TERM Term, LIST* UsedTerms, LIST* Symblist, BOOL Result1, HASH InputClauseToTermLabellist, int Depth) /****************************************************************** INPUT: An existence quantified formula. ??? EK RETURNS: Nothing. EFFECT: The existence quantifier is removed by strong skolemization. The precedence of new Skolem symbols is set in the precedence of the search object. *******************************************************************/ { LIST exlist; /* Variable symbols bound by exists[]() */ LIST pairlist; /* List of pairs (Subterm of AND, free variable symbols not in exlist) */ LIST allfreevariables; LIST newvariables; /* w2..wn*/ LIST mapping; /* List of pairs */ int numberofallfreevariables, acc_length, i; LIST pair, pairscan, pairscan_pred, scan, accumulatedvariables; TERM subterm, w; BOOL strskolemsuccess; /* Indicates whether strong skolemization was possible */ FLAGSTORE Flags; PRECEDENCE Precedence; Flags = prfs_Store(Search); Precedence = prfs_Precedence(Search); /* Necessary so that new variables really are new ! */ if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) symbol_SetStandardVarCounter(term_MaxVar(Topterm)); /* Get list of quantified variable symbols x_k */ exlist = cnf_GetSymbolList(term_ArgumentList(term_FirstArgument(Term))); /* Pop quantifier */ 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)); term_Free(subterm); /* Now for every argument get the list of free variables whose symbols are not in exlist */ pairlist = list_Nil(); for (scan=term_ArgumentList(Term); !list_Empty(scan); scan = list_Cdr(scan)) { pair = list_PairCreate((TERM) list_Car(scan), cnf_FreeVariablesBut((TERM) list_Car(scan), exlist)); if (list_Empty(pairlist)) pairlist = list_List(pair); else { /* First sort subterms by number of free variables */ int pairlength, currentlength; pairlength = list_Length((LIST) list_PairSecond(pair)); pairscan = pairlist; pairscan_pred = list_Nil(); currentlength = 0; while (!list_Empty(pairscan)) { currentlength = list_Length((LIST) list_PairSecond((LIST) list_Car(pairscan))); if (currentlength < pairlength) { pairscan_pred = pairscan; pairscan = list_Cdr(pairscan); } else if (currentlength == pairlength) { /* If both subterms have the same number of free variables compare depth of variables */ if (cnf_HasDeeperVariable((LIST) list_PairSecond((LIST) list_Car(pairscan)), /* in list */ (LIST) list_PairSecond(pair))) { /* new pair */ #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(flag_PSTRSKOLEM)) { fputs("\nTerm ", stdout); term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan))); fputs("\n has deeper variable than ", stdout); term_Print((TERM) list_PairFirst(pair)); } #endif pairscan_pred = pairscan; pairscan = list_Cdr(pairscan); } else break; } else break; } /* New pair has more variables than all others in list */ if (list_Empty(pairscan)) list_Rplacd(pairscan_pred, list_List(pair)); /* New pair is inserted between pairscan_pred and pairscan */ else if (currentlength >= pairlength) { /* Head of list */ if (list_Empty(pairscan_pred)) pairlist = list_Cons(pair, pairlist); else list_InsertNext(pairscan_pred, pair); } /* The case for the same number of variables is not yet implemented */ } } #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(flag_PSTRSKOLEM)) { for (pairscan=pairlist; !list_Empty(pairscan); pairscan = list_Cdr(pairscan)) { LIST l; fputs("\nSubterm ", stdout); term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan))); fputs("\n has free variables ", stdout); for (l=(LIST) list_PairSecond((LIST) list_Car(pairscan)); !list_Empty(l); l = list_Cdr(l)) { term_Print((TERM) list_Car(l)); fputs(" ", stdout); } } } #endif /* Determine number of all free variablein and()--term whose symbols are not in exlist */ /* Create map from ex_variables tp skolem symbols */ allfreevariables = cnf_FreeVariablesBut(Term, exlist); numberofallfreevariables = list_Length(allfreevariables); mapping = list_Nil(); for (scan = exlist; !list_Empty(scan); scan = list_Cdr(scan)) { SYMBOL skolem; skolem = symbol_CreateSkolemFunction(numberofallfreevariables, Precedence); *Symblist = list_Cons((POINTER)skolem,*Symblist); mapping = list_Cons(list_PairCreate(list_Car(scan), (POINTER)skolem), mapping); } list_Delete(allfreevariables); /* Create new variables */ newvariables = list_Nil(); for (i=0; i < numberofallfreevariables; i++) { w = term_CreateStandardVariable(); newvariables = list_Cons(w, newvariables); } #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(flag_PSTRSKOLEM)) { LIST l; fputs("\nNew variables : ", stdout); for (l=newvariables; !list_Empty(l); l = list_Cdr(l)) { term_Print((TERM) list_Car(l)); fputs(" ", stdout); } } #endif /* Now do the replacing */ accumulatedvariables = list_Nil(); acc_length = 0; strskolemsuccess = FALSE; for (pairscan=pairlist; !list_Empty(pairscan); pairscan=list_Cdr(pairscan)) { LIST allist; /* Add bound variables for this subterm */ accumulatedvariables = list_Nconc(accumulatedvariables, (LIST) list_PairSecond((LIST) list_Car(pairscan))); accumulatedvariables = term_DeleteDuplicatesFromList(accumulatedvariables); /* Remove new variables not (no longer) needed */ for (i=0; i < list_Length(accumulatedvariables) - acc_length; i++) { term_Delete((TERM) list_Top(newvariables)); newvariables = list_Pop(newvariables); } acc_length = list_Length(accumulatedvariables); #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(flag_PSTRSKOLEM)) { LIST l; fputs("\n\nSubterm is ", stdout); term_Print((TERM) list_PairFirst((LIST) list_Car(pairscan))); fputs("\nFree variables : ", stdout); for (l=accumulatedvariables; !list_Empty(l); l = list_Cdr(l)) { term_Print((TERM) list_Car(l)); fputs(" ", stdout); } } #endif if (!list_Empty(newvariables)) strskolemsuccess = TRUE; allist = list_Nconc(list_Copy(accumulatedvariables), list_Copy(newvariables)); cnf_SkolemFunctionFormulaMapped((TERM) list_PairFirst((LIST) list_Car(pairscan)), allist, mapping); #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(flag_PSTRSKOLEM)) { fputs("\nSubterm after skolemization : ", stdout); term_Print(list_PairFirst((LIST) list_Car(pairscan))); } #endif list_Delete(allist); cnf_OptimizedSkolemFormula(Search, Topterm, Toplabel, TopAnd, (TERM) list_PairFirst((LIST) list_Car(pairscan)), UsedTerms, Symblist, Result1, InputClauseToTermLabellist, Depth); } while (!list_Empty(newvariables)) { term_Delete((TERM) list_Top(newvariables)); newvariables = list_Pop(newvariables); } list_Delete(accumulatedvariables); /* Only pairs and pairlist left */ list_DeletePairList(pairlist); list_Delete(exlist); list_DeletePairList(mapping); if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM) && strskolemsuccess) { fputs("\nStrong skolemization applied", stdout); } } static void cnf_OptimizedSkolemFormula(PROOFSEARCH Search, TERM topterm, char* toplabel, BOOL TopAnd, TERM term, LIST* UsedTerms, LIST* Symblist, BOOL Result1, HASH InputClauseToTermLabellist, int Depth) /************************************************************** INPUT: Two terms in negation normal form. ??? EK RETURNS: The skolemized term with the optimized skolemization due to Ohlbach and Weidenbach of and further improvements. is used as additional, conjunctively added information. EFFECT: The symbol precedence of the search object is changed because new Skolem symbols are defined. CAUTION: The term is destructively changed. ***************************************************************/ { TERM termL2, provedterm; LIST freevariables, scan, varlist; SYMBOL top; BOOL result2; BOOL optimized; FLAGSTORE Flags; PRECEDENCE Precedence; result2 = FALSE; freevariables = list_Nil(); Flags = prfs_Store(Search); Precedence = prfs_Precedence(Search); top = term_TopSymbol(term); if (fol_IsQuantifier(top)) { if (symbol_Equal(top,fol_All())) { /* For quantified variables store depth if strong skolemization is performed */ if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) { LIST variables; variables = term_ArgumentList(term_FirstArgument(term)); for (scan=variables; !list_Empty(scan); scan=list_Cdr(scan)) { #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) { if (cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))] != -1) { fputs("\nFor variable ", stderr); term_Print((TERM) list_Car(scan)); printf(" depth is already set to %d, now setting it to %d", cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))],Depth); } } #endif #ifdef CHECK_STRSKOLEM if (flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) { fputs("\nVariable ", stdout); term_Print((TERM) list_Car(scan)); printf(" has depth %d in term\n ", Depth); term_Print(term); } #endif cnf_VARIABLEDEPTHARRAY[term_TopSymbol(list_Car(scan))] = Depth; } Depth++; } cnf_PopAllQuantifier(term); cnf_OptimizedSkolemFormula(Search,topterm, toplabel, TopAnd, term, UsedTerms, Symblist, Result1, InputClauseToTermLabellist, Depth); return; } freevariables = fol_FreeVariables(term); optimized = FALSE; if (symbol_Equal(term_TopSymbol(term_SecondArgument(term)), fol_And())) { if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM)) { scan = term_ArgumentList(term_SecondArgument(term)); varlist = term_ArgumentList(term_FirstArgument(term)); while (!list_Empty(scan) && !optimized) { if (!Result1) { if (TopAnd) { if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) { fputs("\nHaveProof not necessary", stdout); } result2 = TRUE; } else { termL2 = cnf_QuantifyAndNegate((TERM) list_Car(scan), varlist, freevariables); result2 = cnf_HaveProofOptSkolem(Search, topterm, toplabel, termL2, UsedTerms, Symblist, InputClauseToTermLabellist); #ifdef CHECK_OPTSKOLEM if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) { fputs("\nHaveProof result : ", stdout); if (result2) fputs("TRUE", stdout); else fputs("FALSE", stdout); } #endif } } if (Result1 || result2) { optimized = TRUE; if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) { fputs("\nIn term ", stdout); term_Print(topterm); fputs("\n subterm ", stdout); term_Print((TERM) list_Car(scan)); puts(" is moved to toplevel."); } provedterm = cnf_MoveProvedTermToTopLevel(topterm, term, list_Car(scan), varlist, freevariables, Precedence); if (flag_GetFlagValue(Flags, flag_POPTSKOLEM)) { fputs("Result : ", stdout); term_Print(topterm); putchar('\n'); } /* provedterm is argument of top AND term */ cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TRUE, provedterm,UsedTerms, Symblist, Result1, InputClauseToTermLabellist, Depth); } else scan = list_Cdr(scan); } } if (!optimized) { /* Optimized skolemization not enabled or not possible */ if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) { optimized = TRUE; /* Strong Skolemization is always possible after exists[..](and(..)) */ cnf_StrongSkolemization(Search, topterm, toplabel, TopAnd, term, UsedTerms, Symblist, Result1, InputClauseToTermLabellist, Depth); } } } else TopAnd = FALSE; if (!optimized) { /* Optimized skolemization not enabled or not possible */ /* Strong skolemization not enabled or not possible */ cnf_Skolemize(term, freevariables, Precedence); } list_Delete(freevariables); cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TopAnd, term,UsedTerms, Symblist,Result1,InputClauseToTermLabellist,Depth); return; } else { if (symbol_Equal(top,fol_And()) || symbol_Equal(top,fol_Or())) { if (symbol_Equal(top,fol_Or())) TopAnd = FALSE; for (scan=term_ArgumentList(term);!list_Empty(scan); scan=list_Cdr(scan)) cnf_OptimizedSkolemFormula(Search, topterm, toplabel, TopAnd, (TERM) list_Car(scan), UsedTerms, Symblist, Result1, InputClauseToTermLabellist, Depth); } } return; } static LIST cnf_SkolemFunctionFormula(TERM term, LIST allist, LIST exlist, PRECEDENCE Precedence) /************************************************************** INPUT: A term , a list of variables, a list of variable symbols and a precedence. RETURNS: The list of new Skolem functions. EFFECT: The term is destructively changed. All variable symbols in which appear in are replaced by skolem functions with respect to which contains the universally quantified variables. New Skolem functions are created and their precedence is set in . ***************************************************************/ { TERM term1; LIST scan, scan1, Result; SYMBOL skolem; int bottom,n; Result = list_Nil(); bottom = vec_ActMax(); n = list_Length(allist); for (scan1=exlist; !list_Empty(scan1); scan1=list_Cdr(scan1)) { vec_Push(term); skolem = symbol_CreateSkolemFunction(n, Precedence); Result = list_Cons((POINTER)skolem, Result); while (bottom != vec_ActMax()) { term1 = (TERM)vec_PopResult(); if (symbol_Equal(term_TopSymbol(term1),(SYMBOL)list_Car(scan1))) { term_RplacTop(term1,skolem); list_Delete(term_ArgumentList(term1)); term_RplacArgumentList(term1,term_CopyTermList(allist)); } if (!list_Empty(term_ArgumentList(term1))) for (scan=term_ArgumentList(term1);!list_Empty(scan);scan=list_Cdr(scan)) vec_Push(list_Car(scan)); } } vec_SetMax(bottom); return Result; } static LIST cnf_OptimizedSkolemization(PROOFSEARCH Search, TERM Term, char* Label, LIST* UsedTerms, LIST* Symblist, BOOL result, BOOL Conjecture, HASH InputClauseToTermLabellist) /************************************************************** INPUT: A term, a shared index and a list of non-ConClauses. ??? EK RETURNS: The list of clauses derived from Term. EFFECT: The term is skolemized using optimized skolemization wrt ShIndex. **************************************************************/ { LIST Clauses; TERM FirstArg; int i; FLAGSTORE Flags; PRECEDENCE Precedence; #ifdef CHECK if (Term == NULL) { misc_StartErrorReport(); misc_ErrorReport("\n In cnf_OptimizedSkolemization: Input term is NULL.\n"); misc_FinishErrorReport(); } #endif Flags = prfs_Store(Search); Precedence = prfs_Precedence(Search); FirstArg = Term; if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) { /* Initializing array */ for (i = 1; i <= symbol__MAXSTANDARDVAR; i++) cnf_VARIABLEDEPTHARRAY[i] = -1; } if (flag_GetFlagValue(Flags, flag_POPTSKOLEM) || flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) { fputs("\nTerm before skolemization : \n ", stdout); fol_PrettyPrintDFG(Term); } if (!fol_IsLiteral(Term)) { if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM) || flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) { if (flag_GetFlagValue(Flags, flag_CNFOPTSKOLEM)) Term = term_Create(fol_And(), list_List(Term)); /* CW hack: definitions are added on top level*/ cnf_OptimizedSkolemFormula(Search, Term, Label, TRUE, FirstArg, UsedTerms, Symblist, result, InputClauseToTermLabellist, 0); } else { LIST Symbols; Symbols = list_Nil(); Term = cnf_SkolemFormula(Term, Precedence, &Symbols); list_Delete(Symbols); } } if (flag_GetFlagValue(Flags, flag_POPTSKOLEM) || flag_GetFlagValue(Flags, flag_PSTRSKOLEM)) { fputs("\nTerm after skolemization : ", stdout); term_Print(Term); } Term = cnf_DistributiveFormula(Term); Clauses = cnf_MakeClauseList(Term, FALSE, Conjecture, Flags, Precedence); term_Delete(Term); return Clauses; } LIST cnf_GetSkolemFunctions(TERM Term, LIST ArgList, LIST* SkolToExVar) /************************************************************** INPUT: A term, the argumentlist of a skolem function, a mapping from a skolem function to a variable RETURNS: The longest argumentlist of all skolem functions found so far. EFFECT: Computes information for renaming variables and replacing skolem functions during de-skolemization. **************************************************************/ { LIST Scan; SYMBOL Top; Top = term_TopSymbol(Term); if (fol_IsQuantifier(Top)) return cnf_GetSkolemFunctions(term_SecondArgument(Term), ArgList, SkolToExVar); if (symbol_IsFunction(Top) && symbol_HasProperty(Top, SKOLEM)) { BOOL found; SYMBOL Var = 0; int Arity; found = FALSE; /* Keep longest argument list of all skolem functions in the clause for renaming */ /* Delete all other argument lists */ Arity = list_Length(term_ArgumentList(Term)); if (Arity > list_Length(ArgList)) { term_DeleteTermList(ArgList); ArgList = term_ArgumentList(Term); } else term_DeleteTermList(term_ArgumentList(Term)); term_RplacArgumentList(Term, NULL); /* Replace skolem function by variable */ if (list_Length(*SkolToExVar) > Arity) { NAT i; LIST SkolScan = *SkolToExVar; for (i = 0; i < Arity; i++) SkolScan = list_Cdr(SkolScan); for (SkolScan = (LIST) list_Car(SkolScan); (SkolScan != list_Nil()) && !found; SkolScan = list_Cdr(SkolScan)) { SYMBOL Skol; Skol = (SYMBOL) list_PairFirst((LIST) list_Car(SkolScan)); if (Skol == term_TopSymbol(Term)) { Var = (SYMBOL) list_PairSecond((LIST) list_Car(SkolScan)); found = TRUE; } } } if (!found) { LIST Pair; NAT i; LIST SkolScan; SkolScan = *SkolToExVar; for (i = 0; i < Arity; i++) { if (list_Cdr(SkolScan) == list_Nil()) list_Rplacd(SkolScan, list_List(NULL)); SkolScan = list_Cdr(SkolScan); } Var = symbol_CreateStandardVariable(); Pair = list_PairCreate((POINTER) term_TopSymbol(Term), (POINTER) Var); if (list_Car(SkolScan) == list_Nil()) list_Rplaca(SkolScan, list_List(Pair)); else list_Rplaca(SkolScan, list_Nconc((LIST) list_Car(SkolScan), list_List(Pair))); } term_RplacTop(Term, Var); } else { for (Scan = term_ArgumentList(Term); Scan != list_Nil(); Scan = list_Cdr(Scan)) ArgList = cnf_GetSkolemFunctions((TERM) list_Car(Scan), ArgList, SkolToExVar); } return ArgList; } void cnf_ReplaceVariable(TERM Term, SYMBOL Old, SYMBOL New) /************************************************************** INPUT: A term, two symbols that are variables EFFECT: In term every occurrence of Old is replaced by New **************************************************************/ { LIST Scan; #ifdef CHECK if (!symbol_IsVariable(Old)) { misc_StartErrorReport(); misc_ErrorReport("\n In cnf_ReplaceVariable: Illegal input symbol.\n"); misc_FinishErrorReport(); } #endif if (symbol_Equal(term_TopSymbol(Term), Old)) term_RplacTop(Term, New); else for (Scan = term_ArgumentList(Term); !list_Empty(Scan); Scan = list_Cdr(Scan)) cnf_ReplaceVariable(list_Car(Scan), Old, New); } LIST cnf_RemoveSkolemFunctions(CLAUSE Clause, LIST* SkolToExVar, LIST Vars) /************************************************************** INPUT: A clause, a list which is a mapping from skolem functions to variables and a list of variables for forall-quantification. RETURNS: A list of terms derived from the clause using deskolemization EFFECT: Arguments of skolem functions are renamed consistently. Skolemfunctions are replaced by variables. **************************************************************/ { LIST Scan; LIST TermScan, TermList, ArgList; TERM Term; int i; TermList = list_Nil(); ArgList = list_Nil(); for (i = 0; i < clause_Length(Clause); i++) { Term = term_Copy(clause_GetLiteralTerm(Clause, i)); ArgList = cnf_GetSkolemFunctions(Term, ArgList, SkolToExVar); TermList = list_Cons(Term, TermList); } if (list_Empty(ArgList)) return TermList; /* Rename variables */ for (Scan = ArgList; Scan != list_Nil(); Scan = list_Cdr(Scan)) { for (TermScan = TermList; TermScan != list_Nil(); TermScan = list_Cdr(TermScan)) { Term = (TERM) list_Car(TermScan); cnf_ReplaceVariable(Term, term_TopSymbol((TERM) list_Car(Scan)), (SYMBOL) list_Car(Vars)); } if (list_Cdr(Vars) == list_Nil()) { SYMBOL New = symbol_CreateStandardVariable(); Vars = list_Nconc(Vars, list_List((POINTER) New)); } Vars = list_Cdr(Vars); } term_DeleteTermList(ArgList); return TermList; } TERM cnf_DeSkolemFormula(LIST Clauses) /************************************************************** INPUT: A list of clauses. RETURNS: A formula built from the clauses. EFFECT: All skolem functions are removed from the clauses. **************************************************************/ { LIST Scan, SkolToExVar, Vars, FreeVars, FreeVarsCopy, VarScan, TermList; TERM VarListTerm, TopTerm, Term; BOOL First; SkolToExVar = list_List(NULL); Vars = list_List((POINTER) symbol_CreateStandardVariable()); TopTerm = term_Create(fol_And(), NULL); for (Scan = Clauses; Scan != list_Nil(); Scan = list_Cdr(Scan)) { TermList = cnf_RemoveSkolemFunctions((CLAUSE) list_Car(Scan), &SkolToExVar, Vars); Term = term_Create(fol_Or(), TermList); FreeVars = fol_FreeVariables(Term); if (!list_Empty(FreeVars)) { FreeVarsCopy = term_CopyTermList(FreeVars); list_Delete(FreeVars); Term = fol_CreateQuantifier(fol_All(), FreeVarsCopy, list_List(Term)); } term_RplacArgumentList(TopTerm, list_Cons(Term, term_ArgumentList(TopTerm))); } VarScan = Vars; First = TRUE; for (Scan = SkolToExVar; Scan != list_Nil(); Scan = list_Cdr(Scan)) { if (list_Empty(list_Car(Scan))) { if (term_TopSymbol(TopTerm) == fol_All()) term_RplacArgumentList(TopTerm, list_Cons(term_Create((SYMBOL) list_Car(VarScan), NULL), term_ArgumentList(TopTerm))); if (!First) TopTerm = fol_CreateQuantifier(fol_All(), list_List(term_Create((SYMBOL) list_Car(VarScan), NULL)), list_List(TopTerm)); } else { LIST ExVarScan; LIST ExVars = list_Nil(); for (ExVarScan = list_Car(Scan); ExVarScan != list_Nil(); ExVarScan = list_Cdr(ExVarScan)) { if (ExVars == list_Nil()) ExVars = list_List(term_Create((SYMBOL) list_PairSecond((LIST) list_Car(ExVarScan)), NULL)); else ExVars = list_Cons(term_Create((SYMBOL) list_PairSecond((LIST) list_Car(ExVarScan)), NULL), ExVars); list_PairFree((LIST) list_Car(ExVarScan)); } list_Delete((LIST) list_Car(Scan)); list_Rplaca(Scan, NULL); if (term_TopSymbol(TopTerm) == fol_Exist()) { VarListTerm = (TERM) list_Car(term_ArgumentList(TopTerm)); term_RplacArgumentList(VarListTerm, list_Nconc(term_ArgumentList(VarListTerm), ExVars)); } else TopTerm = fol_CreateQuantifier(fol_Exist(), ExVars, list_List(TopTerm)); ExVars = list_Nil(); if (!First) TopTerm = fol_CreateQuantifier(fol_All(), list_List(term_Create((SYMBOL) list_Car(VarScan), NULL)), list_List(TopTerm)); } if (!First) VarScan = list_Cdr(VarScan); else First = FALSE; } list_Delete(SkolToExVar); list_Delete(Vars); return TopTerm; } #ifdef OPTCHECK /* Currently unused */ /*static */ LIST cnf_CheckOptimizedSkolemization(LIST* AxClauses, LIST* ConClauses, TERM AxTerm, TERM ConTerm, LIST NonConClauses, LIST* SkolemPredicates, SHARED_INDEX ShIndex, BOOL result) /********************************************************** EFFECT: Used to check the correctness of optimized skolemization ***********************************************************/ { TERM DeSkolemizedAxOpt, DeSkolemizedConOpt, DeSkolemizedAx, DeSkolemizedCon; TERM TopOpt, Top, ToProve; LIST SkolemFunctions2; if (*AxClauses != list_Nil()) { DeSkolemizedAxOpt = cnf_DeSkolemFormula(*AxClauses); if (*ConClauses != list_Nil()) { DeSkolemizedConOpt = cnf_DeSkolemFormula(*ConClauses); TopOpt = term_Create(fol_And(), list_Cons(DeSkolemizedAxOpt, list_List(DeSkolemizedConOpt))); } else TopOpt = DeSkolemizedAxOpt; } else { DeSkolemizedConOpt = cnf_DeSkolemFormula(*ConClauses); TopOpt = DeSkolemizedConOpt; } clause_DeleteClauseList(*AxClauses); clause_DeleteClauseList(*ConClauses); *AxClauses = list_Nil(); *ConClauses = list_Nil(); flag_SetFlagValue(flag_CNFOPTSKOLEM, flag_CNFOPTSKOLEMOFF); if (AxTerm) { *AxClauses = cnf_OptimizedSkolemization(term_Copy(AxTerm), ShIndex, NonConClauses, result,FALSE, ClauseToTermLabellist); } if (ConTerm) { *ConClauses = cnf_OptimizedSkolemization(term_Copy(ConTerm), ShIndex, NonConClauses, result,TRUE, ClauseToTermLabellist); } if (*AxClauses != list_Nil()) { DeSkolemizedAx = cnf_DeSkolemFormula(*AxClauses); if (*ConClauses != list_Nil()) { DeSkolemizedCon = cnf_DeSkolemFormula(*ConClauses); Top = term_Create(fol_And(), list_Cons(DeSkolemizedAx, list_List(DeSkolemizedCon))); } else Top = DeSkolemizedAx; } else { DeSkolemizedCon = cnf_DeSkolemFormula(*ConClauses); Top = DeSkolemizedCon; } clause_DeleteClauseList(*AxClauses); clause_DeleteClausList(*ConClauses); *AxClauses = list_Nil(); *ConClauses = list_Nil(); ToProve = term_Create(fol_Equiv(), list_Cons(TopOpt, list_List(Top))); ToProve = term_Create(fol_Not(), list_List(ToProve)); fol_NormalizeVars(ToProve); ToProve = cnf_ObviousSimplifications(ToProve); term_AddFatherLinks(ToProve); ToProve = ren_Rename(ToProve,SkolemPredicates,FALSE); ToProve = cnf_RemoveEquivImplFromFormula(ToProve); ToProve = cnf_NegationNormalFormula(ToProve); ToProve = cnf_AntiPrenex(ToProve); SkolemFunctions2 = list_Nil(); ToProve = cnf_SkolemFormula(ToProve, &SkolemFunctions2); ToProve = cnf_DistributiveFormula(ToProve); *ConClauses = cnf_MakeClauseList(ToProve); if (ToProve) term_Delete(ToProve); *AxClauses = list_Nil(); return SkolemFunctions2; } #endif PROOFSEARCH cnf_Flotter(LIST AxiomList, LIST ConjectureList, LIST* AxClauses, LIST* AllLabels, HASH TermLabelToClauselist, HASH ClauseToTermLabellist, FLAGSTORE InputFlags, PRECEDENCE InputPrecedence, LIST* Symblist) /************************************************************** INPUT: A list of axiom formulae, a list of conjecture formulae, a pointer to a list in which clauses derived from axiom formulae are stored, a pointer to a list in which clauses derived from conjecture formulae are stored, ??? a pointer to a list of all termlabels, a hasharray in which for every term label the list of clauses derived from the term is stored (if DocProof is set), a hasharray in which for every clause the list of labels of the terms used for deriving the clause is stored (if DocProof is set), a flag store, a precedence a pointer to a list of symbols which have to be deleted later if the ProofSearch object is kept. RETURNS: If KeepProofSearch ??? is TRUE, then the ProofSearch object is not freed but returned. Else, NULL is returned. EFFECT: ??? EK The precedence of new skolem symbols is set in . ***************************************************************/ { LIST Scan, Scan2, FormulaClauses,SkolemFunctions; LIST SkolemPredicates, EmptyClauses, AllFormulae; LIST UsedTerms; TERM AxTerm,Formula; BOOL Result; PROOFSEARCH Search; PRECEDENCE Precedence; FLAGSTORE Flags; NAT Count; HASH InputClauseToTermLabellist; Search = prfs_Create(); /* Initialize the flagstore for the CNF transformation */ Flags = prfs_Store(Search); flag_CleanStore(Flags); flag_InitFlotterFlags(InputFlags, Flags); /* Initialize the precedence */ Precedence = prfs_Precedence(Search); symbol_TransferPrecedence(InputPrecedence, Precedence); if (flag_GetFlagValue(Flags, flag_DOCPROOF)) prfs_AddDocProofSharingIndex(Search); AxTerm = (TERM)NULL; SkolemPredicates = list_Nil(); Result = FALSE; if (flag_GetFlagValue(Flags, flag_DOCPROOF)) InputClauseToTermLabellist = hsh_Create(); else InputClauseToTermLabellist = NULL; symbol_ReinitGenericNameCounters(); for (Scan = AxiomList; !list_Empty(Scan); Scan = list_Cdr(Scan)) { LIST Pair; Pair = list_Car(Scan); AxTerm = (TERM) list_PairSecond(Pair); fol_RemoveImplied(AxTerm); term_AddFatherLinks(AxTerm); fol_NormalizeVars(AxTerm); if (flag_GetFlagValue(Flags, flag_CNFFEQREDUCTIONS)) cnf_PropagateSubstEquations(AxTerm); AxTerm = cnf_ObviousSimplifications(AxTerm); if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) { term_AddFatherLinks(AxTerm); AxTerm = ren_Rename(AxTerm, Precedence, &SkolemPredicates, flag_GetFlagValue(Flags, flag_CNFPRENAMING), TRUE); } AxTerm = cnf_RemoveEquivImplFromFormula(AxTerm); AxTerm = cnf_NegationNormalFormula(AxTerm); AxTerm = cnf_AntiPrenex(AxTerm); list_Rplacd(Pair, (LIST) AxTerm); } AllFormulae = AxiomList; /* At this point the list contains max. 1 element, which is a pair of the label NULL and the negated conjunction of all conjecture formulae. */ Count = 0; for (Scan = ConjectureList; !list_Empty(Scan); Scan = list_Cdr(Scan)) { TERM ConTerm; char* Label; char buf[100]; /* Add label */ if (list_PairFirst(list_Car(Scan)) == NULL) { sprintf(buf, "conjecture%d", Count); Label = string_StringCopy(buf); list_Rplaca((LIST) list_Car(Scan), Label); if (flag_GetFlagValue(Flags, flag_DOCPROOF) && flag_GetFlagValue(Flags, flag_PLABELS)) { printf("\nAdded label %s for conjecture", Label); fol_PrettyPrintDFG((TERM) list_PairSecond(list_Car(Scan))); } } ConTerm = (TERM) list_PairSecond((LIST) list_Car(Scan)); fol_RemoveImplied(ConTerm); term_AddFatherLinks(ConTerm); fol_NormalizeVars(ConTerm); if (flag_GetFlagValue(Flags, flag_CNFFEQREDUCTIONS)) cnf_PropagateSubstEquations(ConTerm); ConTerm = cnf_ObviousSimplifications(ConTerm); if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) { term_AddFatherLinks(ConTerm); ConTerm = ren_Rename(ConTerm, Precedence, &SkolemPredicates, flag_GetFlagValue(Flags, flag_CNFPRENAMING),TRUE); } /* fputs("\nRen:\t",stdout);term_Print(ConTerm);putchar('\n'); */ ConTerm = cnf_RemoveEquivImplFromFormula(ConTerm); ConTerm = cnf_NegationNormalFormula(ConTerm); /* fputs("\nAn:\t",stdout);term_Print(ConTerm);putchar('\n'); */ ConTerm = cnf_AntiPrenex(ConTerm); /* fputs("\nPr:\t",stdout);term_Print(ConTerm);putchar('\n'); */ /* Insert changed term into pair */ list_Rplacd((LIST) list_Car(Scan), (LIST) ConTerm); Count++; } AllFormulae = list_Append(ConjectureList, AllFormulae); for (Scan = ConjectureList;!list_Empty(Scan); Scan = list_Cdr(Scan)) list_Rplaca(Scan,list_PairSecond(list_Car(Scan))); FormulaClauses = list_Nil(); SkolemFunctions = list_Nil(); Count = 0; for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan), Count++) { LIST FormulaClausesTemp; Formula = term_Copy((TERM) list_PairSecond(list_Car(Scan))); #ifdef CHECK_CNF fputs("\nInputFormula : ",stdout); term_Print(Formula); printf("\nLabel : %s", (char*) list_PairFirst(list_Car(Scan))); #endif Formula = cnf_SkolemFormula(Formula,Precedence,&SkolemFunctions); Formula = cnf_DistributiveFormula(Formula); FormulaClausesTemp = cnf_MakeClauseList(Formula,FALSE,FALSE,Flags,Precedence); if (flag_GetFlagValue(Flags, flag_DOCPROOF)) { for (Scan2 = FormulaClausesTemp; !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) { hsh_Put(InputClauseToTermLabellist, list_Car(Scan2), list_PairFirst(list_Car(Scan))); } } FormulaClauses = list_Nconc(FormulaClauses, FormulaClausesTemp); term_Delete(Formula); } /* Trage nun Formula Clauses modulo Reduktion in einen Index ein */ /* red_SatUnit works only on conclauses */ for (Scan = FormulaClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE); /* For FormulaClauses a full saturation */ /* List is deleted in red_SatUnit ! */ EmptyClauses = red_SatUnit(Search, FormulaClauses); if (!list_Empty(EmptyClauses)) { Result = TRUE; /*puts("\nPROOF in FormulaClauses");*/ clause_DeleteClauseList(EmptyClauses); } /* Move all usables to workedoff */ FormulaClauses = list_Copy(prfs_UsableClauses(Search)); for (Scan = FormulaClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) prfs_MoveUsableWorkedOff(Search, (CLAUSE) list_Car(Scan)); list_Delete(FormulaClauses); FormulaClauses = list_Nil(); #ifdef CHECK /*cnf_CheckClauseListsConsistency(ShIndex); */ #endif *Symblist = list_Nil(); for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan)) { LIST Ax, Pair; UsedTerms = list_Nil(); Pair = list_Car(Scan); #ifdef CHECK_CNF fputs("\nFormula : ", stdout); term_Print((TERM) list_PairSecond(Pair)); printf("\nLabel : %s", (char*) list_PairFirst(Pair)); #endif Ax = cnf_OptimizedSkolemization(Search, term_Copy((TERM)list_PairSecond(Pair)), (char*) list_PairFirst(Pair), &UsedTerms, Symblist,Result,FALSE,InputClauseToTermLabellist); /* Set CONCLAUSE flag for clauses derived from conjectures */ if (list_PointerMember(ConjectureList,list_PairSecond(Pair))) { LIST l; for (l = Ax; !list_Empty(l); l = list_Cdr(l)) clause_SetFlag((CLAUSE) list_Car(l), CONCLAUSE); } if (flag_GetFlagValue(Flags, flag_DOCPROOF)) { hsh_PutListWithCompareFunc(TermLabelToClauselist, list_PairFirst(Pair), list_Copy(Ax), (BOOL (*)(POINTER,POINTER))cnf_LabelEqual, (unsigned long (*)(POINTER))hsh_StringHashKey); UsedTerms = list_Cons(list_PairFirst(Pair), UsedTerms); UsedTerms = cnf_DeleteDuplicateLabelsFromList(UsedTerms); for (Scan2 = Ax; !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) { hsh_PutList(ClauseToTermLabellist, list_Car(Scan2), list_Copy(UsedTerms)); hsh_PutList(InputClauseToTermLabellist, list_Car(Scan2), list_Copy(UsedTerms)); } } *AxClauses = list_Nconc(*AxClauses, Ax); list_Delete(UsedTerms); } /* Transfer precedence of new skolem symbols into */ symbol_TransferPrecedence(Precedence, InputPrecedence); list_Delete(ConjectureList); if (flag_GetFlagValue(Flags, flag_DOCPROOF)) hsh_Delete(InputClauseToTermLabellist); if (!flag_GetFlagValue(Flags, flag_INTERACTIVE)) { list_Delete(*Symblist); } *AllLabels = list_Nil(); for (Scan = AllFormulae; !list_Empty(Scan); Scan = list_Cdr(Scan)) { LIST Pair; Pair = list_Car(Scan); term_Delete((TERM) list_PairSecond(Pair)); *AllLabels = list_Cons(list_PairFirst(Pair), *AllLabels); list_PairFree(Pair); } list_Delete(AllFormulae); list_Delete(SkolemFunctions); list_Delete(SkolemPredicates); if (!flag_GetFlagValue(Flags, flag_INTERACTIVE)) { symbol_ResetSkolemIndex(); prfs_Delete(Search); return NULL; } else { /* Delete DocProof clauses */ prfs_DeleteDocProof(Search); return Search; } } LIST cnf_QueryFlotter(PROOFSEARCH Search, TERM Term, LIST* Symblist) /************************************************************** INPUT: A term to derive clauses from, using optimized skolemization, and a ProofSearch object. RETURNS: A list of derived clauses. EFFECT: ??? EK The precedence of new skolem symbols is set in . ***************************************************************/ { LIST SkolemPredicates, SkolemFunctions, IndexedClauses, Scan; LIST ResultClauses, Dummy, EmptyClauses; TERM TermCopy; int Formulae2Clause; BOOL Result; FLAGSTORE Flags, SubProofFlags; PRECEDENCE Precedence; Flags = prfs_Store(Search); Precedence = prfs_Precedence(Search); /* Initialize the flagstore of the cnf_SEARCHCOPY object with default values */ /* and copy the value of flag_DOCPROOF from the global Proofserach object. */ SubProofFlags = prfs_Store(cnf_SEARCHCOPY); flag_InitStoreByDefaults(SubProofFlags); flag_TransferFlag(Flags, SubProofFlags, flag_DOCPROOF); /* Transfer the precedence into the local search object */ symbol_TransferPrecedence(Precedence, prfs_Precedence(cnf_SEARCHCOPY)); SkolemPredicates = SkolemFunctions = list_Nil(); Result = FALSE; prfs_CopyIndices(Search, cnf_SEARCHCOPY); Term = term_Create(fol_Not(), list_List(Term)); fol_NormalizeVars(Term); Term = cnf_ObviousSimplifications(Term); if (flag_GetFlagValue(Flags, flag_CNFRENAMING)) { term_AddFatherLinks(Term); Term = ren_Rename(Term, Precedence, &SkolemPredicates, flag_GetFlagValue(Flags,flag_CNFPRENAMING), TRUE); } Term = cnf_RemoveEquivImplFromFormula(Term); Term = cnf_NegationNormalFormula(Term); Term = cnf_AntiPrenex(Term); TermCopy = term_Copy(Term); TermCopy = cnf_SkolemFormula(TermCopy, Precedence, &SkolemFunctions); TermCopy = cnf_DistributiveFormula(TermCopy); IndexedClauses = cnf_MakeClauseList(TermCopy,FALSE,FALSE,Flags,Precedence); term_Delete(TermCopy); /* red_SatUnit works only on conclauses */ for (Scan = IndexedClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE); EmptyClauses = red_SatUnit(cnf_SEARCHCOPY, IndexedClauses); if (!list_Empty(EmptyClauses)) { Result = TRUE; clause_DeleteClauseList(EmptyClauses); } while (!list_Empty(prfs_UsableClauses(cnf_SEARCHCOPY))) { prfs_MoveUsableWorkedOff(cnf_SEARCHCOPY, (CLAUSE) list_Car(prfs_UsableClauses(cnf_SEARCHCOPY))); } /* Works only if DOCPROOF is false. Otherwise we need labels */ Dummy = list_Nil(); if (flag_GetFlagValue(SubProofFlags, flag_DOCPROOF)) Formulae2Clause = TRUE; else Formulae2Clause = FALSE; flag_SetFlagValue(SubProofFlags, flag_DOCPROOF, flag_DOCPROOFOFF); ResultClauses = cnf_OptimizedSkolemization(cnf_SEARCHCOPY, term_Copy(Term), NULL, &Dummy, Symblist, Result, FALSE, NULL); if (Formulae2Clause) flag_SetFlagValue(SubProofFlags, flag_DOCPROOF, flag_DOCPROOFON); term_Delete(Term); list_Delete(SkolemPredicates); list_Delete(SkolemFunctions); prfs_Clean(cnf_SEARCHCOPY); /* All result clauses of queries are conjecture clauses */ for (Scan=ResultClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) clause_SetFlag((CLAUSE) list_Car(Scan), CONCLAUSE); return ResultClauses; } #ifdef CHECK /* Currently unused */ /*static*/ void cnf_CheckClauseListsConsistency(SHARED_INDEX ShIndex) /************************************************************** INPUT: A shared index and a list of non-ConClauses. EFFECT: When this function is called all clauses in the index must be non-ConClauses, which must also be members of the list. **************************************************************/ { LIST AllClauses, scan; AllClauses = clause_AllIndexedClauses(ShIndex); for (scan = AllClauses; scan != list_Nil(); scan = list_Cdr(scan)) { if (clause_GetFlag((CLAUSE) list_Car(scan), CONCLAUSE)) { misc_StartErrorReport(); misc_ErrorReport("\n In cnf_CheckClauseListsConsistency: Clause is a CONCLAUSE.\n"); misc_FinishErrorReport(); } if (clause_GetFlag((CLAUSE) list_Car(scan), BLOCKED)) { misc_StartErrorReport(); misc_ErrorReport("\n In cnf_CheckClauseListsConsistency: Clause is BLOCKED.\n"); misc_FinishErrorReport(); } } list_Delete(AllClauses); } #endif static LIST cnf_SatUnit(PROOFSEARCH Search, LIST ClauseList) /********************************************************* INPUT: A list of unshared clauses, proof search object RETURNS: A possibly empty list of empty clauses. **********************************************************/ { CLAUSE Given; LIST Scan, Derivables, EmptyClauses, BackReduced; NAT n, Derived; FLAGSTORE Flags; PRECEDENCE Precedence; Flags = prfs_Store(Search); Precedence = prfs_Precedence(Search); Derived = flag_GetFlagValue(Flags, flag_CNFPROOFSTEPS); EmptyClauses = list_Nil(); ClauseList = clause_ListSortWeighed(ClauseList); while (!list_Empty(ClauseList) && list_Empty(EmptyClauses)) { Given = (CLAUSE)list_NCar(&ClauseList); Given = red_CompleteReductionOnDerivedClause(Search, Given, red_ALL); if (Given) { if (clause_IsEmptyClause(Given)) EmptyClauses = list_List(Given); else { /*fputs("\n\nGiven: ",stdout);clause_Print(Given);*/ BackReduced = red_BackReduction(Search, Given, red_USABLE); if (Derived != 0) { Derivables = inf_BoundedDepthUnitResolution(Given, prfs_UsableSharingIndex(Search), FALSE, Flags, Precedence); Derivables = list_Nconc(Derivables, inf_BoundedDepthUnitResolution(Given,prfs_WorkedOffSharingIndex(Search), FALSE, Flags, Precedence)); n = list_Length(Derivables); if (n > Derived) Derived = 0; else Derived -= n; } else Derivables = list_Nil(); Derivables = list_Nconc(BackReduced,Derivables); Derivables = split_ExtractEmptyClauses(Derivables, &EmptyClauses); prfs_InsertUsableClause(Search, Given); for (Scan = Derivables; !list_Empty(Scan); Scan = list_Cdr(Scan)) ClauseList = clause_InsertWeighed(list_Car(Scan), ClauseList, Flags, Precedence); list_Delete(Derivables); } } } clause_DeleteClauseList(ClauseList); return EmptyClauses; } TERM cnf_DefTargetConvert(TERM Target, TERM ToTopLevel, TERM ToProveDef, LIST DefPredArgs, LIST TargetPredArgs, LIST TargetPredVars, LIST VarsForTopLevel, FLAGSTORE Flags, PRECEDENCE Precedence, BOOL* LocallyTrue) /********************************************************** INPUT: A term Target which contains a predicate that might be replaced by its definition. A term ToTopLevel which is the highest level subterm in Target that contains the predicate and can be moved to top level or(). A term ToProveDef which must hold if the definition is to be applied. (IS DESTROYED AND FREED) A list DefPredArgs of the arguments of the predicate in the Definition. A list TargetPredArgs of the arguments of the predicate in Target. A list TargetPredVars of the variables occurring in the arguments of the predicate in Target. A list VarsForTopLevel containing the variables that should be all-quantified at top level to make the proof easier. A flag store. A pointer to a boolean LocallyTrue which is set to TRUE iff the definition can be applied. RETURNS: The Target term which is brought into standard form. **********************************************************/ { TERM orterm, targettoprove; SYMBOL maxvar; /* For normalizing terms */ LIST l1, l2; LIST freevars, vars; /* Free variables in targettoprove */ if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { puts("\nTarget :"); fol_PrettyPrint(Target); } #ifdef CHECK fol_CheckFatherLinks(Target); #endif /* No proof found yet */ *LocallyTrue = FALSE; /* Remove implications from path */ Target = cnf_RemoveImplFromFormulaPath(Target, ToTopLevel); /* Move negations as far down as possible */ Target = cnf_NegationNormalFormulaPath(Target, ToTopLevel); /* Move quantifiers as far down as possible */ Target = cnf_AntiPrenexPath(Target, ToTopLevel); /* Move all-quantified variables from the predicates' arguments to top level */ Target = cnf_MovePredicateVariablesUp(Target, ToTopLevel, VarsForTopLevel); /* Flatten top or() */ Target = cnf_FlattenPath(Target, ToTopLevel); /* Now make sure that all variables in the top forall quantifier are in TargetPredVars */ /* Not necessary, according to CW */ if (symbol_Equal(term_TopSymbol(Target), fol_All())) { targettoprove = term_Copy(term_SecondArgument(Target)); orterm = term_SecondArgument(Target); } else { targettoprove = term_Copy(Target); orterm = Target; } /* Find argument of targettoprove that contains the predicate and remove it */ if (symbol_Equal(term_TopSymbol(targettoprove), fol_Or())) { /* Find subterm that contains the predicate */ LIST arglist; arglist = term_ArgumentList(targettoprove); for (l1=arglist, l2=term_ArgumentList(orterm); !list_Empty(l1); l1 = list_Cdr(l1), l2 = list_Cdr(l2)) { if (term_HasProperSuperterm(ToTopLevel, (TERM) list_Car(l2)) || (ToTopLevel == (TERM) list_Car(l2))) { arglist = list_PointerDeleteElementFree(arglist, list_Car(l1), (void (*)(POINTER))term_Delete); break; } } term_RplacArgumentList(targettoprove, arglist); /* Nothing left for the proof ? */ if (list_Empty(term_ArgumentList(targettoprove))) { term_Delete(targettoprove); term_Delete(ToProveDef); #ifdef CHECK fol_CheckFatherLinks(Target); #endif return Target; } } else { /* Nothing left for the proof */ term_Delete(targettoprove); term_Delete(ToProveDef); #ifdef CHECK fol_CheckFatherLinks(Target); #endif return Target; } /* Normalize variables in ToProveDef with respect to targettoprove */ maxvar = term_MaxVar(targettoprove); symbol_SetStandardVarCounter(maxvar); vars = fol_BoundVariables(ToProveDef); vars = term_DeleteDuplicatesFromList(vars); for (l1=vars; !list_Empty(l1); l1=list_Cdr(l1)) term_ExchangeVariable(ToProveDef, term_TopSymbol(list_Car(l1)), symbol_CreateStandardVariable()); list_Delete(vars); /* Replace arguments of predicate in condition of definition by matching arguments of predicate in target term */ for (l1=DefPredArgs, l2=TargetPredArgs; !list_Empty(l1); l1=list_Cdr(l1), l2=list_Cdr(l2)) term_ReplaceVariable(ToProveDef, term_TopSymbol((TERM) list_Car(l1)), (TERM) list_Car(l2)); targettoprove = term_Create(fol_Not(), list_List(targettoprove)); targettoprove = cnf_NegationNormalFormula(targettoprove); targettoprove = term_Create(fol_Implies(), list_Cons(targettoprove, list_List(ToProveDef))); /* At this point ToProveDef must not be accessed again ! */ /* Add all--quantifier to targettoprove */ freevars = fol_FreeVariables(targettoprove); term_CopyTermsInList(freevars); targettoprove = fol_CreateQuantifier(fol_All(), freevars, list_List(targettoprove)); if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { puts("\nConverted to :"); fol_PrettyPrint(Target); } targettoprove = cnf_NegationNormalFormula(targettoprove); if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { puts("\nToProve for this target :"); fol_PrettyPrint(targettoprove); } *LocallyTrue = cnf_HaveProof(list_Nil(), targettoprove, Flags, Precedence); term_Delete(targettoprove); #ifdef CHECK fol_CheckFatherLinks(Target); #endif return Target; } static TERM cnf_RemoveQuantFromPathAndFlatten(TERM TopTerm, TERM SubTerm) /********************************************************** INPUT: Two terms, must be a subterm of . Superterm of must be an equivalence. Along the path to SubTerm there are only quantifiers or disjunctions. All free variables in the equivalence are free variables in . All free variables in are bound by a universal quantifier (with polarity 1). RETURN: The destructively changed . EFFECT: Removes all quantifiers not binding a variable in from 's path. Moves all universal quantifiers binding free variable in up. is transformed into the form forall([X1,...,Xn],or (equiv(,psi),phi)). **********************************************************/ { TERM Term1, Term2, Flat, Variable; LIST Scan1, Scan2, FreeVars; #ifdef CHECK if (!fol_CheckFormula(TopTerm) || !term_HasPointerSubterm(TopTerm, SubTerm)) { misc_StartErrorReport(); misc_ErrorReport("\nIn cnf_RemoveQuantFromPathAndFlatten: Illegal input."); misc_FinishErrorReport(); } #endif TopTerm = cnf_SimplifyQuantors(TopTerm); term_AddFatherLinks(TopTerm); Term1 = term_Superterm(SubTerm); while (Term1 != TopTerm) { while (symbol_Equal(fol_Or(), term_TopSymbol(Term1)) && (TopTerm != Term1)) { Term1 = term_Superterm(Term1); } if (fol_IsQuantifier(term_TopSymbol(Term1))) { Flat = term_SecondArgument(Term1); Flat = cnf_Flatten(Flat, fol_Or()); Scan1 = fol_QuantifierVariables(Term1); while (!list_Empty(Scan1)) { Variable = (TERM)list_Car(Scan1); if (fol_VarOccursFreely(Variable, SubTerm)) { Scan2 = list_Cdr(Scan1); fol_DeleteQuantifierVariable(Term1, term_TopSymbol(list_Car(Scan1))); Scan1 = Scan2; } else { Scan1 = list_Cdr(Scan1); } } if (fol_IsQuantifier(term_TopSymbol(Term1))) { /* still variables, but not binding a variable in the equivalence term */ LIST ArgList; term_RplacArgumentList(Flat, list_PointerDeleteOneElement(term_ArgumentList(Flat), SubTerm)); ArgList = term_ArgumentList(Term1); term_RplacArgumentList(Term1, list_Nil()); Term2 = term_Create(term_TopSymbol(Term1), ArgList); term_RplacArgumentList(Term1, list_Cons(SubTerm, list_List(Term2))); term_RplacTop(Term1, fol_Or()); Scan1 = term_ArgumentList(Term1); while (!list_Empty(Scan1)) { term_RplacSuperterm((TERM)list_Car(Scan1), Term1); Scan1 = list_Cdr(Scan1); } } } else { #ifdef CHECK if (!symbol_Equal(term_TopSymbol(Term1), fol_Or())) { misc_StartErrorReport(); misc_ErrorReport("\nIn cnf_RemoveQuantFromPathAndFlatten: Illegal term Term1"); misc_FinishErrorReport(); } #endif Term1 = cnf_Flatten(Term1, fol_Or()); } } FreeVars = fol_FreeVariables(Term1); if (!list_Empty(FreeVars)) { term_CopyTermsInList(FreeVars); TopTerm = fol_CreateQuantifier(fol_All(), FreeVars, list_List(Term1)); } return TopTerm; } TERM cnf_DefConvert(TERM Def, TERM FoundPredicate, TERM* ToProve) /********************************************************* INPUT: A term Def which is an equivalence (P(x1,..,xn) <=> Formula) that can be converted to standard form. The subterm that holds the defined predicate. A pointer to a term ToProve into which a term is stored that has to be proved before applying the definition. RETURNS: The converted definition : forall([..], or(equiv(..,..), ..)) ************************************************************/ { TERM orterm; #ifdef CHECK fol_CheckFatherLinks(Def); #endif Def = cnf_RemoveImplFromFormulaPath(Def, FoundPredicate); /* Remove implications along the path */ Def = cnf_NegationNormalFormulaPath(Def, FoundPredicate); /* Move not's as far down as possible */ #ifdef CHECK if (!fol_CheckFormula(Def)) { misc_StartErrorReport(); misc_ErrorReport("\nIn cnf_DefConvert: Illegal input Formula.\n"); misc_FinishErrorReport(); } if (!term_HasPointerSubterm(Def, FoundPredicate)) { misc_StartErrorReport(); misc_ErrorReport("\nIn cnf_DefConvert: Illegal input SubTerm.\n"); misc_FinishErrorReport(); } #endif Def = cnf_RemoveQuantFromPathAndFlatten(Def, term_Superterm(FoundPredicate)); term_AddFatherLinks(Def); #ifdef CHECK if (!fol_CheckFormula(Def)) { misc_StartErrorReport(); misc_ErrorReport("\nIn cnf_DefConvert: Illegal term Def."); misc_FinishErrorReport(); } if (!term_HasPointerSubterm(Def, FoundPredicate)) { misc_StartErrorReport(); misc_ErrorReport("\nIn cnf_DefConvert: Illegal term FoundPredicate."); misc_FinishErrorReport(); } #endif /* Find top level or() */ if (symbol_Equal(term_TopSymbol(Def), fol_All())) { /* Make sure there are several arguments */ if (symbol_Equal(term_TopSymbol(term_SecondArgument(Def)), fol_Or()) && (list_Length(term_ArgumentList(term_SecondArgument(Def))) == 1)) { TERM t; t = term_SecondArgument(Def); term_RplacSecondArgument(Def, term_FirstArgument(term_SecondArgument(Def))); term_Free(t); orterm = NULL; term_RplacSuperterm(term_SecondArgument(Def), Def); } else orterm = term_SecondArgument(Def); } else { /* Make sure there are several arguments */ if (symbol_Equal(term_TopSymbol(Def), fol_Or()) && (list_Length(term_ArgumentList(Def)) == 1)) { TERM t; t = Def; Def = term_FirstArgument(Def); term_Free(t); orterm = NULL; term_RplacSuperterm(term_SecondArgument(Def), Def); } else orterm = Def; } /* If there is something to prove */ if (orterm != (TERM) NULL) { TERM equiv; LIST args; equiv = (TERM) NULL; /* In pell 10 there are no conditions for the equivalence */ if (symbol_Equal(term_TopSymbol(orterm), fol_Equiv())) { equiv = orterm; *ToProve = NULL; } else { TERM t; /* First find equivalence term among arguments */ args = term_ArgumentList(orterm); equiv = term_Superterm(FoundPredicate); /* Delete equivalence from list */ args = list_PointerDeleteElement(args, equiv); term_RplacArgumentList(orterm, args); /* ToProve consists of all the definitions arguments except the equivalence */ *ToProve = term_Copy(orterm); /* Now not(*ToProve) implies the equivalence */ /* Negate *ToProve */ *ToProve = term_Create(fol_Not(), list_List(*ToProve)); *ToProve = cnf_NegationNormalFormula(*ToProve); term_AddFatherLinks(*ToProve); /* Now convert definition to implication form */ term_RplacTop(orterm, fol_Implies()); t = term_Create(fol_Not(), list_List(term_Create(fol_Or(), term_ArgumentList(orterm)))); term_RplacArgumentList(orterm, list_Cons(t, list_List(equiv))); Def = cnf_NegationNormalFormula(Def); term_AddFatherLinks(Def); } } #ifdef CHECK fol_CheckFatherLinks(Def); #endif return Def; } LIST cnf_HandleDefinition(PROOFSEARCH Search, LIST Pair, LIST Axioms, LIST Sorts, LIST Conjectures) /******************************************************************* INPUT: A PROOFSEARCH object, a pair (label, term) and 3 lists of pairs. If the term in pair is a definition, the defined predicate is expanded in all the lists and added to the proofsearch object. RETURNS: The pair with the converted definition: forall([..], or(equiv(..,..), .......)) ********************************************************************/ { TERM definition, defpredicate, equivterm; BOOL alwaysapplicable; /* Is set to TRUE iff the definition can always be applied */ FLAGSTORE Flags; PRECEDENCE Precedence; Flags = prfs_Store(Search); Precedence = prfs_Precedence(Search); /* The axiomlist consists of (label, formula) pairs */ definition = list_PairSecond(Pair); /* Test if Definition contains a definition */ defpredicate = (TERM) NULL; if (cnf_ContainsDefinition(definition, &defpredicate)) { TERM toprove; LIST allformulae, scan; /* Create list of all formula pairs */ /* Check if definition may be applied to each formula */ allformulae = list_Copy(Axioms); allformulae = list_Nconc(allformulae, list_Copy(Sorts)); allformulae = list_Nconc(allformulae, list_Copy(Conjectures)); #ifdef CHECK for (scan=allformulae; !list_Empty(scan); scan=list_Cdr(scan)) { if (!list_Empty((LIST) list_Car(scan))) { if (!term_IsTerm((TERM) list_PairSecond((LIST) list_Car(scan)))) fol_CheckFatherLinks((TERM) list_PairSecond((LIST) list_Car(scan))); } } #endif /* Convert definition to standard form */ if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { fputs("\nPredicate : ", stdout); symbol_Print(term_TopSymbol(defpredicate)); } definition = cnf_DefConvert(definition, defpredicate, &toprove); if (toprove == NULL) alwaysapplicable = TRUE; else alwaysapplicable = FALSE; prfs_SetDefinitions(Search, list_Cons(term_Copy(definition), prfs_Definitions(Search))); if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { if (alwaysapplicable) { fputs("\nAlways Applicable : ", stdout); fol_PrettyPrint(definition); } } /* Definition is converted to a form where the equivalence is the first argument of the disjunction */ equivterm = term_SecondArgument(term_Superterm(defpredicate)); scan = allformulae; while (!list_Empty(scan)) { BOOL localfound; LIST pair, targettermvars; /* Pair label / term */ pair = list_Car(scan); /* Pair may be NULL if it is a definition that could be deleted */ if ((pair != NULL) && (definition != (TERM) list_PairSecond(pair))) { TERM target, targetpredicate, totoplevel; LIST varsfortoplevel; target = (TERM) list_PairSecond(pair); targettermvars = varsfortoplevel = list_Nil(); /* If definition is not always applicable, check if it is applicable for this formula */ localfound = FALSE; if (!alwaysapplicable) { if (cnf_ContainsPredicate(target, term_TopSymbol(defpredicate), &targetpredicate, &totoplevel, &targettermvars, &varsfortoplevel)) { TERM toprovecopy; toprovecopy = term_Copy(toprove); target = cnf_DefTargetConvert(target, totoplevel, toprovecopy, term_ArgumentList(defpredicate), term_ArgumentList(targetpredicate), targettermvars, varsfortoplevel, Flags, Precedence, &localfound); list_Delete(targettermvars); list_Delete(varsfortoplevel); targettermvars = varsfortoplevel = list_Nil(); list_Rplacd(pair, (LIST) target); if (localfound) list_Rplacd(pair, (LIST) cnf_ApplyDefinitionOnce(defpredicate, equivterm, list_PairSecond(pair), targetpredicate, Flags)); } } else { if (cnf_ContainsPredicate(target, term_TopSymbol(defpredicate), &targetpredicate, &totoplevel, &targettermvars, &varsfortoplevel)) list_Rplacd(pair, (LIST) cnf_ApplyDefinitionOnce(defpredicate, equivterm, list_PairSecond(pair), targetpredicate, Flags)); else scan = list_Cdr(scan); list_Delete(targettermvars); list_Delete(varsfortoplevel); targettermvars = varsfortoplevel = list_Nil(); } } else scan = list_Cdr(scan); } list_Delete(allformulae); /* toprove can be NULL if the definition can always be applied */ if (toprove != (TERM) NULL) term_Delete(toprove); list_Rplacd(Pair, (LIST) definition); } return Pair; } LIST cnf_ApplyDefinitionToClause(CLAUSE Clause, TERM Predicate, TERM Expansion, FLAGSTORE Flags, PRECEDENCE Precedence) /************************************************************** INPUT: A clause, two terms and a flag store and a precedence. RETURNS: The list of clauses where each occurrence of Predicate is replaced by Expansion. ***************************************************************/ { NAT i; BOOL changed; LIST args, scan, symblist; TERM clauseterm, argument; changed = FALSE; /* Build term from clause */ args = list_Nil(); for (i = 0; i < clause_Length(Clause); i++) { argument = clause_GetLiteralTerm(Clause, i); /* with sign */ args = list_Cons(term_Copy(argument), args); } clauseterm = term_Create(fol_Or(), args); for (scan=term_ArgumentList(clauseterm); !list_Empty(scan); scan=list_Cdr(scan)) { BOOL isneg; argument = (TERM) list_Car(scan); if (symbol_Equal(term_TopSymbol(argument), fol_Not())) { argument = term_FirstArgument(argument); isneg = TRUE; } else isneg = FALSE; /* Try to match with predicate */ cont_StartBinding(); if (unify_Match(cont_LeftContext(), Predicate, argument)) { SUBST subst; TERM newargument; subst = subst_ExtractMatcher(); newargument = subst_Apply(subst, term_Copy(Expansion)); subst_Free(subst); if (isneg) newargument = term_Create(fol_Not(), list_List(newargument)); term_Delete((TERM) list_Car(scan)); list_Rplaca(scan, newargument); changed = TRUE; } cont_BackTrack(); } if (changed) { /* Build term and derive list of clauses */ LIST result; if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { puts("\nClause before applying def :"); clause_Print(Clause); puts("\nPredicate :"); fol_PrettyPrint(Predicate); puts("\nExpansion :"); fol_PrettyPrint(Expansion); } symblist = list_Nil(); clauseterm = cnf_Cnf(clauseterm, Precedence, &symblist); result = cnf_MakeClauseList(clauseterm,FALSE,FALSE,Flags,Precedence); list_Delete(symblist); term_Delete(clauseterm); if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) { LIST l; puts("\nClauses derived by expanding definition :"); for (l = result; !list_Empty(l); l=list_Cdr(l)) { clause_Print((CLAUSE) list_Car(l)); fputs("\n", stdout); } } return result; } else { term_Delete(clauseterm); return list_Nil(); } } BOOL cnf_PropagateSubstEquations(TERM StartTerm) /************************************************************* INPUT: A term where we assume that father links are established and that no variable is bound by more than one quantifier. RETURNS: TRUE, if any substitutions were made, FALSE otherwise. EFFECT: Function looks for equations of the form x=t where x does not occur in t. If x=t occurs negatively and disjunctively below a universal quantifier binding x or if x=t occurs positively and conjunctively below an existential quantifier binding x, all occurrences of x are replaced by t in . **************************************************************/ { LIST Subequ; TERM QuantorTerm, Equation, EquationTerm; SYMBOL Variable; BOOL Hit, Substituted; #ifdef CHECK if (fol_VarBoundTwice(StartTerm)) { misc_StartErrorReport(); misc_ErrorReport("\n In cnf_PropagateSubstEquations: Variables of"); misc_ErrorReport("\n input term are not normalized."); misc_FinishErrorReport(); } #endif Substituted = FALSE; Subequ = fol_GetSubstEquations(StartTerm); for ( ; !list_Empty(Subequ); Subequ = list_Pop(Subequ)) { Hit = FALSE; Equation = list_Car(Subequ); Variable = symbol_Null(); QuantorTerm = term_Null(); EquationTerm = term_Null(); if (term_IsVariable(term_FirstArgument(Equation)) && !term_ContainsVariable(term_SecondArgument(Equation), term_TopSymbol(term_FirstArgument(Equation)))) { Variable = term_TopSymbol(term_FirstArgument(Equation)); QuantorTerm = fol_GetBindingQuantifier(Equation, Variable); EquationTerm = term_SecondArgument(Equation); Hit = fol_PolarCheck(Equation, QuantorTerm); } if (!Hit && term_IsVariable(term_SecondArgument(Equation)) && !term_ContainsVariable(term_FirstArgument(Equation), term_TopSymbol(term_SecondArgument(Equation)))) { Variable = term_TopSymbol(term_SecondArgument(Equation)); QuantorTerm = fol_GetBindingQuantifier(Equation, Variable); EquationTerm = term_FirstArgument(Equation); Hit = fol_PolarCheck(Equation, QuantorTerm); } if (Hit) { fol_DeleteQuantifierVariable(QuantorTerm,Variable); term_ReplaceVariable(StartTerm, Variable, EquationTerm); /* We replace everythere ! */ term_AddFatherLinks(StartTerm); if (symbol_Equal(term_TopSymbol(QuantorTerm),fol_Equality())) /* Trivial Formula */ fol_SetTrue(QuantorTerm); else fol_SetTrue(Equation); Substituted = TRUE; } } /* was freed in the loop. */ return Substituted; }