/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                   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$                                        * */
/* $State$                                            * */
/* $Date$                             * */
/* $Author$                                       * */
/* *                                                        * */
/* *             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));
}