clause.h

/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                   CLAUSES                              * */
/* *                                                        * */
/* *  $Module:   CLAUSE                                     * */
/* *                                                        * */
/* *  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: 21527 $                                       * */
/* $State$                                            * */
/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $                             * */
/* $Author: duraid $                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile$ */

#ifndef _CLAUSE_
#define _CLAUSE_

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

#include "sharing.h"
#include "foldfg.h"
#include "order.h"
#include "subst.h"
#include "flags.h"
#include "symbol.h"

/**************************************************************/
/* Data Structures and Constants                              */
/**************************************************************/

/* Means weight of literal or clause is undefined */
extern const NAT clause_WEIGHTUNDEFINED;

extern int clause_CLAUSECOUNTER;

typedef enum {MAXIMAL=1, STRICTMAXIMAL=2, LITSELECT=4} MAXFLAG;

typedef enum {CLAUSE_DELETION, EMPTY_SORT, SORT_RESOLUTION,
	      EQUALITY_RESOLUTION, EQUALITY_FACTORING, MERGING_PARAMODULATION,
	      PARAMODULATION, ORDERED_PARAMODULATION,
	      SUPERPOSITION_RIGHT,  SUPERPOSITION_LEFT,
	      SIMPLE_HYPER, ORDERED_HYPER, UR_RESOLUTION,
	      GENERAL_RESOLUTION, GENERAL_FACTORING, SPLITTING, INPUT,
	      CONDENSING, ASSIGNMENT_EQUATION_DELETION, OBVIOUS_REDUCTIONS,
	      SORT_SIMPLIFICATION, REWRITING, CONTEXTUAL_REWRITING,
	      MATCHING_REPLACEMENT_RESOLUTION, UNIT_CONFLICT, DEFAPPLICATION,
	      TERMINATOR, TEMPORARY
} RULE;

typedef unsigned long SPLITFIELDENTRY;
typedef SPLITFIELDENTRY* SPLITFIELD;

typedef enum  {WORKEDOFF=1,CLAUSESELECT=2,DOCCLAUSE=4,CONCLAUSE=8,BLOCKED=16,
	       NOPARAINTO=32, MARKED=64, HIDDEN=128} CLAUSE_FLAGS;


/* As there are a lot of implications a clauses properties may have */
/* for the prover, this information should be kept with the clause. */
/* That for a flagfield is foreseen, most likely an integer used    */
/* like the sort-Bitfield existing for term, now used for varoccs.  */

typedef struct CLAUSE_HELP{
  int      clausenumber;
  NAT      weight;     /* The sum of the weight of all literals */
  NAT      depth;      /* The depth of the clause in the derivation  */
  NAT      validlevel; /* Level of splitting where clause is valid. */
  SPLITFIELD splitfield;
  unsigned splitfield_length;
  
  LIST     parentCls, parentLits; /* Parents clauses' clause and lit numbers.*/
  NAT      flags;
  SYMBOL   maxVar;     /* The maximal variable symbol in the clause */
  struct LITERAL_HELP{
    NAT    maxLit;     /* for clause intern literal ordering */
    NAT    weight;     /* weight of the <atomWithSign> below */
    BOOL   oriented;   /* Flag, TRUE if clause is oriented, i.e. equalities
			  with bigger first arg and all other predicates */
    struct CLAUSE_HELP *owningClause;
    TERM   atomWithSign; /* Pointer to the term, where an unshared
			    Term for the sign of negative literals
			    is supplied additionally.              */
  } **literals;        /* An Array of (c+a+s) literalpointers in this order. */
  int      c;          /* number of constraint literals */
  int      a;          /* number of antecedent literals */
  int	   s;          /* number of succedent literals */
  RULE    origin;
} *CLAUSE, CLAUSE_NODE;

typedef struct LITERAL_HELP *LITERAL, LITERAL_NODE;


/**************************************************************/
/* Functions Prototypes                                       */
/**************************************************************/

/**************************************************************/
/* Functions on clauses and literals creation and deletion.   */
/**************************************************************/

void    clause_Init(void);

CLAUSE  clause_CreateBody(int);
CLAUSE  clause_Create(LIST, LIST, LIST, FLAGSTORE, PRECEDENCE);
CLAUSE  clause_CreateCrude(LIST, LIST, LIST, BOOL);
CLAUSE  clause_CreateUnnormalized(LIST, LIST, LIST);
CLAUSE  clause_CreateFromLiterals(LIST, BOOL, BOOL, BOOL, FLAGSTORE, PRECEDENCE);
void    clause_Delete(CLAUSE);

LITERAL clause_LiteralCreate(TERM, CLAUSE);
LITERAL clause_LiteralCreateNegative(TERM, CLAUSE);        /* Unused */
void    clause_LiteralDelete(LITERAL);

LIST    clause_CopyConstraint(CLAUSE);
LIST    clause_CopyAntecedentExcept(CLAUSE, int);
LIST    clause_CopySuccedent(CLAUSE);
LIST    clause_CopySuccedentExcept(CLAUSE, int);


/**************************************************************/
/* Functions to use the sharing for clauses and literals.     */
/**************************************************************/

void    clause_InsertIntoSharing(CLAUSE, SHARED_INDEX, FLAGSTORE, PRECEDENCE);
void    clause_DeleteFromSharing(CLAUSE, SHARED_INDEX, FLAGSTORE, PRECEDENCE);

void    clause_MakeUnshared(CLAUSE, SHARED_INDEX);
void    clause_MoveSharedClause(CLAUSE, SHARED_INDEX, SHARED_INDEX, FLAGSTORE, PRECEDENCE);
void    clause_DeleteSharedLiteral(CLAUSE, int, SHARED_INDEX, FLAGSTORE, PRECEDENCE);

void    clause_LiteralInsertIntoSharing(LITERAL, SHARED_INDEX);
void    clause_LiteralDeleteFromSharing(LITERAL, SHARED_INDEX);  /* Used only in clause.c */

void    clause_DeleteClauseList(LIST);
void    clause_DeleteSharedClauseList(LIST, SHARED_INDEX, FLAGSTORE, PRECEDENCE);
void    clause_DeleteAllIndexedClauses(SHARED_INDEX, FLAGSTORE, PRECEDENCE); /* Necessary? */
void    clause_PrintAllIndexedClauses(SHARED_INDEX);       /* For Debugging */
LIST    clause_AllIndexedClauses(SHARED_INDEX);

/**************************************************************/
/* Clause Comparisons                                         */
/**************************************************************/

BOOL    clause_IsHornClause(CLAUSE);
int     clause_CompareAbstract(CLAUSE, CLAUSE);

/**************************************************************/
/* Clause and literal Input and Output Functions              */
/**************************************************************/

void    clause_Print(CLAUSE);
void    clause_PrintVerbose(CLAUSE, FLAGSTORE, PRECEDENCE);
void    clause_PrintMaxLitsOnly(CLAUSE, FLAGSTORE, PRECEDENCE); /* For Debugging */
void    clause_FPrint(FILE*, CLAUSE);                /* For Debugging */
void    clause_FPrintRule(FILE*, CLAUSE);
void    clause_FPrintOtter(FILE*, CLAUSE);           /* Unused */
void    clause_FPrintCnfDFG(FILE* , BOOL, LIST, LIST, FLAGSTORE, PRECEDENCE);
void    clause_FPrintCnfDFGProblem(FILE* , const char*, const char*, const char*, const char*, LIST);
void    clause_FPrintCnfFormulasDFGProblem(FILE* , BOOL, const char*, const char*, const char*, const char*, LIST, LIST, FLAGSTORE, PRECEDENCE);
void    clause_FPrintCnfDFGDerivables(FILE*, LIST, BOOL);
void    clause_FPrintDFG(FILE*, CLAUSE, BOOL);
void    clause_FPrintDFGStep(FILE*, CLAUSE, BOOL);
void    clause_FPrintFormulaDFG(FILE*, CLAUSE, BOOL);
void    clause_FPrintCnfOtter(FILE*, LIST, FLAGSTORE);

void    clause_LiteralPrint(LITERAL);                /* For Debugging */
void    clause_LiteralListPrint(LIST);               /* For Debugging */
void    clause_LiteralPrintUnsigned(LITERAL);        /* For Debugging */
void    clause_LiteralPrintSigned(LITERAL);          /* For Debugging */
void    clause_LiteralFPrint(FILE*, LITERAL);        /* For Debugging */

void    clause_ListPrint(LIST);

void    clause_PrintParentClauses(CLAUSE);           /* For Debugging */
void    clause_PrintOrigin(CLAUSE);                  /* For Debugging */
void    clause_FPrintOrigin(FILE*, CLAUSE);

/**************************************************************/
/* Specials                                                   */
/**************************************************************/

CLAUSE  clause_Copy(CLAUSE);
LITERAL clause_LiteralCopy(LITERAL);

static __inline__ LIST clause_CopyClauseList(LIST List)
{
  return list_CopyWithElement(List, (POINTER (*)(POINTER)) clause_Copy);
}

void    clause_DeleteLiteral(CLAUSE, int, FLAGSTORE, PRECEDENCE);
void    clause_DeleteLiteralNN(CLAUSE, int);
void    clause_DeleteLiterals(CLAUSE, LIST, FLAGSTORE, PRECEDENCE);  /* Unused */
LIST    clause_GetLiteralSubSetList(CLAUSE, int, int, FLAGSTORE, PRECEDENCE);
void    clause_ReplaceLiteralSubSet(CLAUSE, int, int, LIST, FLAGSTORE, PRECEDENCE);
void    clause_FixLiteralOrder(CLAUSE, FLAGSTORE, PRECEDENCE);

SYMBOL  clause_AtomMaxVar(TERM);
void    clause_SetMaxLitFlags(CLAUSE, FLAGSTORE, PRECEDENCE);
SYMBOL  clause_LiteralMaxVar(LITERAL);        /* Used only in clause.c */
SYMBOL  clause_SearchMaxVar(CLAUSE);
void    clause_UpdateMaxVar(CLAUSE);

void    clause_RenameVarsBiggerThan(CLAUSE, SYMBOL);
void    clause_Normalize(CLAUSE);
void    clause_SetSortConstraint(CLAUSE, BOOL, FLAGSTORE, PRECEDENCE);
void    clause_SubstApply(SUBST, CLAUSE);
void    clause_ReplaceVariable(CLAUSE, SYMBOL, TERM);
void    clause_OrientEqualities(CLAUSE, FLAGSTORE, PRECEDENCE);
NAT     clause_NumberOfVarOccs(CLAUSE);
NAT     clause_NumberOfSymbolOccurrences(CLAUSE, SYMBOL);
NAT     clause_ComputeWeight(CLAUSE, FLAGSTORE);
NAT     clause_LiteralComputeWeight(LITERAL, FLAGSTORE);
NAT     clause_ComputeTermDepth(CLAUSE);
NAT     clause_MaxTermDepthClauseList(LIST);
NAT     clause_ComputeSize(CLAUSE);
BOOL    clause_WeightCorrect(CLAUSE, FLAGSTORE, PRECEDENCE);   /* Unused */

LIST    clause_MoveBestLiteralToFront(LIST, SUBST, SYMBOL,
				      BOOL (*)(LITERAL, NAT, LITERAL, NAT));


LIST    clause_InsertWeighed(CLAUSE, LIST, FLAGSTORE, PRECEDENCE);
LIST    clause_ListSortWeighed(LIST);

BOOL    clause_HasTermSortConstraintLits(CLAUSE);
BOOL    clause_HasSolvedConstraint(CLAUSE);
BOOL    clause_IsDeclarationClause(CLAUSE);
BOOL    clause_IsSortTheoryClause(CLAUSE, FLAGSTORE, PRECEDENCE);
BOOL    clause_IsPartOfDefinition(CLAUSE, TERM, int*, LIST);
BOOL    clause_IsPotentialSortTheoryClause(CLAUSE, FLAGSTORE, PRECEDENCE);
BOOL    clause_HasOnlyVarsInConstraint(CLAUSE, FLAGSTORE, PRECEDENCE);
BOOL    clause_HasSortInSuccedent(CLAUSE, FLAGSTORE, PRECEDENCE);
BOOL    clause_ContainsPotPredDef(CLAUSE, FLAGSTORE, PRECEDENCE, NAT*, LIST*);
BOOL    clause_LitsHaveCommonVar(LITERAL, LITERAL);

void    clause_SelectLiteral(CLAUSE, FLAGSTORE);
void    clause_SetSpecialFlags(CLAUSE,BOOL, FLAGSTORE, PRECEDENCE);

BOOL    clause_LiteralIsLiteral(LITERAL);
BOOL    clause_IsClause(CLAUSE, FLAGSTORE, PRECEDENCE);
BOOL    clause_IsUnorderedClause(CLAUSE);
BOOL    clause_ContainsPositiveEquations(CLAUSE);
BOOL    clause_ContainsNegativeEquations(CLAUSE);
int     clause_ContainsFolAtom(CLAUSE,BOOL*,BOOL*,BOOL*,BOOL*);
BOOL    clause_ContainsVariables(CLAUSE);
BOOL    clause_ContainsFunctions(CLAUSE);
BOOL    clause_ContainsSymbol(CLAUSE, SYMBOL);
void    clause_ContainsSortRestriction(CLAUSE,BOOL*,BOOL*);
BOOL    clause_ImpliesFiniteDomain(CLAUSE);
BOOL    clause_ImpliesNonTrivialDomain(CLAUSE);
LIST    clause_FiniteMonadicPredicates(LIST);

CLAUSE  clause_GetNumberedCl(int, LIST);
LIST    clause_NumberSort(LIST);
LIST    clause_NumberDelete(LIST,int);
void    clause_Check(CLAUSE, FLAGSTORE, PRECEDENCE);

void    clause_DeleteFlatFromIndex(CLAUSE, st_INDEX);
void    clause_InsertFlatIntoIndex(CLAUSE, st_INDEX);
void    clause_DeleteClauseListFlatFromIndex(LIST, st_INDEX);

RULE    clause_GetOriginFromString(const char*);

void    clause_CountSymbols(CLAUSE);

LIST    clause_ListOfPredicates(CLAUSE);
LIST    clause_ListOfConstants(CLAUSE);
LIST    clause_ListOfVariables(CLAUSE);
LIST    clause_ListOfFunctions(CLAUSE);

/* special output functions for clauses with parent pointers */
void clause_PParentsFPrint(FILE*, CLAUSE);
void clause_PParentsListFPrint(FILE*, LIST L);
void clause_PParentsPrint(CLAUSE);
void clause_PParentsListPrint(LIST);
void clause_PParentsFPrintGen(FILE*, CLAUSE, BOOL);


/**************************************************************/
/* Inline Functions                                           */
/**************************************************************/

/**************************************************************/
/* Accessing Literals 1                                       */
/**************************************************************/

static __inline__ TERM clause_LiteralSignedAtom(LITERAL L)
{
  return L->atomWithSign;
}


static __inline__ CLAUSE clause_LiteralOwningClause(LITERAL L)
{
  return L->owningClause;
}

static __inline__ void clause_LiteralSetOwningClause(LITERAL L, CLAUSE C)
{
  L->owningClause = C;
}


static __inline__ void clause_LiteralSetOrientedEquality(LITERAL L)
{
  L->oriented = TRUE;
}

static __inline__ void clause_LiteralSetNoOrientedEquality(LITERAL L)
{
  L->oriented = FALSE;
}


static __inline__ NAT clause_LiteralWeight(LITERAL L)
{
#ifdef CHECK
  if (L->weight == clause_WEIGHTUNDEFINED) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In clause_LiteralWeight:");
    misc_ErrorReport(" Tried to access undefined weight.");
    misc_FinishErrorReport();
  }
#endif
  return L->weight;
}


static __inline__ void clause_UpdateLiteralWeight(LITERAL L, FLAGSTORE Flags)
{
  L->weight = clause_LiteralComputeWeight(L, Flags);
}


static __inline__ void clause_LiteralFlagReset(LITERAL L)
{
  L->maxLit = 0;
}

static __inline__ BOOL clause_LiteralGetFlag(LITERAL L, MAXFLAG Flag)
{
  return ((L->maxLit & Flag) != 0);
}

static __inline__ void clause_LiteralSetFlag(LITERAL L, MAXFLAG Flag)
{
  L->maxLit = (L->maxLit) | Flag;
}

static __inline__ BOOL clause_LiteralIsMaximal(LITERAL L)
{
  return clause_LiteralGetFlag(L, MAXIMAL);
}



static __inline__ BOOL clause_LiteralIsOrientedEquality(LITERAL L)
{
  return L->oriented;
}


static __inline__ BOOL clause_LiteralIsNotOrientedEquality(LITERAL L)
{
  return !(L->oriented);
}


/**************************************************************/
/* Literal Comparison 1                                       */
/**************************************************************/

static __inline__ BOOL clause_LiteralIsNegative(LITERAL L)
{
  return (term_TopSymbol(clause_LiteralSignedAtom(L)) == fol_Not());
}

static __inline__ BOOL clause_LiteralIsPositive(LITERAL L)
{
  return !clause_LiteralIsNegative(L);
}


static __inline__ BOOL clause_LiteralsAreComplementary(LITERAL L1, LITERAL L2)
{
  return ((clause_LiteralIsNegative(L1) &&
	   clause_LiteralIsPositive(L2)) ||
	  (clause_LiteralIsNegative(L2) &&
	   clause_LiteralIsPositive(L1)));      /* xor */
}

static __inline__ BOOL clause_HyperLiteralIsBetter(LITERAL Dummy1, NAT S1,
						   LITERAL Dummy2, NAT S2)
/**************************************************************
  INPUT:   Two literals and its sizes wrt. some substitution.
  RETURNS: TRUE, if the first literal is 'better' than the second literal,
           FALSE otherwise.
  EFFECT:  A literal is 'better' than another, if S1 > Ss.
           Since we have to find unifiable complementary literals
	   for every remaining antecedent literal, it seems to be
	   a good idea to try the most 'difficult' literal first,
	   in order to stop the search as early as possible..
	   Here we prefer the literal with the highest number
	   of symbols..
           This function is used as parameter for the function
	   clause_MoveBestLiteralToFront.
  CAUTION: The parameters <Dummy1> and <Dummy2> are unused, they're just
           added to keep the compiler quiet.
***************************************************************/
{
  return (S1 > S2);
}


/**************************************************************/
/* Accessing Literals 2                                       */
/**************************************************************/

static __inline__ TERM clause_LiteralAtom(LITERAL L)
{
  if (clause_LiteralIsNegative(L))
    return term_FirstArgument(clause_LiteralSignedAtom(L));
  else
    return clause_LiteralSignedAtom(L);
}


static __inline__ SYMBOL clause_LiteralPredicate(LITERAL L)
{
  return term_TopSymbol(clause_LiteralAtom(L));
}

static __inline__ BOOL clause_LiteralIsPredicate(LITERAL L)
{
  return !fol_IsEquality(clause_LiteralAtom(L));
}

static __inline__ BOOL clause_LiteralIsEquality(LITERAL L)
{
  return fol_IsEquality(clause_LiteralAtom(L));
}

static __inline__ BOOL clause_LiteralIsSort(LITERAL L)
{
  SYMBOL S;
  S = clause_LiteralPredicate(L);
  return (symbol_IsPredicate(S) &&
	  (symbol_Arity(S) == 1));
}


static __inline__ void clause_LiteralSetAtom(LITERAL L, TERM A)
{
  if (clause_LiteralIsNegative(L))
    list_Rplaca(term_ArgumentList(clause_LiteralSignedAtom(L)),A);
  else
    L->atomWithSign = A;
}

static __inline__ void clause_LiteralSetNegAtom(LITERAL L, TERM A)
{
  list_Rplaca(term_ArgumentList(clause_LiteralSignedAtom(L)), A);
}

static __inline__ void clause_LiteralSetPosAtom(LITERAL L, TERM A)
{
  L->atomWithSign = A;
}

static __inline__ void clause_NLiteralSetLiteral(LITERAL L, TERM LIT)
{
  L->atomWithSign = LIT;
}

/**************************************************************/
/* Memory management                                          */
/**************************************************************/

static __inline__ void clause_LiteralFree(LITERAL L)
{
  memory_Free(L, sizeof(LITERAL_NODE));
}


/**************************************************************/
/* Functions to access literals.                                 */
/**************************************************************/

static __inline__ LITERAL clause_GetLiteral(CLAUSE C, int Index)
{
  return C->literals[Index];
}

static __inline__ void clause_SetLiteral(CLAUSE C, int Index, LITERAL L)
{
  C->literals[Index]= L;
}

static __inline__ TERM clause_GetLiteralTerm(CLAUSE C, int Index)
{
  return clause_LiteralSignedAtom(clause_GetLiteral(C, Index));
}

static __inline__ TERM clause_GetLiteralAtom(CLAUSE C, int Index)
{
  return clause_LiteralAtom(clause_GetLiteral(C, Index));
}

static __inline__ int clause_NumOfConsLits(CLAUSE Clause)
{
  return Clause->c;
}

static __inline__ int clause_NumOfAnteLits(CLAUSE Clause)
{
  return Clause->a;
}

static __inline__ int clause_NumOfSuccLits(CLAUSE Clause)
{
  return Clause->s;
}

static __inline__ void clause_SetNumOfConsLits(CLAUSE Clause, int Number)
{
  Clause->c = Number;
}

static __inline__ void clause_SetNumOfAnteLits(CLAUSE Clause, int Number)
{
  Clause->a = Number;
}

static __inline__ void clause_SetNumOfSuccLits(CLAUSE Clause, int Number)
{
  Clause->s = Number;
}

static __inline__ int clause_Length(CLAUSE Clause)
{
  return (clause_NumOfConsLits(Clause) +
	  clause_NumOfAnteLits(Clause) +
	  clause_NumOfSuccLits(Clause));
}


static __inline__ int clause_LastLitIndex(CLAUSE Clause)
{
  return clause_Length(Clause) - 1;
}

static __inline__ int clause_FirstLitIndex(void)
{
  return 0;
}

static __inline__ int clause_FirstConstraintLitIndex(CLAUSE Clause)
{
  return 0;
}

static __inline__ int clause_FirstAntecedentLitIndex(CLAUSE Clause)
{
  return clause_NumOfConsLits(Clause);
}

static __inline__ int clause_FirstSuccedentLitIndex(CLAUSE Clause)
{
  return (clause_NumOfAnteLits(Clause) + clause_NumOfConsLits(Clause));
}


static __inline__ int clause_LastConstraintLitIndex(CLAUSE Clause)
{
  return clause_NumOfConsLits(Clause) - 1;
}

static __inline__ int clause_LastAntecedentLitIndex(CLAUSE Clause)
{
  return clause_FirstSuccedentLitIndex(Clause) - 1;
}

static __inline__ int clause_LastSuccedentLitIndex(CLAUSE Clause)
{
  return clause_Length(Clause) - 1;
}

static __inline__ LIST clause_GetLiteralList(CLAUSE Clause)
/**************************************************************
  INPUT:   A clause.
  RETURNS: A new list is created containing all literals of the
           clause. The list contains pointers, not literal indexes.
***************************************************************/
{
  LIST Result;
  int  i;

  Result = list_Nil();
  for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++)
    Result = list_Cons(clause_GetLiteral(Clause, i), Result);
  return Result;
}


static __inline__ LIST clause_GetLiteralListExcept(CLAUSE Clause, int Index)
/**************************************************************
  INPUT:   A clause.
  RETURNS: A new list is created containing all literals of the
           clause except the literal at <Index>. The list contains
	   pointers, not literal indexes.
***************************************************************/
{
  LIST Result;
  int  i;

  Result = list_Nil();
  for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++)
    if (i != Index)
      Result = list_Cons(clause_GetLiteral(Clause, i), Result);
  return Result;
}


/**************************************************************/
/* Clause Access Macros                                       */
/**************************************************************/

static __inline__ int clause_Counter(void)
{
  return clause_CLAUSECOUNTER;
}

static __inline__ void clause_SetCounter(int Value)
{
#ifdef CHECK
  if (Value < 0) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In clause_SetCounter: new counter value is negative.");
    misc_FinishErrorReport();
  }
#endif
  clause_CLAUSECOUNTER = Value;
}

static __inline__ int clause_IncreaseCounter(void)
{
#ifdef CHECK
  if (clause_CLAUSECOUNTER == INT_MAX) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In clause_IncreaseCounter: counter overflow.");
    misc_FinishErrorReport();
  }
#endif
  return clause_CLAUSECOUNTER++;
}

static __inline__ void clause_DecreaseCounter(void)
{
#ifdef CHECK
  if (clause_CLAUSECOUNTER == 0) {
    misc_FinishErrorReport();
    misc_ErrorReport("\n In clause_DecreaseCounter: counter underflow.");
    misc_FinishErrorReport();
  }
#endif
  clause_CLAUSECOUNTER--;
}

static __inline__ NAT clause_Depth(CLAUSE Clause)
{
  return Clause->depth;
}

static __inline__ void clause_SetDepth(CLAUSE Clause, NAT NewDepth)
{
  Clause->depth = NewDepth;
}


static __inline__ NAT clause_Weight(CLAUSE Clause)
{
#ifdef CHECK
  if (Clause->weight == clause_WEIGHTUNDEFINED) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In clause_Weight: Tried to access undefined weight.");
    misc_FinishErrorReport();
  }
#endif
  return Clause->weight;
}

static __inline__ void clause_UpdateWeight(CLAUSE Clause, FLAGSTORE Flags)
{
  Clause->weight = clause_ComputeWeight(Clause, Flags);
}


static __inline__ int clause_Number(const CLAUSE Clause)
{
  return Clause->clausenumber;
}

static __inline__ void clause_SetNumber(CLAUSE Clause, int Number)
{
  Clause->clausenumber = Number;
}

static __inline__ void clause_NewNumber(CLAUSE Clause)
{
  Clause->clausenumber = clause_IncreaseCounter();
}


static __inline__ NAT clause_SplitLevel(CLAUSE Clause)
{
  return Clause->validlevel;
}

static __inline__ BOOL clause_CheckSplitLevel(CLAUSE Clause)
/**************************************************************
  INPUT:   A clause.
  RETURNS: TRUE, if the splitlevel invariant for the clause is fulfilled.
  EFFECT:  Checks, if the validlevel of the clause is the order
           of the highest set bit in the SPLITFIELD entry
           of the clause.
***************************************************************/
{
  if (Clause->validlevel == 0)
    return (Clause->splitfield == NULL);
  else {
    int i, j;
    for (i = Clause->splitfield_length-1; i >= 0; i--)
      if (Clause->splitfield[i] != 0)
	break;
    for (j = sizeof(SPLITFIELDENTRY)*CHAR_BIT-1; j >= 0; j--)
      if (Clause->splitfield[i] & ((SPLITFIELDENTRY)1 << j))
	break;
    return (Clause->validlevel == (i*sizeof(SPLITFIELDENTRY)*CHAR_BIT+j));
  }
}

static __inline__ LIST clause_ParentClauses(CLAUSE Clause)
{
  return Clause->parentCls;
}

static __inline__ LIST clause_ParentLiterals(CLAUSE Clause)
{
  return Clause->parentLits;
}


static __inline__ SYMBOL clause_MaxVar(CLAUSE Clause)
{
  return Clause->maxVar;
}

static __inline__ void clause_SetMaxVar(CLAUSE Clause, SYMBOL Variable)
{
  Clause->maxVar = Variable;
}


static __inline__ RULE clause_Origin(CLAUSE Clause)
{
  return Clause->origin;
}

static __inline__ BOOL clause_Exists(CLAUSE Clause)
{
  return (Clause != (CLAUSE)NULL);
}

static __inline__ BOOL clause_LiteralExists(LITERAL L)
{
  return (L != (LITERAL)NULL);
}

static __inline__ CLAUSE clause_Null(void)
{
  return (CLAUSE) NULL;
}

static __inline__ void clause_SetSplitLevel(CLAUSE Clause, NAT Level)
{
  Clause->validlevel = Level;
}

static __inline__ void clause_InitSplitData(CLAUSE C)
{
  C->splitfield = NULL;
  C->splitfield_length = 0;
  clause_SetSplitLevel(C, 0);
}

static __inline__ void clause_SetSplitField(CLAUSE Clause, SPLITFIELD B,
					    unsigned Length)
{
  unsigned i;
  if (Clause->splitfield_length != Length) {
    if (Clause->splitfield != NULL) {
      memory_Free(Clause->splitfield,
		  sizeof(SPLITFIELDENTRY) * Clause->splitfield_length);
    }
    if (Length != 0) {
      Clause->splitfield = memory_Malloc(sizeof(SPLITFIELDENTRY) * Length);
    }
    else
      Clause->splitfield = NULL;
    Clause->splitfield_length = Length;
  }
  for (i=0; i < Length; i++)
    Clause->splitfield[i] = B[i];
}


static __inline__ NAT  clause_ComputeSplitFieldAddress(NAT n, NAT* field)
{
  *field = 0;
  while (n >= (sizeof(SPLITFIELDENTRY) * CHAR_BIT)) {
    (*field)++;
    n -= sizeof(SPLITFIELDENTRY) * CHAR_BIT;
  }
  return n;
}

static __inline__ void clause_ExpandSplitField(CLAUSE C, NAT Length)
{
  SPLITFIELD NewField;
  NAT i;
  if (C->splitfield_length < Length) {
    NewField = memory_Malloc(sizeof(SPLITFIELDENTRY) * Length);
    for (i=0; i < C->splitfield_length; i++)
      NewField[i] = C->splitfield[i];
    for (i=C->splitfield_length; i < Length; i++)
      NewField[i] = 0;
    if (C->splitfield != NULL) {
      memory_Free(C->splitfield,
		  sizeof(SPLITFIELDENTRY) * C->splitfield_length);
    }
    C->splitfield = NewField;
    C->splitfield_length = Length;
  }
}

static __inline__ void clause_UpdateSplitField(CLAUSE C1, CLAUSE C2)
  /* Add the split data of <C2> to <C1> */
{
  unsigned i;
  if (C1->splitfield_length < C2->splitfield_length)
    clause_ExpandSplitField(C1, C2->splitfield_length);
  for (i=0; i < C2->splitfield_length; i++)
    C1->splitfield[i] = C1->splitfield[i] | C2->splitfield[i];
}

static __inline__ void clause_ClearSplitField(CLAUSE C)
{
  int i;

  for (i=C->splitfield_length-1; i >=0; i--)
    C->splitfield[i] = 0;
}
	
static __inline__ void clause_SetSplitFieldBit(CLAUSE Clause, NAT n)
{
  unsigned field;
  
  n = clause_ComputeSplitFieldAddress(n, &field);
  if (field >= Clause->splitfield_length)
    clause_ExpandSplitField(Clause, field + 1);
  Clause->splitfield[field] = (Clause->splitfield[field]) |
    ((SPLITFIELDENTRY)1 << n);
}

static __inline__ BOOL clause_GetFlag(CLAUSE Clause, CLAUSE_FLAGS Flag)
{
  return (Clause->flags & Flag) != 0;
}

static __inline__ void clause_SetFlag(CLAUSE Clause, CLAUSE_FLAGS Flag)
{
  Clause->flags = Clause->flags | Flag;
}

static __inline__ void clause_RemoveFlag(CLAUSE Clause, CLAUSE_FLAGS Flag)
{
  if (Clause->flags & Flag)
    Clause->flags = Clause->flags - Flag;
}

static __inline__ void clause_ClearFlags(CLAUSE Clause)
{
  Clause->flags = 0;
}


static __inline__ BOOL clause_DependsOnSplitLevel(CLAUSE C, NAT N)
{
  if (N==0)
    return TRUE;
  else {
    unsigned field;
    N = clause_ComputeSplitFieldAddress(N, &field);
    if (field >= C->splitfield_length)
      return FALSE;
    else
      return (C->splitfield[field] & ((SPLITFIELDENTRY)1 << N)) != 0;
  }
}

static __inline__ void clause_SetSplitDataFromFather(CLAUSE Result,
						     CLAUSE Father)
{
  if (clause_GetFlag(Father, CONCLAUSE))
    clause_SetFlag(Result, CONCLAUSE);
  clause_SetSplitLevel(Result, clause_SplitLevel(Father));
  clause_SetSplitField(Result, Father->splitfield, Father->splitfield_length);
}

static __inline__ void clause_UpdateSplitDataFromNewSplitting(CLAUSE Result,
							      CLAUSE Father,
							      NAT Level)
{
  unsigned field;
  NAT i;
  
  clause_SetSplitLevel(Result, Level);
  Level = clause_ComputeSplitFieldAddress(Level, &field);

  if (field >= Result->splitfield_length) {
    if (Result->splitfield != NULL)
      memory_Free(Result->splitfield,
		  sizeof(SPLITFIELDENTRY) * Result->splitfield_length);
    Result->splitfield = memory_Malloc((field + 1) * sizeof(SPLITFIELDENTRY));
    Result->splitfield_length = field + 1;
  }
  if (clause_GetFlag(Father, CONCLAUSE))
    clause_SetFlag(Result, CONCLAUSE);
  for (i=0; i < Father->splitfield_length; i++)
    Result->splitfield[i] = Father->splitfield[i];
  for (i=Father->splitfield_length; i < Result->splitfield_length; i++)
    Result->splitfield[i] = 0;
  Result->splitfield[field] = (Result->splitfield[field] | ((SPLITFIELDENTRY)1 << Level));
}

static __inline__ void clause_UpdateSplitDataFromPartner(CLAUSE Result,
							 CLAUSE Partner)
{
  if (clause_GetFlag(Partner, CONCLAUSE))
    clause_SetFlag(Result, CONCLAUSE);
  if (clause_SplitLevel(Partner) == 0)
    return;
  /* Set Split level to misc_Max(Partner, Result) */
  clause_SetSplitLevel(Result, clause_SplitLevel(Partner) > clause_SplitLevel(Result)
		       ? clause_SplitLevel(Partner)
		       : clause_SplitLevel(Result));
  clause_UpdateSplitField(Result, Partner);
}

static __inline__ void clause_SetSplitDataFromList(CLAUSE Result, LIST List)
{
  CLAUSE TempClause;
  LIST Scan;
  NAT  l;
  Scan = List;
  l = Result->splitfield_length;
  while (!list_Empty(Scan)) {
    TempClause = (CLAUSE) list_Top(Scan);
    if (clause_GetFlag(TempClause, CONCLAUSE))
      clause_SetFlag(Result, CONCLAUSE);
    clause_SetSplitLevel(Result,
			 clause_SplitLevel(TempClause) > clause_SplitLevel(Result)
			 ? clause_SplitLevel(TempClause)
			 : clause_SplitLevel(Result));
    if (l < TempClause->splitfield_length)
      l = TempClause->splitfield_length;
    Scan = list_Cdr(Scan);
  }
  if (l > Result->splitfield_length) {
    if (Result->splitfield != NULL)
      memory_Free(Result->splitfield,
		  sizeof(SPLITFIELDENTRY) * Result->splitfield_length);
    Result->splitfield = memory_Malloc(sizeof(SPLITFIELDENTRY) * l);
    Result->splitfield_length = l;
  }
  
  for (l=0; l < Result->splitfield_length; l++)
    Result->splitfield[l] = 0;
  
  while (!list_Empty(List)) {
    TempClause= (CLAUSE) list_Top(List);
    List = list_Cdr(List);
    for (l=0; l < TempClause->splitfield_length; l++)
      Result->splitfield[l] = Result->splitfield[l] | TempClause->splitfield[l];
  }
}


static __inline__ void clause_SetSplitDataFromParents(CLAUSE Result,
						      CLAUSE Mother,
						      CLAUSE Father)
{
  NAT i;
  if (clause_GetFlag(Father, CONCLAUSE) || clause_GetFlag(Mother, CONCLAUSE))
    clause_SetFlag(Result, CONCLAUSE);
  if ((clause_SplitLevel(Father) == 0) && (clause_SplitLevel(Mother) == 0))
    return;
  clause_SetSplitLevel(Result, clause_SplitLevel(Mother) > clause_SplitLevel(Father)
		       ? clause_SplitLevel(Mother)
		       : clause_SplitLevel(Father));
  
  if (Mother->splitfield_length > Father->splitfield_length) {
    if (Result->splitfield != NULL)
      memory_Free(Result->splitfield,
		  sizeof(SPLITFIELDENTRY) * Result->splitfield_length);
    Result->splitfield = memory_Malloc(sizeof(SPLITFIELDENTRY) *
				       Mother->splitfield_length);
    Result->splitfield_length = Mother->splitfield_length;
    for (i=0; i < Father->splitfield_length; i++)
      Result->splitfield[i] =
	Mother->splitfield[i] | Father->splitfield[i];
    for (i=Father->splitfield_length; i < Mother->splitfield_length; i++)
      Result->splitfield[i] = Mother->splitfield[i];
  }
  else {
    if (Result->splitfield != NULL)
      memory_Free(Result->splitfield,
		  sizeof(SPLITFIELDENTRY) * Result->splitfield_length);
    Result->splitfield = memory_Malloc(sizeof(SPLITFIELDENTRY) *
				       Father->splitfield_length);
    Result->splitfield_length = Father->splitfield_length;
    for (i=0; i < Mother->splitfield_length; i++)
      Result->splitfield[i] =
	Mother->splitfield[i] | Father->splitfield[i];
    for (i=Mother->splitfield_length; i < Father->splitfield_length; i++)
      Result->splitfield[i] = Father->splitfield[i];
  }
}

static __inline__ void clause_SetParentClauses(CLAUSE Clause, LIST PClauses)
{
  Clause->parentCls = PClauses;
}

static __inline__ void clause_AddParentClause(CLAUSE Clause, int PClause)
{
  Clause->parentCls = list_Cons((POINTER) PClause, Clause->parentCls);
}

static __inline__ void clause_SetParentLiterals(CLAUSE Clause, LIST PLits)
{
  Clause->parentLits = PLits;
}

static __inline__ void clause_AddParentLiteral(CLAUSE Clause, int PLit)
{
  Clause->parentLits = list_Cons((POINTER) PLit, Clause->parentLits);
}


static __inline__ BOOL clause_ValidityIsNotSmaller(CLAUSE C1, CLAUSE C2)
{
  return (C1->validlevel <= C2->validlevel);
}

static __inline__ BOOL clause_IsMoreValid(CLAUSE C1, CLAUSE C2)
{
  return (C1->validlevel < C2->validlevel);
}


static __inline__ BOOL  clause_CompareAbstractLEQ (CLAUSE Left, CLAUSE Right) 
/**************************************************************
  INPUT:   Two clauses.
  RETURNS: TRUE if left <= right, FALSE otherwise.
  EFFECTS: Internal function used to compare clauses for
           sorting.
  CAUTION: Expects clause literal order to be fixed.
***************************************************************/
{
  return (BOOL) (clause_CompareAbstract(Left, Right) <= 0);
}


static __inline__ BOOL clause_IsFromRewriting(CLAUSE Clause)
{
  return Clause->origin == REWRITING;
}

static __inline__ BOOL clause_IsFromCondensing(CLAUSE Clause)
{
  return Clause->origin == CONDENSING;
}

static __inline__ BOOL clause_IsFromObviousReductions(CLAUSE Clause)
{
  return Clause->origin == OBVIOUS_REDUCTIONS;
}

static __inline__ BOOL clause_IsFromSortSimplification(CLAUSE Clause)
{
  return Clause->origin == SORT_SIMPLIFICATION;
}

static __inline__ BOOL clause_IsFromMatchingReplacementResolution(CLAUSE Clause)
{
  return Clause->origin == MATCHING_REPLACEMENT_RESOLUTION;
}

static __inline__  BOOL clause_IsFromClauseDeletion(CLAUSE Clause)
{
  return Clause->origin == CLAUSE_DELETION;
}

static __inline__ BOOL clause_IsFromEmptySort(CLAUSE Clause)
{
  return Clause->origin == EMPTY_SORT;
}

static __inline__ BOOL clause_IsFromSortResolution(CLAUSE Clause)
{
  return Clause->origin == SORT_RESOLUTION;
}

static __inline__ BOOL clause_IsFromUnitConflict(CLAUSE Clause)
{
  return Clause->origin == UNIT_CONFLICT;
}

static __inline__ BOOL clause_IsFromEqualityResolution(CLAUSE Clause)
{
  return Clause->origin == EQUALITY_RESOLUTION;
}

static __inline__ BOOL clause_IsFromEqualityFactoring(CLAUSE Clause)
{
  return Clause->origin == EQUALITY_FACTORING;
}

static __inline__ BOOL clause_IsFromMergingParamodulation(CLAUSE Clause)
{
  return Clause->origin == MERGING_PARAMODULATION;
}

static __inline__ BOOL clause_IsFromSuperpositionRight(CLAUSE Clause)
{
  return Clause->origin == SUPERPOSITION_RIGHT;
}

static __inline__ BOOL clause_IsFromSuperpositionLeft(CLAUSE Clause)
{
  return Clause->origin == SUPERPOSITION_LEFT;
}

static __inline__ BOOL clause_IsFromGeneralResolution(CLAUSE Clause)
{
  return Clause->origin == GENERAL_RESOLUTION;
}

static __inline__ BOOL clause_IsFromGeneralFactoring(CLAUSE Clause)
{
  return Clause->origin == GENERAL_FACTORING;
}

static __inline__ BOOL clause_IsFromSplitting(CLAUSE Clause)
{
  return Clause->origin == SPLITTING;
}

static __inline__ BOOL clause_IsFromDefApplication(CLAUSE Clause)
{
  return Clause->origin == DEFAPPLICATION;
}

static __inline__ BOOL clause_IsFromTerminator(CLAUSE Clause)
{
  return Clause->origin == TERMINATOR;
}

static __inline__ BOOL clause_IsTemporary(CLAUSE Clause)
{
  return Clause->origin == TEMPORARY;
}

static __inline__ BOOL clause_IsFromInput(CLAUSE Clause)
{
  return Clause->origin == INPUT;
}


static __inline__ BOOL clause_HasReducedPredecessor(CLAUSE Clause)
{
  RULE origin = clause_Origin(Clause);

  return (origin == CONDENSING                   ||
	  origin == REWRITING                    ||
	  origin == SPLITTING                    ||
	  origin == ASSIGNMENT_EQUATION_DELETION ||
	  origin == SORT_SIMPLIFICATION          ||
	  origin == OBVIOUS_REDUCTIONS);
}

static __inline__ BOOL clause_IsSplitFather(CLAUSE C1, CLAUSE C2)
{
  return (C1->clausenumber == (int)list_Car(C2->parentCls));
}


static __inline__ void clause_SetFromRewriting(CLAUSE Clause)
{
  Clause->origin = REWRITING;
}

static __inline__ void clause_SetFromContextualRewriting(CLAUSE Clause)
{
  Clause->origin = CONTEXTUAL_REWRITING;
}

static __inline__ void clause_SetFromUnitConflict(CLAUSE Clause)
{
  Clause->origin = UNIT_CONFLICT;
}

static __inline__ void clause_SetFromCondensing(CLAUSE Clause)
{
  Clause->origin = CONDENSING;
}

static __inline__ void clause_SetFromAssignmentEquationDeletion(CLAUSE Clause)
{
  Clause->origin = ASSIGNMENT_EQUATION_DELETION;
}

static __inline__ void clause_SetFromObviousReductions(CLAUSE Clause)
{
  Clause->origin = OBVIOUS_REDUCTIONS;
}

static __inline__ void clause_SetFromSortSimplification(CLAUSE Clause)
{
  Clause->origin = SORT_SIMPLIFICATION;
}

static __inline__ void clause_SetFromMatchingReplacementResolution(CLAUSE Clause)
{
  Clause->origin = MATCHING_REPLACEMENT_RESOLUTION;
}

static __inline__ void clause_SetFromClauseDeletion(CLAUSE Clause)
{
  Clause->origin = CLAUSE_DELETION;
}

static __inline__ void clause_SetFromEmptySort(CLAUSE Clause)
{
  Clause->origin = EMPTY_SORT;
}

static __inline__ void clause_SetFromSortResolution(CLAUSE Clause)
{
  Clause->origin = SORT_RESOLUTION;
}

static __inline__ void clause_SetFromEqualityResolution(CLAUSE Clause)
{
  Clause->origin = EQUALITY_RESOLUTION;
}

static __inline__ void clause_SetFromEqualityFactoring(CLAUSE Clause)
{
  Clause->origin = EQUALITY_FACTORING;
}

static __inline__ void clause_SetFromMergingParamodulation(CLAUSE Clause)
{
  Clause->origin = MERGING_PARAMODULATION;
}

static __inline__ void clause_SetFromParamodulation(CLAUSE Clause)
{
  Clause->origin = PARAMODULATION;
}
static __inline__ void clause_SetFromOrderedParamodulation(CLAUSE Clause)
{
  Clause->origin = ORDERED_PARAMODULATION;
}
static __inline__ void clause_SetFromSuperpositionRight(CLAUSE Clause)
{
  Clause->origin = SUPERPOSITION_RIGHT;
}

static __inline__ void clause_SetFromSuperpositionLeft(CLAUSE Clause)
{
  Clause->origin = SUPERPOSITION_LEFT;
}

static __inline__ void clause_SetFromGeneralResolution(CLAUSE Clause)
{
  Clause->origin = GENERAL_RESOLUTION;
}

static __inline__ void clause_SetFromOrderedHyperResolution(CLAUSE Clause)
{
  Clause->origin = ORDERED_HYPER;
}

static __inline__ void clause_SetFromSimpleHyperResolution(CLAUSE Clause)
{
  Clause->origin = SIMPLE_HYPER;
}

static __inline__ void clause_SetFromURResolution(CLAUSE Clause)
{
  Clause->origin = UR_RESOLUTION;
}

static __inline__ void clause_SetFromGeneralFactoring(CLAUSE Clause)
{
  Clause->origin = GENERAL_FACTORING;
}

static __inline__ void clause_SetFromSplitting(CLAUSE Clause)
{
  Clause->origin = SPLITTING;
}

static __inline__ void clause_SetFromDefApplication(CLAUSE Clause)
{
  Clause->origin = DEFAPPLICATION;
}

static __inline__ void clause_SetFromTerminator(CLAUSE Clause)
{
  Clause->origin = TERMINATOR;
}

static __inline__ void clause_SetTemporary(CLAUSE Clause)
{
  Clause->origin = TEMPORARY;
}


static __inline__ void clause_SetFromInput(CLAUSE Clause)
{
  Clause->origin = INPUT;
}


static __inline__ LITERAL clause_FirstConstraintLit(CLAUSE Clause)
{
  return Clause->literals[0];
}

static __inline__ LITERAL clause_FirstAntecedentLit(CLAUSE Clause)
{
  return Clause->literals[clause_FirstAntecedentLitIndex(Clause)];
}

static __inline__ LITERAL clause_FirstSuccedentLit(CLAUSE Clause)
{
  return Clause->literals[clause_FirstSuccedentLitIndex(Clause)];
}

static __inline__ LITERAL clause_LastConstraintLit(CLAUSE Clause)
{
  return Clause->literals[clause_LastConstraintLitIndex(Clause)];
}

static __inline__ LITERAL clause_LastAntecedentLit(CLAUSE Clause)
{
  return Clause->literals[clause_LastAntecedentLitIndex(Clause)];
}

static __inline__ LITERAL clause_LastSuccedentLit(CLAUSE Clause)
{
  return Clause->literals[clause_LastSuccedentLitIndex(Clause)];
}


static __inline__ BOOL clause_HasEmptyConstraint(CLAUSE Clause)
{
  return clause_NumOfConsLits(Clause) == 0;
}

static __inline__ BOOL clause_HasEmptyAntecedent(CLAUSE Clause)
{
  return clause_NumOfAnteLits(Clause) == 0;
}

static __inline__ BOOL clause_HasEmptySuccedent(CLAUSE Clause)
{
  return clause_NumOfSuccLits(Clause) == 0;
}


static __inline__ BOOL clause_IsGround(CLAUSE Clause)
{
#ifdef CHECK
  if (!symbol_Equal(clause_MaxVar(Clause), clause_SearchMaxVar(Clause))) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In clause_IsGround: Clause is corrupted.");
    misc_FinishErrorReport();
  }
#endif
  return (symbol_VarIndex(clause_MaxVar(Clause)) ==
	  symbol_GetInitialStandardVarCounter());
}

static __inline__ BOOL clause_IsEmptyClause(CLAUSE C)
{
  return (C != (CLAUSE)NULL &&
	  clause_HasEmptyAntecedent(C) &&
	  clause_HasEmptySuccedent(C)  &&
	  clause_HasEmptyConstraint(C));
}

static __inline__ int clause_LiteralGetIndex(LITERAL L)
{
  int j = 0;

  while (clause_GetLiteral(clause_LiteralOwningClause(L), j) != L)
    j++;

  return j;
}

static __inline__ BOOL clause_LiteralIsFromConstraint(LITERAL Literal)
{
  int    index  = clause_LiteralGetIndex(Literal);
  CLAUSE clause = clause_LiteralOwningClause(Literal);

  return (index <= clause_LastConstraintLitIndex(clause) &&
	  index >= clause_FirstConstraintLitIndex(clause));
}

static __inline__ BOOL clause_LiteralIsFromAntecedent(LITERAL Literal)
{
  int    index  = clause_LiteralGetIndex(Literal);
  CLAUSE clause = clause_LiteralOwningClause(Literal);

  return (index <= clause_LastAntecedentLitIndex(clause) &&
	  index >= clause_FirstAntecedentLitIndex(clause));
}

static __inline__ BOOL clause_LiteralIsFromSuccedent(LITERAL Literal)
{
   int    index;
   CLAUSE clause;
   index  = clause_LiteralGetIndex(Literal);
   clause = clause_LiteralOwningClause(Literal);
   return (index <= clause_LastSuccedentLitIndex(clause) &&
	   index >= clause_FirstSuccedentLitIndex(clause));
}

static __inline__ BOOL clause_IsSimpleSortClause(CLAUSE Clause)
{
  return (clause_HasEmptyAntecedent(Clause) &&
	  (clause_NumOfSuccLits(Clause) == 1) &&
	  clause_LiteralIsSort(clause_GetLiteral(Clause,
				clause_NumOfConsLits(Clause))) &&
	  clause_HasSolvedConstraint(Clause));
}

static __inline__ BOOL clause_IsSubsortClause(CLAUSE Clause)
{
  return (clause_IsSimpleSortClause(Clause) &&
	  term_IsVariable(term_FirstArgument(
            clause_LiteralSignedAtom(
	      clause_GetLiteral(Clause, clause_NumOfConsLits(Clause))))));
}


static __inline__ BOOL clause_HasSuccLits(CLAUSE Clause)
{
  return (clause_NumOfSuccLits(Clause) > 1);
}

static __inline__ BOOL clause_HasGroundSuccLit(CLAUSE Clause)
{
  int  i, l;

  l = clause_Length(Clause);
  for (i = clause_FirstSuccedentLitIndex(Clause); i < l; i++)
    if (term_IsGround(Clause->literals[i]->atomWithSign))
      return TRUE;
  
  return FALSE;
}

static __inline__ LITERAL clause_GetGroundSuccLit(CLAUSE Clause)
{
  int  i, l;

  l = clause_Length(Clause);
  for (i = clause_FirstSuccedentLitIndex(Clause); i < l; i++)
    if (term_IsGround(Clause->literals[i]->atomWithSign))
      return Clause->literals[i];

  return (LITERAL)NULL;
}


static __inline__ void clause_Free(CLAUSE Clause)
{
  memory_Free(Clause, sizeof(CLAUSE_NODE));
}


static __inline__ void clause_ReInit(CLAUSE Clause,
				     FLAGSTORE Flags,
				     PRECEDENCE Precedence)
{
  clause_Normalize(Clause);
  clause_SetMaxLitFlags(Clause, Flags, Precedence);
  clause_UpdateWeight(Clause, Flags);
  clause_UpdateMaxVar(Clause);
}

static __inline__ void clause_OrientAndReInit(CLAUSE Clause, FLAGSTORE Flags,
					      PRECEDENCE Precedence)
{
  clause_OrientEqualities(Clause, Flags, Precedence);
  clause_ReInit(Clause, Flags, Precedence);
}

static __inline__ void clause_SetDataFromFather(CLAUSE Result, CLAUSE Father,
						int i, FLAGSTORE Flags,
						PRECEDENCE Precedence)
{
  clause_OrientAndReInit(Result, Flags, Precedence);
  clause_SetSplitDataFromFather(Result, Father);
  clause_SetDepth(Result, clause_Depth(Father) + 1);
  clause_AddParentClause(Result, clause_Number(Father));
  clause_AddParentLiteral(Result, i);
}


static __inline__ void clause_SetDataFromParents(CLAUSE Result, CLAUSE Father,
						 int i, CLAUSE Mother, int j,
						 FLAGSTORE Flags,
						 PRECEDENCE Precedence)
{
  clause_OrientAndReInit(Result, Flags, Precedence);
  clause_SetSplitDataFromParents(Result, Father, Mother);
  clause_SetDepth(Result,
		  misc_Max(clause_Depth(Father), clause_Depth(Mother)) +1);
  clause_AddParentClause(Result, clause_Number(Father));
  clause_AddParentLiteral(Result, i);
  clause_AddParentClause(Result, clause_Number(Mother));
  clause_AddParentLiteral(Result, j);
}


#endif