/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *             CONGRUENCE CLOSURE ALGORITHM               * */
/* *                                                        * */
/* *  $Module:   CLOSURE                                    * */
/* *                                                        * */
/* *  Copyright (C) 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                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/**************************************************************/
/* Include                                                    */
/**************************************************************/

#include "closure.h"


/**************************************************************/
/* Global constants and variable                              */
/**************************************************************/

/* standard initial size of a closure's stacks */
static const int cc_RASSTDSIZE = 64;
/* cc_RASSTDSIZE * ld(cc_RASSTDSIZE) */
static const int cc_SIZELDSIZE = 384;
/* the virtual term "true" has number 0 */
static const ELEMENT cc_NOOFTRUE = 0;


static struct {
  PARTITION partition;
  TABLE table;
  RAS car, cdr, size, pending, combine;
} cc_CLOSURE;

/* the closure consists of a partition, a signature table, stacks for         */
/* (circularly linked) lists of predecessors of equivalence classes (i. e.    */
/* terms with direct subterms from this class), for the sizes of these lists, */
/* for pending terms (the ones to be worked off) and for terms to be combined */
/* in the same equivalence class                                              */


/**************************************************************/
/* Inline functions                                           */
/**************************************************************/

static __inline__ PARTITION cc_GetPartition(void)
{
  return cc_CLOSURE.partition;
}


static __inline__ void cc_SetPartition(PARTITION partition)
{
  cc_CLOSURE.partition = partition;
}


static __inline__ TABLE cc_GetTable(void)
{
  return cc_CLOSURE.table;
}


static __inline__ void cc_SetTable(TABLE table)
{
  cc_CLOSURE.table = table;
}


static __inline__ RAS cc_GetCars(void)
{
  return cc_CLOSURE.car;
}


static __inline__ TERM cc_GetCar(int index)
{
  return (TERM) ras_Get(cc_GetCars(), index);
}


static __inline__ void cc_SetCars(RAS car)
{
  cc_CLOSURE.car = car;
}


static __inline__ RAS cc_GetCdrs(void)
{
  return cc_CLOSURE.cdr;
}


static __inline__ int cc_GetCdr(int index)
{
  return (int) ras_Get(cc_GetCdrs(), index);
}


static __inline__ void cc_SetCdrs(RAS cdr)
{
  cc_CLOSURE.cdr = cdr;
}


static __inline__ void cc_SetCdr(int index, int cdr)
{
  ras_Set(cc_GetCdrs(), index, (POINTER) cdr);
}


static __inline__ RAS cc_GetSizes(void)
{
  return cc_CLOSURE.size;
}


static __inline__ int cc_GetSize(int index)
{
  return (int) ras_Get(cc_GetSizes(), index);
}


static __inline__ void cc_SetSizes(RAS size)
{
  cc_CLOSURE.size = size;
}


static __inline__ void cc_SetSize(int index, int size)
{
  ras_Set(cc_GetSizes(), index, (POINTER) size);
}


static __inline__ RAS cc_GetPending(void)
{
  return cc_CLOSURE.pending;
}


static __inline__ void cc_SetPending(RAS pending)
{
  cc_CLOSURE.pending = pending;
}


static __inline__ RAS cc_GetCombine(void)
{
  return cc_CLOSURE.combine;
}


static __inline__ void cc_SetCombine(RAS combine)
{
  cc_CLOSURE.combine = combine;
}


/**************************************************************/
/* Functions                                                  */
/**************************************************************/

static int cc_Number(int actno, TERM term, TERM pred)
/***************************************************************
  INPUT:   the actual number of terms, the term to be numbered
           and its predecessor (may be the empty term
           term_Null())
  RETURNS: the new number of terms after recursively numbering
           the term and its subterms
  EFFECT:  stores a term's number as its size, partially
           initializes its predecessor list and pushes all
           subterms to the pending stack
***************************************************************/
{
  LIST terms;

#ifdef CHECK
  if (actno < 0) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cc_Number: negative actual number of terms.");
    misc_FinishErrorReport();
  }
#endif

  term_SetSize(term, actno++);
  cc_SetCars(ras_Push(cc_GetCars(), pred));
  cc_SetPending(ras_Push(cc_GetPending(), term));
  for (terms = term_ArgumentList(term); !list_Empty(terms); terms =
      list_Cdr(terms))
    actno = cc_Number(actno, list_Car(terms), term);
  return actno;
}


static void cc_Union(ECLASS c1, ECLASS c2)
/***************************************************************
  EFFECT:  unions c1 and c2, therefore the signatures of the
           predecessors of one class change, so these
           predecessors have to be deleted from the signature
           table and become pending again; sets new class's
           predecessor list and its size to the concatenation of
           the old lists resp. the sum of the old sizes
***************************************************************/
{
  int aux, size;
  TERM term;

#ifdef CHECK
  if (part_Find(cc_GetPartition(), c1) != c1) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cc_Union: first class corrupted, i. e. is not ");
    misc_ErrorReport("the representative.");
    misc_FinishErrorReport();
  }
  if (part_Find(cc_GetPartition(), c2) != c2) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cc_Union: second class corrupted, i. e. is not ");
    misc_ErrorReport("the representative.");
    misc_FinishErrorReport();
  }
#endif

  if (c1 != c2) {

    /* make c1 the class with the bigger (or at least not smaller) list: */
    if (cc_GetSize(c1) < cc_GetSize(c2)) {
      aux = c1;
      c1  = c2;
      c2  = aux;
    }

    /* delete c2's predecessors from signature table and add them to pending: */
    for (size = cc_GetSize(c2), aux = c2; size > 0; size--) {
      term = cc_GetCar(aux);
      aux  = cc_GetCdr(aux);
      table_Delete(cc_GetTable(), term);
      cc_SetPending(ras_Push(cc_GetPending(), term));
    }

    if (cc_GetSize(c2) > 0) {  /* then GetSize(c1) ( >= GetSize(c2) ) > 0 too */

      /* union circularly linked lists by exchanging cdrs: */
      aux = cc_GetCdr(c1);
      cc_SetCdr(c1, cc_GetCdr(c2));
      cc_SetCdr(c2, aux);

      cc_SetSize(c1, cc_GetSize(c1) + cc_GetSize(c2));
    }
    part_Union(cc_GetPartition(), c1, c2);
  }
}


static void cc_InitData(CLAUSE clause)
/***************************************************************
  INPUT:  the clause to investigate
  EFFECT: pushes clause's atoms and their subterms on the
          pending stack, initializes each predecessor list with
          the list containing only a term's father, and unions
          the equivalence classes of the terms of the same
          antecedent equation
***************************************************************/
{
  int last, actno, i, ld;
  TERM atom;
  RAS cdr, size;

  cc_SetCars(ras_InitWithSize(cc_GetCars(), cc_RASSTDSIZE));
  cc_SetPending(ras_InitWithSize(cc_GetPending(), cc_RASSTDSIZE));
  ras_FastPush(cc_GetCars(), term_Null());  /* "true" has no predecessors */
  actno = 1;
  last  = clause_LastLitIndex(clause);
  for (i = clause_FirstLitIndex(); i <= last; i++) {
    atom = clause_GetLiteralAtom(clause, i);
    if (fol_IsEquality(atom)) {
      actno = cc_Number(actno, term_FirstArgument(atom), term_Null());
      actno = cc_Number(actno, term_SecondArgument(atom), term_Null());
    }
    else
      actno = cc_Number(actno, atom, term_Null());
  }
  cc_SetPartition(part_Init(cc_GetPartition(), actno));
  cc_SetTable(table_Init(cc_GetTable(), symbol_ActIndex() - 1,
                         clause_MaxVar(clause), actno - 1));
  cdr  = ras_InitWithSize(cc_GetCdrs(), actno);
  size = ras_InitWithSize(cc_GetSizes(), actno);
  for (i = 0; i < actno; i++) {
    ras_FastPush(cdr, (POINTER) i);  /* form a cycle */
    ras_FastPush(size, (POINTER) (cc_GetCar(i) == term_Null()? 0 : 1));
  }
  cc_SetCdrs(cdr);
  cc_SetSizes(size);

  /* compute ceil(ld(actno)) avoiding mathbib-logarithm's rounding errors: */
  for (ld = 0, i = actno - 1; i > 0; i >>= 1)
    ld++;

  cc_SetCombine(ras_InitWithSize(cc_GetCombine(), actno * ld + 1));

  /* for every antecedent equation union equivalence classes of its terms  */
  /* (a non-equational atom is represented as the equation atom = "true"): */
  last = clause_LastAntecedentLitIndex(clause);
  for (i = clause_FirstLitIndex(); i <= last; i++) {
    atom = clause_GetLiteralAtom(clause, i);
    if (fol_IsEquality(atom))
      cc_Union(term_Size(term_FirstArgument(atom)),  /* clause not shared, therefore */
	       term_Size(term_SecondArgument(atom))); /* here no cc_Find needed */
    else
      cc_Union(term_Size(atom), part_Find(cc_GetPartition(), cc_NOOFTRUE));
  }

}


static BOOL cc_Outit(CLAUSE clause)
/***************************************************************
  RETURNS: the decision, if the clause is a tautology
***************************************************************/
{
  int last, i;
  BOOL result;
  TERM atom;

#ifdef CHECK
  if (!ras_Empty(cc_GetPending())) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In cc_Outit: there are terms left to work off.");
    misc_FinishErrorReport();
  }
#endif

  last   = clause_LastLitIndex(clause);
  for (i = clause_FirstSuccedentLitIndex(clause), result = FALSE;
       i <= last && !result; i++) {
    atom = clause_GetLiteralAtom(clause, i);
    if (fol_IsEquality(atom))
      result = part_Equivalent(cc_GetPartition(),
			       term_Size(term_FirstArgument(atom)),
			       term_Size(term_SecondArgument(atom)));
    else
      result = part_Equivalent(cc_GetPartition(), term_Size(atom), cc_NOOFTRUE);
  }
  return result;
}


/**************************************************************/
/* Main functions                                             */
/**************************************************************/

void cc_Init(void)
{
  cc_SetPartition(part_Create(cc_RASSTDSIZE));
  cc_SetTable(table_Create(cc_RASSTDSIZE, cc_RASSTDSIZE, cc_RASSTDSIZE));
  cc_SetCars(ras_CreateWithSize(cc_RASSTDSIZE));
  cc_SetCdrs(ras_CreateWithSize(cc_RASSTDSIZE));
  cc_SetSizes(ras_CreateWithSize(cc_RASSTDSIZE));
  cc_SetPending(ras_CreateWithSize(cc_RASSTDSIZE));
  cc_SetCombine(ras_CreateWithSize(cc_SIZELDSIZE));
}


void cc_Free(void)
{
  part_Free(cc_GetPartition());
  table_Free(cc_GetTable());
  ras_Free(cc_GetCars());
  ras_Free(cc_GetCdrs());
  ras_Free(cc_GetSizes());
  ras_Free(cc_GetPending());
  ras_Free(cc_GetCombine());
}


BOOL cc_Tautology(CLAUSE clause)
/***************************************************************
  INPUT:   the clause to test
  RETURNS: the decision, if the clause - where all variables are
           regarded as skolem constants - is a tautology, using
           the congruence closure algorithm of Downey, Sethi and
           Tarjan
  CAUTION: overrides the sizes of the clause's terms
***************************************************************/
{
  TERM term, query;

  cc_InitData(clause);
  while (!ras_Empty(cc_GetPending())) {

    /* propagate the closure: */
    while (!ras_Empty(cc_GetPending())) {
      term  = ras_Pop(cc_GetPending());
      query = table_QueryAndEnter(cc_GetTable(), cc_GetPartition(), term);
      if (query != term_Null()) {
        ras_FastPush(cc_GetCombine(), term);
        ras_FastPush(cc_GetCombine(), query);
      }
    }
    while (!ras_Empty(cc_GetCombine()))
      cc_Union(part_Find(cc_GetPartition(), term_Size(ras_Pop(cc_GetCombine()))),
	       part_Find(cc_GetPartition(), term_Size(ras_Pop(cc_GetCombine()))));
  }
  return cc_Outit(clause);
}