diff options
Diffstat (limited to 'test/spass/clause.h')
| -rw-r--r-- | test/spass/clause.h | 1589 |
1 files changed, 1589 insertions, 0 deletions
diff --git a/test/spass/clause.h b/test/spass/clause.h new file mode 100644 index 0000000..d163d35 --- /dev/null +++ b/test/spass/clause.h @@ -0,0 +1,1589 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * 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 + |