diff options
Diffstat (limited to 'test/spass/renaming.c')
| -rw-r--r-- | test/spass/renaming.c | 1508 |
1 files changed, 1508 insertions, 0 deletions
diff --git a/test/spass/renaming.c b/test/spass/renaming.c new file mode 100644 index 00000000..55c89c5a --- /dev/null +++ b/test/spass/renaming.c @@ -0,0 +1,1508 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * RENAMING * */ +/* * * */ +/* * $Module: RENAMING * */ +/* * * */ +/* * Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001 * */ +/* * MPI fuer Informatik * */ +/* * * */ +/* * This program is free software; you can redistribute * */ +/* * it and/or modify it under the terms of the GNU * */ +/* * General Public License as published by the Free * */ +/* * Software Foundation; either version 2 of the License, * */ +/* * or (at your option) any later version. * */ +/* * * */ +/* * This program is distributed in the hope that it will * */ +/* * be useful, but WITHOUT ANY WARRANTY; without even * */ +/* * the implied warranty of MERCHANTABILITY or FITNESS * */ +/* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ +/* * License for more details. * */ +/* * * */ +/* * You should have received a copy of the GNU General * */ +/* * Public License along with this program; if not, write * */ +/* * to the Free Software Foundation, Inc., 59 Temple * */ +/* * Place, Suite 330, Boston, MA 02111-1307 USA * */ +/* * * */ +/* * * */ +/* $Revision: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + +#include "renaming.h" + +static NAT ren_STAMPID; + +static BOOL ren_RootDistanceSmaller(RENAMING,RENAMING); +static BOOL ren_AFactorOk(TERM,TERM); +static BOOL ren_BFactorOk(TERM,TERM); +static BOOL ren_AExtraFactorOk(TERM,TERM); +static BOOL ren_BExtraFactorOk(TERM,TERM); +static BOOL ren_AFactorBigger3(TERM,TERM); +static BOOL ren_BFactorBigger3(TERM,TERM); +static TERM ren_FormulaRename(TERM, LIST, PRECEDENCE, LIST*); +static LIST ren_GetRenamings(TERM, TERM, int); +static BOOL ren_HasBenefit(TERM, TERM, int); +static int ren_Polarity(TERM); +static BOOL ren_PFactorOk(TERM); +static BOOL ren_PExtraFactorOk(TERM); +static BOOL ren_PFactorBigger3(TERM); +static BOOL ren_NotPFactorOk(TERM); +static BOOL ren_NotPExtraFactorOk(TERM); +static BOOL ren_NotPFactorBigger3(TERM); +static void ren_ResetTermStamp(TERM); + +void ren_Init(void) +/********************************************************** + INPUT: None. + RETURNS: void. + EFFECT: Initializes the renaming module, in particular + the stamp id used in this module. +***********************************************************/ +{ + ren_STAMPID = term_GetStampID(); +} + +static BOOL ren_RootDistanceSmaller(RENAMING Ren1, RENAMING Ren2) +{ + return term_RootDistanceSmaller(ren_Hit(Ren1), ren_Hit(Ren2)); +} + + +static void ren_ResetTermStamp(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: void. + EFFECT: The Term stamp of term as well as the stamps of + all its subterms (up to atom level) are reset. +***********************************************************/ +{ + SYMBOL Top; + + term_ResetTermStamp(Term); + Top = term_TopSymbol(Term); + + if (!symbol_IsPredicate(Top)) { + if (fol_IsQuantifier(Top)) + ren_ResetTermStamp(term_SecondArgument(Term)); + else { + LIST Scan; + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + ren_ResetTermStamp(list_Car(Scan)); + } + } +} + +static BOOL ren_HasNEquivFathers(TERM Term1, TERM Term2, NAT n) +/********************************************************** + INPUT: Two terms, where <Term2> is a proper subterm of <Term1> + and a number. + RETURNS: TRUE if <Term2> has a <n>-father that are equivalences + and below <Term1> +***********************************************************/ +{ + Term2 = term_Superterm(Term2); + + while (Term1 != Term2) { + if (symbol_Equal(term_TopSymbol(Term2),fol_Equiv())) { + n--; + if (n == 0) + return TRUE; + } + Term2 = term_Superterm(Term2); + } + + return FALSE; +} + + +static BOOL ren_PExtraFactorOk(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: TRUE if transforming the term <Term> in positive polarity context + results in more than two clauses. +***********************************************************/ +{ + SYMBOL Top; + TERM T1, T2; + BOOL Ok; + + /* if <Term> has the stamp, it will be renamed */ + if (term_HasTermStamp(Term) || term_IsAtom(Term)) + return FALSE; + + Top = term_TopSymbol(Term); + + if (fol_IsQuantifier(Top)) + return ren_PExtraFactorOk(term_SecondArgument(Term)); + + if (symbol_Equal(Top,fol_Not())) + return ren_NotPExtraFactorOk(term_FirstArgument(Term)); + + if (symbol_Equal(Top,fol_Equiv())) { + T1 = term_FirstArgument(Term); + T2 = term_SecondArgument(Term); + return (ren_PFactorOk(T1) || ren_NotPFactorOk(T2) || + ren_NotPFactorOk(T1) || ren_PFactorOk(T2)); + } + if (symbol_Equal(Top,fol_And())) { + return (list_Length(term_ArgumentList(Term)) > 2 || + ren_PFactorOk(term_FirstArgument(Term)) || + ren_PFactorOk(term_SecondArgument(Term))); + } + if (symbol_Equal(Top,fol_Implies())) { + T1 = term_FirstArgument(Term); + T2 = term_SecondArgument(Term); + Ok = ren_PFactorOk(T2); + return ((ren_NotPFactorOk(T1) && (Ok || ren_NotPExtraFactorOk(T1))) || + (Ok && ren_PExtraFactorOk(T2))); + } + + if (symbol_Equal(Top,fol_Or())) { + LIST Scan; + Ok = FALSE; /* is set to TRUE if a subterm with p factor >1 occurred */ + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + if (ren_PFactorOk(list_Car(Scan))) { + if (Ok || ren_PExtraFactorOk(list_Car(Scan))) + return TRUE; /* if two subterms with p>1 or one subterm with p>2 */ + Ok = TRUE; + } + } + + return FALSE; /* <Term> is a trivial disjunction */ +} + +static BOOL ren_PFactorOk(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: TRUE if transforming the term <Term> in positive polarity context + results in more than one clause. +***********************************************************/ +{ + SYMBOL Top; + + /* if <Term> has the stamp, it will be renamed */ + if (term_HasTermStamp(Term) || term_IsAtom(Term)) + return FALSE; + + Top = term_TopSymbol(Term); + + if (symbol_Equal(Top,fol_Equiv()) || symbol_Equal(Top,fol_And())) + return TRUE; + + if (symbol_Equal(Top,fol_Not())) + return ren_NotPFactorOk(term_FirstArgument(Term)); + + if (fol_IsQuantifier(Top)) + return ren_PFactorOk(term_SecondArgument(Term)); + + if (symbol_Equal(Top,fol_Implies())) + return (ren_NotPFactorOk(term_FirstArgument(Term)) || + ren_PFactorOk(term_SecondArgument(Term))); + + if (symbol_Equal(Top,fol_Or())) { + LIST Scan; + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + if (ren_PFactorOk(list_Car(Scan))) + return TRUE; + } + + return FALSE; /* <Term> is a trivial disjunction */ +} + + +static BOOL ren_NotPExtraFactorOk(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: TRUE if transforming the term <Term> in negative polarity context + results in more than two clauses. +***********************************************************/ +{ + SYMBOL Top; + + /* if <Term> has the stamp, it will be renamed */ + if (term_HasTermStamp(Term) || term_IsAtom(Term)) + return FALSE; + + Top = term_TopSymbol(Term); + + if (symbol_Equal(Top,fol_Not())) + return ren_PExtraFactorOk(term_FirstArgument(Term)); + + if (fol_IsQuantifier(Top)) + return ren_NotPExtraFactorOk(term_SecondArgument(Term)); + + if (symbol_Equal(Top,fol_Equiv())) { + TERM T1, T2; + T1 = term_FirstArgument(Term); + T2 = term_SecondArgument(Term); + return (ren_PFactorOk(T1) || ren_PFactorOk(T2) || + ren_NotPFactorOk(T1) || ren_NotPFactorOk(T2)); + } + if (symbol_Equal(Top,fol_Or())) { + if (list_Length(term_ArgumentList(Term))>2 || + ren_NotPFactorOk(term_FirstArgument(Term)) || + ren_NotPFactorOk(term_SecondArgument(Term))) + return TRUE; + else + return FALSE; + } + if (symbol_Equal(Top,fol_Implies())) { + if (ren_PFactorOk(term_FirstArgument(Term)) || + ren_NotPFactorOk(term_SecondArgument(Term))) + return TRUE; + else + return FALSE; + } + + if (symbol_Equal(Top,fol_And())) { + LIST Scan; + BOOL Ok; + Ok = FALSE; + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + if (ren_NotPFactorOk(list_Car(Scan))) { + if (Ok || ren_NotPExtraFactorOk(list_Car(Scan))) + return TRUE; /* if two subterms with -p>1 or one subterm with -p>2 */ + Ok = TRUE; + } + } + + return FALSE; /* Either <Term> is a trivial conjunction or an atom */ +} + + +static BOOL ren_NotPFactorOk(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: TRUE if transforming the term <Term> in negative polarity context + results in more than one clause. +***********************************************************/ +{ + SYMBOL Top; + + /* if <Term> has the stamp, it will be renamed */ + if (term_HasTermStamp(Term) || term_IsAtom(Term)) + return FALSE; + + Top = term_TopSymbol(Term); + + if (symbol_Equal(Top,fol_Equiv()) || symbol_Equal(Top,fol_Or()) || + symbol_Equal(Top,fol_Implies())) + return TRUE; + + if (symbol_Equal(Top,fol_Not())) + return ren_PFactorOk(term_FirstArgument(Term)); + + if (fol_IsQuantifier(Top)) + return ren_NotPFactorOk(term_SecondArgument(Term)); + + if (symbol_Equal(Top,fol_And())) { + LIST Scan; + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + if (ren_NotPFactorOk(list_Car(Scan))) + return TRUE; + } + + return FALSE; /* <Term> is a trivial conjunction */ +} + + +static BOOL ren_PFactorBigger3(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: TRUE if transforming the term <Term> in positive + polarity context results in more than three clauses. +***********************************************************/ +{ + SYMBOL Top; + TERM T1, T2; + LIST Scan; + BOOL Ok; + + /* if <Term> has the stamp, it will be renamed */ + if (term_HasTermStamp(Term) || term_IsAtom(Term)) + return FALSE; + + Top = term_TopSymbol(Term); + + if (fol_IsQuantifier(Top)) + return ren_PFactorBigger3(term_SecondArgument(Term)); + + if (symbol_Equal(Top, fol_Not())) + return ren_NotPFactorBigger3(term_FirstArgument(Term)); + + if (symbol_Equal(Top, fol_And())) { + unsigned char Limit; /* invariant: p >= Limit */ + Limit = list_Length(term_ArgumentList(Term)); + for (Scan=term_ArgumentList(Term); !list_Empty(Scan) && Limit<=3; + Scan=list_Cdr(Scan)) + if (ren_PFactorOk(list_Car(Scan))) { + Limit++; + if (Limit<=3 && ren_PExtraFactorOk(list_Car(Scan))) { + Limit++; + if (Limit<=3 && ren_PFactorBigger3(list_Car(Scan))) + Limit++; /* works for unary conjunction, too */ + } + } + return (Limit>3); + } + if (symbol_Equal(Top, fol_Or())) { + Ok = FALSE; /* is set to TRUE if a subterm with p factor >1 occurred */ + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + if (ren_PFactorOk(list_Car(Scan))) { + if (Ok || ren_PFactorBigger3(list_Car(Scan))) + return TRUE; /* if two subterms with p>1 or one subterm with p>3 */ + Ok = TRUE; + } + return FALSE; + } + + T1 = term_FirstArgument(Term); + T2 = term_SecondArgument(Term); + + if (symbol_Equal(Top, fol_Implies())) { + Ok = ren_PFactorOk(T2); + /* return TRUE if -p(T1)>3 || p(T2)>3 || (-p(T1)>1 && p(T2)>1) */ + return ((ren_NotPFactorOk(T1) && (Ok || ren_NotPFactorBigger3(T1))) || + (Ok && ren_PFactorBigger3(T2))); + } + if (symbol_Equal(Top, fol_Equiv())) { + unsigned char T1Limit, T2Limit, NotT1Limit, NotT2Limit; + T1Limit = ren_PFactorOk(T1) ? 1 : 0; + NotT1Limit = ren_NotPFactorOk(T1) ? 1 : 0; + T2Limit = ren_PFactorOk(T2) ? 1 : 0; + NotT2Limit = ren_NotPFactorOk(T2) ? 1 : 0; + /* return TRUE, if p(T1)>2 || p(T2)>2 || -p(T1)>2 || -p(T2)>2 or at */ + /* least two values out of { p(T1),p(T2),-p(T1),-p(T2) } are > 1 */ + return ((T1Limit + NotT2Limit + NotT1Limit + T2Limit >= 2) || + (T1Limit!=0 && ren_PExtraFactorOk(T1)) || + (T2Limit!=0 && ren_PExtraFactorOk(T2)) || + (NotT1Limit!=0 && ren_NotPExtraFactorOk(T1)) || + (NotT2Limit!=0 && ren_NotPExtraFactorOk(T2))); + } + misc_StartErrorReport(); + misc_ErrorReport(" \n In ren_PFactorBigger3: unknown first order operator."); + misc_FinishErrorReport(); + return FALSE; +} + + +static BOOL ren_NotPFactorBigger3(TERM Term) +/********************************************************** + INPUT: A term. + RETURNS: TRUE if transforming the term <Term> in negative + polarity context results in more than three clauses. +***********************************************************/ +{ + SYMBOL Top; + TERM T1, T2; + LIST Scan; + BOOL Ok; + + /* if <Term> has the stamp, it will be renamed */ + if (term_HasTermStamp(Term) || term_IsAtom(Term)) + return FALSE; + + Top = term_TopSymbol(Term); + + if (fol_IsQuantifier(Top)) + return ren_NotPFactorBigger3(term_SecondArgument(Term)); + + if (symbol_Equal(Top, fol_Not())) + return ren_PFactorBigger3(term_FirstArgument(Term)); + + if (symbol_Equal(Top, fol_Or())) { + unsigned char Limit; /* invariant: -p >= Limit */ + Limit = list_Length(term_ArgumentList(Term)); + for (Scan=term_ArgumentList(Term); !list_Empty(Scan) && Limit<=3; + Scan=list_Cdr(Scan)) + if (ren_NotPFactorOk(list_Car(Scan))) { + Limit++; + if (Limit<=3 && ren_NotPExtraFactorOk(list_Car(Scan))) { + Limit++; + if (Limit<=3 && ren_NotPFactorBigger3(list_Car(Scan))) + Limit++; /* works for unary disjunction, too */ + } + } + return (Limit>3); + } + if (symbol_Equal(Top, fol_And())) { + Ok = FALSE; /* is set to TRUE if a subterm with -p factor >1 occurred */ + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + if (ren_NotPFactorOk(list_Car(Scan))) { + if (Ok || ren_NotPFactorBigger3(list_Car(Scan))) + return TRUE; /* if two subterms with -p>1 or one subterm with -p>3 */ + Ok = TRUE; + } + return FALSE; + } + + T1 = term_FirstArgument(Term); + T2 = term_SecondArgument(Term); + + if (symbol_Equal(Top, fol_Implies())) { + Ok = ren_NotPFactorOk(T2); + /* return TRUE if p(T1)>2 || -p(T2)>2 || (p(T1)>1 && -p(T2)>1) */ + return ((ren_PFactorOk(T1) && (Ok || ren_PExtraFactorOk(T1))) || + (Ok && ren_NotPExtraFactorOk(T2))); + } + if (symbol_Equal(Top, fol_Equiv())) { + unsigned char T1Limit, T2Limit, NotT1Limit, NotT2Limit; + T1Limit = ren_PFactorOk(T1) ? 1 : 0; + NotT1Limit = ren_NotPFactorOk(T1) ? 1 : 0; + T2Limit = ren_PFactorOk(T2) ? 1 : 0; + NotT2Limit = ren_NotPFactorOk(T2) ? 1 : 0; + /* return TRUE, if p(T1)>2 || p(T2)>2 || -p(T1)>2 || -p(T2)>2 or at */ + /* least two values out of { p(T1),p(T2),-p(T1),-p(T2) } are > 1 */ + return ((T1Limit + NotT2Limit + NotT1Limit + T2Limit >= 2) || + (T1Limit!=0 && ren_PExtraFactorOk(T1)) || + (T2Limit!=0 && ren_PExtraFactorOk(T2)) || + (NotT1Limit!=0 && ren_NotPExtraFactorOk(T1)) || + (NotT2Limit!=0 && ren_NotPExtraFactorOk(T2))); + } + misc_StartErrorReport(); + misc_ErrorReport(" \n In ren_NotPFactorBigger3: unknown first order operator."); + misc_FinishErrorReport(); + return FALSE; +} + + +static BOOL ren_AFactorOk(TERM Term1, TERM Term2) +/********************************************************** + INPUT: Two terms where <Term1> is a superterm of <Term2> + RETURNS: TRUE if the A-Factor of Term2 in Term1 is larger than one. +***********************************************************/ +{ + SYMBOL Top; + TERM Super; + + if (Term1 == Term2) + return FALSE; + + Super = term_Superterm(Term2); + Top = term_TopSymbol(Super); + + if (symbol_Equal(Top,fol_And()) || fol_IsQuantifier(Top)) + return ren_AFactorOk(Term1, Super); + + if (symbol_Equal(Top,fol_Not())) + return ren_BFactorOk(Term1, Super); + + if (symbol_Equal(Top,fol_Or())) { + LIST Scan; + TERM Sub; + for (Scan=term_ArgumentList(Super);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Sub = (TERM)list_Car(Scan); + if (Sub != Term2 && ren_PFactorOk(Sub)) + return TRUE; + } + return ren_AFactorOk(Term1, Super); + } + + if (symbol_Equal(Top,fol_Implies())) { + if (Term2 == term_FirstArgument(Super)) + return ren_BFactorOk(Term1, Super); + else + return (ren_NotPFactorOk(term_FirstArgument(Super)) || ren_AFactorOk(Term1, Super)); + } + if (symbol_Equal(Top,fol_Equiv())) { + int Pol; + Pol = ren_Polarity(Super); + if (Pol == 0) + return TRUE; + if (Term2 == term_FirstArgument(Super)) + Term2 = term_SecondArgument(Super); + else + Term2 = term_FirstArgument(Super); + + if (Pol == 1) + return (ren_NotPFactorOk(Term2) || ren_AFactorOk(Term1,Super)); + else + return (ren_PFactorOk(Term2) || ren_BFactorOk(Term1,Super)); + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_AFactorOk: Unknown first order operator."); + misc_FinishErrorReport(); + return FALSE; +} + +static BOOL ren_AExtraFactorOk(TERM Term1, TERM Term2) +/********************************************************** + INPUT: Two terms where <Term1> is a superterm of <Term2> + RETURNS: TRUE if the A-Factor of Term2 in Term1 is larger than two. +***********************************************************/ +{ + SYMBOL Top; + TERM Super; + BOOL Ok; + + if (Term1 == Term2) + return FALSE; + + Super = term_Superterm(Term2); + Top = term_TopSymbol(Super); + + if (symbol_Equal(Top,fol_And()) || fol_IsQuantifier(Top)) + return ren_AExtraFactorOk(Term1, Super); + + if (symbol_Equal(Top,fol_Not())) + return ren_BExtraFactorOk(Term1, Super); + + if (symbol_Equal(Top,fol_Or())) { + LIST Scan; + TERM Sub; + Ok = FALSE; + for (Scan=term_ArgumentList(Super);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Sub = (TERM)list_Car(Scan); + if (Sub != Term2 && ren_PFactorOk(Sub)) { + if (Ok || ren_PExtraFactorOk(Sub)) + return TRUE; + Ok = TRUE; + } + } + /* return TRUE if (p>1 for one subterm and a>1) or a>2 */ + return (ren_AFactorOk(Term1,Super) && + (Ok || ren_AExtraFactorOk(Term1, Super))); + } + + if (symbol_Equal(Top,fol_Implies())) { + if (Term2 == term_FirstArgument(Super)) + return ren_BExtraFactorOk(Term1, Super); + else { + TERM T1; + T1 = term_FirstArgument(Super); + Ok = ren_AFactorOk(Term1, Super); + /* return TRUE if (-p>1 and a>1) or -p>2 or a>2 */ + return ((ren_NotPFactorOk(T1) && (Ok || ren_NotPExtraFactorOk(T1))) || + (Ok && ren_AExtraFactorOk(Term1,Super))); + } + } + if (symbol_Equal(Top,fol_Equiv())) { + if (Term2 == term_FirstArgument(Super)) + Term2 = term_SecondArgument(Super); + else + Term2 = term_FirstArgument(Super); + + switch (ren_Polarity(Super)) { + case 0: + return (ren_PFactorOk(Term2) || ren_NotPFactorOk(Term2) || + ren_AFactorOk(Term1,Super) || ren_BFactorOk(Term1,Super)); + case 1: + Ok = ren_AFactorOk(Term1, Super); + return ((ren_NotPFactorOk(Term2) && (Ok || ren_NotPExtraFactorOk(Term2))) || + (Ok && ren_AExtraFactorOk(Term1,Super))); + case -1: + Ok = ren_BFactorOk(Term1, Super); + return ((ren_PFactorOk(Term2) && (Ok || ren_PExtraFactorOk(Term2))) || + (Ok && ren_BExtraFactorOk(Term1,Super))); + } + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_AExtraFactorOk: Unknown first order operator."); + misc_FinishErrorReport(); + return FALSE; +} + + +static BOOL ren_AFactorBigger3(TERM Term1, TERM Term2) +/********************************************************** + INPUT: Two terms where <Term1> is a superterm of <Term2> + RETURNS: TRUE if the A-Factor of Term2 in Term1 is larger than three. +***********************************************************/ +{ + TERM Super; + SYMBOL Top; + BOOL Ok; + + if (Term1 == Term2) + return FALSE; + + Super = term_Superterm(Term2); + Top = term_TopSymbol(Super); + + if (symbol_Equal(Top,fol_And()) || fol_IsQuantifier(Top)) + return ren_AFactorBigger3(Term1, Super); + + if (symbol_Equal(Top,fol_Not())) + return ren_BFactorBigger3(Term1, Super); + + if (symbol_Equal(Top, fol_Or())) { + LIST Scan; + TERM Sub; + Ok = FALSE; /* is set to TRUE if a subterm with p factor >1 occurred */ + for (Scan=term_ArgumentList(Super);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Sub = list_Car(Scan); + if (Term2 != Sub && ren_PFactorOk(Sub)) { + if (Ok || ren_PFactorBigger3(Sub)) + return TRUE; /* if two subterms with p>1 or one subterm with p>3 */ + Ok = TRUE; + } + } + return (ren_AFactorOk(Term1, Super) && + (Ok || ren_AFactorBigger3(Term1, Super))); + } + if (symbol_Equal(Top,fol_Implies())) { + if (Term2 == term_FirstArgument(Super)) + return ren_BFactorBigger3(Term1, Super); + else { + TERM T1; + T1 = term_FirstArgument(Super); + Ok = ren_AFactorOk(Term1, Super); + /* return TRUE if (-p>1 and a>1) or -p>3 or a>3 */ + return ((ren_NotPFactorOk(T1) && (Ok || ren_NotPFactorBigger3(T1))) || + (Ok && ren_AFactorBigger3(Term1, Super))); + } + } + if (symbol_Equal(Top,fol_Equiv())) { + if (Term2 == term_FirstArgument(Super)) + Term2 = term_SecondArgument(Super); + else + Term2 = term_FirstArgument(Super); + + switch (ren_Polarity(Super)) { + case 0: { + unsigned ALimit, BLimit, PLimit, NotPLimit; + ALimit = ren_AFactorOk(Term1, Super) ? 1 : 0; + BLimit = ren_BFactorOk(Term1, Super) ? 1 : 0; + PLimit = ren_PFactorOk(Term2) ? 1 : 0; + NotPLimit = ren_NotPFactorOk(Term2) ? 1 : 0; + /* return TRUE if a>2 || b>2 || p>2 || -p>2 or at least */ + /* two values out of { a, b, p, -p } are > 1 */ + return ((ALimit + BLimit + PLimit + NotPLimit >= 2) || + (PLimit!=0 && ren_PExtraFactorOk(Term2)) || + (NotPLimit!=0 && ren_NotPExtraFactorOk(Term2)) || + (ALimit!=0 && ren_AExtraFactorOk(Term1,Super)) || + (BLimit!=0 && ren_BExtraFactorOk(Term1,Super))); + } + case 1: + Ok = ren_AFactorOk(Term1, Super); + /* return TRUE if a>3 || -p>3 || (a>1 && -p>1) */ + return ((ren_NotPFactorOk(Term2) && (Ok || ren_NotPFactorBigger3(Term2))) || + (Ok && ren_AFactorBigger3(Term1, Super))); + case -1: + Ok = ren_BFactorOk(Term1, Super); + /* return TRUE if b>3 || p>3 || (b>1 && p>1) */ + return ((ren_PFactorOk(Term2) && (Ok || ren_PFactorBigger3(Term2))) || + (Ok && ren_BFactorBigger3(Term1, Super))); + } + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_AFactorBigger3: Unknown first order operator."); + misc_FinishErrorReport(); + return FALSE; +} + + +static BOOL ren_BFactorOk(TERM Term1, TERM Term2) +/********************************************************** + INPUT: Two terms where <Term1> is a superterm of <Term2> + RETURNS: TRUE if the B-Factor of Term2 in Term1 is larger than one. +***********************************************************/ +{ + SYMBOL Top; + TERM Super; + + if (Term1 == Term2) + return FALSE; + + Super = term_Superterm(Term2); + Top = term_TopSymbol(Super); + + if (symbol_Equal(Top,fol_Or()) || fol_IsQuantifier(Top)) + return ren_BFactorOk(Term1, Super); + + if (symbol_Equal(Top,fol_Not())) + return ren_AFactorOk(Term1, Super); + + if (symbol_Equal(Top,fol_And())) { + LIST Scan; + TERM Sub; + for (Scan=term_ArgumentList(Super);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Sub = (TERM)list_Car(Scan); + if (Sub != Term2 && ren_NotPFactorOk(Sub)) + return TRUE; + } + return ren_BFactorOk(Term1, Super); + } + + if (symbol_Equal(Top,fol_Implies())) { + if (Term2 == term_FirstArgument(Super)) + return (ren_PFactorOk(term_SecondArgument(Super)) || ren_AFactorOk(Term1, Super)); + else + return ren_BFactorOk(Term1, Super); + } + if (symbol_Equal(Top,fol_Equiv())) { + int Pol; + Pol = ren_Polarity(Super); + if (Pol == 0) + return TRUE; + if (Term2 == term_FirstArgument(Super)) + Term2 = term_SecondArgument(Super); + else + Term2 = term_FirstArgument(Super); + + if (Pol == 1) + return (ren_PFactorOk(Term2) || ren_AFactorOk(Term1,Super)); + else + return (ren_NotPFactorOk(Term2) || ren_BFactorOk(Term1,Super)); + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_BFactorOk: Unknown first order operator."); + misc_FinishErrorReport(); + return FALSE; +} + +static BOOL ren_BExtraFactorOk(TERM Term1, TERM Term2) +/********************************************************** + INPUT: Two terms where <Term1> is a superterm of <Term2> + RETURNS: TRUE if the B-Factor of Term2 in Term1 is larger than two. +***********************************************************/ +{ + SYMBOL Top; + TERM Super; + BOOL Ok; + + if (Term1 == Term2) + return FALSE; + + Super = term_Superterm(Term2); + Top = term_TopSymbol(Super); + + if (symbol_Equal(Top,fol_Or()) || fol_IsQuantifier(Top)) + return ren_BExtraFactorOk(Term1, Super); + + if (symbol_Equal(Top,fol_Not())) + return ren_AExtraFactorOk(Term1, Super); + + if (symbol_Equal(Top,fol_And())) { + LIST Scan; + TERM Sub; + Ok = FALSE; + for (Scan=term_ArgumentList(Super);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Sub = (TERM)list_Car(Scan); + if (Sub != Term2 && ren_NotPFactorOk(Sub)) { + if (Ok || ren_NotPExtraFactorOk(Sub)) + return TRUE; + Ok = TRUE; + } + } + /* return TRUE if (-p>1 for one subterm and b>1) or b>2 */ + return (ren_BFactorOk(Term1,Super) && + (Ok || ren_BExtraFactorOk(Term1, Super))); + } + + if (symbol_Equal(Top,fol_Implies())) { + if (Term2 == term_FirstArgument(Super)) { + TERM T2; + T2 = term_SecondArgument(Super); + Ok = ren_AFactorOk(Term1, Super); + /* return TRUE if (p>1 and a>1) or p>2 or a>2 */ + return ((ren_PFactorOk(T2) && (Ok || ren_PExtraFactorOk(T2))) || + (Ok && ren_AExtraFactorOk(Term1, Super))); + } + else + return ren_BExtraFactorOk(Term1, Super); + } + if (symbol_Equal(Top,fol_Equiv())) { + if (Term2 == term_FirstArgument(Super)) + Term2 = term_SecondArgument(Super); + else + Term2 = term_FirstArgument(Super); + + switch (ren_Polarity(Super)) { + case 0: + return (ren_PFactorOk(Term2) || ren_NotPFactorOk(Term2) || + ren_AFactorOk(Term1,Super) || ren_BFactorOk(Term1,Super)); + case 1: + Ok = ren_AFactorOk(Term1, Super); + return ((ren_PFactorOk(Term2) && (Ok || ren_PExtraFactorOk(Term2))) || + (Ok && ren_AExtraFactorOk(Term1,Super))); + case -1: + Ok = ren_BFactorOk(Term1, Super); + return ((ren_NotPFactorOk(Term2) && (Ok || ren_NotPExtraFactorOk(Term2))) || + (Ok && ren_BExtraFactorOk(Term1,Super))); + } + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_BExtraFactorOk: Unknown first order operator."); + misc_FinishErrorReport(); + return FALSE; +} + +static BOOL ren_BFactorBigger3(TERM Term1, TERM Term2) +/********************************************************** + INPUT: Two terms where <Term1> is a superterm of <Term2> + RETURNS: TRUE if the B-Factor of Term2 in Term1 is larger than three. +***********************************************************/ +{ + TERM Super; + SYMBOL Top; + BOOL Ok; + + if (Term1 == Term2) + return FALSE; + + Super = term_Superterm(Term2); + Top = term_TopSymbol(Super); + + if (fol_IsQuantifier(Top) || symbol_Equal(Top, fol_Or())) + return ren_BFactorBigger3(Term1, Super); + + if (symbol_Equal(Top, fol_Not())) + return ren_AFactorBigger3(Term1, Super); + + if (symbol_Equal(Top, fol_And())) { + LIST Scan; + TERM Sub; + Ok = FALSE; /* is set to TRUE if a subterm with -p factor >1 occurred */ + for (Scan=term_ArgumentList(Super);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Sub = list_Car(Scan); + if (Term2 != Sub && ren_NotPFactorOk(Sub)) { + if (Ok || ren_NotPFactorBigger3(Sub)) + return TRUE; /* if two subterms with -p>1 or one subterm with -p>3 */ + Ok = TRUE; + } + } + return (ren_BFactorOk(Term1, Super) && + (Ok || ren_BFactorBigger3(Term1, Super))); + } + if (symbol_Equal(Top,fol_Implies())) { + if (Term2 == term_FirstArgument(Super)) { + TERM T2; + T2 = term_SecondArgument(Super); + Ok = ren_AFactorOk(Term1, Super); + /* return TRUE if (p>1 and a>1) or p>3 or a>3 */ + return ((ren_PFactorOk(T2) && (Ok || ren_PFactorBigger3(T2))) || + (Ok && ren_AFactorBigger3(Term1, Super))); + } + else + return ren_BFactorBigger3(Term1, Super); + } + if (symbol_Equal(Top,fol_Equiv())) { + if (Term2 == term_FirstArgument(Super)) + Term2 = term_SecondArgument(Super); + else + Term2 = term_FirstArgument(Super); + + switch (ren_Polarity(Super)) { + case 0: { + unsigned ALimit, BLimit, PLimit, NotPLimit; + ALimit = ren_AFactorOk(Term1, Super) ? 1 : 0; + BLimit = ren_BFactorOk(Term1, Super) ? 1 : 0; + PLimit = ren_PFactorOk(Term2) ? 1 : 0; + NotPLimit = ren_NotPFactorOk(Term2) ? 1 : 0; + /* return TRUE if a>2 || b>2 || p>2 || -p>2 or at least */ + /* two values out of { a, b, p, -p } are > 1 */ + return ((ALimit + BLimit + PLimit + NotPLimit >= 2) || + (PLimit!=0 && ren_PExtraFactorOk(Term2)) || + (NotPLimit!=0 && ren_NotPExtraFactorOk(Term2)) || + (ALimit!=0 && ren_AExtraFactorOk(Term1,Super)) || + (BLimit!=0 && ren_BExtraFactorOk(Term1,Super))); + } + case 1: + Ok = ren_AFactorOk(Term1, Super); + /* return TRUE if a>3 || -p>3 || (a>1 && -p>1) */ + return ((ren_PFactorOk(Term2) && (Ok || ren_PFactorBigger3(Term2))) || + (Ok && ren_AFactorBigger3(Term1, Super))); + case -1: + Ok = ren_BFactorOk(Term1, Super); + /* return TRUE if b>3 || p>3 || (b>1 && p>1) */ + return ((ren_NotPFactorOk(Term2) && (Ok || ren_NotPFactorBigger3(Term2))) || + (Ok && ren_BFactorBigger3(Term1, Super))); + } + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_BFactorBigger3: Unknown first order operator."); + misc_FinishErrorReport(); + return FALSE; +} + + +static BOOL ren_HasBenefit(TERM Term1, TERM Term2, int Pol) +/********************************************************** + INPUT: Two terms and the polarity of the 2nd term in the overall formula. + RETURNS: TRUE if renaming <Term1> in <Term2> results in a positive benefit. + CAUTION: It is assumed that all superterms are set ! +***********************************************************/ +{ + BOOL PFacOk, NotPFacOk, AFacOk, BFacOk; + + switch (Pol) { + + case 0: + PFacOk = ren_PFactorOk(Term2); + NotPFacOk = ren_NotPFactorOk(Term2); + AFacOk = ren_AFactorOk(Term1,Term2); + BFacOk = ren_BFactorOk(Term1,Term2); + return ((AFacOk && BFacOk && PFacOk && NotPFacOk) || + (AFacOk && PFacOk && (ren_PExtraFactorOk(Term2) || ren_AExtraFactorOk(Term1,Term2))) || + (BFacOk && NotPFacOk && (ren_NotPExtraFactorOk(Term2) || ren_BExtraFactorOk(Term1,Term2)))); + break; + + case 1: + return (ren_PFactorOk(Term2) && ren_AFactorOk(Term1,Term2)); + break; + + case -1: + return (ren_NotPFactorOk(Term2) && ren_BFactorOk(Term1,Term2)); + break; + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_HasBenefit: Unknown polarity."); + misc_FinishErrorReport(); + return FALSE; +} + +static BOOL ren_HasNonZeroBenefit(TERM Term1, int Pol1, TERM Term2, int Pol2) +/********************************************************** + INPUT: Two terms and the polarity of the terms in the overall formula. + RETURNS: TRUE if renaming <Term1> in <Term2> results in non-zero positive benefit. + CAUTION: It is assumed that all superterms are set ! +***********************************************************/ +{ + BOOL PFacOk, NotPFacOk, AFacOk, BFacOk, PEFacOk, NotPEFacOk, AEFacOk, BEFacOk; + switch (Pol2) { + case 0: + PFacOk = ren_PFactorOk(Term2); + NotPFacOk = ren_NotPFactorOk(Term2); + AFacOk = ren_AFactorOk(Term1,Term2); + BFacOk = ren_BFactorOk(Term1,Term2); + PEFacOk = PFacOk && ren_PExtraFactorOk(Term2); + NotPEFacOk = NotPFacOk && ren_NotPExtraFactorOk(Term2); + AEFacOk = AFacOk && ren_AExtraFactorOk(Term1,Term2); + BEFacOk = BFacOk && ren_BExtraFactorOk(Term1,Term2); + + return ((AFacOk && BFacOk && PFacOk && NotPFacOk && (AEFacOk || BEFacOk || PEFacOk || NotPEFacOk)) || + (PEFacOk && AEFacOk) || (NotPEFacOk && BEFacOk) || + (AFacOk && ren_PFactorBigger3(Term2)) || + (BFacOk && ren_NotPFactorBigger3(Term2)) || + (PFacOk && ren_AFactorBigger3(Term1, Term2)) || + (NotPFacOk && ren_BFactorBigger3(Term1, Term2)) || + /* The following conditions don't imply benefit > 0, but allow */ + /* some additional renamings with benefit 0. */ + (Pol1 == 0 && (symbol_Equal(term_TopSymbol(Term2),fol_Equiv()) || + ren_HasNEquivFathers(Term1,Term2,1))) || + ren_HasNEquivFathers(Term1,Term2,2)); + break; + + case 1: + /* return TRUE if (p>1 && a>2) || (p>2 && a>1) */ + AFacOk = ren_AFactorOk(Term1,Term2); + return ((ren_PFactorOk(Term2) && (AFacOk || ren_AFactorOk(Term1,Term2))) || + (AFacOk && ren_AExtraFactorOk(Term1,Term2))); + break; + + case -1: + /* return TRUE if (-p>1 && b>2) || (-p>2 && b>1) */ + BFacOk = ren_BFactorOk(Term1,Term2); + return ((ren_NotPFactorOk(Term2) && (BFacOk || ren_NotPExtraFactorOk(Term2))) || + (BFacOk && ren_BExtraFactorOk(Term1,Term2))); + break; + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_HasNonZeroBenefit: Unknown polarity."); + misc_FinishErrorReport(); + return FALSE; +} + + +static LIST ren_GetRenamings(TERM Term1, TERM Term2, int Pol) +/********************************************************** + INPUT: Two terms and the polarity of the 2nd term in the overall formula. + RETURNS: The list of subterms below <Term2> that have a positive renaming + benefit. + EFFECT: All renamed formulae are stamped. +***********************************************************/ +{ + SYMBOL Top; + LIST Result,Scan; + + Result = list_Nil(); + + /* Don't rename formulae starting with "not" */ + while (symbol_Equal(term_TopSymbol(Term2), fol_Not())) { + Term2 = term_FirstArgument(Term2); + Pol = -Pol; + } + + if (term_IsAtom(Term2)) + return Result; + + Top = term_TopSymbol(Term2); + + /* Don't rename arguments of a quantifier */ + if (term_Superterm(Term2) && + !fol_IsQuantifier(term_TopSymbol(term_Superterm(Term2))) && + ren_HasBenefit(Term1, Term2, Pol)) { + Result = list_Cons(Term2,Result); + term_SetTermStamp(Term2); + Term1 = Term2; + } + + if (fol_IsQuantifier(Top)) + Result = list_Nconc(Result,ren_GetRenamings(Term1, term_SecondArgument(Term2), Pol)); + else if (symbol_Equal(Top,fol_And()) || symbol_Equal(Top,fol_Or())) + for (Scan=term_ArgumentList(Term2);!list_Empty(Scan);Scan=list_Cdr(Scan)) + Result = list_Nconc(Result,ren_GetRenamings(Term1,list_Car(Scan),Pol)); + else if (symbol_Equal(Top,fol_Implies())) { + Result = list_Nconc(Result,ren_GetRenamings(Term1,term_FirstArgument(Term2),-Pol)); + Result = list_Nconc(Result,ren_GetRenamings(Term1,term_SecondArgument(Term2),Pol)); + } else if (symbol_Equal(Top,fol_Equiv())) { + Result = list_Nconc(Result, ren_GetRenamings(Term1,term_FirstArgument(Term2),0)); + Result = list_Nconc(Result, ren_GetRenamings(Term1,term_SecondArgument(Term2),0)); + } else { + misc_StartErrorReport(); + misc_ErrorReport("In ren_GetRenamings: Unknown first-order operator."); + misc_FinishErrorReport(); + } + + return Result; +} + +static int ren_Polarity(TERM Term) +/********************************************************** + INPUT: A term where the existence of superterms is assumed!. + RETURNS: The polarity of Term with respect to its superterms. +***********************************************************/ +{ + TERM SuperTerm; + + SuperTerm = term_Superterm(Term); + + if (SuperTerm) { + SYMBOL Top; + Top = term_TopSymbol(SuperTerm); + if (symbol_Equal(Top,fol_And()) || symbol_Equal(Top,fol_Or()) || + fol_IsQuantifier(Top)) + return ren_Polarity(SuperTerm); + if (symbol_Equal(Top,fol_Not())) + return (-ren_Polarity(SuperTerm)); + if (symbol_Equal(Top,fol_Equiv())) + return 0; + if (symbol_Equal(Top,fol_Implies())) { + if (Term == term_FirstArgument(SuperTerm)) + return (-ren_Polarity(SuperTerm)); + else + return ren_Polarity(SuperTerm); + } + misc_StartErrorReport(); + misc_ErrorReport("In ren_Polarity: Unknown first-order operator."); + misc_FinishErrorReport(); + } + + return 1; +} + + +static LIST ren_RemoveTerm(TERM Term, LIST Renamings) +/********************************************************** + INPUT: A formula and a list of renamings. + RETURNS: The renaming list where <Term> is removed from + the renamings. + CAUTION: The list and the renamings are destructively changed. +***********************************************************/ +{ + LIST Scan; + RENAMING Renaming; + + /* Remove the Term from all renamings. In case the Hit term equals <Term> */ + /* turn the renaming into a general renaming */ + for (Scan=Renamings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Renaming = (RENAMING)list_Car(Scan); + if (ren_Hit(Renaming) == Term) { + if (list_Empty(ren_Matches(Renaming))) { + ren_Delete(Renaming); + list_Rplaca(Scan, NULL); + } + else + ren_SetGeneral(Renaming, TRUE); + } + else + ren_SetMatches(Renaming, list_PointerDeleteElement(ren_Matches(Renaming), Term)); + } + + /* Take care for the NULL pointers */ + Renamings = list_PointerDeleteElement(Renamings, NULL); + + return Renamings; +} + +static LIST ren_RemoveAllSubterms(TERM Term, LIST Renamings) +/********************************************************** + INPUT: A formula and a list of renamings. + RETURNS: The renaming list where <Term> and all its subterms are + removed from the renamings. + CAUTION: The list and the renamings are destructively changed. +***********************************************************/ +{ + Renamings = ren_RemoveTerm(Term, Renamings); + + if (!symbol_IsPredicate(term_TopSymbol(Term))) { + if (fol_IsQuantifier(term_TopSymbol(Term))) + Renamings = ren_RemoveAllSubterms(term_SecondArgument(Term), Renamings); + else { + LIST Scan; + for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) + Renamings = ren_RemoveAllSubterms(list_Car(Scan), Renamings); + } + } + + return Renamings; +} + + + +static LIST ren_SolveDependencies(LIST Renamings) +/********************************************************** + INPUT: A list of renamings sorted by depth of the hits. + RETURNS: The renaming list where dependences are solved, i.e., if + a formula occurs in the matches of some renaming, then + all its subterms are removed from other renamings, since + the formulae of additional matches completely disappear + after application of the renaming. + In case a subterm is the hit of another renaming but this + renaming has further matches, the further matches are turned + into new individual renamings. + CAUTION: The list and the renamings are destructively changed. +***********************************************************/ +{ + LIST Scan; + RENAMING Renaming; + TERM ActMatch; + + if (list_Empty(Renamings)) + return Renamings; + + Renaming = (RENAMING)list_Car(Renamings); + for (Scan=ren_Matches(Renaming);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + ActMatch = (TERM)list_Car(Scan); + list_Rplacd(Renamings, ren_RemoveAllSubterms(ActMatch, list_Cdr(Renamings))); + } + list_Rplacd(Renamings, ren_SolveDependencies(list_Cdr(Renamings))); + + return Renamings; +} + + +static TERM ren_FormulaRename(TERM Term, LIST Renamings, PRECEDENCE Precedence, + LIST *SkolemSymbols) +/********************************************************** + INPUT: A term and a list of renamings where all + dependencies between the renaming terms are + solved and a precedence. + RETURNS: The renamed formula with respect to the renaming + list and all newly introduced Skolem symbols for + renamings are added to <SkolemSymbols>. + EFFECT: New Skolem predicates are created, and their precedence + is set in <Precedence>. + CAUTION: The formula <Term> is destructively changed. + The renamings are destructively changed. +***********************************************************/ +{ + TERM Result,ActTerm,Hit,DefTerm,Superterm,NewTerm; + LIST Scan,FreeVariables,Args,AllMatches; + SYMBOL ActSymbol; + RENAMING Renaming; + + DefTerm = (TERM)NULL; + AllMatches = list_Nil(); + + if (!list_Empty(Renamings)) + Result = term_Create(fol_And(),list_List(Term)); + else + return Term; + + ActSymbol = 0; + + while (!list_Empty(Renamings)) { + + Renaming = (RENAMING)list_Car(Renamings); + Renamings = list_Cdr(Renamings); + Hit = ren_Hit(Renaming); + Superterm = term_Superterm(Hit); + FreeVariables = fol_FreeVariables(Hit); + ActSymbol = symbol_CreateSkolemPredicate(list_Length(FreeVariables), + Precedence); + *SkolemSymbols = list_Cons((POINTER)ActSymbol,*SkolemSymbols); + + /* printf("\n");fol_PrettyPrintDFG(ren_Hit(Renaming));printf("\n");*/ + + /* Install Definition */ + if (ren_General(Renaming)) /* for general renamings the hit formula will be eventually deleted */ + Hit = term_Copy(Hit); + NewTerm = term_Create(ActSymbol, term_CopyTermList(FreeVariables)); + switch (ren_OverallPolarity(Renaming)) { + case 0: + DefTerm = term_Create(fol_Equiv(),list_Cons(term_Copy(NewTerm),list_List(Hit))); + break; + + case 1: + DefTerm = term_Create(fol_Implies(),list_Cons(term_Copy(NewTerm),list_List(Hit))); + break; + + case -1: + DefTerm = term_Create(fol_Implies(),list_Cons(Hit,list_List(term_Copy(NewTerm)))); + break; + } + term_RplacSuperterm(term_FirstArgument(DefTerm),DefTerm); + term_RplacSuperterm(term_SecondArgument(DefTerm),DefTerm); + if (!list_Empty(FreeVariables)) + DefTerm = fol_CreateQuantifier(fol_All(), term_CopyTermList(FreeVariables), + list_List(DefTerm)); + term_RplacArgumentList(Result,list_Nconc(term_ArgumentList(Result),list_List(DefTerm))); + + /* Replace hit if renaming is not general */ + if (!ren_General(Renaming)) { + term_RplacSuperterm(NewTerm, Superterm); + for (Args=term_ArgumentList(Superterm);!list_Empty(Args); Args=list_Cdr(Args)) + if ((TERM)list_Car(Args) == Hit) { + list_Rplaca(Args, NewTerm); + break; + } + } + else + term_Delete(NewTerm); + + + for (Scan=ren_Matches(Renaming); !list_Empty(Scan); Scan=list_Cdr(Scan)) { + + ActTerm = (TERM)list_Car(Scan); + Superterm = term_Superterm(ActTerm); + + /* Always make new predicate term */ + NewTerm = term_Create(ActSymbol, term_CopyTermList(FreeVariables)); + /* Bind the variables correctly */ + /*puts("\n"); fol_PrettyPrintDFG(Result); + printf("\n Hit:\n"); term_PrettyPrint(Hit); + printf("\n ActTerm:\n"); term_PrettyPrint(ActTerm); printf("\n");*/ + cont_StartBinding(); + if (unify_MatchFlexible(cont_LeftContext(), Hit, ActTerm)) + cont_ApplyBindingsModuloMatching(cont_LeftContext(), NewTerm, TRUE); + else { + misc_StartErrorReport(); + misc_ErrorReport("\n In ren_FormulaRename: Further match is no instance of hit.\n"); + misc_FinishErrorReport(); + } + cont_BackTrack(); + + /* Now replace match */ + term_RplacSuperterm(NewTerm, Superterm); + for (Args=term_ArgumentList(Superterm);!list_Empty(Args); Args=list_Cdr(Args)) + if (list_Car(Args) == ActTerm) { + list_Rplaca(Args, NewTerm); + break; + } + } + AllMatches = list_Nconc(ren_Matches(Renaming), AllMatches); /* Delete later due to dependencies */ + ren_SetMatches(Renaming, list_Nil()); + list_Delete(FreeVariables); + } + list_DeleteWithElement(AllMatches, (void (*)(POINTER)) term_Delete); + return Result; +} + +static LIST ren_FreeRenaming(LIST Renamings) +/********************************************************** + INPUT: A list of renamings. + RETURNS: The list of candidates without renamings that have + benefit zero. + CAUTION: Destructive. +***********************************************************/ +{ + LIST Scan; + TERM Father, Term; + RENAMING Candidate; + + for (Scan=Renamings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Candidate = (RENAMING)list_Car(Scan); + if (list_Empty(ren_Matches(Candidate))) { + Term = ren_Hit(Candidate); + Father = term_Superterm(Term); + while (!term_HasTermStamp(Father) && term_Superterm(Father)) { + Father = term_Superterm(Father); + } + + term_ResetTermStamp(Term); /* Needed for P-Factor check */ + if (ren_General(Candidate) || /* a general renaming without matches is useless */ + !ren_HasNonZeroBenefit(Father, ren_Polarity(Father), + Term, ren_OverallPolarity(Candidate))) { + ren_Delete(Candidate); + list_Rplaca(Scan,NULL); + } else { + /* Term will be renamed */ + term_SetTermStamp(Term); /* Undo temporary change */ + } + } + } + + Renamings = list_PointerDeleteElement(Renamings,NULL); + + return Renamings; +} + +static LIST ren_FurtherMatches(TERM Formula, LIST Formulas) +/********************************************************** + INPUT: A formula and a list of formulas that are candidates + for renaming inside the formula. + RETURNS: A list of renamings where additional matches of + the already found formulas in <Formula> are considered. + First the most general formula <Hit> of any renaming inside + <Formula> is computed, then all instances of <Hit> inside + <Formula> built the actual renaming. + No formula occurs twice in the resulting renamings. +***********************************************************/ +{ + LIST Scan1, Scan2, Allmatches, Matchables, Renamings; + TERM Hit; + int Polarity, NewPol; + + Allmatches = list_Nil(); + Renamings = list_Nil(); + + for (Scan1=Formulas; !list_Empty(Scan1); Scan1=list_Cdr(Scan1)) { + Hit = (TERM)list_Car(Scan1); + + if (!list_PointerMember(Allmatches, Hit)) { + Matchables = list_Cons(Hit, fol_Generalizations(Formula, Hit)); + Hit = fol_MostGeneralFormula(Matchables); /* Could be further improved: construct it ! */ + list_Delete(Matchables); + + if (!list_PointerMember(Allmatches, Hit)) { /* Potentially <Hit> is now different */ + Allmatches = list_Cons(Hit,Allmatches); + Matchables = fol_Instances(Formula, Hit); + Polarity = ren_Polarity(Hit); + + for (Scan2=Matchables; !list_Empty(Scan2); Scan2=list_Cdr(Scan2)) { + if (list_PointerMember(Allmatches, list_Car(Scan2))) + list_Rplaca(Scan2, NULL); + else { + NewPol = ren_Polarity(list_Car(Scan2)); + if (NewPol != Polarity) + Polarity = 0; + } + } + Matchables = list_PointerDeleteElement(Matchables, NULL); + Allmatches = list_Nconc(list_Copy(Matchables), Allmatches); + Renamings = list_Cons(ren_Create(Hit, Matchables, Polarity),Renamings); + } + } + } + list_Delete(Allmatches); + + return Renamings; +} + + +TERM ren_Rename(TERM Term, PRECEDENCE Precedence, LIST *SkolemSymbols, + BOOL Document, BOOL Match) +/********************************************************** + INPUT: A term, a precedence, a pointer to a list of + Skolem symbols, a flag indicating whether the + renamings should be documented and a flag + indicating whether matching subterms should be + renamed using the same predicate. + RETURNS: The possibly changed Term where subformulae are renamed + if this results in a smaller clause normal form, with + respect to the number of clauses. The newly introduced + Skolem predicates are added to <SkolemSymbols>. + The precedence of the new symbols is set in <Precedence>. + CAUTION: Formulae are changed destructively. + This function expects that both conjunctions and disjunction + have at least two arguments! +***********************************************************/ +{ + LIST Renamings, Scan, Formulas; + + Renamings = list_Nil(); + Formulas = list_Nil(); + + if (term_StampOverflow(ren_STAMPID)) + ren_ResetTermStamp(Term); + +#ifdef CHECK + fol_CheckFatherLinks(Term); +#endif + + term_StartStamp(); + + Formulas = ren_GetRenamings(Term, Term, 1); + + /* Formulas = list_GreaterNumberSort(Formulas, (NAT (*)(POINTER)) fol_Depth); */ + + if (Match) + Renamings = ren_FurtherMatches(Term, Formulas); + else { + for (Scan=Formulas;!list_Empty(Scan);Scan=list_Cdr(Scan)) + Renamings = list_Cons(ren_Create(list_Car(Scan),list_Nil(),ren_Polarity(list_Car(Scan))),Renamings); + } + + Renamings = ren_FreeRenaming(Renamings); + + Renamings = list_Sort(Renamings, (BOOL (*) (POINTER, POINTER))ren_RootDistanceSmaller); + /* for dependencies sort renamings top down */ + + Renamings = ren_SolveDependencies(Renamings); /* dependencies in further matches */ + + Renamings = ren_FreeRenaming(Renamings); /* possibly depency solving has created non-zero benefit renamings */ + + if (!list_Empty(Renamings) && Document) { + puts("\n\n\t Renaming term:"); + fol_PrettyPrintDFG(Term); + for (Scan=Renamings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + puts("\n"); + ren_PrettyPrint((RENAMING)list_Car(Scan)); + } + puts("\n"); + } + + Term = ren_FormulaRename(Term, Renamings, Precedence, SkolemSymbols); + + if (!list_Empty(Renamings) && Document) { + puts("\n\n\t Renamed term:"); + fol_PrettyPrintDFG(Term); + puts("\n"); + } + + list_DeleteWithElement(Renamings, (void (*)(POINTER)) ren_Delete); + list_Delete(Formulas); + + term_StopStamp(); + + return Term; +} + +void ren_PrettyPrint(RENAMING Ren) +/********************************************************** + INPUT: A renaming. + EFFECT: pretty prints the renaming to <stdout> +***********************************************************/ +{ + LIST Matches; + + puts("\t Renaming:"); + puts("\n\t ========= \n"); + fol_PrettyPrintDFG(ren_Hit(Ren)); + puts("\n\n\t Instances:"); + for (Matches=ren_Matches(Ren); !list_Empty(Matches); Matches=list_Cdr(Matches)) { + fol_PrettyPrintDFG(list_Car(Matches)); + puts("\n"); + } + printf("\n\t Polarity: %d\n", ren_OverallPolarity(Ren)); + printf("\n\t General : %d\n", (ren_General(Ren) ? 1 : 0)); +} |