MultiSource/Applications/SPASS/terminator.c - third_party/llvm-test-suite - Git at Google

 /**************************************************************/
 /* ********************************************************** */
 /* *                                                        * */
 /* *                TERMINATOR                              * */
 /* *                                                        * */
 /* *  $Module:   REDRULES                                   * */
 /* *                                                        * */
 /* *  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                                    * */
 /* *                                                        * */
 /* ********************************************************** */
 /**************************************************************/

 /* $RCSfile$ */

 /**************************************************************/
 /* Includes                                                   */
 /**************************************************************/

 #include "terminator.h"
 #include "list.h"


 static LIST red_GetTerminatorPartnerLits(TERM Atom, LITERAL Lit,
 					 BOOL UnitsOnly, LIST IndexList)
 /**************************************************************
   INPUT:   An atom, a literal, a boolean flag and a list of SHARED_INDEXes.
   RETURNS: A list of literals with sign complementary to <Lit>
            that are unifiable with <Atom>. The literals are searched
            in all SHARED_INDEXes from <IndexList>. Additionally,
            if <Unitsonly> is true, only literals from unit clauses
 	   are returned.
   EFFECT:  <Atom> is a copy of <Lit> where some substitution
            was applied and equality literals might have been swapped.
 	   <Lit> is just needed to check whether the unifiable
 	   literals are complementary.
 ***************************************************************/
 {
   LIST    Result, Unifiers, LitScan;
   LITERAL NextLit;

   Result   = list_Nil();
   for ( ; !list_Empty(IndexList); IndexList = list_Cdr(IndexList)) {
     Unifiers = st_GetUnifier(cont_LeftContext(),
 			     sharing_Index(list_Car(IndexList)),
 			     cont_RightContext(), Atom);
     for ( ; !list_Empty(Unifiers); Unifiers = list_Pop(Unifiers)) {
       if (!term_IsVariable(list_Car(Unifiers))) {
 	for (LitScan = sharing_NAtomDataList(list_Car(Unifiers));
 	     !list_Empty(LitScan); LitScan = list_Cdr(LitScan)) {
 	  NextLit = list_Car(LitScan);
 	  if (clause_LiteralsAreComplementary(Lit, NextLit) &&
 	      (!UnitsOnly || clause_Length(clause_LiteralOwningClause(NextLit))==1))
 	    /* The partner literals must have complementary sign and
 	       if <UnitsOnly> == TRUE they must be from unit clauses. */
 	    Result = list_Cons(NextLit, Result);
 	}
       }
     }
   }
   return Result;
 }


 static CLAUSE red_CreateTerminatorEmptyClause(LIST FoundMap, FLAGSTORE Flags,
 					      PRECEDENCE Precedence)
 /**************************************************************
   INPUT:   A list of pairs (l1, l2), where l1 and l2 are unifiable
            literals with complementary sign and a flag store.
 	   More accurately, a substitution s exists,
 	   such that l1 s = l2 s for all pairs (l1,l2) in
 	   <FoundMap>.
 	   For all literals l from the involved clauses
 	   there exists one pair (l1,l2) in <FoundMap>
 	   with l1=l or l2=l.
 	   The flags store and the precedence are needed to create
 	   the new clause.
   RETURNS: A newly created empty clause, where the data
            (parents,...) is set according to <FoundMap>.
 ***************************************************************/
 {
   CLAUSE  Result, PClause;
   LITERAL Lit;
   LIST    Parents;
   NAT     depth;

   Result  = clause_Create(list_Nil(), list_Nil(), list_Nil(), Flags, Precedence);
   Parents = list_Nil();
   depth   = 0;
   for (; !list_Empty(FoundMap); FoundMap = list_Cdr(FoundMap)) {
     Lit     = list_PairSecond(list_Car(FoundMap));
     PClause = clause_LiteralOwningClause(Lit);
     Parents = list_Cons(PClause, Parents);
     depth   = misc_Max(depth, clause_Depth(PClause));
     clause_AddParentClause(Result, clause_Number(PClause));
     clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit));

     Lit     = list_PairFirst(list_Car(FoundMap));
     PClause = clause_LiteralOwningClause(Lit);
     Parents = list_Cons(PClause, Parents);
     depth   = misc_Max(depth, clause_Depth(PClause));
     clause_AddParentClause(Result, clause_Number(PClause));
     clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit));
   }
   clause_SetFromTerminator(Result);
   clause_SetDepth(Result, depth+1);
   clause_SetSplitDataFromList(Result, Parents);
   list_Delete(Parents);
   return Result;
 }


 static BOOL red_TerminatorLitIsBetter(LITERAL L1, NAT S1, LITERAL L2, NAT S2)
 /**************************************************************
   INPUT:   Two literals and its sizes wrt. some substitution.
   RETURNS: TRUE, if <L1> is 'better' than <L2>, FALSE otherwise.
   EFFECT:  1. Positive literals are 'better' than negative literals
            2. If both literals have the same sign, the bigger literal
 	      is better.
 	   This is an heuristic that has shown to be useful in practice.
 	   This function is used as parameter for the function
 	   clause_MoveBestLiteralToFront.
 ***************************************************************/
 {
   if ((clause_LiteralIsNegative(L2) && clause_LiteralIsPositive(L1)) ||
       /* The following conditions do the same as this condition: */
       /* (!clause_LiteralsAreComplementary(L1, L2) && S1 > S2)   */
       (clause_LiteralIsPositive(L1) && S1 > S2) ||
       (clause_LiteralIsNegative(L2) && S1 > S2))
     return TRUE;
   else
     return FALSE;
 }


 static CLAUSE red_SearchTerminator(NAT n, LIST RestLits, LIST FoundMap,
 				   SUBST Subst, SYMBOL GlobalMaxVar,
 				   LIST IndexList, FLAGSTORE Flags,
 				   PRECEDENCE Precedence)
 /**************************************************************
   INPUT:   A natural number, a list of literals, a list of pairs,
            a substitution, the maximum variable occurring in all
 	   involved clauses, a list of SHARED_INDEXes, a flag store
 	   and a precedence.
   RETURNS: An empty clause, if a terminator situation was found,
            NULL otherwise.
   EFFECT:  This recursive function implements the search for
            a terminator situation with at most <n> non-unit clauses.
 	   <RestLits> is the lists of literals actually missing
 	   a complementary partner literal.
 	   <FoundMap> is a list of pairs (l1,l2), where l1 and l2
 	   are complementary, unifiable literals.
 	   <Subst> is the common substitution of all those pairs.
 	   <GlobalMaxVar> is the maximum variable from all
 	   involved clauses.
 	   To enable the search all involved clauses are made
 	   variable-disjoint.
 	   At the moment the function stops, if ANY terminator
 	   situation occurred. This might not be desirable
 	   if splitting is enabled, since there might be other
 	   terminator situations resulting in an empty clause
 	   of lower split level.
 	   The flag store and the precedence are needed to create
 	   the new clause.
 ***************************************************************/
 {
   if (list_Empty(RestLits)) {
     /* We found a terminator situation, so stop the recursion */
     return red_CreateTerminatorEmptyClause(FoundMap, Flags, Precedence);
   } else {
     CLAUSE  Result, PClauseCopy;
     LITERAL Lit, PLit;
     SYMBOL  NewMaxVar;
     SUBST   NewSubst, RightSubst;
     TERM    AtomCopy;
     LIST    ClashList, ToDoList;
     BOOL    Swapped;
     NAT     Limit;
     int     PLitInd;

     Swapped   = FALSE;
     Result    = clause_Null();
     clause_MoveBestLiteralToFront(RestLits, Subst, GlobalMaxVar,
 				  red_TerminatorLitIsBetter);
     Lit       = list_Car(RestLits);
     RestLits  = list_Cdr(RestLits);
     AtomCopy  = subst_Apply(Subst, term_Copy(clause_LiteralAtom(Lit)));

     /* The following 'endless' loop runs twice for equality literals */
     /* and only once for other literals.                             */
     while (TRUE) {
       ClashList = red_GetTerminatorPartnerLits(AtomCopy, Lit, n==0, IndexList);
       for (; !list_Empty(ClashList) && Result==NULL;
 	   ClashList = list_Pop(ClashList)) {
 	PLit        = list_Car(ClashList);
 	PLitInd     = clause_LiteralGetIndex(PLit);
 	PClauseCopy = clause_Copy(clause_LiteralOwningClause(PLit));
 	Limit       = clause_Length(PClauseCopy) == 1 ? n : n-1;

 	clause_RenameVarsBiggerThan(PClauseCopy, GlobalMaxVar);

 	PLit        = clause_GetLiteral(PClauseCopy, PLitInd);
 	FoundMap    = list_Cons(list_PairCreate(Lit, PLit), FoundMap);
 	ToDoList    = clause_GetLiteralListExcept(PClauseCopy, PLitInd);
 	ToDoList    = list_Nconc(ToDoList, list_Copy(RestLits));

 	NewMaxVar   = clause_SearchMaxVar(PClauseCopy);
 	if (symbol_GreaterVariable(GlobalMaxVar, NewMaxVar))
 	  NewMaxVar = GlobalMaxVar;

 	cont_Check();
 	if (!unify_UnifyNoOC(cont_LeftContext(), AtomCopy,
 			     cont_RightContext(), clause_LiteralAtom(PLit))) {
 	  misc_StartErrorReport();
 	  misc_ErrorReport("\n In red_SearchTerminator: Unification failed.");
 	  misc_FinishErrorReport();
 	}
 	subst_ExtractUnifier(cont_LeftContext(), &NewSubst,
 			     cont_RightContext(), &RightSubst);
 	cont_Reset();

 	/* The domains of both substitutions are disjoint */
 	/* so we do just a simple union operation.        */
 	NewSubst = subst_NUnion(NewSubst, RightSubst);
 	RightSubst = NewSubst;
 	NewSubst  = subst_Compose(NewSubst, subst_Copy(Subst));
 	subst_Delete(RightSubst);

 	Result = red_SearchTerminator(Limit, ToDoList, FoundMap, NewSubst,
 				      NewMaxVar, IndexList, Flags, Precedence);

 	clause_Delete(PClauseCopy);
 	subst_Delete(NewSubst);
 	list_Delete(ToDoList);
 	list_PairFree(list_Car(FoundMap));
 	FoundMap = list_Pop(FoundMap);
       }
       /* loop control */
       if (!fol_IsEquality(AtomCopy) || Swapped || Result!=NULL)
 	break;
       else {
 	list_Delete(ClashList);
 	term_EqualitySwap(AtomCopy);
 	Swapped = TRUE;
       }
     }
     /* cleanup */
     term_Delete(AtomCopy);
     /* <ClashList> may be non-empty since the loop stops */
     /* if a terminator was found.                       */
     list_Delete(ClashList);

     return Result;
   }
 }


 CLAUSE red_Terminator(CLAUSE RedClause, NAT n, SHARED_INDEX WoIndex,
 		      SHARED_INDEX UsIndex, FLAGSTORE Flags,
 		      PRECEDENCE Precedence)
 /**************************************************************
   INPUT:   A clause, two shared indexes, a number <n>
            restricting the number of non-unit clauses in
 	   a possible terminator situation, a flag store
 	   and a precedence.
   RETURNS: An empty clause if a terminator with at most <n>
            non-unit clauses is found, NULL otherwise.
   EFFECT:  See also description of red_SearchTerminator.
 ***************************************************************/
 {
   LIST   Rest, IndexList;
   CLAUSE Result;

   if (clause_Length(RedClause) > 1)  /* non-unit clause */
     n--;

   /* Pass the indexes as a list to sub-functions */
   IndexList = list_Cons(WoIndex, list_List(UsIndex));
   Rest      = clause_GetLiteralList(RedClause);
   Result    = red_SearchTerminator(n, Rest, list_Nil(), subst_Nil(),
 				   clause_MaxVar(RedClause), IndexList, Flags,
 				   Precedence);

   /* cleanup */
   list_Delete(IndexList);
   list_Delete(Rest);

   return Result;
 }
	/**************************************************************/
	/* ********************************************************** */
	/* * * */
	/* * TERMINATOR * */
	/* * * */
	/* * $Module: REDRULES * */
	/* * * */
	/* * 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 * */
	/* * * */
	/* ********************************************************** */
	/**************************************************************/

	/* $RCSfile$ */

	/**************************************************************/
	/* Includes */
	/**************************************************************/

	#include "terminator.h"
	#include "list.h"


	static LIST red_GetTerminatorPartnerLits(TERM Atom, LITERAL Lit,
	BOOL UnitsOnly, LIST IndexList)
	/**************************************************************
	INPUT: An atom, a literal, a boolean flag and a list of SHARED_INDEXes.
	RETURNS: A list of literals with sign complementary to <Lit>
	that are unifiable with <Atom>. The literals are searched
	in all SHARED_INDEXes from <IndexList>. Additionally,
	if <Unitsonly> is true, only literals from unit clauses
	are returned.
	EFFECT: <Atom> is a copy of <Lit> where some substitution
	was applied and equality literals might have been swapped.
	<Lit> is just needed to check whether the unifiable
	literals are complementary.
	***************************************************************/
	{
	LIST Result, Unifiers, LitScan;
	LITERAL NextLit;

	Result = list_Nil();
	for ( ; !list_Empty(IndexList); IndexList = list_Cdr(IndexList)) {
	Unifiers = st_GetUnifier(cont_LeftContext(),
	sharing_Index(list_Car(IndexList)),
	cont_RightContext(), Atom);
	for ( ; !list_Empty(Unifiers); Unifiers = list_Pop(Unifiers)) {
	if (!term_IsVariable(list_Car(Unifiers))) {
	for (LitScan = sharing_NAtomDataList(list_Car(Unifiers));
	!list_Empty(LitScan); LitScan = list_Cdr(LitScan)) {
	NextLit = list_Car(LitScan);
	if (clause_LiteralsAreComplementary(Lit, NextLit) &&
	(!UnitsOnly \|\| clause_Length(clause_LiteralOwningClause(NextLit))==1))
	/* The partner literals must have complementary sign and
	if <UnitsOnly> == TRUE they must be from unit clauses. */
	Result = list_Cons(NextLit, Result);
	}
	}
	}
	}
	return Result;
	}


	static CLAUSE red_CreateTerminatorEmptyClause(LIST FoundMap, FLAGSTORE Flags,
	PRECEDENCE Precedence)
	/**************************************************************
	INPUT: A list of pairs (l1, l2), where l1 and l2 are unifiable
	literals with complementary sign and a flag store.
	More accurately, a substitution s exists,
	such that l1 s = l2 s for all pairs (l1,l2) in
	<FoundMap>.
	For all literals l from the involved clauses
	there exists one pair (l1,l2) in <FoundMap>
	with l1=l or l2=l.
	The flags store and the precedence are needed to create
	the new clause.
	RETURNS: A newly created empty clause, where the data
	(parents,...) is set according to <FoundMap>.
	***************************************************************/
	{
	CLAUSE Result, PClause;
	LITERAL Lit;
	LIST Parents;
	NAT depth;

	Result = clause_Create(list_Nil(), list_Nil(), list_Nil(), Flags, Precedence);
	Parents = list_Nil();
	depth = 0;
	for (; !list_Empty(FoundMap); FoundMap = list_Cdr(FoundMap)) {
	Lit = list_PairSecond(list_Car(FoundMap));
	PClause = clause_LiteralOwningClause(Lit);
	Parents = list_Cons(PClause, Parents);
	depth = misc_Max(depth, clause_Depth(PClause));
	clause_AddParentClause(Result, clause_Number(PClause));
	clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit));

	Lit = list_PairFirst(list_Car(FoundMap));
	PClause = clause_LiteralOwningClause(Lit);
	Parents = list_Cons(PClause, Parents);
	depth = misc_Max(depth, clause_Depth(PClause));
	clause_AddParentClause(Result, clause_Number(PClause));
	clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit));
	}
	clause_SetFromTerminator(Result);
	clause_SetDepth(Result, depth+1);
	clause_SetSplitDataFromList(Result, Parents);
	list_Delete(Parents);
	return Result;
	}


	static BOOL red_TerminatorLitIsBetter(LITERAL L1, NAT S1, LITERAL L2, NAT S2)
	/**************************************************************
	INPUT: Two literals and its sizes wrt. some substitution.
	RETURNS: TRUE, if <L1> is 'better' than <L2>, FALSE otherwise.
	EFFECT: 1. Positive literals are 'better' than negative literals
	2. If both literals have the same sign, the bigger literal
	is better.
	This is an heuristic that has shown to be useful in practice.
	This function is used as parameter for the function
	clause_MoveBestLiteralToFront.
	***************************************************************/
	{
	if ((clause_LiteralIsNegative(L2) && clause_LiteralIsPositive(L1)) \|\|
	/* The following conditions do the same as this condition: */
	/* (!clause_LiteralsAreComplementary(L1, L2) && S1 > S2) */
	(clause_LiteralIsPositive(L1) && S1 > S2) \|\|
	(clause_LiteralIsNegative(L2) && S1 > S2))
	return TRUE;
	else
	return FALSE;
	}


	static CLAUSE red_SearchTerminator(NAT n, LIST RestLits, LIST FoundMap,
	SUBST Subst, SYMBOL GlobalMaxVar,
	LIST IndexList, FLAGSTORE Flags,
	PRECEDENCE Precedence)
	/**************************************************************
	INPUT: A natural number, a list of literals, a list of pairs,
	a substitution, the maximum variable occurring in all
	involved clauses, a list of SHARED_INDEXes, a flag store
	and a precedence.
	RETURNS: An empty clause, if a terminator situation was found,
	NULL otherwise.
	EFFECT: This recursive function implements the search for
	a terminator situation with at most <n> non-unit clauses.
	<RestLits> is the lists of literals actually missing
	a complementary partner literal.
	<FoundMap> is a list of pairs (l1,l2), where l1 and l2
	are complementary, unifiable literals.
	<Subst> is the common substitution of all those pairs.
	<GlobalMaxVar> is the maximum variable from all
	involved clauses.
	To enable the search all involved clauses are made
	variable-disjoint.
	At the moment the function stops, if ANY terminator
	situation occurred. This might not be desirable
	if splitting is enabled, since there might be other
	terminator situations resulting in an empty clause
	of lower split level.
	The flag store and the precedence are needed to create
	the new clause.
	***************************************************************/
	{
	if (list_Empty(RestLits)) {
	/* We found a terminator situation, so stop the recursion */
	return red_CreateTerminatorEmptyClause(FoundMap, Flags, Precedence);
	} else {
	CLAUSE Result, PClauseCopy;
	LITERAL Lit, PLit;
	SYMBOL NewMaxVar;
	SUBST NewSubst, RightSubst;
	TERM AtomCopy;
	LIST ClashList, ToDoList;
	BOOL Swapped;
	NAT Limit;
	int PLitInd;

	Swapped = FALSE;
	Result = clause_Null();
	clause_MoveBestLiteralToFront(RestLits, Subst, GlobalMaxVar,
	red_TerminatorLitIsBetter);
	Lit = list_Car(RestLits);
	RestLits = list_Cdr(RestLits);
	AtomCopy = subst_Apply(Subst, term_Copy(clause_LiteralAtom(Lit)));

	/* The following 'endless' loop runs twice for equality literals */
	/* and only once for other literals. */
	while (TRUE) {
	ClashList = red_GetTerminatorPartnerLits(AtomCopy, Lit, n==0, IndexList);
	for (; !list_Empty(ClashList) && Result==NULL;
	ClashList = list_Pop(ClashList)) {
	PLit = list_Car(ClashList);
	PLitInd = clause_LiteralGetIndex(PLit);
	PClauseCopy = clause_Copy(clause_LiteralOwningClause(PLit));
	Limit = clause_Length(PClauseCopy) == 1 ? n : n-1;

	clause_RenameVarsBiggerThan(PClauseCopy, GlobalMaxVar);

	PLit = clause_GetLiteral(PClauseCopy, PLitInd);
	FoundMap = list_Cons(list_PairCreate(Lit, PLit), FoundMap);
	ToDoList = clause_GetLiteralListExcept(PClauseCopy, PLitInd);
	ToDoList = list_Nconc(ToDoList, list_Copy(RestLits));

	NewMaxVar = clause_SearchMaxVar(PClauseCopy);
	if (symbol_GreaterVariable(GlobalMaxVar, NewMaxVar))
	NewMaxVar = GlobalMaxVar;

	cont_Check();
	if (!unify_UnifyNoOC(cont_LeftContext(), AtomCopy,
	cont_RightContext(), clause_LiteralAtom(PLit))) {
	misc_StartErrorReport();
	misc_ErrorReport("\n In red_SearchTerminator: Unification failed.");
	misc_FinishErrorReport();
	}
	subst_ExtractUnifier(cont_LeftContext(), &NewSubst,
	cont_RightContext(), &RightSubst);
	cont_Reset();

	/* The domains of both substitutions are disjoint */
	/* so we do just a simple union operation. */
	NewSubst = subst_NUnion(NewSubst, RightSubst);
	RightSubst = NewSubst;
	NewSubst = subst_Compose(NewSubst, subst_Copy(Subst));
	subst_Delete(RightSubst);

	Result = red_SearchTerminator(Limit, ToDoList, FoundMap, NewSubst,
	NewMaxVar, IndexList, Flags, Precedence);

	clause_Delete(PClauseCopy);
	subst_Delete(NewSubst);
	list_Delete(ToDoList);
	list_PairFree(list_Car(FoundMap));
	FoundMap = list_Pop(FoundMap);
	}
	/* loop control */
	if (!fol_IsEquality(AtomCopy) \|\| Swapped \|\| Result!=NULL)
	break;
	else {
	list_Delete(ClashList);
	term_EqualitySwap(AtomCopy);
	Swapped = TRUE;
	}
	}
	/* cleanup */
	term_Delete(AtomCopy);
	/* <ClashList> may be non-empty since the loop stops */
	/* if a terminator was found. */
	list_Delete(ClashList);

	return Result;
	}
	}


	CLAUSE red_Terminator(CLAUSE RedClause, NAT n, SHARED_INDEX WoIndex,
	SHARED_INDEX UsIndex, FLAGSTORE Flags,
	PRECEDENCE Precedence)
	/**************************************************************
	INPUT: A clause, two shared indexes, a number <n>
	restricting the number of non-unit clauses in
	a possible terminator situation, a flag store
	and a precedence.
	RETURNS: An empty clause if a terminator with at most <n>
	non-unit clauses is found, NULL otherwise.
	EFFECT: See also description of red_SearchTerminator.
	***************************************************************/
	{
	LIST Rest, IndexList;
	CLAUSE Result;

	if (clause_Length(RedClause) > 1) /* non-unit clause */
	n--;

	/* Pass the indexes as a list to sub-functions */
	IndexList = list_Cons(WoIndex, list_List(UsIndex));
	Rest = clause_GetLiteralList(RedClause);
	Result = red_SearchTerminator(n, Rest, list_Nil(), subst_Nil(),
	clause_MaxVar(RedClause), IndexList, Flags,
	Precedence);

	/* cleanup */
	list_Delete(IndexList);
	list_Delete(Rest);

	return Result;
	}