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,