Google Git
Sign in
fuchsia / third_party / llvm-test-suite / refs/tags/llvmorg-12.0.1 / . / MultiSource / Applications / SPASS / cnf.c
blob: 3de67aa457e34f96650cf1c6f6e53de69e21a299 [file] [log] [blame]
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * CNF TRANSLATOR * */
/* * * */
/* * $Module: CNF * */
/* * * */
/* * Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001 * */
/* * MPI fuer Informatik * */
/* * * */
/* * This program is free software; you can redistribute * */
/* * it and/or modify it under the terms of the GNU * */
/* * General Public License as published by the Free * */
/* * Software Foundation; either version 2 of the License, * */
/* * or (at your option) any later version. * */
/* * * */
/* * This program is distributed in the hope that it will * */
/* * be useful, but WITHOUT ANY WARRANTY; without even * */
/* * the implied warranty of MERCHANTABILITY or FITNESS * */
/* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */
/* * License for more details. * */
/* * * */
/* * You should have received a copy of the GNU General * */
/* * Public License along with this program; if not, write * */
/* * to the Free Software Foundation, Inc., 59 Temple * */
/* * Place, Suite 330, Boston, MA 02111-1307 USA * */
/* * * */
/* * * */
/* $Revision$ * */
/* $State$ * */
/* $Date$ * */
/* $Author$ * */
/* * * */
/* * Contact: * */
/* * Christoph Weidenbach * */
/* * MPI fuer Informatik * */
/* * Stuhlsatzenhausweg 85 * */
/* * 66123 Saarbruecken * */
/* * Email: weidenb@mpi-sb.mpg.de * */
/* * Germany * */
/* * * */
/* ********************************************************** */
/**************************************************************/
/* $RCSfile$ */
#include "cnf.h"
#include "rules-inf.h"
#include "rules-red.h"
static TERM cnf_AntiPrenexPath(TERM, TERM);
static TERM cnf_ApplyDefinitionInternOnce(TERM, TERM, TERM, TERM, BOOL*);
static SYMBOL cnf_GetDualSymbol(SYMBOL symbol);
static TERM cnf_IsDefinition(TERM);
static void cnf_OptimizedSkolemFormula(PROOFSEARCH, TERM, char*, BOOL, TERM,
LIST*, LIST*, BOOL, HASH, int);
static int cnf_PredicateOccurrences(TERM, SYMBOL);
static void cnf_RplacVar(TERM, LIST, LIST);
static LIST cnf_SatUnit(PROOFSEARCH, LIST);
static LIST cnf_SkolemFunctionFormula(TERM, LIST, LIST, PRECEDENCE);
/* For every variable the depth in the current term, required for */
/* strong skolemization */
static int* cnf_VARIABLEDEPTHARRAY;
/* Holds a copy of the ProofSearch--Object built by cnf_Flotter */
/* during cnf_QueryFlotter */
static PROOFSEARCH cnf_SEARCHCOPY;
/* Proofsearch--Object for the function cnf_HaveProof. We need this */
/* to reduce the number of term stamps required. */
static PROOFSEARCH cnf_HAVEPROOFPS;
void cnf_Init(FLAGSTORE Flags)
/***************************************************************
INPUT: A flag store.
RETURNS: None.
SUMMARY: Initializes the CNF Module.
EFFECTS: Initializes global variables.
CAUTION: MUST BE CALLED BEFORE ANY OTHER CNF-FUNCTION.
***************************************************************/
{
/* If strong skolemization is performed, allocate array for variable depth */
if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM))
cnf_VARIABLEDEPTHARRAY = (int*) memory_Malloc(sizeof(int[symbol__MAXSTANDARDVAR + 1]));
else
cnf_VARIABLEDEPTHARRAY = NULL;
cnf_SEARCHCOPY = prfs_Create();
cnf_HAVEPROOFPS = prfs_Create();
}
void cnf_Free(FLAGSTORE Flags)
/**************************************************************
INPUT: A flag store.
RETURNS: None.
SUMMARY: Frees the CNF Module.
***************************************************************/
{
/* If strong skolemization is performed, free array for variable depth */
if (flag_GetFlagValue(Flags, flag_CNFSTRSKOLEM)) {
memory_Free(cnf_VARIABLEDEPTHARRAY, sizeof(int) * (symbol__NOOFSTANDARDVAR + 1));
cnf_VARIABLEDEPTHARRAY = NULL;
}
prfs_Delete(cnf_SEARCHCOPY);
cnf_SEARCHCOPY = NULL;
prfs_Delete(cnf_HAVEPROOFPS);
cnf_HAVEPROOFPS = NULL;
}
static int cnf_GetFormulaPolarity(TERM term, TERM subterm)
/**********************************************************
INPUT: Two terms term and subterm where subterm is a
subterm of term.
RETURNS: The polarity of subterm in term.
********************************************************/
{
LIST scan;
TERM term1;
int polterm1,bottom;
bottom = vec_ActMax();
vec_Push((POINTER) 1);
vec_Push(term);
do {
term1 = (TERM)vec_PopResult();
polterm1 = (int)vec_PopResult();
if (term1 == subterm) {
vec_SetMax(bottom);
return polterm1;
}else
if (symbol_Equal(term_TopSymbol(term1),fol_Not())) {
vec_Push((POINTER) (- polterm1));
vec_Push(list_Car(term_ArgumentList(term1)));
}
if (symbol_Equal(term_TopSymbol(term1),fol_Exist()) ||
symbol_Equal(term_TopSymbol(term1),fol_All())) {
vec_Push((POINTER)polterm1);
vec_Push(list_Second(term_ArgumentList(term1)));
}
else
if (symbol_Equal(term_TopSymbol(term1),fol_Implies())) {
vec_Push((POINTER) (- polterm1));
vec_Push(list_Car(term_ArgumentList(term1)));
vec_Push((POINTER) polterm1);
vec_Push(list_Second(term_ArgumentList(term1)));
}
else
if (symbol_Equal(term_TopSymbol(term1),fol_Equiv())) {
vec_Push(0);
vec_Push(list_Car(term_ArgumentList(term1)));
vec_Push(0);
vec_Push(list_Second(term_ArgumentList(term1)));
}
else
if (symbol_Equal(term_TopSymbol(term1),fol_And()) ||
symbol_Equal(term_TopSymbol(term1),fol_Or())) {
for (scan = term_ArgumentList(term1);
!list_Empty(scan);
scan = list_Cdr(scan)) {
vec_Push((POINTER) polterm1);
vec_Push(list_Car(scan));
}
}
} while (bottom != vec_ActMax());
vec_SetMax(bottom);
misc_StartErrorReport();
misc_ErrorReport("\n In cnf_GetFormulaPolarity: Wrong arguments !\n");
misc_FinishErrorReport();
return -2;
}
static BOOL cnf_ContainsDefinitionIntern(TERM TopDef, TERM Def, int Polarity,
TERM* FoundPred)
/**********************************************************
INPUT: A term TopDef which is the top level term of the recursion.
A term Def which is searched for a definition.
A pointer to a term into which the predicate of the definition
is stored if it is found.
RETURNS: TRUE if Def contains a definition that can be converted
to standard form.
********************************************************/
{
/* AND / OR */
/* In these cases Def cannot be converted to standard form */
if ((symbol_Equal(term_TopSymbol(Def),fol_And()) && (Polarity == 1)) ||
(symbol_Equal(term_TopSymbol(Def),fol_Or()) && (Polarity == -1)))
return FALSE;
if (symbol_Equal(term_TopSymbol(Def), fol_And()) ||
symbol_Equal(term_TopSymbol(Def),fol_Or())) {
/* Polarity is ok */
LIST l;
for (l=term_ArgumentList(Def); !list_Empty(l); l=list_Cdr(l))
if (cnf_ContainsDefinitionIntern(TopDef, list_Car(l), Polarity, FoundPred))
return TRUE;
return FALSE;
}
/* Quantifiers */
if (fol_IsQuantifier(term_TopSymbol(Def)))
return cnf_ContainsDefinitionIntern(TopDef, term_SecondArgument(Def), Polarity, FoundPred);
/* Negation */
if (symbol_Equal(term_TopSymbol(Def),fol_Not()))
return cnf_ContainsDefinitionIntern(TopDef, term_FirstArgument(Def), -Polarity, FoundPred);
/* Implication */
if (symbol_Equal(term_TopSymbol(Def),fol_Implies())) {
if (Polarity==1) {
if (cnf_ContainsDefinitionIntern(TopDef, term_FirstArgument(Def), -Polarity, FoundPred))
return TRUE;
return cnf_ContainsDefinitionIntern(TopDef, term_SecondArgument(Def), Polarity, FoundPred);
}
return FALSE;
}
/* Equivalence */
if (symbol_Equal(term_TopSymbol(Def),fol_Equiv()) && (Polarity==1)) {
/* Check if equivalence itself is in correct form */
TERM defpredicate;
defpredicate = cnf_IsDefinition(Def);
if (defpredicate != (TERM) NULL) {
LIST predicate_vars, l, defpath;
BOOL allquantifierfound;
TERM super;
int pol;
/* Check if predicate occurs several times in TopDef */
/* if (cnf_PredicateOccurrences(TopDef, term_TopSymbol(defpredicate)) > 1) {}
puts("\n Predicate occurs more than once.");
return FALSE; */
/* Now make sure that the variables of the predicate are */
/* all--quantified and not in the scope of an exist quantifier */
/* predicate_vars = list_Copy(term_ArgumentList(defpredicate)); */
predicate_vars = term_ListOfVariables(defpredicate);
predicate_vars = term_DeleteDuplicatesFromList(predicate_vars);
/* So far (going bottom--up) no all-quantifier was found for */
/* a variable of the predicates' arguments */
allquantifierfound = FALSE;
/* Build defpath here by going bottom up */
/* At first, list of superterms on path is top down */
defpath = list_Nil();
super = Def;
while (super != (TERM) NULL) {
defpath = list_Cons(super, defpath);
super = term_Superterm(super);
}
/* No go top down and add polarities */
pol = 1;
for (l=defpath; !list_Empty(l); l=list_Cdr(l)) {
list_Rplaca(l, list_PairCreate((TERM) list_Car(l), (LIST) pol));
if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Not()))
pol = -pol;
else {
if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Implies()) &&
(term_FirstArgument((TERM) list_Car(l)) == (TERM) list_Car(list_Cdr(l))))
pol = -pol;
else
if (symbol_Equal(term_TopSymbol((TERM) list_Car(l)), fol_Equiv()))
pol = 0;
}
}
/* <defpath> 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 <Term> and <Symbol> that is assumed to be associative.
RETURNS: If the top symbol of <Term> is <Symbol> the <Term> is flattened
as long as it contains further direct subterms starting with <Symbol>
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 <Term> and <Symbol> that is assumed to be associative,
and a predicate term which is a subterm of term
RETURNS: If the top symbol of <Term> is <Symbol> the <Term> is flattened
as long as it contains further direct subterms starting with <Symbol>
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 <Precedence>.
***************************************************************/
{
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 <Precedence>.
***************************************************************/
{
/* 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 <Precedence>.
***************************************************************/
{
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 <Term1> of <Term>, a subterm <Proved> of <Term1>,
a list of existence quantified variables <VarList>,
a list of free variables <FreeList> and a precedence.
<Term1> is of the form
exists[...](t1 and t2 and ... and Proved and ..)
RETURNS: A new term, where <Proved> is removed from the arguments
of <Term1>.
EFFECT: The precedence of new Skolem functions is set in <Precedence>
*******************************************************************/
{
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 <Precedence>.
*********************************************************/
{
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 <term> and further improvements.
<rest> 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 <term>, a list <allist> of variables, a list <exlist>
of variable symbols and a precedence.
RETURNS: The list of new Skolem functions.
EFFECT: The term is destructively changed. All variable symbols
in <exlist> which appear in <term> are replaced by skolem functions
with respect to <allist> which contains the universally quantified
variables.
New Skolem functions are created and their precedence is set
in <Precedence>.
***************************************************************/
{
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 <InputPrecedence>.
***************************************************************/
{
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 <InputPrecedence> */
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 <Search>.
***************************************************************/
{
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, <SubTerm> must be a subterm of <TopTerm>.
Superterm of <SubTerm> 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 <SubTerm>.
All free variables in <SubTerm> are bound by a universal quantifier
(with polarity 1).
RETURN: The destructively changed <TopTerm>.
EFFECT: Removes all quantifiers not binding a variable in <SubTerm>
from <subTerm>'s path.
Moves all universal quantifiers binding free variable
in <SubTerm> up.
<TopTerm> is transformed into the form
forall([X1,...,Xn],or (equiv(<SubTerm>,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 <StartTerm>.
**************************************************************/
{
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;
}
}
/* <Subequ> was freed in the loop. */
return Substituted;
}