/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                     SUBSUMPTION                        * */
/* *                                                        * */
/* *  $Module:   SUBSUMPTION                                * */ 
/* *                                                        * */
/* *  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 "subsumption.h"

static NAT multvec_i[subs__MAXLITS];
static NAT multvec_j[subs__MAXLITS];
static NAT stamp;

static BOOL subs_InternIdc(CLAUSE, int, CLAUSE);
static BOOL subs_InternIdcEq(CLAUSE, int, CLAUSE);
static BOOL subs_InternIdcEqExcept(CLAUSE, int, CLAUSE, int);
static BOOL subs_InternIdcRes(CLAUSE, int, int, int);

/* The following functions are currently unused */
BOOL subs_IdcTestlits(CLAUSE, CLAUSE, LITPTR*);
BOOL subs_Testlits(CLAUSE, CLAUSE);


void subs_Init(void) 
{
  int i;

  stamp = 0;
  for (i = 0; i < subs__MAXLITS; i++)
    multvec_i[i] = multvec_j[i] = 0;
}


static BOOL subs_TestlitsEq(CLAUSE c1, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1 and c2.
  RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{
  TERM  t1,t2;
  int   i,j,n,k;
  BOOL  found;

  n    = clause_Length(c1);
  k    = clause_Length(c2);

  for (i = 0; i < n; i++){
    j     = 0;
    found = FALSE;
    t1    = clause_GetLiteralTerm(c1,i);

    do {
      t2 = clause_GetLiteralTerm(c2,j);
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(), t1, t2))
	found = TRUE;
      else{
	if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) &&
	    fol_IsEquality(fol_Atom(t1)) &&
	    fol_IsEquality(fol_Atom(t2)) &&
	    (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,i)) ||
	     clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) {
	  cont_BackTrackAndStart();
	  if (unify_Match(cont_LeftContext(),
			  term_FirstArgument(fol_Atom(t1)),
			  term_SecondArgument(fol_Atom(t2))) &&
	      unify_Match(cont_LeftContext(),
			  term_SecondArgument(fol_Atom(t1)),
			  term_FirstArgument(fol_Atom(t2))))
	    found = TRUE;
	  else 
	    j++;
	}
	else
	  j++;
      }
      cont_BackTrack();
      
    } while (!found && j < k);
       
    if (!found)
      return FALSE;
  }

  return TRUE;
}


static BOOL subs_STMultiIntern(int i, CLAUSE c1, CLAUSE c2)
/**********************************************************
  INPUT:   Integers i,j and two clauses c1 and c2
           i and j stand for the i-th and the j-th literal 
	   in the clause c1 respectively c2. 
  RETURNS: FALSE if c1 does not multisubsume c2 and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{  
  int  n,j;
  TERM lit1,lit2;

  j       = 0;
  n       = clause_Length(c2);
  lit1    = clause_GetLiteralTerm(c1,i);

  while (j < n) {
    if (multvec_j[j] != stamp) {
      lit2    = clause_GetLiteralTerm(c2,j);
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(),lit1,lit2)) {
	if (i == (clause_Length(c1)-1)) {
	  cont_BackTrack();
	  return TRUE;
	}
	multvec_j[j] = stamp;
	if (subs_STMultiIntern(i+1, c1, c2)) {
	  cont_BackTrack();
	  return TRUE;
	}
	multvec_j[j] = 0;
      }
      cont_BackTrack();
      if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
	  fol_IsEquality(fol_Atom(lit1)) &&
	  fol_IsEquality(fol_Atom(lit2)) &&
	  (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,i)) ||
	   clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) {
	cont_StartBinding();
	if (unify_Match(cont_LeftContext(),
			term_FirstArgument(fol_Atom(lit1)),
			term_SecondArgument(fol_Atom(lit2))) &&
	    unify_Match(cont_LeftContext(),
			term_SecondArgument(fol_Atom(lit1)),
			term_FirstArgument(fol_Atom(lit2)))) {
	  if (i == (clause_Length(c1)-1)) {
	    cont_BackTrack();
	    return TRUE;
	  }
	  multvec_j[j] = stamp;
	  if (subs_STMultiIntern(i+1, c1, c2)) {
	    cont_BackTrack();
	    return TRUE;
	  }
	  multvec_j[j] = 0;
	}
	cont_BackTrack();
      }
    }
    j++;
  }
  return FALSE;
}


BOOL subs_STMulti(CLAUSE c1, CLAUSE c2)
{
  BOOL Result;
  int  n;

  n = clause_Length(c1);

  /*printf("\n St-Multi: %d -> %d",clause_Number(c1),clause_Number(c2));*/

  if (n > clause_Length(c2) ||
      (n > 1 && !subs_TestlitsEq(c1,c2))) {
    /*fputs(" Testlits failure ", stdout);*/
    return(FALSE);
  }

  if (++stamp == NAT_MAX) {
    int i;
    stamp = 1;
    for (i = 0; i < subs__MAXLITS; i++)
    multvec_i[i] = multvec_j[i] = 0;
  }
  /*unify_SaveState();*/
  Result = subs_STMultiIntern(0,c1,c2);
  /*unify_CheckState();*/
  return Result;
}


static BOOL subs_TestlitsEqExcept(CLAUSE C1, CLAUSE C2)
{
  TERM  t1,t2;
  int   i,j,n,k;
  BOOL  found;

  n    = clause_Length(C1);
  k    = clause_Length(C2);

  i = 0;
  while (multvec_i[i] == stamp && i < n)
    i++;

  while (i < n) {
    j     = 0;
    found = FALSE;
    t1    = clause_GetLiteralTerm(C1,i);

    do {
      if (multvec_j[j] == stamp)
	j++;
      else {
	t2 = clause_GetLiteralTerm(C2,j);
	cont_StartBinding();
	if (unify_MatchBindings(cont_LeftContext(), t1, t2))
	  found = TRUE;
	else {
	  if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) &&
	      fol_IsEquality(fol_Atom(t1)) &&
	      fol_IsEquality(fol_Atom(t2)) &&
	      (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) ||
	       clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
	    cont_BackTrackAndStart();
	    if (unify_MatchBindings(cont_LeftContext(),
				    term_FirstArgument(fol_Atom(t1)),
				    term_SecondArgument(fol_Atom(t2))) &&
		unify_MatchBindings(cont_LeftContext(),
				    term_SecondArgument(fol_Atom(t1)),
				    term_FirstArgument(fol_Atom(t2))))
	      found = TRUE;
	    else 
	      j++;
	  }
	  else
	    j++;
	}
	cont_BackTrack();
      }  /* else */
    } while (!found && (j < k));
       
    if (!found) 
      return FALSE;
    do
      i++;
    while (multvec_i[i] == stamp && i < n);
  } /* while i < n */


  return TRUE;
}


static BOOL subs_STMultiExceptIntern(CLAUSE C1, CLAUSE C2)
{
  int  n, i, j, k;
  NAT  occs, occsaux;
  TERM lit1,lit2;

  i    = -1;
  k    = 0;
  occs = 0;
  j    = 0;
  n    = clause_Length(C2);

  while (k < clause_Length(C1)) {
    /* Select Literal with maximal number of variable occurrences. */
    if (multvec_i[k] != stamp) {
      if (i < 0) {
	i    = k;
	occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i));
      } else
	if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k)))
	    > occs) {
	  i    = k;
	  occs = occsaux;
	}
    }
    k++;
  }

  if (i < 0)
    return TRUE;

  lit1 = clause_GetLiteralTerm(C1, i);
  multvec_i[i] = stamp;

  while (j < n) {
    if (multvec_j[j] != stamp) {
      lit2 = clause_GetLiteralTerm(C2, j);
      cont_StartBinding();
      if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) {
	multvec_j[j] = stamp;
	if (subs_STMultiExceptIntern(C1, C2)) {
	  cont_BackTrack();
	  return TRUE;
	}
	multvec_j[j] = 0;
      }
      cont_BackTrack();
      if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
	  fol_IsEquality(fol_Atom(lit1)) &&
	  fol_IsEquality(fol_Atom(lit2)) &&
	  (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) ||
	   clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
	cont_StartBinding();
	if (unify_MatchBindings(cont_LeftContext(),
				term_FirstArgument(fol_Atom(lit1)),
				term_SecondArgument(fol_Atom(lit2))) &&
	    unify_MatchBindings(cont_LeftContext(),
				term_SecondArgument(fol_Atom(lit1)),
				term_FirstArgument(fol_Atom(lit2)))) {
	  multvec_j[j] = stamp;
	  if (subs_STMultiExceptIntern(C1, C2)) {
	    cont_BackTrack();
	    return TRUE;
	  }
	  multvec_j[j] = 0;
	}
	cont_BackTrack();
      }
    }
    j++;
  }
  multvec_i[i] = 0;
  return FALSE;
}


BOOL subs_STMultiExcept(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ)
/**********************************************************
  INPUT:   Two clauses and for each clause a literal that is
           already bound to each other. If the literal value is negative,
	   a general subsumption test is performed.
  RETURNS: TRUE if the first clause subsumes the second one.
  CAUTION: The weight of the clauses must be up to date!
***********************************************************/
{
  BOOL Result;
  int  n;

  n = clause_Length(C1);

  if (n > clause_Length(C2) ||
      (clause_Weight(C1)-clause_LiteralWeight(clause_GetLiteral(C1,ExceptI))) >
      (clause_Weight(C2)-clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ))))
    return FALSE;

  if (++stamp == NAT_MAX) {
    int i;
    stamp = 1;
    for (i = 0; i < subs__MAXLITS; i++)
      multvec_i[i] = multvec_j[i] = 0;
  }
  multvec_i[ExceptI] = stamp;
  multvec_j[ExceptJ] = stamp;

  if (n > 1 && !subs_TestlitsEqExcept(C1, C2))
    return FALSE;

  /*unify_SaveState();*/
  Result = subs_STMultiExceptIntern(C1, C2);
  /*unify_CheckState();*/
  return Result;
}


static BOOL subs_PartnerTest(CLAUSE C1, int c1l, int c1r, CLAUSE C2, int c2l, int c2r)
/**********************************************************
  INPUT:   Two clauses and for each clause a starting left index
           and an exclusive right index.
  RETURNS: TRUE if every literal inside the bounds of the first clause
           can be matched against a literal inside the bounds of the
	   second clause.
  CAUTION: None.
***********************************************************/
{
  TERM  t1,t2;
  int   j;
  BOOL  found;

  if (c1l == c1r)
    return TRUE;

  while (multvec_i[c1l] == stamp && c1l < c1r)
    c1l++;

  if (c1l < c1r) {
    if  (c2l == c2r)
      return FALSE;
    else
      do {
	j     = c2l;
	found = FALSE;
	t1    = clause_GetLiteralTerm(C1,c1l);

	do {
	  if (multvec_j[j] == stamp)
	    j++;
	  else {
	    t2 = clause_GetLiteralTerm(C2,j);
	    cont_StartBinding();
	    if (unify_MatchBindings(cont_LeftContext(), t1, t2))
	      found = TRUE;
	    else {
	      if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) &&
		  fol_IsEquality(fol_Atom(t1)) &&
		  fol_IsEquality(fol_Atom(t2)) &&
		  (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,c1l)) ||
		   clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
		cont_BackTrackAndStart();
		if (unify_MatchBindings(cont_LeftContext(),
					term_FirstArgument(fol_Atom(t1)),
					term_SecondArgument(fol_Atom(t2))) &&
		    unify_MatchBindings(cont_LeftContext(),
					term_SecondArgument(fol_Atom(t1)),
					term_FirstArgument(fol_Atom(t2))))
		  found = TRUE;
		else 
		  j++;
	      }
	      else
		j++;
	    }
	    cont_BackTrack();
	  }  /* else */
	} while (!found && (j < c2r));
       
	if (!found) 
	  return FALSE;
	do
	  c1l++;
	while (multvec_i[c1l] == stamp && c1l < c1r);
      } while (c1l < c1r);
  }
  return TRUE;
}


static BOOL subs_SubsumesInternBasic(CLAUSE C1, int c1fa, int c1fs, int c1l, 
				     CLAUSE C2, int c2fa, int c2fs, int c2l)
{
  int  i, j, n, k;
  NAT  occs, occsaux;
  TERM lit1,lit2;

  i    = -1;
  k    = clause_FirstLitIndex();
  occs = 0;

  while (k < c1l) {     /* Select literal with maximal variable occurrences. */
    if (multvec_i[k] != stamp) {
      if (i < 0) {
	i    = k;
	occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i));
      } else
	if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k)))
	    > occs) {
	  i    = k;
	  occs = occsaux;
	}
    }
    k++;
  }

  if (i < 0)
    return TRUE;

  lit1         = clause_GetLiteralTerm(C1, i);
  multvec_i[i] = stamp;

  if (i < c1fa) {                 /* Only consider relevant partner literals */
    j = clause_FirstLitIndex();
    n = c2fa;
  }
  else if (i < c1fs) {
    j = c2fa;
    n = c2fs;
  }
  else {
    j = c2fs;
    n = c2l;
  }

  while (j < n) {
    if (multvec_j[j] != stamp) {
      lit2 = clause_GetLiteralTerm(C2, j);
      cont_StartBinding();
      if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) {
	multvec_j[j] = stamp;
	if (subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l)) {
	  cont_BackTrack();
	  return TRUE;
	}
	multvec_j[j] = 0;
      }
      cont_BackTrack();
      if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
	  fol_IsEquality(fol_Atom(lit1)) &&
	  fol_IsEquality(fol_Atom(lit2)) &&
	  (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) ||
	   clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
	cont_StartBinding();
	if (unify_MatchBindings(cont_LeftContext(),
				term_FirstArgument(fol_Atom(lit1)),
				term_SecondArgument(fol_Atom(lit2))) &&
	    unify_MatchBindings(cont_LeftContext(),
				term_SecondArgument(fol_Atom(lit1)),
				term_FirstArgument(fol_Atom(lit2)))) {
	  multvec_j[j] = stamp;
	  if (subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l)) {
	    cont_BackTrack();
	    return TRUE;
	  }
	  multvec_j[j] = 0;
	}
	cont_BackTrack();
      }
    }
    j++;
  }
  multvec_i[i] = 0;
  return FALSE;
}


BOOL subs_SubsumesBasic(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ)
/**********************************************************
  INPUT:   Two clauses and for each clause a literal that are
           already bound to each other. If the literal value is negative,
	   a general subsumption test is performed.
  RETURNS: TRUE if the first clause subsumes the second one with respect
           to basic restrictions on the sort literals.
  CAUTION: The weight of the clauses must be up to date!
***********************************************************/
{
  BOOL Result;
  int  c1fa,c1fs,c1l,c2fa,c2fs,c2l,lw1,lw2;

  c1fa = clause_FirstAntecedentLitIndex(C1);
  c1fs = clause_FirstSuccedentLitIndex(C1);
  c1l  = clause_Length(C1);
  c2fa = clause_FirstAntecedentLitIndex(C2);
  c2fs = clause_FirstSuccedentLitIndex(C2);
  c2l  = clause_Length(C2);

  lw1 = (ExceptI >= clause_FirstLitIndex() ?
	 clause_LiteralWeight(clause_GetLiteral(C1,ExceptI)) : 0);
  lw2 = (ExceptJ >= clause_FirstLitIndex() ?
	 clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ)) : 0);

  if (c1l > c2l ||                               /* Multiset restriction */
      (clause_Weight(C1)-lw1) >  (clause_Weight(C2)-lw2)) {
    return FALSE;
  }

  if (++stamp == NAT_MAX) {
    int i;
    stamp = 1;
    for (i = 0; i < subs__MAXLITS; i++)
      multvec_i[i] = multvec_j[i] = 0;
  }

  if (ExceptI >= clause_FirstLitIndex())
    multvec_i[ExceptI] = stamp;
  if (ExceptJ >= clause_FirstLitIndex())
    multvec_j[ExceptJ] = stamp;

  if (c1l > 1 && 
      (!subs_PartnerTest(C1,clause_FirstConstraintLitIndex(C1),c1fa,
			 C2,clause_FirstConstraintLitIndex(C2),c2fa) ||
       !subs_PartnerTest(C1,c1fa,c1fs,C2,c2fa,c2fs) ||
       !subs_PartnerTest(C1,c1fs,c1l,C2,c2fs,c2l)))
    return FALSE;

#ifdef CHECK
  cont_SaveState();
#endif

  Result = subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l);

#ifdef CHECK
  cont_CheckState();
#endif

  return Result;
}


static BOOL subs_SubsumesInternWithSignature(int i, CLAUSE c1, CLAUSE c2, BOOL Variants, LIST* Bindings)
/**********************************************************
  INPUT:   
  RETURNS: 
  CAUTION: 
***********************************************************/
{  
  int  n,j;
  TERM lit1,lit2;
  LIST NewBindings,Scan;

  j           = 0;
  n           = clause_Length(c2);
  lit1        = clause_GetLiteralTerm(c1,i);
  NewBindings = list_Nil();

  while (j < n) {
    if (multvec_j[j] != stamp) {
      lit2    = clause_GetLiteralTerm(c2,j);
      cont_StartBinding();
      if (fol_SignatureMatch(lit1,lit2,&NewBindings,Variants)) {
	if (i == (clause_Length(c1)-1)) {
	  *Bindings = list_Nconc(NewBindings,*Bindings);
	  return TRUE;
	}
	multvec_j[j] = stamp;
	if (subs_SubsumesInternWithSignature(i+1, c1, c2,Variants,&NewBindings)) {
	  *Bindings = list_Nconc(NewBindings,*Bindings);
	  return TRUE;
	}
	multvec_j[j] = 0;
      }      
      for (Scan=NewBindings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { /* Backtrack bindings */
	if (symbol_IsVariable((SYMBOL)list_Car(Scan)))
	  term_ClearBinding((SYMBOL)list_Car(Scan));
	else
	  symbol_ContextClearValue((SYMBOL)list_Car(Scan));
      }
      list_Delete(NewBindings);
      NewBindings = list_Nil();
      if (symbol_Equal(term_TopSymbol(fol_Atom(lit1)),term_TopSymbol(fol_Atom(lit2))) &&
	  fol_IsEquality(fol_Atom(lit1))) {
	if (fol_SignatureMatch(term_FirstArgument(fol_Atom(lit1)),
			       term_SecondArgument(fol_Atom(lit2)), &NewBindings, Variants) &&
	    fol_SignatureMatch(term_SecondArgument(fol_Atom(lit1)),
			       term_FirstArgument(fol_Atom(lit2)), &NewBindings, Variants)) {
	  if (i == (clause_Length(c1)-1)) {
	    *Bindings = list_Nconc(NewBindings,*Bindings);
	    return TRUE;
	  }
	  multvec_j[j] = stamp;
	  if (subs_SubsumesInternWithSignature(i+1, c1, c2,Variants,&NewBindings)) {
	    *Bindings = list_Nconc(NewBindings,*Bindings);
	    return TRUE;
	  }
	  multvec_j[j] = 0;
	}
	for (Scan=NewBindings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { /* Backtrack bindings */
	  if (symbol_IsVariable((SYMBOL)list_Car(Scan)))
	    term_ClearBinding((SYMBOL)list_Car(Scan));
	  else
	    symbol_ContextClearValue((SYMBOL)list_Car(Scan));
	}
	list_Delete(NewBindings);
	NewBindings = list_Nil();
      }
    }
    j++;
  }
  return FALSE;
}

BOOL subs_SubsumesWithSignature(CLAUSE C1, CLAUSE C2, BOOL Variants, LIST *Bindings)
/**********************************************************
  INPUT:   Two clauses .
  RETURNS: TRUE if the first clause subsumes the second one where
           we allow signature symbols to be matched as well.
	   If <Variants> is TRUE variables must be mapped to variables.
	   Returns the signature symbols that were bound.
  EFFECT:  Symbol context bindings are established.
***********************************************************/
{
  BOOL Result;

  if (clause_Length(C1) > clause_Length(C2) ||
      clause_NumOfSuccLits(C1) > clause_NumOfSuccLits(C2) ||
      (clause_NumOfAnteLits(C1) + clause_NumOfConsLits(C1)) > 
      (clause_NumOfAnteLits(C2) + clause_NumOfConsLits(C2))) {   /* Multiset restriction */
    return FALSE;
  }

  if (++stamp == NAT_MAX) {
    int i;
    stamp = 1;
    for (i = 0; i < subs__MAXLITS; i++)
      multvec_i[i] = multvec_j[i] = 0;
  }

  term_NewMark();
  Result =  subs_SubsumesInternWithSignature(clause_FirstLitIndex(),C1,C2,Variants, Bindings);
  *Bindings = list_DeleteElementIf(*Bindings, (BOOL (*)(POINTER)) symbol_IsVariable);
  return Result;
}

static BOOL subs_SubsumesIntern(CLAUSE C1, int c1fs, int c1l, CLAUSE C2, int c2fs, int c2l)
{
  int  i, j, n, k;
  NAT  occs, occsaux;
  TERM lit1,lit2;

  i    = -1;
  k    = clause_FirstLitIndex();
  occs = 0;

  while (k < c1l) {     /* Select literal with maximal variable occurrences. */
    if (multvec_i[k] != stamp) {
      if (i < 0) {
	i    = k;
	occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i));
      } else
	if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k)))
	    > occs) {
	  i    = k;
	  occs = occsaux;
	}
    }
    k++;
  }

  if (i < 0)
    return TRUE;

  lit1         = clause_GetLiteralTerm(C1, i);
  multvec_i[i] = stamp;

  if (i < c1fs) {                  /* Only consider relevant partner literals */
    j = clause_FirstLitIndex();
    n = c2fs;
  }
  else {
    j = c2fs;
    n = c2l;
  }

  while (j < n) {
    if (multvec_j[j] != stamp) {
      lit2 = clause_GetLiteralTerm(C2, j);
      cont_StartBinding();
      if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) {
	multvec_j[j] = stamp;
	if (subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l)) {
	  cont_BackTrack();
	  return TRUE;
	}
	multvec_j[j] = 0;
      }
      cont_BackTrack();
      if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
	  fol_IsEquality(fol_Atom(lit1)) &&
	  fol_IsEquality(fol_Atom(lit2)) &&
	  (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) ||
	   clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) {
	cont_StartBinding();
	if (unify_MatchBindings(cont_LeftContext(),
				term_FirstArgument(fol_Atom(lit1)),
				term_SecondArgument(fol_Atom(lit2))) &&
	    unify_MatchBindings(cont_LeftContext(),
				term_SecondArgument(fol_Atom(lit1)),
				term_FirstArgument(fol_Atom(lit2)))) {
	  multvec_j[j] = stamp;
	  if (subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l)) {
	    cont_BackTrack();
	    return TRUE;
	  }
	  multvec_j[j] = 0;
	}
	cont_BackTrack();
      }
    }
    j++;
  }
  multvec_i[i] = 0;
  return FALSE;
}


BOOL subs_Subsumes(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ)
/**********************************************************
  INPUT:   Two clauses and for each clause a literal that is
           already bound to each other. If the literal value is negative,
	   a general subsumption test is performed.
  RETURNS: TRUE if the first clause subsumes the second one.
  CAUTION: The weight of the clauses must be up to date!
***********************************************************/
{
  BOOL Result;
  int  c1fs, c1l, c2fs, c2l, lw1, lw2;

  c1fs   = clause_FirstSuccedentLitIndex(C1);
  c1l    = clause_Length(C1);
  c2fs   = clause_FirstSuccedentLitIndex(C2);
  c2l    = clause_Length(C2);
  
  lw1 = (ExceptI >= clause_FirstLitIndex() ?
	 clause_LiteralWeight(clause_GetLiteral(C1,ExceptI)) : 0);
  lw2 = (ExceptJ >= clause_FirstLitIndex() ?
	 clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ)) : 0);

  if (c1l > c2l ||                               /* Multiset restriction */
      (clause_Weight(C1) - lw1) > (clause_Weight(C2) - lw2))
    return FALSE;

  if (++stamp == NAT_MAX) {
    int i;
    stamp = 1;
    for (i = 0; i < subs__MAXLITS; i++)
      multvec_i[i] = multvec_j[i] = 0;
  }

  if (ExceptI >= clause_FirstLitIndex())
    multvec_i[ExceptI] = stamp;
  if (ExceptJ >= clause_FirstLitIndex())
    multvec_j[ExceptJ] = stamp;

  if (c1l > 1 && 
      (!subs_PartnerTest(C1,clause_FirstConstraintLitIndex(C1),c1fs,
			 C2,clause_FirstConstraintLitIndex(C2),c2fs) ||
       !subs_PartnerTest(C1,c1fs,c1l,C2,c2fs,c2l)))
    return FALSE;

#ifdef CHECK
  cont_SaveState();
#endif

  Result = subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l);
  
#ifdef CHECK
  cont_CheckState();
#endif

  return Result;
}


BOOL subs_ST(int i, int j, CLAUSE c1, CLAUSE c2)
/**********************************************************
  INPUT:   Integers i,j and two clauses c1 and c2.
           i and j stand for the i-th and the j-th literal 
	   in the clause c1 respectively c2.
  RETURNS: FALSE if c1 does not subsume c2 and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{  
  cont_StartBinding();

  while ((j < clause_Length(c2)) &&
	 !(unify_Match(cont_LeftContext(),
		       clause_GetLiteralTerm(c1,i),
		       clause_GetLiteralTerm(c2,j)))){
    j++;
    cont_BackTrackAndStart();
  }

  if (j >= clause_Length(c2)) {
    cont_BackTrack();
    return FALSE;
  }

  if ((i == (clause_Length(c1)-1)) || subs_ST(i+1, 0, c1, c2))
    return TRUE;
  else
    cont_BackTrack();

  if (++j == clause_Length(c2))
    return FALSE;

  return subs_ST(i, j, c1, c2);
}


BOOL subs_Testlits(CLAUSE c1, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1 and c2.
  RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{
  TERM   t1;
  int  i,j;
  BOOL found;

  for (i = 0; i < clause_Length(c1); i++){
    j     = 0;
    found = FALSE;
    t1    = clause_GetLiteralTerm(c1,i);

    do {
      cont_StartBinding();
      if (!(found = unify_Match(cont_LeftContext(), t1, clause_GetLiteralTerm(c2,j))))
	j++;
      cont_BackTrack();
      
    } while (!found && (j < clause_Length(c2)));
       
    if (!found)
      return FALSE;
  }

  return TRUE;
}


static LIST subs_GetVariables(TERM t)
/**********************************************************
  INPUT:   A term.
  RETURNS: The list of non bound variables of the term.
  CAUTION: None.
***********************************************************/
{
  LIST scan,insert,symbols,end;

  symbols = term_VariableSymbols(t);
  insert  = symbols;
  end     = list_Nil();

  for (scan = symbols; !list_Empty(scan); scan = list_Cdr(scan)) {
    if (!cont_VarIsBound(cont_LeftContext(), (SYMBOL)list_Car(scan))) {
      end    = insert;
      list_Rplaca(insert, list_Car(scan));
      insert = list_Cdr(insert);
    }
  }

  if (!list_Empty(insert)) {
    list_Delete(insert);
    if (list_Empty(end))
      symbols = list_Nil();
    else
      list_Rplacd(end,list_Nil());
  }

  return(symbols);
}


static BOOL subs_SubsumptionPossible(CLAUSE c1, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1 and c2.
  RETURNS: TRUE if every literal in c1 can independently be
           matched to a literal in c2.
  CAUTION: None.
***********************************************************/
{
  int i,j;

  for (i = 0; i < clause_Length(c1); i++) {
    for (j = 0; j < clause_Length(c2); j++) {
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(),
		      clause_GetLiteralTerm(c1,i),
		      clause_GetLiteralTerm(c2,j)))
	j = clause_Length(c2) + 1;
      cont_BackTrack();
    }
    if (j == clause_Length(c2))
      return FALSE;
  }

  return TRUE;
}


BOOL subs_IdcTestlits(CLAUSE c1, CLAUSE c2, LITPTR* litptr)
/**********************************************************
  INPUT:   Two clauses c1, c2  and a pointer to a litptr structure.
  RETURNS: FALSE if c1 can not independently be matched 
           to c2 and TRUE otherwise.
  CAUTION: A structure is build and litptr points to that structure.
***********************************************************/
{
  LIST  TermIndexlist,VarSymbList,TermSymbList;
  int   i;

  if (subs_SubsumptionPossible(c1,c2)) {
 
    TermIndexlist  = list_Nil();
    VarSymbList    = list_Nil();
    TermSymbList   = list_Nil();
 
    for (i = 0; i < clause_Length(c1); i++) {
      VarSymbList = subs_GetVariables(clause_GetLiteralTerm(c1,i));
   
      if (VarSymbList != list_Nil()){
	TermIndexlist = list_Cons((POINTER)i, TermIndexlist);         
	TermSymbList  = list_Cons(VarSymbList,TermSymbList);
      } 
    }
  
    *litptr = litptr_Create(TermIndexlist,TermSymbList); 

    list_Delete(TermSymbList);
    list_Delete(TermIndexlist);

    return TRUE;
  }
  return FALSE;
}


static BOOL subs_SubsumptionVecPossible(CLAUSE c1, int vec, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1 and c2 and a vector pointer.
  RETURNS: TRUE if all literals in c1 which indexes stand
           in the vector with bottom pointer vec can 
	   independently be matched to a literal in c2.
  CAUTION: None.
***********************************************************/
{
  int i,j;

  for (i = vec; i < vec_ActMax(); i++) {
    for (j = 0; j < clause_Length(c2); j++) {
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(),
		      clause_GetLiteralTerm(c1, (int) vec_GetNth(i)), 
		      clause_GetLiteralTerm(c2,j)))
	j = clause_Length(c2) + 1;
      cont_BackTrack();
    }
    if (j == clause_Length(c2))
      return FALSE;
  }
  
  return TRUE;
}


static BOOL subs_SubsumptionVecPossibleEq(CLAUSE c1, int vec, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1 and c2 and a vector pointer.
  RETURNS: TRUE if all literals in c1 which indexes stand
           in the vector with bottom pointer vec can 
	   independently be matched to a literal in c2.
  CAUTION: None.
***********************************************************/
{
  int    i,j,n;
  TERM   lit1,lit2;
  
  n = clause_Length(c2);
  for (i = vec; i < vec_ActMax(); i++) {
    lit1 = clause_GetLiteralTerm(c1, (int) vec_GetNth(i));
    for (j=0;j<n;j++) {
      lit2 = clause_GetLiteralTerm(c2,j);
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(),lit1,lit2)) {
	j = n + 1;
	cont_BackTrack();
      }
      else {
	cont_BackTrack();
	if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
	    fol_IsEquality(fol_Atom(lit1)) &&
	    fol_IsEquality(fol_Atom(lit2)) &&
	    (clause_LiteralIsNotOrientedEquality(
               clause_GetLiteral(c1, (int)vec_GetNth(i))) ||
	     clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) {
	  cont_StartBinding();
	  if (unify_Match(cont_LeftContext(),
			  term_FirstArgument(fol_Atom(lit1)),
			  term_SecondArgument(fol_Atom(lit2))) &&
	      unify_Match(cont_LeftContext(),
			  term_SecondArgument(fol_Atom(lit1)),
			  term_FirstArgument(fol_Atom(lit2))))
	      j = n+1;
	  cont_BackTrack();
	}
      }
    }
    if (j==n)
	return FALSE;
  }
  
  return TRUE;
}


static BOOL subs_IdcVecTestlits(CLAUSE c1, int vec, CLAUSE c2, LITPTR* litptr)
/**********************************************************
  INPUT:   Two clauses c1, c2, a pointer to a literal structure and
           a vector pointer.
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec do not subsume c2 and TRUE otherwise.
  CAUTION: A structure is build and litptr points to that structure.
***********************************************************/
{
  LIST  TermIndexlist,VarSymbList,TermSymbList;
  int   i;
  
  if (subs_SubsumptionVecPossible(c1,vec,c2)) {
    
    TermIndexlist  = list_Nil();
    VarSymbList    = list_Nil();
    TermSymbList   = list_Nil();
    
    for (i = vec; i < vec_ActMax(); i++) {
      VarSymbList =
	subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i)));
   
      if (VarSymbList != list_Nil()){
	TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist);         
	TermSymbList  = list_Cons(VarSymbList,TermSymbList);
      } 
    }
	    
    *litptr = litptr_Create(TermIndexlist,TermSymbList); 

    list_Delete(TermSymbList);
    list_Delete(TermIndexlist);
	
    return TRUE;
  }
  return FALSE;
}


static BOOL subs_IdcVecTestlitsEq(CLAUSE c1, int vec, CLAUSE c2,
				  LITPTR* litptr)
/**********************************************************
  INPUT:   Two clauses c1, c2, a pointer to a literal structure and
           a vector pointer.
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec do not subsume c2 and TRUE otherwise.
  CAUTION: A structure is build and litptr points to that structure.
***********************************************************/
{
  LIST  TermIndexlist,VarSymbList,TermSymbList;
  int   i;
  
  if (subs_SubsumptionVecPossibleEq(c1,vec,c2)) {
    
    TermIndexlist  = list_Nil();
    VarSymbList    = list_Nil();
    TermSymbList   = list_Nil();
    
    for (i = vec; i < vec_ActMax(); i++){
      VarSymbList =
	subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i)));
   
      if (VarSymbList != list_Nil()){
	TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist);         
	TermSymbList  = list_Cons(VarSymbList,TermSymbList);
      } 
    }
	    
    *litptr = litptr_Create(TermIndexlist,TermSymbList); 

    list_Delete(TermSymbList);
    list_Delete(TermIndexlist);
	
    return TRUE;
  }
  return FALSE;
}


static void subs_CompVec(LITPTR litptr)
/**********************************************************
  INPUT:   A  LITPTR pointer.
  RETURNS: None.
  CAUTION: Indexes are pushed on the vector. These indexes build
           a component with respect to the structure litptr and to the 
	   actual bindings.
***********************************************************/
{
  LIST complist, end, scan;
  int  lit,n,i,j;

  n        = litptr_Length(litptr);
  complist = list_Nil();


  if (n > 0){
    for (j = 0; j < n; j++) {
      if (!literal_GetUsed(litptr_Literal(litptr,j))) {
	complist = list_Cons((POINTER)j,complist);
	vec_Push((POINTER)literal_GetLitIndex(litptr_Literal(litptr,j)));
	literal_PutUsed(litptr_Literal(litptr,j), TRUE);
	j = n + 1;
      }
    }

    if (j != n) {
      end = complist;
      for (scan = complist; !list_Empty(scan); scan = list_Cdr(scan)) {
	lit = (int)list_Car(scan);
	for (i = 0; i < n; i++) {
	  if (!literal_GetUsed(litptr_Literal(litptr,i)) &&
	     list_HasIntersection(literal_GetLitVarList(litptr_Literal(litptr,lit)),
				  literal_GetLitVarList(litptr_Literal(litptr,i)))) {
	    list_Rplacd(end,list_List((POINTER)i));
	    end = list_Cdr(end);
	    vec_Push((POINTER)literal_GetLitIndex(litptr_Literal(litptr,i)));
	    literal_PutUsed(litptr_Literal(litptr,i), TRUE);
	  }
	}
      }
      list_Delete(complist);
    }
  }
}


static BOOL subs_StVec(int i, int j, CLAUSE c1, CLAUSE c2)
/**********************************************************
  INPUT:   Integers i,j and two clauses c1 and c2.
           i is a pointer to vector and represents a 
	   literal in clause c1 and j stand for the j-th 
	   literal in the clause c2.
  RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{  
  int a;
    
  if (j >= clause_Length(c2))
    return FALSE;
    
  a = j;
  
  cont_StartBinding();

  while ((a < clause_Length(c2)) && 
	 !(unify_Match(cont_LeftContext(),
		       clause_GetLiteralTerm(c1, (int) vec_GetNth(i)),
		       clause_GetLiteralTerm(c2,a)))){
    a++;
    cont_BackTrackAndStart();
  }
  
  if (a >= clause_Length(c2)) {
    cont_BackTrack();
    return FALSE;
  }

  if ((i == (vec_ActMax()-1)) || subs_StVec(i+1, 0, c1, c2))
    return TRUE;
  else 
    cont_BackTrack();

  return subs_StVec(i, a+1, c1, c2);
}


static int subs_SearchTop(CLAUSE c1, int vec, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1, c2, a vector pointer vec.
  RETURNS: The index of that literal in c1 which has the least positive
           matching tests with the literals in c2.
  CAUTION: None.
***********************************************************/
{
  int index, i, j, zaehler;

  index = (int)vec_GetNth(vec);

  for (i = vec; i < vec_ActMax(); i++) {
    zaehler = 0;
    j       = 0;
    while (j < clause_Length(c2) && zaehler < 2) {
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(),
		      clause_GetLiteralTerm(c1, (int) vec_GetNth(i)),
		      clause_GetLiteralTerm(c2,j))) {
	zaehler++;
      }
      cont_BackTrack();
      j++;
    }

    if (zaehler == 0 || zaehler == 1) {
      index = (int)vec_GetNth(i);
      return index;
    }
  }
  return index;
}


static BOOL subs_TcVec(CLAUSE c1, int vec, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1, c2, a vector pointer vec.
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec do not subsume c2 and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{
  int a,top_index;
  a    = 0;

  top_index = subs_SearchTop(c1,vec,c2);
    
  do {
    cont_StartBinding();
    while ((a < clause_Length(c2)) &&
	   !(unify_Match(cont_LeftContext(),
			 clause_GetLiteralTerm(c1,top_index),
			 clause_GetLiteralTerm(c2,a)))) {
      a++;
      cont_BackTrackAndStart();
    }
    
    if (a >= clause_Length(c2)){
      cont_BackTrack();
      return FALSE;
    }

    if ((vec - vec_ActMax()) == 1) 
      return TRUE;		
    
    if (subs_InternIdc(c1, vec, c2))
      return TRUE;
    else {
      cont_BackTrack();	/* Dies ist der 'Hurra' Fall.*/
      a++;			
    }

  } while (a < clause_Length(c2));
  
  return FALSE;
}

static BOOL subs_TcVecEq(CLAUSE c1, int vec, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1, c2, a vector pointer vec.
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec do not subsume c2 and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{
  int a,top_index;
  BOOL search;
  TERM lit1,lit2;

  a         = 0;
  top_index = subs_SearchTop(c1,vec,c2);
  lit1      = clause_GetLiteralTerm(c1,top_index);
    
  do {
    search = TRUE;

    while (a < clause_Length(c2) && search) {
      lit2 = clause_GetLiteralTerm(c2,a);
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(),lit1,lit2))
	search = FALSE;
      else {
	if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
	    fol_IsEquality(fol_Atom(lit1)) &&
	    fol_IsEquality(fol_Atom(lit2)) &&
	    (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,top_index)) ||
	     clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,a)))) {
	  cont_BackTrackAndStart();
	  if (unify_Match(cont_LeftContext(),
			  term_FirstArgument(fol_Atom(lit1)),
			  term_SecondArgument(fol_Atom(lit2))) &&
	      unify_Match(cont_LeftContext(),
			  term_SecondArgument(fol_Atom(lit1)),
			  term_FirstArgument(fol_Atom(lit2))))
	    search = FALSE;
	}
	if (search) {
	  a++;
	  cont_BackTrack();
	}
      }
    }
    
    if (a >= clause_Length(c2)) {
      cont_BackTrack();
      return FALSE;
    }

    if ((vec_ActMax() - vec) == 1) 
      return TRUE;		
    
    if (subs_InternIdcEq(c1, vec, c2))
      return TRUE;
    else {
      cont_BackTrack();
      a++;			
    }

  } while (a < clause_Length(c2));
  
  return FALSE;
}


static BOOL subs_InternIdc(CLAUSE c1, int vec, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1, c2, a vector pointer vec.
  RETURNS: FALSE if the literals of c1 which are designed by
           the elements of vec do not subsume c2 and TRUE otherwise.
  CAUTION: 
***********************************************************/
{
  int        locvec;
  LITPTR litptr;
  
  
  if (!subs_IdcVecTestlits(c1,vec,c2,&litptr))
    return FALSE;

  locvec = vec_ActMax();
  
  do {
    subs_CompVec(litptr);	
    if (!vec_IsMax(locvec)) {
      if (!subs_TcVec(c1,locvec,c2)) {
	vec_SetMax(locvec);
	litptr_Delete(litptr);
	return FALSE;
      } 
      else
	vec_SetMax(locvec);
    }
  } while (!litptr_AllUsed(litptr));

  litptr_Delete(litptr);
  
  return TRUE;
}


static BOOL subs_InternIdcEq(CLAUSE c1, int vec, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1, c2, a vector pointer vec.
  RETURNS: FALSE if the literals of c1 which are designed by
           the elements of vec do not subsume c2 and TRUE otherwise.
  CAUTION: 
***********************************************************/
{
  int        locvec;
  LITPTR litptr;
  
  
  if (!subs_IdcVecTestlitsEq(c1,vec,c2,&litptr))
    return FALSE;

  locvec = vec_ActMax();
  
  do {
    subs_CompVec(litptr);	
    if (!vec_IsMax(locvec)) {
      if (!subs_TcVecEq(c1,locvec,c2)) {
	vec_SetMax(locvec);
	litptr_Delete(litptr);
	return FALSE;
      } 
      else
	vec_SetMax(locvec);
    }

  } while (!litptr_AllUsed(litptr));

  litptr_Delete(litptr);
  
  return TRUE;
}


BOOL subs_Idc(CLAUSE c1, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1, c2.
  RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
  CAUTION: 
***********************************************************/
{
  int  i,vec;
  BOOL Result;

  vec = vec_ActMax();

  for (i = 0; i < clause_Length(c1); i++)
    vec_Push((POINTER) i);

  Result = subs_InternIdc(c1,vec,c2);
    
  vec_SetMax(vec);

  cont_Reset();
    
  return Result;
}


BOOL subs_IdcEq(CLAUSE c1, CLAUSE c2)
/**********************************************************
  INPUT:   Two clauses c1, c2.
  RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
  CAUTION: 
***********************************************************/
{
  int  i,vec;
  BOOL Result;

  /*fputs("\n Idc on:  ", stdout); clause_Print(c1);
    putchar('\t'); clause_Print(c2); */ 
  vec = vec_ActMax();

  for (i = 0; i < clause_Length(c1); i++)
    vec_Push((POINTER) i);

  Result = subs_InternIdcEq(c1,vec,c2);
    
  vec_SetMax(vec);

  cont_Reset();

  /*printf(" Result: %s ",(Result ? "TRUE" : "FALSE"));*/

  return Result;
}


BOOL subs_IdcEqMatch(CLAUSE c1, CLAUSE c2, SUBST subst)
/**********************************************************
  INPUT:   Two clauses c1, c2.
  RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise.
  CAUTION: 
***********************************************************/
{
  int  i,vec;
  BOOL Result;

  /* fputs("\n Idc on:  ", stdout); clause_Print(c1);
     putchar('\t'); clause_Print(c2);   DBG */
  vec = vec_ActMax();

  for (i = 0; i < clause_Length(c1); i++)
    vec_Push((POINTER) i);

  i = 0;        /* Doesn't matter, there is a general cont_Reset below */
  unify_EstablishMatcher(cont_LeftContext(), subst);

  Result = subs_InternIdcEq(c1,vec,c2);
    
  vec_SetMax(vec);

  cont_Reset();

  /*fputs("\nsubs_Idc end: ",stdout); clause_Print(c1); clause_Print(c2); DBG */

  return Result;
}


static BOOL subs_SubsumptionVecPossibleRes(CLAUSE c1, int vec,
					   int beg, int end)
/**********************************************************
  INPUT:   Two clauses c1 and c2 and three vector pointer
           vec,beg and end.
  RETURNS: TRUE if all literals in c1 which indexes stand
           in the vector with bottom pointer vec can 
	   independently be matched to a literal in c2
	   which indexes stand in the vector between the
	   pointers beg and end (exclusive).
  CAUTION: None.
***********************************************************/
{
  int  j,i;

  for (i = vec; i < vec_ActMax(); i++) {
    for (j = beg; j < end; j++){
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(),
		      clause_GetLiteralTerm(c1, (int) vec_GetNth(i)), 
		      clause_GetLiteralTerm(c1, (int) vec_GetNth(j))))
	j = end+1;
      cont_BackTrack();
    }
    if (j == end)
      return FALSE;
  }
  return TRUE;
}


static BOOL subs_IdcVecTestlitsRes(CLAUSE c1, int vec,
				   int beg, int end, LITPTR* litptr)
/**********************************************************
  INPUT:   A clause c1, a pointer to a literal structure and
           three  vector pointer vec, beg and end.
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec can not be matched independently
	   to literal in c2 which are designated by the elements
	   of the vector between the pointers beg and end (exclusive).
  CAUTION: A structure is build and litptr points to that structure.
***********************************************************/
{
  LIST  TermIndexlist,VarSymbList,TermSymbList;
  int   i;
  
  if (subs_SubsumptionVecPossibleRes(c1,vec,beg,end)) {
    
    TermIndexlist  = list_Nil();
    VarSymbList    = list_Nil();
    TermSymbList   = list_Nil();
    
    for (i = vec; i < vec_ActMax(); i++) {
      VarSymbList =
	subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i)));
      
      if (VarSymbList != list_Nil()) {
	TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist);         
	TermSymbList  = list_Cons(VarSymbList,TermSymbList);
      } 
    }
    
    *litptr = litptr_Create(TermIndexlist,TermSymbList); 
    
    list_Delete(TermSymbList);
    list_Delete(TermIndexlist);
    
    return TRUE;
  }
  return FALSE;
}


static int subs_SearchTopRes(CLAUSE c1, int vec, int beg, int end)
/**********************************************************
  INPUT:   A clause c1, three vector pointers vec, beg and end.
  RETURNS: The index of that literal in c1 which has the least positive
           matching tests with the literals in c2 with respect to
	   vector and the vector pointers beg and end.
  CAUTION: None.
***********************************************************/
{
  int  index,i,j,zaehler;
    
  index = (int) vec_GetNth(vec);

  for (i = vec; i < vec_ActMax(); i++) {
    zaehler = 0;
    j       = beg;
    while ((j < end) && (zaehler < 2)) {
      cont_StartBinding();
      if (unify_Match(cont_LeftContext(),
		      clause_GetLiteralTerm(c1, (int) vec_GetNth(i)),
		      clause_GetLiteralTerm(c1, (int) vec_GetNth(j)))) {
	zaehler++;
      }
      cont_BackTrack();
      j++;
    }

    if (zaehler == 0 || zaehler == 1) {
      index = (int)vec_GetNth(i);
      return index;
    }
  }
  return index;
}


static BOOL subs_TcVecRes(CLAUSE c1, int vec, int beg, int end)
/**********************************************************
  INPUT:   A clause c1, three vector pointers vec,beg and end.
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec do not subsume c2 with 
	   respect to the vector and the vector pointers
	   beg and end and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{
  int  a,top_index;

  a = beg;

  top_index = subs_SearchTopRes(c1,vec,beg,end);
    
  do {
    cont_StartBinding();
    while ((a < end) && 
	   !unify_Match(cont_LeftContext(),
			clause_GetLiteralTerm(c1,top_index),
			clause_GetLiteralTerm(c1,(int)vec_GetNth(a)))) {
      a++;
      cont_BackTrackAndStart();
    }
    
    if (a >= end){
      cont_BackTrack();
      return FALSE;
    }

    if ((vec - vec_ActMax()) == 1)
      return TRUE;		    
                                    
    if (subs_InternIdcRes(c1, vec, beg, end))
      return TRUE;
    else {
      cont_BackTrack();	
      a++;
    }

  } while (a < end);
  
  return FALSE;
}
       

static BOOL subs_InternIdcRes(CLAUSE c1, int vec, int beg, int end)
/**********************************************************
  INPUT:   A clause c1 and three  vector pointers vec,beg and end.
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec do not subsume c2 with respect
	   to vector and the vector pointers beg and end 
	   and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{
  int        locvec;
  LITPTR litptr;
  
  
  if (!subs_IdcVecTestlitsRes(c1,vec,beg,end,&litptr))
    return FALSE;

  locvec = vec_ActMax();
  
  do {
    subs_CompVec(litptr);	
    if (!vec_IsMax(locvec)) {
      if (!subs_TcVecRes(c1,locvec,beg,end)) {
	vec_SetMax(locvec);
	litptr_Delete(litptr);
	return FALSE;
      } 
      else
	vec_SetMax(locvec);
    }
  } while (!litptr_AllUsed(litptr));

  litptr_Delete(litptr);
  
  return TRUE;
}


BOOL subs_IdcRes(CLAUSE c1, int beg, int end)
/**********************************************************
  INPUT:   A clause c1 and two vector pointers beg and end.
  RETURNS: FALSE if c1 do not subsume c2 with respect to
           vector and the vector pointers beg and end
	   and TRUE otherwise.
  CAUTION: 
***********************************************************/
{
  int  i,vec;
  BOOL Result;
  
  vec = vec_ActMax();
  
  for (i = 0; i < clause_Length(c1); i++)
    vec_Push((POINTER) i);
  
  Result = subs_InternIdcRes(c1, vec, beg, end);
  
  vec_SetMax(vec);
  
  cont_Reset();
  
  return Result;
}


static BOOL subs_TcVecEqExcept(CLAUSE c1, int vec, CLAUSE c2, int i2)
/**********************************************************
  INPUT:   Two clauses c1, c2, a vector pointer vec.
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec do not subsume c2 and TRUE otherwise.
  CAUTION: None.
***********************************************************/
{
  int a,top_index;
  BOOL search;
  TERM lit1,lit2;

  a         = 0;
  top_index = subs_SearchTop(c1,vec,c2);
  lit1      = clause_GetLiteralTerm(c1,top_index);
    
  do {
    search = TRUE;

    while (a < clause_Length(c2) && search) {
      if (a != i2) {
	lit2 = clause_GetLiteralTerm(c2,a);
	cont_StartBinding();
	if (unify_Match(cont_LeftContext(),lit1,lit2))
	    search = FALSE;
	else {
	  if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
	      fol_IsEquality(fol_Atom(lit1)) &&
	      fol_IsEquality(fol_Atom(lit2)) &&
	      (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,top_index)) ||
	       clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,a)))) {
	    cont_BackTrackAndStart();
	    if (unify_Match(cont_LeftContext(),
			    term_FirstArgument(fol_Atom(lit1)),
			    term_SecondArgument(fol_Atom(lit2))) &&
		unify_Match(cont_LeftContext(),
			    term_SecondArgument(fol_Atom(lit1)),
			    term_FirstArgument(fol_Atom(lit2))))
	      search = FALSE;
	  }
	  if (search) {
	    a++;
	    cont_BackTrack();
	  }
	}
      }
      else
	a++;
    }
    
    if (a>=clause_Length(c2)) {
      cont_BackTrack();
      return FALSE;
    }

    if ((vec_ActMax() - vec) == 1) 
      return TRUE;		
    
    if (subs_InternIdcEqExcept(c1, vec, c2, i2))
      return TRUE;
    else {
      cont_BackTrack();
      a++;			
    }

  } while (a < clause_Length(c2));
  
  return FALSE;
}


static BOOL subs_SubsumptionVecPossibleEqExcept(CLAUSE c1, int vec,
						CLAUSE c2, int i2)
/**********************************************************
  INPUT:   Two clauses c1 and c2 and a vector pointer
           and an accept literal index for c2.
  RETURNS: TRUE if all literals in c1 which indexes stand
           in the vector with bottom pointer vec can 
	   independently be matched to a literal in c2.
  CAUTION: None.
***********************************************************/
{
  int    i,j,n;
  TERM   lit1,lit2;

  n = clause_Length(c2);
  for (i = vec; i < vec_ActMax(); i++) {
    lit1 = clause_GetLiteralTerm(c1, (int) vec_GetNth(i));
    for (j = 0; j < n; j++) {
      if (j != i2) { 
	lit2 = clause_GetLiteralTerm(c2,j);
	cont_StartBinding();
	if (unify_Match(cont_LeftContext(),lit1,lit2))
	  j = n + 1;
	else {
	  if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) &&
	      fol_IsEquality(fol_Atom(lit1)) &&
	      fol_IsEquality(fol_Atom(lit2)) &&
	      (clause_LiteralIsNotOrientedEquality(
                 clause_GetLiteral(c1,(int)vec_GetNth(i))) ||
	       clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) {
	    cont_BackTrackAndStart();
	    if (unify_Match(cont_LeftContext(),
			    term_FirstArgument(fol_Atom(lit1)),
			    term_SecondArgument(fol_Atom(lit2))) &&
		unify_Match(cont_LeftContext(),
			    term_SecondArgument(fol_Atom(lit1)),
			    term_FirstArgument(fol_Atom(lit2))))
	      j = n+1;
	  }
	}
	cont_BackTrack();
      }
    }
    if (j==n)
      return FALSE;
  }
  
  return TRUE;
}


static BOOL subs_IdcVecTestlitsEqExcept(CLAUSE c1, int vec,
					CLAUSE c2, int i2, LITPTR* litptr)
/**********************************************************
  INPUT:   Two clauses c1, c2, a pointer to a literal structure and
           a vector pointer and a literal index i2 in c2
  RETURNS: FALSE if the literals of c1 which are designated by
           the elements of vec do not subsume c2 and TRUE otherwise.
  CAUTION: A structure is build and litptr points to that structure.
  ***********************************************************/
{
  LIST  TermIndexlist,VarSymbList,TermSymbList;
  int   i;
  
  if (subs_SubsumptionVecPossibleEqExcept(c1,vec,c2,i2)) {
    
    TermIndexlist  = list_Nil();
    VarSymbList    = list_Nil();
    TermSymbList   = list_Nil();
    
    for (i = vec; i < vec_ActMax(); i++) {
      VarSymbList =
	subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i)));
   
      if (VarSymbList != list_Nil()){
	TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist);         
	TermSymbList  = list_Cons(VarSymbList,TermSymbList);
      } 
    }
	    
    *litptr = litptr_Create(TermIndexlist,TermSymbList); 

    list_Delete(TermSymbList);
    list_Delete(TermIndexlist);
	
    return TRUE;
  }
  return FALSE;
}


static BOOL subs_InternIdcEqExcept(CLAUSE c1, int vec, CLAUSE c2, int i2)
/**********************************************************
  INPUT:   Two clauses c1, c2, a vector pointer vec and a literal
           i2 in c2 which must not be considered
  RETURNS: FALSE if the literals of c1 which are designed by
           the elements of vec do not subsume c2/i2 and TRUE otherwise.
  CAUTION: 
***********************************************************/
{
  int        locvec;
  LITPTR litptr;
  
  
  if (!subs_IdcVecTestlitsEqExcept(c1,vec,c2,i2,&litptr))
    return FALSE;

  locvec = vec_ActMax();
  
  do {
    subs_CompVec(litptr);	
    if (!vec_IsMax(locvec)) {
      if (!subs_TcVecEqExcept(c1,locvec,c2,i2)) {
	vec_SetMax(locvec);
	litptr_Delete(litptr);
	return FALSE;
      } 
      else
	vec_SetMax(locvec);
    }
  } while (!litptr_AllUsed(litptr));

  litptr_Delete(litptr);
  
  return TRUE;
}


BOOL subs_IdcEqMatchExcept(CLAUSE c1, int i1, CLAUSE c2, int i2,
				  SUBST subst)
/**********************************************************
  INPUT:   Two clauses c1, c2 with the indices of two literals
           which need not to be considered and a matcher
  RETURNS: TRUE if (<c1>/<i1>)<subst> subsumes (<c2>/<i2>)<subst>
  CAUTION: 
***********************************************************/
{
  int  i,vec;
  BOOL Result;

  /*fputs("\n IdcEQExcept on:  \n\t", stdout);
    subst_Print(subst); fputs("\n\t", stdout);
    clause_Print(c1); printf(" \t\t%d \n\t",i1); 
    clause_Print(c2);  printf(" \t\t%d \n\t",i2);*/

  if (clause_Length(c1) == 1)
    Result = TRUE;
  else {
    vec = vec_ActMax();

    for (i = 0; i < clause_Length(c1); i++)
      if (i != i1)
	vec_Push((POINTER) i);

    i = 0;    /* Doesn't matter, there is a general cont_Reset below */
    unify_EstablishMatcher(cont_LeftContext(), subst);

    Result = subs_InternIdcEqExcept(c1,vec,c2,i2);

    /* printf("Result : %d",Result); */

    vec_SetMax(vec);

    cont_Reset();
  }

  return Result;
}