From 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 12:34:43 +0000 Subject: Updated raytracer test. Added SPASS test. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/spass/cnf.c | 4787 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 4787 insertions(+) create mode 100644 test/spass/cnf.c (limited to 'test/spass/cnf.c') diff --git a/test/spass/cnf.c b/test/spass/cnf.c new file mode 100644 index 00000000..bf52a264 --- /dev/null +++ b/test/spass/cnf.c @@ -0,0 +1,4787 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * 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: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + +#include "cnf.h" +#include "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; +} -- cgit