MultiSource/Applications/SPASS/rules-ur.c - llvm-test-suite - Git at Google

 /**************************************************************/
 /* ********************************************************** */
 /* *                                                        * */
 /* *                UR-RESOLUTION                           * */
 /* *                                                        * */
 /* *  $Module:   INFERENCE RULES                            * */
 /* *                                                        * */
 /* *  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 "rules-ur.h"
 #include "list.h"


 static LIST inf_GetURPartnerLits(TERM Atom, LITERAL Lit,
 				 BOOL Unit, SHARED_INDEX Index)
 /**************************************************************
   INPUT:   An atom, a literal, a boolean flag and a SHARED_INDEX.
   RETURNS: A list of literals with sign complementary to <Lit>
            that are unifiable with <Atom>. If <Unit> is true,
 	   only literals from unit clauses are returned, if <Unit>
 	   is false, only literals from non-unit clauses are
 	   returned.
   EFFECT:  <Atom> is a copy of <Lit>'s atom 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 PLit;
   int     length;

   Result   = list_Nil();
   Unifiers = st_GetUnifier(cont_LeftContext(), sharing_Index(Index),
 			   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)) {
 	PLit   = list_Car(LitScan);
 	length = clause_Length(clause_LiteralOwningClause(PLit));
 	if (clause_LiteralsAreComplementary(Lit, PLit) &&
 	    ((Unit && length==1) || (!Unit && length!=1)))
 	  /* The partner literals must have complementary sign and
 	     if <Unit> == TRUE they must be from unit clauses,
 	     if <Unit> == FALSE they must be from non-unit clauses. */
 	  Result = list_Cons(PLit, Result);
       }
     }
   }
   return Result;
 }


 static CLAUSE inf_CreateURUnitResolvent(CLAUSE Clause, int i, SUBST Subst,
 					LIST FoundMap, FLAGSTORE Flags,
 					PRECEDENCE Precedence)
 /**************************************************************
   INPUT:   A non-unit clause, a literal index from the clause,
            a substitution, a list of pairs (l1, l2) of literals,
 	   where l1 is from the non-unit clause and l2 is from a
 	   unit clause, a flag store and a precedence.
   RETURNS: The resolvent of this UR resolution inference. The
            clause consists of the literal at index <i> in <Clause>
 	   after application of <Subst>.
   EFFECT:  The flag store and the precedence are needed to create
            the new clause.
 ***************************************************************/
 {
   CLAUSE  Result, PClause;
   LITERAL Lit;
   TERM    Atom;
   LIST    Parents;
   NAT     depth;

   /* Create atom for resolvent */
   Atom = subst_Apply(Subst, term_Copy(clause_GetLiteralAtom(Clause, i)));
   /* Create clause */
   Parents = list_List(Atom);
   if (i <= clause_LastConstraintLitIndex(Clause))
     Result = clause_Create(Parents, list_Nil(), list_Nil(), Flags, Precedence);
   else if (i <= clause_LastAntecedentLitIndex(Clause))
     Result = clause_Create(list_Nil(), Parents, list_Nil(), Flags, Precedence);
   else
     Result = clause_Create(list_Nil(), list_Nil(), Parents, Flags, Precedence);
   list_Delete(Parents);

   /* Get parent clauses and literals, calculate depth of resolvent */
   Parents = list_List(Clause);
   depth   = clause_Depth(Clause);
   for ( ; !list_Empty(FoundMap); FoundMap = list_Cdr(FoundMap)) {
     Lit     = list_PairSecond(list_Car(FoundMap)); /* Literal from unit */
     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)); /* Is from <Clause> */
     clause_AddParentClause(Result, clause_Number(Clause));
     clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit));
   }
   clause_SetFromURResolution(Result);
   clause_SetDepth(Result, depth+1);
   clause_SetSplitDataFromList(Result, Parents);
   list_Delete(Parents);

   return Result;
 }


 static LIST inf_SearchURResolvents(CLAUSE Clause, int i, LIST FoundMap,
 				   LIST RestLits, SUBST Subst,
 				   SYMBOL GlobalMaxVar, SHARED_INDEX Index,
 				   FLAGSTORE Flags, PRECEDENCE Precedence)
 /**************************************************************
   INPUT:   A non-unit clause, a literal index from <Clause>.
            <FoundMap> is a list of pairs (l1,l2) of unifiable literals,
 	   where l1 is from <Clause> and l2 is from a unit clause.
 	   <RestLits> is a list of literals from <Clause> where
 	   we haven't found unifiable literals from unit clauses
 	   so far.
 	   <Subst> is the overall substitution for <Clause>
 	   (not for the unit-clauses!).
 	   <GlobalMaxVar> is the maximal variable encountered so far.
 	   <Index> is used to search unifiable literals.
 	   The flag store and the precedence are needed to create
 	   the new clauses.
   RETURNS: A list of UR resolution resolvents.
 ***************************************************************/
 {
   if (list_Empty(RestLits)) {
     /* Stop the recursion */
     return list_List(inf_CreateURUnitResolvent(Clause, i, Subst, FoundMap,
 					       Flags, Precedence));
   } else {
     LITERAL Lit, PLit;
     SYMBOL  NewMaxVar;
     SUBST   NewSubst, RightSubst;
     TERM    AtomCopy, PAtom;
     LIST    Result, Partners;
     BOOL    Swapped;

     Result   = list_Nil();
     Swapped  = FALSE;
     /* Choose the unmatched literal with the most symbols */
     RestLits = clause_MoveBestLiteralToFront(list_Copy(RestLits), Subst,
 					     GlobalMaxVar,
 					     clause_HyperLiteralIsBetter);
     Lit      = list_Car(RestLits);
     RestLits = list_Pop(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) {
       Partners = inf_GetURPartnerLits(AtomCopy, Lit, TRUE, Index);
       for ( ; !list_Empty(Partners); Partners = list_Pop(Partners)) {
 	PLit    = list_Car(Partners);

 	/* Rename the atom */
 	PAtom   = term_Copy(clause_LiteralAtom(PLit));
 	term_StartMaxRenaming(GlobalMaxVar);
 	term_Rename(PAtom);
 	/* Get the new global maximal variable */
 	NewMaxVar = term_MaxVar(PAtom);
 	if (symbol_GreaterVariable(GlobalMaxVar, NewMaxVar))
 	  NewMaxVar = GlobalMaxVar;

 	/* Get the substitution */
 	cont_Check();
 	if (!unify_UnifyNoOC(cont_LeftContext(), AtomCopy,
 			     cont_RightContext(), PAtom)) {
 	  misc_StartErrorReport();
 	  misc_ErrorReport("\n In inf_SearchURResolvents: Unification failed.");
 	  misc_FinishErrorReport();
 	}
 	subst_ExtractUnifier(cont_LeftContext(), &NewSubst,
 			     cont_RightContext(), &RightSubst);
 	cont_Reset();
 	subst_Delete(RightSubst);  /* Forget substitution for unit clause */
 	term_Delete(PAtom);  /* Was just needed to get the substitution */

 	/* Build the composition of the substitutions */
 	RightSubst = NewSubst;
 	NewSubst = subst_Compose(NewSubst, subst_Copy(Subst));
 	subst_Delete(RightSubst);

 	FoundMap    = list_Cons(list_PairCreate(Lit, PLit), FoundMap);

 	Result = list_Nconc(inf_SearchURResolvents(Clause,i,FoundMap,RestLits,
 						   NewSubst,NewMaxVar,Index,
 						   Flags, Precedence),
 			    Result);

 	list_PairFree(list_Car(FoundMap));
 	FoundMap = list_Pop(FoundMap);
 	subst_Delete(NewSubst);
       }
       /* loop control */
       if (!fol_IsEquality(AtomCopy) || Swapped)
 	break;
       else {
 	term_EqualitySwap(AtomCopy);
 	Swapped = TRUE;
       }
     }
     /* cleanup */
     term_Delete(AtomCopy);
     list_Delete(RestLits);

     return Result;
   }
 }


 static LIST inf_NonUnitURResolution(CLAUSE Clause, int SpecialLitIndex,
 				    LIST FoundMap, SUBST Subst,
 				    SYMBOL GlobalMaxVar, SHARED_INDEX Index,
 				    FLAGSTORE Flags, PRECEDENCE Precedence)
 /**************************************************************
   INPUT:   A non-unit clause, a literal index from <Clause>.
            <FoundMap> is a list of pairs (l1,l2) of unifiable literals,
 	   where l1 is from <Clause> and l2 is from a unit clause.
 	   At this point the list has at most one element.
 	   <Subst> is the substitution for <Clause>.
 	   <GlobalMaxVar> is the maximal variable encountered so far.
 	   <Index> is used to search unifiable literals.
 	   The flag store and the precedence are needed to create
 	   the new clauses.
   RETURNS: The list of UR resolution resolvents.
   EFFECT:  If inf_URResolution was called with a unit clause,
            <SpecialLitIndex> is the index of a literal from a non-unit
 	   clause, that is unifiable with the unit clause's literal,
 	   otherwise it is set to -1.
 ***************************************************************/
 {
   LIST Result, RestLits;
   int  i, last;

   Result = list_Nil();
   RestLits = clause_GetLiteralListExcept(Clause, SpecialLitIndex);
   last = clause_LastLitIndex(Clause);
   for (i = clause_FirstLitIndex(); i <= last; i++) {
     /* <i> is the index of the literal that remains in the resolvent */
     if (i != SpecialLitIndex) {
       RestLits = list_PointerDeleteOneElement(RestLits,
 					      clause_GetLiteral(Clause,i));

       Result = list_Nconc(inf_SearchURResolvents(Clause, i, FoundMap, RestLits,
 						 Subst, GlobalMaxVar, Index,
 						 Flags, Precedence),
 			  Result);

       RestLits = list_Cons(clause_GetLiteral(Clause, i), RestLits);
     }
   }
   list_Delete(RestLits);
   return Result;
 }


 LIST inf_URResolution(CLAUSE Clause, SHARED_INDEX Index, FLAGSTORE Flags,
 		      PRECEDENCE Precedence)
 /**************************************************************
   INPUT:   A clause, a shared index, a flag store and a precedence.
   RETURNS: The list of UR resolution resolvents.
   EFFECT:  The flag store and the precedence are needed to create
            the resolvents.
 ***************************************************************/
 {
   LIST Result;

   if (clause_Length(Clause) != 1) {
     /* Clause isn't unit clause */
     Result = inf_NonUnitURResolution(Clause, -1, list_Nil(), subst_Nil(),
 				     clause_MaxVar(Clause), Index, Flags,
 				     Precedence);
   }
   else {
     /* Clause is unit clause, so search partner literals in non-unit clauses */
     LITERAL Lit, PLit;
     TERM    Atom;
     LIST    Partners, FoundMap;
     SYMBOL  MaxVar, PMaxVar;
     SUBST   LeftSubst, RightSubst;
     CLAUSE  PClause;
     int     PLitInd;
     BOOL    Swapped;

     Result   = list_Nil();
     Lit      = clause_GetLiteral(Clause, clause_FirstLitIndex());
     Atom     = term_Copy(clause_LiteralAtom(Lit));
     Swapped  = FALSE;

     /* The following 'endless' loop runs twice for equality literals */
     /* and only once for other literals.                             */
     while (TRUE) {
       /* Get complementary literals from non-unit clauses */
       Partners = inf_GetURPartnerLits(Atom, Lit, FALSE, Index);

       for ( ; !list_Empty(Partners); Partners = list_Pop(Partners)) {
 	PLit     = list_Car(Partners);
 	PLitInd  = clause_LiteralGetIndex(PLit);
 	PClause  = clause_LiteralOwningClause(PLit); /* non-unit clause */

 	PMaxVar   = clause_MaxVar(PClause);
 	term_StartMaxRenaming(PMaxVar);
 	term_Rename(Atom);              /* Rename atom from unit clause */
 	MaxVar = term_MaxVar(Atom);
 	if (symbol_GreaterVariable(PMaxVar, MaxVar))
 	  MaxVar = PMaxVar;

 	/* Get the substitution */
 	cont_Check();
 	unify_UnifyNoOC(cont_LeftContext(), clause_LiteralAtom(PLit),
 			cont_RightContext(), Atom);
 	subst_ExtractUnifier(cont_LeftContext(), &LeftSubst,
 			     cont_RightContext(), &RightSubst);
 	cont_Reset();
 	/* We don't need the substitution for the unit clause */
 	subst_Delete(RightSubst);

 	FoundMap = list_List(list_PairCreate(PLit, Lit));

 	Result = list_Nconc(inf_NonUnitURResolution(PClause, PLitInd, FoundMap,
 						    LeftSubst, MaxVar, Index,
 						    Flags, Precedence),
 			    Result);

 	list_DeletePairList(FoundMap);
 	subst_Delete(LeftSubst);
       }
       /* loop control */
       if (!fol_IsEquality(Atom) || Swapped)
 	break;
       else {
 	term_EqualitySwap(Atom);
 	Swapped = TRUE;
       }
     }  /* end of endless loop */
     term_Delete(Atom);
   }
   return Result;
 }
	/**************************************************************/
	/* ********************************************************** */
	/* * * */
	/* * UR-RESOLUTION * */
	/* * * */
	/* * $Module: INFERENCE RULES * */
	/* * * */
	/* * 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 "rules-ur.h"
	#include "list.h"


	static LIST inf_GetURPartnerLits(TERM Atom, LITERAL Lit,
	BOOL Unit, SHARED_INDEX Index)
	/**************************************************************
	INPUT: An atom, a literal, a boolean flag and a SHARED_INDEX.
	RETURNS: A list of literals with sign complementary to <Lit>
	that are unifiable with <Atom>. If <Unit> is true,
	only literals from unit clauses are returned, if <Unit>
	is false, only literals from non-unit clauses are
	returned.
	EFFECT: <Atom> is a copy of <Lit>'s atom 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 PLit;
	int length;

	Result = list_Nil();
	Unifiers = st_GetUnifier(cont_LeftContext(), sharing_Index(Index),
	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)) {
	PLit = list_Car(LitScan);
	length = clause_Length(clause_LiteralOwningClause(PLit));
	if (clause_LiteralsAreComplementary(Lit, PLit) &&
	((Unit && length==1) \|\| (!Unit && length!=1)))
	/* The partner literals must have complementary sign and
	if <Unit> == TRUE they must be from unit clauses,
	if <Unit> == FALSE they must be from non-unit clauses. */
	Result = list_Cons(PLit, Result);
	}
	}
	}
	return Result;
	}


	static CLAUSE inf_CreateURUnitResolvent(CLAUSE Clause, int i, SUBST Subst,
	LIST FoundMap, FLAGSTORE Flags,
	PRECEDENCE Precedence)
	/**************************************************************
	INPUT: A non-unit clause, a literal index from the clause,
	a substitution, a list of pairs (l1, l2) of literals,
	where l1 is from the non-unit clause and l2 is from a
	unit clause, a flag store and a precedence.
	RETURNS: The resolvent of this UR resolution inference. The
	clause consists of the literal at index <i> in <Clause>
	after application of <Subst>.
	EFFECT: The flag store and the precedence are needed to create
	the new clause.
	***************************************************************/
	{
	CLAUSE Result, PClause;
	LITERAL Lit;
	TERM Atom;
	LIST Parents;
	NAT depth;

	/* Create atom for resolvent */
	Atom = subst_Apply(Subst, term_Copy(clause_GetLiteralAtom(Clause, i)));
	/* Create clause */
	Parents = list_List(Atom);
	if (i <= clause_LastConstraintLitIndex(Clause))
	Result = clause_Create(Parents, list_Nil(), list_Nil(), Flags, Precedence);
	else if (i <= clause_LastAntecedentLitIndex(Clause))
	Result = clause_Create(list_Nil(), Parents, list_Nil(), Flags, Precedence);
	else
	Result = clause_Create(list_Nil(), list_Nil(), Parents, Flags, Precedence);
	list_Delete(Parents);

	/* Get parent clauses and literals, calculate depth of resolvent */
	Parents = list_List(Clause);
	depth = clause_Depth(Clause);
	for ( ; !list_Empty(FoundMap); FoundMap = list_Cdr(FoundMap)) {
	Lit = list_PairSecond(list_Car(FoundMap)); /* Literal from unit */
	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)); /* Is from <Clause> */
	clause_AddParentClause(Result, clause_Number(Clause));
	clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit));
	}
	clause_SetFromURResolution(Result);
	clause_SetDepth(Result, depth+1);
	clause_SetSplitDataFromList(Result, Parents);
	list_Delete(Parents);

	return Result;
	}


	static LIST inf_SearchURResolvents(CLAUSE Clause, int i, LIST FoundMap,
	LIST RestLits, SUBST Subst,
	SYMBOL GlobalMaxVar, SHARED_INDEX Index,
	FLAGSTORE Flags, PRECEDENCE Precedence)
	/**************************************************************
	INPUT: A non-unit clause, a literal index from <Clause>.
	<FoundMap> is a list of pairs (l1,l2) of unifiable literals,
	where l1 is from <Clause> and l2 is from a unit clause.
	<RestLits> is a list of literals from <Clause> where
	we haven't found unifiable literals from unit clauses
	so far.
	<Subst> is the overall substitution for <Clause>
	(not for the unit-clauses!).
	<GlobalMaxVar> is the maximal variable encountered so far.
	<Index> is used to search unifiable literals.
	The flag store and the precedence are needed to create
	the new clauses.
	RETURNS: A list of UR resolution resolvents.
	***************************************************************/
	{
	if (list_Empty(RestLits)) {
	/* Stop the recursion */
	return list_List(inf_CreateURUnitResolvent(Clause, i, Subst, FoundMap,
	Flags, Precedence));
	} else {
	LITERAL Lit, PLit;
	SYMBOL NewMaxVar;
	SUBST NewSubst, RightSubst;
	TERM AtomCopy, PAtom;
	LIST Result, Partners;
	BOOL Swapped;

	Result = list_Nil();
	Swapped = FALSE;
	/* Choose the unmatched literal with the most symbols */
	RestLits = clause_MoveBestLiteralToFront(list_Copy(RestLits), Subst,
	GlobalMaxVar,
	clause_HyperLiteralIsBetter);
	Lit = list_Car(RestLits);
	RestLits = list_Pop(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) {
	Partners = inf_GetURPartnerLits(AtomCopy, Lit, TRUE, Index);
	for ( ; !list_Empty(Partners); Partners = list_Pop(Partners)) {
	PLit = list_Car(Partners);

	/* Rename the atom */
	PAtom = term_Copy(clause_LiteralAtom(PLit));
	term_StartMaxRenaming(GlobalMaxVar);
	term_Rename(PAtom);
	/* Get the new global maximal variable */
	NewMaxVar = term_MaxVar(PAtom);
	if (symbol_GreaterVariable(GlobalMaxVar, NewMaxVar))
	NewMaxVar = GlobalMaxVar;

	/* Get the substitution */
	cont_Check();
	if (!unify_UnifyNoOC(cont_LeftContext(), AtomCopy,
	cont_RightContext(), PAtom)) {
	misc_StartErrorReport();
	misc_ErrorReport("\n In inf_SearchURResolvents: Unification failed.");
	misc_FinishErrorReport();
	}
	subst_ExtractUnifier(cont_LeftContext(), &NewSubst,
	cont_RightContext(), &RightSubst);
	cont_Reset();
	subst_Delete(RightSubst); /* Forget substitution for unit clause */
	term_Delete(PAtom); /* Was just needed to get the substitution */

	/* Build the composition of the substitutions */
	RightSubst = NewSubst;
	NewSubst = subst_Compose(NewSubst, subst_Copy(Subst));
	subst_Delete(RightSubst);

	FoundMap = list_Cons(list_PairCreate(Lit, PLit), FoundMap);

	Result = list_Nconc(inf_SearchURResolvents(Clause,i,FoundMap,RestLits,
	NewSubst,NewMaxVar,Index,
	Flags, Precedence),
	Result);

	list_PairFree(list_Car(FoundMap));
	FoundMap = list_Pop(FoundMap);
	subst_Delete(NewSubst);
	}
	/* loop control */
	if (!fol_IsEquality(AtomCopy) \|\| Swapped)
	break;
	else {
	term_EqualitySwap(AtomCopy);
	Swapped = TRUE;
	}
	}
	/* cleanup */
	term_Delete(AtomCopy);
	list_Delete(RestLits);

	return Result;
	}
	}


	static LIST inf_NonUnitURResolution(CLAUSE Clause, int SpecialLitIndex,
	LIST FoundMap, SUBST Subst,
	SYMBOL GlobalMaxVar, SHARED_INDEX Index,
	FLAGSTORE Flags, PRECEDENCE Precedence)
	/**************************************************************
	INPUT: A non-unit clause, a literal index from <Clause>.
	<FoundMap> is a list of pairs (l1,l2) of unifiable literals,
	where l1 is from <Clause> and l2 is from a unit clause.
	At this point the list has at most one element.
	<Subst> is the substitution for <Clause>.
	<GlobalMaxVar> is the maximal variable encountered so far.
	<Index> is used to search unifiable literals.
	The flag store and the precedence are needed to create
	the new clauses.
	RETURNS: The list of UR resolution resolvents.
	EFFECT: If inf_URResolution was called with a unit clause,
	<SpecialLitIndex> is the index of a literal from a non-unit
	clause, that is unifiable with the unit clause's literal,
	otherwise it is set to -1.
	***************************************************************/
	{
	LIST Result, RestLits;
	int i, last;

	Result = list_Nil();
	RestLits = clause_GetLiteralListExcept(Clause, SpecialLitIndex);
	last = clause_LastLitIndex(Clause);
	for (i = clause_FirstLitIndex(); i <= last; i++) {
	/* <i> is the index of the literal that remains in the resolvent */
	if (i != SpecialLitIndex) {
	RestLits = list_PointerDeleteOneElement(RestLits,
	clause_GetLiteral(Clause,i));

	Result = list_Nconc(inf_SearchURResolvents(Clause, i, FoundMap, RestLits,
	Subst, GlobalMaxVar, Index,
	Flags, Precedence),
	Result);

	RestLits = list_Cons(clause_GetLiteral(Clause, i), RestLits);
	}
	}
	list_Delete(RestLits);
	return Result;
	}


	LIST inf_URResolution(CLAUSE Clause, SHARED_INDEX Index, FLAGSTORE Flags,
	PRECEDENCE Precedence)
	/**************************************************************
	INPUT: A clause, a shared index, a flag store and a precedence.
	RETURNS: The list of UR resolution resolvents.
	EFFECT: The flag store and the precedence are needed to create
	the resolvents.
	***************************************************************/
	{
	LIST Result;

	if (clause_Length(Clause) != 1) {
	/* Clause isn't unit clause */
	Result = inf_NonUnitURResolution(Clause, -1, list_Nil(), subst_Nil(),
	clause_MaxVar(Clause), Index, Flags,
	Precedence);
	}
	else {
	/* Clause is unit clause, so search partner literals in non-unit clauses */
	LITERAL Lit, PLit;
	TERM Atom;
	LIST Partners, FoundMap;
	SYMBOL MaxVar, PMaxVar;
	SUBST LeftSubst, RightSubst;
	CLAUSE PClause;
	int PLitInd;
	BOOL Swapped;

	Result = list_Nil();
	Lit = clause_GetLiteral(Clause, clause_FirstLitIndex());
	Atom = term_Copy(clause_LiteralAtom(Lit));
	Swapped = FALSE;

	/* The following 'endless' loop runs twice for equality literals */
	/* and only once for other literals. */
	while (TRUE) {
	/* Get complementary literals from non-unit clauses */
	Partners = inf_GetURPartnerLits(Atom, Lit, FALSE, Index);

	for ( ; !list_Empty(Partners); Partners = list_Pop(Partners)) {
	PLit = list_Car(Partners);
	PLitInd = clause_LiteralGetIndex(PLit);
	PClause = clause_LiteralOwningClause(PLit); /* non-unit clause */

	PMaxVar = clause_MaxVar(PClause);
	term_StartMaxRenaming(PMaxVar);
	term_Rename(Atom); /* Rename atom from unit clause */
	MaxVar = term_MaxVar(Atom);
	if (symbol_GreaterVariable(PMaxVar, MaxVar))
	MaxVar = PMaxVar;

	/* Get the substitution */
	cont_Check();
	unify_UnifyNoOC(cont_LeftContext(), clause_LiteralAtom(PLit),
	cont_RightContext(), Atom);
	subst_ExtractUnifier(cont_LeftContext(), &LeftSubst,
	cont_RightContext(), &RightSubst);
	cont_Reset();
	/* We don't need the substitution for the unit clause */
	subst_Delete(RightSubst);

	FoundMap = list_List(list_PairCreate(PLit, Lit));

	Result = list_Nconc(inf_NonUnitURResolution(PClause, PLitInd, FoundMap,
	LeftSubst, MaxVar, Index,
	Flags, Precedence),
	Result);

	list_DeletePairList(FoundMap);
	subst_Delete(LeftSubst);
	}
	/* loop control */
	if (!fol_IsEquality(Atom) \|\| Swapped)
	break;
	else {
	term_EqualitySwap(Atom);
	Swapped = TRUE;
	}
	} /* end of endless loop */
	term_Delete(Atom);
	}
	return Result;
	}