| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * 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$ * */ |
| /* $State$ * */ |
| /* $Date$ * */ |
| /* $Author$ * */ |
| /* * * */ |
| /* * Contact: * */ |
| /* * Christoph Weidenbach * */ |
| /* * MPI fuer Informatik * */ |
| /* * Stuhlsatzenhausweg 85 * */ |
| /* * 66123 Saarbruecken * */ |
| /* * Email: weidenb@mpi-sb.mpg.de * */ |
| /* * Germany * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| /* $RCSfile$ */ |
| |
| #include "clause.h" |
| |
| /**************************************************************/ |
| /* Global variables and constants */ |
| /**************************************************************/ |
| |
| /* Means weight of literal or clause is undefined */ |
| const NAT clause_WEIGHTUNDEFINED = NAT_MAX; |
| |
| int clause_CLAUSECOUNTER; |
| NAT clause_STAMPID; |
| |
| /* The following array is used for bucket sort on clauses */ |
| #define clause_MAXWEIGHT 20 |
| LIST clause_SORT[clause_MAXWEIGHT+1]; |
| |
| /**************************************************************/ |
| /* Inline functions */ |
| /**************************************************************/ |
| |
| static __inline__ void clause_FreeLitArray(CLAUSE Clause) |
| { |
| NAT Length = clause_Length(Clause); |
| if (Length > 0) |
| memory_Free(Clause->literals, sizeof(LITERAL) * Length); |
| } |
| |
| |
| /**************************************************************/ |
| /* Primitive literal functions */ |
| /**************************************************************/ |
| |
| BOOL clause_LiteralIsLiteral(LITERAL Literal) |
| /********************************************************* |
| INPUT: A literal. |
| RETURNS: TRUE, if 'Literal' is not NULL and has a predicate |
| symbol as its atoms top symbol. |
| **********************************************************/ |
| { |
| return ((Literal != NULL) && |
| symbol_IsPredicate(clause_LiteralPredicate(Literal))); |
| } |
| |
| NAT clause_LiteralComputeWeight(LITERAL Literal, FLAGSTORE Flags) |
| /********************************************************* |
| INPUT: A literal and a flag store. |
| RETURNS: The weight of the literal. |
| CAUTION: This function does not update the weight of the literal! |
| **********************************************************/ |
| { |
| TERM Term; |
| int Bottom; |
| NAT Number; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralComputeWeight :"); |
| misc_ErrorReport("Illegal Input. Input not a literal."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Term = clause_LiteralSignedAtom(Literal); |
| Bottom = stack_Bottom(); |
| Number = 0; |
| |
| do { |
| if (term_IsComplex(Term)) { |
| Number += flag_GetFlagValue(Flags, flag_FUNCWEIGHT); |
| stack_Push(term_ArgumentList(Term)); |
| } |
| else |
| if (term_IsVariable(Term)) |
| Number += flag_GetFlagValue(Flags, flag_VARWEIGHT); |
| else |
| Number += flag_GetFlagValue(Flags, flag_FUNCWEIGHT); |
| |
| while (!stack_Empty(Bottom) && list_Empty(stack_Top())) |
| stack_Pop(); |
| if (!stack_Empty(Bottom)) { |
| Term = (TERM) list_Car(stack_Top()); |
| stack_RplacTop(list_Cdr(stack_Top())); |
| } |
| } while (!stack_Empty(Bottom)); |
| |
| return Number; |
| |
| } |
| |
| LITERAL clause_LiteralCreate(TERM Atom, CLAUSE Clause) |
| /********************************************************** |
| INPUT: A Pointer to a signed Predicate-Term and one to a |
| clause it shall belong to. |
| RETURNS: An appropriate literal where the other values |
| are set to default values. |
| MEMORY: A LITERAL_NODE is allocated. |
| CAUTION: The weight of the literal is not set correctly! |
| ***********************************************************/ |
| { |
| LITERAL Result; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Atom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralCreate:"); |
| misc_ErrorReport("\n Illegal input. Input not a term."); |
| misc_FinishErrorReport(); |
| } |
| if (!symbol_IsPredicate(term_TopSymbol(Atom)) && |
| (term_TopSymbol(Atom) != fol_Not())) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralCreate:"); |
| misc_ErrorReport("\n Illegal input. No predicate- or negated term."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE)); |
| |
| Result->atomWithSign = Atom; |
| Result->oriented = FALSE; |
| Result->weight = clause_WEIGHTUNDEFINED; |
| Result->maxLit = 0; |
| Result->owningClause = Clause; |
| |
| return Result; |
| } |
| |
| |
| LITERAL clause_LiteralCreateNegative(TERM Atom, CLAUSE Clause) |
| /********************************************************** |
| INPUT: A Pointer to a unsigned Predicate-Term and one to a |
| clause it shall belong to. |
| RETURNS: An appropriate literal where the other values |
| are set to default values and the term gets a sign. |
| MEMORY: A LITERAL_NODE is allocated. |
| CAUTION: The weight of the literal is not set correctly! |
| ***********************************************************/ |
| { |
| LITERAL Result; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Atom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralCreateNegative:"); |
| misc_ErrorReport("\n Illegal input. Input not an atom."); |
| misc_FinishErrorReport(); |
| } |
| if (!symbol_IsPredicate(term_TopSymbol(Atom)) && |
| (term_TopSymbol(Atom) != fol_Not())) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralCreateNegative:"); |
| misc_ErrorReport("\n Illegal input. Input term not normalized."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE)); |
| |
| term_RplacSupertermList(Atom, list_Nil()); |
| |
| Result->atomWithSign = term_Create(fol_Not(), list_List(Atom)); |
| Result->oriented = FALSE; |
| Result->maxLit = 0; |
| Result->weight = clause_WEIGHTUNDEFINED; |
| Result->owningClause = Clause; |
| |
| return Result; |
| } |
| |
| |
| void clause_LiteralDelete(LITERAL Literal) |
| /********************************************************* |
| INPUT: A literal, which has an unshared Atom. For Shared |
| literals clause_LiteralDeleteFromSharing(Lit) is |
| available. |
| RETURNS: Nothing. |
| MEMORY: The Atom of 'Literal' is deleted and its memory |
| is freed as well as the LITERAL_NODE. |
| **********************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralDelete:"); |
| misc_ErrorReport("\n Illegal input. Input not a literal."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_Delete(clause_LiteralSignedAtom(Literal)); |
| |
| clause_LiteralFree(Literal); |
| } |
| |
| |
| void clause_LiteralInsertIntoSharing(LITERAL Lit, SHARED_INDEX ShIndex) |
| /********************************************************** |
| INPUT: A Literal with an unshared Atom and an Index. |
| RETURNS: The literal with a shared Atom inserted into the |
| 'Index'. |
| MEMORY: Allocates TERM_NODE memory needed to insert 'Lit' |
| into the sharing and frees the memory of the |
| unshared Atom. |
| ***********************************************************/ |
| { |
| |
| TERM Atom; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Lit)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralInsertIntoSharing:"); |
| misc_ErrorReport("\n Illegal literal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Atom = clause_LiteralAtom(Lit); |
| |
| clause_LiteralSetAtom(Lit, sharing_Insert(Lit, Atom, ShIndex)); |
| |
| term_Delete(Atom); |
| } |
| |
| |
| void clause_LiteralDeleteFromSharing(LITERAL Lit, SHARED_INDEX ShIndex) |
| /********************************************************** |
| INPUT: A Literal and an 'Index'. |
| RETURNS: Nothing. |
| MEMORY: Deletes 'Lit' from Sharing, frees no more used |
| TERM memory and frees the LITERAL_NODE. |
| ********************************************************/ |
| { |
| |
| TERM Atom; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Lit)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralDeleteFromSharing:"); |
| misc_ErrorReport("\n Illegal literal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Atom = clause_LiteralAtom(Lit); |
| |
| if (clause_LiteralIsNegative(Lit)) { |
| list_Free(term_ArgumentList(clause_LiteralSignedAtom(Lit))); |
| term_Free(clause_LiteralSignedAtom(Lit)); |
| } |
| |
| sharing_Delete(Lit, Atom, ShIndex); |
| |
| clause_LiteralFree(Lit); |
| |
| } |
| |
| |
| static LIST clause_CopyLitInterval(CLAUSE Clause, int Start, int End) |
| /************************************************************** |
| INPUT: A clause and two integers representing |
| literal indices. |
| RETURNS: Copies of all literals in <Clause> with index i and |
| in the interval [Start:End] are prepended to <List>. |
| MEMORY: All atoms are copied. |
| ***************************************************************/ |
| { |
| TERM Atom; |
| LIST List; |
| |
| List = list_Nil(); |
| |
| for ( ; Start <= End; Start++) { |
| Atom = term_Copy(clause_GetLiteralAtom(Clause, Start)); |
| List = list_Cons(Atom, List); |
| } |
| |
| return List; |
| } |
| |
| |
| static LIST clause_CopyLitIntervalExcept(CLAUSE Clause, int Start, int End, |
| int i) |
| /************************************************************** |
| INPUT: A clause and three integers representing |
| literal indeces. |
| RETURNS: A list of atoms from literals within the interval |
| [Start:End] except the literal at index <i>. |
| MEMORY: All atoms are copied. |
| ***************************************************************/ |
| { |
| TERM Atom; |
| LIST Result; |
| |
| Result = list_Nil(); |
| for ( ; End >= Start; End--) |
| if (End != i) { |
| Atom = term_Copy(clause_GetLiteralAtom(Clause, End)); |
| Result = list_Cons(Atom, Result); |
| } |
| return Result; |
| } |
| |
| |
| LIST clause_CopyConstraint(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: The list of copied constraint literals from <Clause>. |
| ***************************************************************/ |
| { |
| return clause_CopyLitInterval(Clause, |
| clause_FirstConstraintLitIndex(Clause), |
| clause_LastConstraintLitIndex(Clause)); |
| } |
| |
| |
| LIST clause_CopyAntecedentExcept(CLAUSE Clause, int i) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: A list containing copies of all antecedent literals |
| except <i>. |
| ***************************************************************/ |
| { |
| return clause_CopyLitIntervalExcept(Clause, |
| clause_FirstAntecedentLitIndex(Clause), |
| clause_LastAntecedentLitIndex(Clause), |
| i); |
| } |
| |
| LIST clause_CopySuccedent(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: The list of copied succedent literals from <Clause>. |
| ***************************************************************/ |
| { |
| return clause_CopyLitInterval(Clause, |
| clause_FirstSuccedentLitIndex(Clause), |
| clause_LastSuccedentLitIndex(Clause)); |
| } |
| |
| |
| LIST clause_CopySuccedentExcept(CLAUSE Clause, int i) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: A list containing copies of all succedent literals |
| except <i>. |
| ***************************************************************/ |
| { |
| return clause_CopyLitIntervalExcept(Clause, |
| clause_FirstSuccedentLitIndex(Clause), |
| clause_LastSuccedentLitIndex(Clause), |
| i); |
| } |
| |
| |
| /**************************************************************/ |
| /* Specials */ |
| /**************************************************************/ |
| |
| BOOL clause_IsUnorderedClause(CLAUSE Clause) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: TRUE, if the invariants concerning splitting etc. hold |
| Invariants concerning maximality restrictions are not tested. |
| **********************************************************/ |
| { |
| return ((Clause != NULL) && |
| clause_CheckSplitLevel(Clause) && |
| (clause_IsEmptyClause(Clause) || |
| /* Check the first literal as a "random" sample */ |
| clause_LiteralIsLiteral(clause_GetLiteral(Clause,clause_FirstLitIndex()))) && |
| (clause_SplitLevel(Clause) == 0 || Clause->splitfield_length>0) && |
| clause_DependsOnSplitLevel(Clause,clause_SplitLevel(Clause))); |
| } |
| |
| |
| BOOL clause_IsClause(CLAUSE Clause, FLAGSTORE FlagStore, PRECEDENCE Precedence) |
| /********************************************************* |
| INPUT: A clause, a flag store and a precedence. |
| RETURNS: TRUE, if literals are correctly ordered and the |
| invariants concerning splitting etc. hold |
| **********************************************************/ |
| { |
| int i; |
| LITERAL ActLit; |
| |
| if (!clause_IsUnorderedClause(Clause)) |
| return FALSE; |
| |
| for (i=clause_FirstAntecedentLitIndex(Clause);i<=clause_LastSuccedentLitIndex(Clause);i++) { |
| ActLit = clause_GetLiteral(Clause,i); |
| if (fol_IsEquality(clause_LiteralSignedAtom(ActLit))) { |
| ord_RESULT HelpRes; |
| |
| HelpRes = |
| ord_Compare(term_FirstArgument(clause_LiteralSignedAtom(ActLit)), |
| term_SecondArgument(clause_LiteralSignedAtom(ActLit)), |
| FlagStore, Precedence); |
| |
| if (ord_IsSmallerThan(HelpRes)) |
| return FALSE; |
| } |
| } |
| |
| return TRUE; |
| } |
| |
| |
| BOOL clause_ContainsPositiveEquations(CLAUSE Clause) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: TRUE, if the clause contains a positive equality literal. |
| **********************************************************/ |
| { |
| int i; |
| |
| for (i = clause_FirstSuccedentLitIndex(Clause); |
| i < clause_Length(Clause); |
| i++) |
| if (clause_LiteralIsEquality(clause_GetLiteral(Clause, i))) |
| return TRUE; |
| |
| return FALSE; |
| } |
| |
| |
| BOOL clause_ContainsNegativeEquations(CLAUSE Clause) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: TRUE, if the clause contains a positive equality literal. |
| **********************************************************/ |
| { |
| int i; |
| |
| for (i = clause_FirstAntecedentLitIndex(Clause); |
| i < clause_FirstSuccedentLitIndex(Clause); |
| i++) |
| if (clause_LiteralIsEquality(clause_GetLiteral(Clause, i))) |
| return TRUE; |
| |
| return FALSE; |
| } |
| |
| |
| int clause_ContainsFolAtom(CLAUSE Clause, BOOL *Prop, BOOL *Grd, BOOL *Monadic, |
| BOOL *NonMonadic) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: The number of boolean variables changed. |
| If <*Prop> is FALSE and the clause contains a propositional |
| variable, it is changed to TRUE. |
| If <*Grd> is FALSE and the clause contains a non-propositional |
| ground atom, it is changed to TRUE. |
| If <*Monadic> is FALSE and the clause contains a monadic atom, |
| it is changed to TRUE. |
| If <*NonMonadic> is FALSE and the clause contains an at least |
| 2-place non-equality atom, it is changed to TRUE. |
| **********************************************************/ |
| { |
| int i,Result,Arity; |
| BOOL Ground; |
| |
| Result = 0; |
| i = clause_FirstLitIndex(); |
| |
| while (Result < 4 && |
| i < clause_Length(Clause) && |
| (!(*Prop) || !(*Monadic) || !(*NonMonadic))) { |
| Arity = symbol_Arity(term_TopSymbol(clause_GetLiteralAtom(Clause,i))); |
| Ground = term_IsGround(clause_GetLiteralAtom(Clause,i)); |
| if (!(*Prop) && Arity == 0) { |
| Result++; |
| *Prop = TRUE; |
| } |
| if (!(*Grd) && Arity > 0 && Ground && |
| !fol_IsEquality(clause_GetLiteralAtom(Clause,i))) { |
| Result++; |
| *Grd = TRUE; |
| } |
| if (!(*Monadic) && Arity == 1 && !Ground) { |
| Result++; |
| *Monadic = TRUE; |
| } |
| if (!(*NonMonadic) && Arity > 1 && !Ground && |
| !fol_IsEquality(clause_GetLiteralAtom(Clause,i))) { |
| Result++; |
| *NonMonadic = TRUE; |
| } |
| i++; |
| } |
| return Result; |
| } |
| |
| |
| BOOL clause_ContainsVariables(CLAUSE Clause) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: TRUE, if the clause contains at least one variable |
| **********************************************************/ |
| { |
| int i; |
| TERM Term; |
| |
| for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) { |
| Term = clause_GetLiteralAtom(Clause,i); |
| if (term_NumberOfVarOccs(Term)>0) |
| return TRUE; |
| } |
| |
| return FALSE; |
| } |
| |
| |
| void clause_ContainsSortRestriction(CLAUSE Clause, BOOL *Sortres, BOOL *USortres) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: TRUE, if the clause contains a negative monadic atom with |
| a variable argument |
| **********************************************************/ |
| { |
| int i; |
| TERM Term; |
| |
| for (i = clause_FirstLitIndex(); |
| i <= clause_LastAntecedentLitIndex(Clause) && (!*Sortres || !*USortres); |
| i++) { |
| Term = clause_GetLiteralAtom(Clause,i); |
| if (symbol_IsBaseSort(term_TopSymbol(Term))) { |
| *USortres = TRUE; |
| if (symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term)))) |
| *Sortres = TRUE; |
| } |
| } |
| } |
| |
| BOOL clause_ContainsFunctions(CLAUSE Clause) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: TRUE, if the clause contains at least one function symbol |
| **********************************************************/ |
| { |
| int i; |
| TERM Term; |
| |
| for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) { |
| Term = clause_GetLiteralAtom(Clause,i); |
| if (term_ContainsFunctions(Term)) |
| return TRUE; |
| } |
| |
| return FALSE; |
| } |
| |
| BOOL clause_ContainsSymbol(CLAUSE Clause, SYMBOL Symbol) |
| /********************************************************* |
| INPUT: A clause and a symbol. |
| RETURNS: TRUE, if the clause contains the symbol |
| **********************************************************/ |
| { |
| int i; |
| |
| for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) |
| if (term_ContainsSymbol(clause_GetLiteralAtom(Clause,i), Symbol)) |
| return TRUE; |
| return FALSE; |
| } |
| |
| NAT clause_NumberOfSymbolOccurrences(CLAUSE Clause, SYMBOL Symbol) |
| /********************************************************* |
| INPUT: A clause and a symbol. |
| RETURNS: the number of occurrences of <Symbol> in <Clause> |
| **********************************************************/ |
| { |
| int i; |
| NAT Result; |
| |
| Result = 0; |
| |
| for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) |
| Result += term_NumberOfSymbolOccurrences(clause_GetLiteralAtom(Clause,i), Symbol); |
| |
| return Result; |
| } |
| |
| BOOL clause_ImpliesFiniteDomain(CLAUSE Clause) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: TRUE, if the clause consists of a positive disjunction |
| of equations, where each equation is of the form "x=t" for |
| some variable "x" and ground term "t" |
| **********************************************************/ |
| { |
| int i; |
| TERM Term; |
| |
| if (clause_FirstLitIndex() != clause_FirstSuccedentLitIndex(Clause)) |
| return FALSE; |
| |
| for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) { |
| Term = clause_GetLiteralTerm(Clause,i); |
| if (!symbol_Equal(term_TopSymbol(Term),fol_Equality()) || |
| (!symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term))) && |
| !symbol_IsVariable(term_TopSymbol(term_SecondArgument(Term)))) || |
| (symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term))) && |
| !term_IsGround(term_SecondArgument(Term))) || |
| (symbol_IsVariable(term_TopSymbol(term_SecondArgument(Term))) && |
| !term_IsGround(term_FirstArgument(Term)))) |
| return FALSE; |
| } |
| |
| return TRUE; |
| } |
| |
| BOOL clause_ImpliesNonTrivialDomain(CLAUSE Clause) |
| /********************************************************* |
| INPUT: A clause. |
| RETURNS: TRUE, if the clause consists of a negative equation |
| with two syntactically different arguments |
| **********************************************************/ |
| { |
| if (clause_Length(Clause) == 1 && |
| !clause_HasEmptyAntecedent(Clause) && |
| clause_LiteralIsEquality(clause_FirstAntecedentLit(Clause)) && |
| !term_Equal(term_FirstArgument(clause_LiteralAtom(clause_FirstAntecedentLit(Clause))), |
| term_SecondArgument(clause_LiteralAtom(clause_FirstAntecedentLit(Clause))))) |
| return TRUE; |
| |
| return FALSE; |
| } |
| |
| LIST clause_FiniteMonadicPredicates(LIST Clauses) |
| /********************************************************* |
| INPUT: A list of clauses. |
| RETURNS: A list of all predicate symbols that are guaranteed |
| to have a finite extension in any minimal Herbrand model. |
| These predicates must only positively occur |
| in unit clauses and must have a ground term argument. |
| **********************************************************/ |
| { |
| LIST Result, NonFinite, Scan; |
| CLAUSE Clause; |
| int i, n; |
| SYMBOL Pred; |
| |
| Result = list_Nil(); |
| NonFinite = list_Nil(); |
| |
| for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| Clause = (CLAUSE)list_Car(Scan); |
| n = clause_Length(Clause); |
| for (i=clause_FirstSuccedentLitIndex(Clause);i<n;i++) { |
| Pred = term_TopSymbol(clause_GetLiteralAtom(Clause,i)); |
| if (symbol_Arity(Pred) == 1 && |
| !list_PointerMember(NonFinite, (POINTER)Pred)) { |
| if (term_NumberOfVarOccs(clause_GetLiteralAtom(Clause,i)) > 0 || |
| n > 1) { |
| NonFinite = list_Cons((POINTER)Pred, NonFinite); |
| Result = list_PointerDeleteElement(Result, (POINTER)Pred); |
| } |
| else { |
| if (!list_PointerMember(Result, (POINTER)Pred)) |
| Result = list_Cons((POINTER)Pred, Result); |
| } |
| } |
| } |
| } |
| list_Delete(NonFinite); |
| |
| Result = list_PointerDeleteElement(Result, (POINTER)fol_Equality()); |
| |
| return Result; |
| } |
| |
| NAT clause_NumberOfVarOccs(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause. |
| RETURNS: The number of variable occurrences in the clause. |
| ***************************************************************/ |
| { |
| int i,n; |
| NAT Result; |
| |
| Result = 0; |
| n = clause_Length(Clause); |
| |
| for (i = clause_FirstLitIndex(); i < n; i++) |
| Result += term_NumberOfVarOccs(clause_GetLiteralTerm(Clause,i)); |
| |
| return Result; |
| } |
| |
| |
| NAT clause_ComputeWeight(CLAUSE Clause, FLAGSTORE Flags) |
| /************************************************************** |
| INPUT: A clause and a flag store. |
| RETURNS: The Weight of the literals in the clause, |
| up to now the number of variable symbols plus |
| twice the number of signature symbols. |
| EFFECT: The weight of the literals is updated, but not the |
| weight of the clause! |
| ***************************************************************/ |
| { |
| int i, n; |
| NAT Weight; |
| LITERAL Lit; |
| |
| Weight = 0; |
| n = clause_Length(Clause); |
| |
| for (i = clause_FirstLitIndex(); i < n; i++) { |
| Lit = clause_GetLiteral(Clause, i); |
| clause_UpdateLiteralWeight(Lit, Flags); |
| Weight += clause_LiteralWeight(Lit); |
| } |
| return Weight; |
| } |
| |
| |
| NAT clause_ComputeTermDepth(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause. |
| RETURNS: Maximal depth of a literal in <Clause>. |
| ***************************************************************/ |
| { |
| int i,n; |
| NAT Depth,Help; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_ComputeTermDepth:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Depth = 0; |
| n = clause_Length(Clause); |
| |
| for (i = clause_FirstLitIndex();i < n;i++) { |
| Help = term_Depth(clause_GetLiteralAtom(Clause,i)); |
| if (Help > Depth) |
| Depth = Help; |
| } |
| return Depth; |
| } |
| |
| NAT clause_MaxTermDepthClauseList(LIST Clauses) |
| /************************************************************** |
| INPUT: A list of clauses. |
| RETURNS: Maximal depth of a clause in <Clauses>. |
| ***************************************************************/ |
| { |
| NAT Depth,Help; |
| |
| Depth = 0; |
| |
| while (!list_Empty(Clauses)) { |
| Help = clause_ComputeTermDepth(list_Car(Clauses)); |
| if (Help > Depth) |
| Depth = Help; |
| Clauses = list_Cdr(Clauses); |
| } |
| |
| return Depth; |
| } |
| |
| |
| NAT clause_ComputeSize(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause. |
| RETURNS: The Size of the literals in the clause, |
| up to now the number of symbols. |
| ***************************************************************/ |
| { |
| int i,n; |
| NAT Size; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_ComputeSize:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Size = 0; |
| n = clause_Length(Clause); |
| |
| for (i = clause_FirstLitIndex();i < n;i++) |
| Size += term_ComputeSize(clause_GetLiteralTerm(Clause,i)); |
| |
| return Size; |
| } |
| |
| |
| BOOL clause_WeightCorrect(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence) |
| /********************************************************* |
| INPUT: A clause, a flag store and a precedence. |
| RETURNS: TRUE iff the weight fields of the clause and its |
| literals are correct. |
| **********************************************************/ |
| { |
| int i, n; |
| NAT Weight, Help; |
| LITERAL Lit; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_WeightCorrect:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Weight = 0; |
| n = clause_Length(Clause); |
| |
| for (i = clause_FirstLitIndex(); i < n; i++) { |
| Lit = clause_GetLiteral(Clause, i); |
| Help = clause_LiteralComputeWeight(Lit, Flags); |
| if (Help != clause_LiteralWeight(Lit)) |
| return FALSE; |
| Weight += Help; |
| } |
| |
| return (clause_Weight(Clause) == Weight); |
| } |
| |
| |
| LIST clause_InsertWeighed(CLAUSE Clause, LIST UsList, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /********************************************************* |
| INPUT: A clause, a list to insert the clause into, |
| a flag store and a precedence. |
| RETURNS: The list where the clause is inserted wrt its |
| weight (Weight(Car(list)) <= Weight(Car(Cdr(list)))). |
| MEMORY: A new listnode is allocated. |
| **********************************************************/ |
| { |
| LIST Scan; |
| NAT Weight; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_InsertWeighted:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Weight = clause_Weight(Clause); |
| |
| Scan = UsList; |
| |
| if (list_Empty(Scan) || |
| (clause_Weight(list_Car(Scan)) > Weight)) { |
| return list_Cons(Clause, Scan); |
| |
| } else { |
| while (!list_Empty(list_Cdr(Scan)) && |
| (clause_Weight(list_Car(list_Cdr(Scan))) <= Weight)) { |
| Scan = list_Cdr(Scan); |
| } |
| list_Rplacd(Scan, list_Cons(Clause, list_Cdr(Scan))); |
| return UsList; |
| } |
| } |
| |
| |
| LIST clause_ListSortWeighed(LIST Clauses) |
| /********************************************************* |
| INPUT: A list of clauses. |
| RETURNS: The clause list sorted with respect to the weight |
| of clauses, minimal weight first. |
| EFFECT: The original list is destructively changed! |
| This function doesn't sort stable! |
| The function uses bucket sort for clauses with weight |
| smaller than clause_MAXWEIGHT, and the usual list sort |
| function for clauses with weight >= clause_MAXWEIGHT. |
| This implies the function uses time O(n-c + c*log c), |
| where n is the length of the list and c is the number |
| of clauses with weight >= clause_MAXWEIGHT. |
| For c=0 you get time O(n), for c=n you get time (n*log n). |
| **********************************************************/ |
| { |
| int weight; |
| LIST Scan; |
| |
| for (Scan=Clauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) { |
| weight = clause_Weight(list_Car(Scan)); |
| if (weight < clause_MAXWEIGHT) |
| clause_SORT[weight] = list_Cons(list_Car(Scan),clause_SORT[weight]); |
| else |
| clause_SORT[clause_MAXWEIGHT] = list_Cons(list_Car(Scan),clause_SORT[clause_MAXWEIGHT]); |
| } |
| Scan = list_NumberSort(clause_SORT[clause_MAXWEIGHT], |
| (NAT (*)(POINTER)) clause_Weight); |
| clause_SORT[clause_MAXWEIGHT] = list_Nil(); |
| for (weight = clause_MAXWEIGHT-1; weight >= 0; weight--) { |
| Scan = list_Nconc(clause_SORT[weight],Scan); |
| clause_SORT[weight] = list_Nil(); |
| } |
| list_Delete(Clauses); |
| return Scan; |
| } |
| |
| |
| LITERAL clause_LiteralCopy(LITERAL Literal) |
| /********************************************************* |
| INPUT: A literal. |
| RETURNS: An unshared copy of the literal, where the owning |
| clause-slot is set to NULL. |
| MEMORY: Memory for a new LITERAL_NODE and all its TERMs |
| subterms is allocated. |
| **********************************************************/ |
| { |
| |
| LITERAL Result; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralCopy:"); |
| misc_ErrorReport("\n Illegal input. Input not a literal."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE)); |
| |
| Result->atomWithSign = term_Copy(clause_LiteralSignedAtom(Literal)); |
| Result->oriented = clause_LiteralIsOrientedEquality(Literal); |
| |
| Result->maxLit = Literal->maxLit; |
| Result->weight = Literal->weight; |
| Result->owningClause = (POINTER)NULL; |
| |
| return Result; |
| } |
| |
| |
| CLAUSE clause_Copy(CLAUSE Clause) |
| /********************************************************* |
| INPUT: A Clause. |
| RETURNS: An unshared copy of the Clause. |
| MEMORY: Memory for a new CLAUSE_NODE, LITERAL_NODE and |
| all its TERMs subterms is allocated. |
| **********************************************************/ |
| { |
| |
| CLAUSE Result; |
| int i,c,a,s,l; |
| |
| Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE)); |
| |
| Result->clausenumber = clause_Number(Clause); |
| Result->maxVar = clause_MaxVar(Clause); |
| Result->flags = Clause->flags; |
| clause_InitSplitData(Result); |
| Result->validlevel = clause_SplitLevel(Clause); |
| clause_SetSplitField(Result, Clause->splitfield, Clause->splitfield_length); |
| Result->depth = clause_Depth(Clause); |
| Result->weight = Clause->weight; |
| Result->parentCls = list_Copy(clause_ParentClauses(Clause)); |
| Result->parentLits = list_Copy(clause_ParentLiterals(Clause)); |
| Result->origin = clause_Origin(Clause); |
| |
| Result->c = (c = clause_NumOfConsLits(Clause)); |
| Result->a = (a = clause_NumOfAnteLits(Clause)); |
| Result->s = (s = clause_NumOfSuccLits(Clause)); |
| |
| l = c + a + s; |
| if (l != 0) |
| Result->literals = (LITERAL *)memory_Malloc(l * sizeof(LITERAL)); |
| |
| for (i = 0; i < l; i++) { |
| clause_SetLiteral(Result, i, |
| clause_LiteralCopy(clause_GetLiteral(Clause, i))); |
| clause_LiteralSetOwningClause((Result->literals[i]), Result); |
| } |
| |
| return Result; |
| } |
| |
| |
| SYMBOL clause_LiteralMaxVar(LITERAL Literal) |
| /********************************************************* |
| INPUT: A literal. |
| RETURNS: The maximal symbol of the literals variables, |
| if the literal is ground, symbol_GetInitialStandardVarCounter(). |
| **********************************************************/ |
| { |
| |
| TERM Term; |
| int Bottom; |
| SYMBOL MaxSym,Help; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralMaxVar:"); |
| misc_ErrorReport("\n Illegal input. Input not a literal."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Bottom = stack_Bottom(); |
| MaxSym = symbol_GetInitialStandardVarCounter(); |
| Term = clause_LiteralAtom(Literal); |
| |
| do { |
| if (term_IsComplex(Term)) |
| stack_Push(term_ArgumentList(Term)); |
| else |
| if (term_IsVariable(Term)) |
| MaxSym = ((MaxSym < (Help = term_TopSymbol(Term))) ? |
| Help : MaxSym); |
| while (!stack_Empty(Bottom) && list_Empty(stack_Top())) |
| stack_Pop(); |
| if (!stack_Empty(Bottom)) { |
| Term = (TERM) list_Car(stack_Top()); |
| stack_RplacTop(list_Cdr(stack_Top())); |
| } |
| } while (!stack_Empty(Bottom)); |
| |
| return MaxSym; |
| } |
| |
| |
| SYMBOL clause_AtomMaxVar(TERM Term) |
| /********************************************************* |
| INPUT: A term. |
| RETURNS: The maximal symbol of the lcontained variables, |
| if <Term> is ground, symbol_GetInitialStandardVarCounter(). |
| **********************************************************/ |
| { |
| int Bottom; |
| SYMBOL VarSym,Help; |
| |
| Bottom = stack_Bottom(); |
| VarSym = symbol_GetInitialStandardVarCounter(); |
| |
| do { |
| if (term_IsComplex(Term)) |
| stack_Push(term_ArgumentList(Term)); |
| else |
| if (term_IsVariable(Term)) |
| VarSym = ((VarSym < (Help = term_TopSymbol(Term))) ? |
| Help : VarSym); |
| while (!stack_Empty(Bottom) && list_Empty(stack_Top())) |
| stack_Pop(); |
| if (!stack_Empty(Bottom)) { |
| Term = (TERM)list_Car(stack_Top()); |
| stack_RplacTop(list_Cdr(stack_Top())); |
| } |
| } while (!stack_Empty(Bottom)); |
| |
| return VarSym; |
| } |
| |
| |
| void clause_SetMaxLitFlags(CLAUSE Clause, FLAGSTORE FlagStore, |
| PRECEDENCE Precedence) |
| /********************************************************** |
| INPUT: A clause, a flag store and a precedence. |
| RETURNS: Nothing. |
| EFFECT: Sets the maxLit-flag for maximal literals. |
| ***********************************************************/ |
| { |
| int i,j,n,fa; |
| LITERAL ActLit,CompareLit; |
| BOOL Result, Twin; |
| ord_RESULT HelpRes; |
| |
| n = clause_Length(Clause); |
| fa = clause_FirstAntecedentLitIndex(Clause); |
| clause_RemoveFlag(Clause,CLAUSESELECT); |
| for (i = clause_FirstLitIndex(); i < n; i++) |
| clause_LiteralFlagReset(clause_GetLiteral(Clause, i)); |
| if (term_StampOverflow(clause_STAMPID)) |
| for (i = clause_FirstLitIndex(); i < n; i++) |
| term_ResetTermStamp(clause_LiteralSignedAtom(clause_GetLiteral(Clause, i))); |
| term_StartStamp(); |
| |
| /*printf("\n Start: "); clause_Print(Clause);*/ |
| |
| for (i = fa; i < n; i++) { |
| ActLit = clause_GetLiteral(Clause, i); |
| if (!term_HasTermStamp(clause_LiteralSignedAtom(ActLit))) { |
| Result = TRUE; |
| Twin = FALSE; |
| for (j = fa; j < n && Result; j++) |
| if (i != j) { |
| CompareLit = clause_GetLiteral(Clause, j); |
| HelpRes = ord_LiteralCompare(clause_LiteralSignedAtom(ActLit), |
| clause_LiteralIsOrientedEquality(ActLit), |
| clause_LiteralSignedAtom(CompareLit), |
| clause_LiteralIsOrientedEquality(CompareLit), |
| FALSE, FlagStore, Precedence); |
| |
| /*printf("\n\tWe compare: "); |
| fol_PrintDFG(clause_LiteralAtom(ActLit)); |
| putchar(' '); |
| fol_PrintDFG(clause_LiteralAtom(CompareLit)); |
| printf(" Result: "); ord_Print(HelpRes);*/ |
| |
| if (ord_IsEqual(HelpRes)) |
| Twin = TRUE; |
| if (ord_IsSmallerThan(HelpRes)) |
| Result = FALSE; |
| if (ord_IsGreaterThan(HelpRes)) |
| term_SetTermStamp(clause_LiteralSignedAtom(CompareLit)); |
| } |
| if (Result) { |
| clause_LiteralSetFlag(ActLit, MAXIMAL); |
| if (!Twin) |
| clause_LiteralSetFlag(ActLit, STRICTMAXIMAL); |
| } |
| } |
| } |
| term_StopStamp(); |
| /*printf("\n End: "); clause_Print(Clause);*/ |
| } |
| |
| |
| SYMBOL clause_SearchMaxVar(CLAUSE Clause) |
| /********************************************************** |
| INPUT: A clause. |
| RETURNS: The maximal symbol of the clauses variables. |
| If the clause is ground, symbol_GetInitialStandardVarCounter(). |
| ***********************************************************/ |
| { |
| int i, n; |
| SYMBOL Help, MaxSym; |
| |
| n = clause_Length(Clause); |
| |
| MaxSym = symbol_GetInitialStandardVarCounter(); |
| |
| for (i = 0; i < n; i++) { |
| Help = clause_LiteralMaxVar(clause_GetLiteral(Clause, i)); |
| if (Help > MaxSym) |
| MaxSym = Help; |
| } |
| return MaxSym; |
| } |
| |
| |
| void clause_RenameVarsBiggerThan(CLAUSE Clause, SYMBOL MinVar) |
| /********************************************************** |
| INPUT: A clause and a variable symbol. |
| RETURNS: The clause with variables renamed in a way, that |
| all vars are (excl.) bigger than MinVar. |
| ***********************************************************/ |
| { |
| int i,n; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_RenameVarsBiggerThan:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (MinVar != symbol_GetInitialStandardVarCounter()) { |
| n = clause_Length(Clause); |
| |
| term_StartMaxRenaming(MinVar); |
| |
| for (i = clause_FirstLitIndex(); i < n; i++) |
| term_Rename(clause_GetLiteralTerm(Clause, i)); |
| } |
| } |
| |
| void clause_Normalize(CLAUSE Clause) |
| /********************************************************** |
| INPUT: A clause. |
| RETURNS: The term with normalized Variables, DESTRUCTIVE |
| on the variable subterms' topsymbols. |
| ***********************************************************/ |
| { |
| int i,n; |
| |
| n = clause_Length(Clause); |
| |
| term_StartMinRenaming(); |
| |
| for (i = clause_FirstLitIndex(); i < n; i++) |
| term_Rename(clause_GetLiteralTerm(Clause, i)); |
| } |
| |
| |
| void clause_SubstApply(SUBST Subst, CLAUSE Clause) |
| /********************************************************** |
| INPUT: A clause. |
| RETURNS: Nothing. |
| EFFECTS: Applies the substitution to the clause. |
| ***********************************************************/ |
| { |
| int i,n; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_SubstApply:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| n = clause_Length(Clause); |
| |
| for (i=clause_FirstLitIndex(); i<n; i++) |
| clause_LiteralSetAtom(clause_GetLiteral(Clause, i), |
| subst_Apply(Subst,clause_GetLiteralAtom(Clause,i))); |
| } |
| |
| |
| void clause_ReplaceVariable(CLAUSE Clause, SYMBOL Var, TERM Term) |
| /********************************************************** |
| INPUT: A clause, a variable symbol, and a term. |
| RETURNS: Nothing. |
| EFFECTS: All occurences of the variable <Var> in <Clause> |
| are replaced by copies if <Term>. |
| CAUTION: The maximum variable of the clause is not updated! |
| ***********************************************************/ |
| { |
| int i, li; |
| |
| #ifdef CHECK |
| if (!symbol_IsVariable(Var)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_ReplaceVariable: symbol is not a variable"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| li = clause_LastLitIndex(Clause); |
| for (i = clause_FirstLitIndex(); i <= li; i++) |
| term_ReplaceVariable(clause_GetLiteralAtom(Clause,i), Var, Term); |
| } |
| |
| |
| void clause_UpdateMaxVar(CLAUSE Clause) |
| /********************************************************** |
| INPUT: A clause. |
| RETURNS: Nothing. |
| EFFECTS: Actualizes the MaxVar slot wrt the actual literals. |
| ***********************************************************/ |
| { |
| clause_SetMaxVar(Clause, clause_SearchMaxVar(Clause)); |
| } |
| |
| |
| |
| void clause_OrientEqualities(CLAUSE Clause, FLAGSTORE FlagStore, |
| PRECEDENCE Precedence) |
| /********************************************************** |
| INPUT: An unshared clause, a flag store and a precedence. |
| RETURNS: Nothing. |
| EFFECTS: Reorders the arguments of equality literals |
| wrt. the ordering. Thus first arguments aren't smaller |
| after the application. |
| ***********************************************************/ |
| { |
| int i,length; |
| LITERAL EqLit; |
| ord_RESULT HelpRes; |
| |
| /*printf("\n Clause: ");clause_Print(Clause);*/ |
| |
| length = clause_Length(Clause); |
| |
| for (i = clause_FirstLitIndex(); i < length; i++) { |
| EqLit = clause_GetLiteral(Clause, i); |
| |
| if (clause_LiteralIsEquality(EqLit)) { |
| HelpRes = ord_Compare(term_FirstArgument(clause_LiteralAtom(EqLit)), |
| term_SecondArgument(clause_LiteralAtom(EqLit)), |
| FlagStore, Precedence); |
| |
| /*printf("\n\tWe compare: "); |
| fol_PrintDFG(term_FirstArgument(clause_LiteralAtom(EqLit))); |
| putchar(' '); |
| fol_PrintDFG(term_SecondArgument(clause_LiteralAtom(EqLit))); |
| printf("\nResult: "); ord_Print(HelpRes);*/ |
| |
| switch(HelpRes) { |
| |
| case ord_SMALLER_THAN: |
| /* printf("\nSwapping: "); |
| term_Print(clause_LiteralAtom(EqLit)); DBG */ |
| term_EqualitySwap(clause_LiteralAtom(EqLit)); |
| clause_LiteralSetOrientedEquality(EqLit); |
| /* Swapped = TRUE; */ |
| break; |
| case ord_GREATER_THAN: |
| clause_LiteralSetOrientedEquality(EqLit); |
| break; |
| default: |
| clause_LiteralSetNoOrientedEquality(EqLit); |
| break; |
| } |
| } |
| else |
| clause_LiteralSetNoOrientedEquality(EqLit); |
| } |
| } |
| |
| |
| void clause_InsertFlatIntoIndex(CLAUSE Clause, st_INDEX Index) |
| /********************************************************** |
| INPUT: An unshared clause and an index. |
| EFFECT: The atoms of <Clause> are inserted into the index. |
| A link from the atom to its literal via the supertermlist |
| is established. |
| ***********************************************************/ |
| { |
| int i,n; |
| LITERAL Lit; |
| TERM Atom ; |
| |
| n = clause_Length(Clause); |
| |
| for (i=clause_FirstLitIndex();i<n;i++) { |
| Lit = clause_GetLiteral(Clause,i); |
| Atom = clause_LiteralAtom(Lit); |
| term_RplacSupertermList(Atom, list_List(Lit)); |
| st_EntryCreate(Index, Atom, Atom, cont_LeftContext()); |
| } |
| } |
| |
| void clause_DeleteFlatFromIndex(CLAUSE Clause, st_INDEX Index) |
| /********************************************************** |
| INPUT: An unshared clause and an index. |
| EFFECT: The clause is deleted from the index and deleted itself. |
| ***********************************************************/ |
| { |
| int i,n; |
| LITERAL Lit; |
| TERM Atom ; |
| |
| n = clause_Length(Clause); |
| |
| for (i=clause_FirstLitIndex();i<n;i++) { |
| Lit = clause_GetLiteral(Clause,i); |
| Atom = clause_LiteralAtom(Lit); |
| list_Delete(term_SupertermList(Atom)); |
| term_RplacSupertermList(Atom, list_Nil()); |
| st_EntryDelete(Index, Atom, Atom, cont_LeftContext()); |
| } |
| clause_Delete(Clause); |
| } |
| |
| |
| void clause_DeleteClauseListFlatFromIndex(LIST Clauses, st_INDEX Index) |
| /********************************************************** |
| INPUT: An list of unshared clause and an index. |
| EFFECT: The clauses are deleted from the index and deleted itself. |
| The list is deleted. |
| ***********************************************************/ |
| { |
| LIST Scan; |
| |
| for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| clause_DeleteFlatFromIndex(list_Car(Scan), Index); |
| |
| list_Delete(Clauses); |
| } |
| |
| |
| /******************************************************************/ |
| /* Some special functions used by hyper inference/reduction rules */ |
| /******************************************************************/ |
| |
| static void clause_VarToSizeMap(SUBST Subst, NAT* Map, NAT MaxIndex) |
| /************************************************************** |
| INPUT: A substitution, an array <Map> of size <MaxIndex>+1. |
| RETURNS: Nothing. |
| EFFECT: The index i within the array corresponds to the index |
| of a variable x_i. For each variable x_i, 0<=i<=MaxIndex |
| the size of its substitution term is calculated |
| and written to Map[i]. |
| ***************************************************************/ |
| { |
| NAT *Scan; |
| |
| #ifdef CHECK |
| if (subst_Empty(Subst) || Map == NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_VarToSizeMap: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| /* Initialization */ |
| for (Scan = Map + MaxIndex; Scan >= Map; Scan--) |
| *Scan = 1; |
| /* Compute the size of substitution terms */ |
| for ( ; !subst_Empty(Subst); Subst = subst_Next(Subst)) |
| Map[subst_Dom(Subst)] = term_ComputeSize(subst_Cod(Subst)); |
| } |
| |
| |
| static NAT clause_ComputeTermSize(TERM Term, NAT* VarMap) |
| /************************************************************** |
| INPUT: A term and a an array of NATs. |
| RETURNS: The number of symbols in the term. |
| EFFECT: This function calculates the number of symbols in <Term> |
| with respect to some substitution s. |
| A naive way to do this is to apply the substitution |
| to a copy of the term, and to count the number of symbols |
| in the copied term. |
| We use a more sophisticated algorithm, that first stores |
| the size of every variable's substitution term in <VarMap>. |
| We then 'scan' the term and for a variable occurrence x_i |
| we simply add the corresponding value VarMap[i] to the result. |
| This way we avoid copying the term and the substitution terms, |
| which is especially useful if we reuse the VarMap several times. |
| ***************************************************************/ |
| { |
| NAT Stack, Size; |
| |
| #ifdef CHECK |
| if (!term_IsTerm(Term)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_ComputeTermSize: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Size = 0; |
| Stack = stack_Bottom(); |
| do { |
| if (VarMap!=NULL && symbol_IsVariable(term_TopSymbol(Term))) |
| Size += VarMap[symbol_VarIndex(term_TopSymbol(Term))]; |
| else { |
| Size++; |
| if (term_IsComplex(Term)) |
| stack_Push(term_ArgumentList(Term)); |
| } |
| while (!stack_Empty(Stack) && list_Empty(stack_Top())) |
| stack_Pop(); |
| |
| if (!stack_Empty(Stack)) { |
| Term = list_Car(stack_Top()); |
| stack_RplacTop(list_Cdr(stack_Top())); |
| } |
| } while (!stack_Empty(Stack)); |
| |
| return Size; |
| } |
| |
| |
| LIST clause_MoveBestLiteralToFront(LIST Literals, SUBST Subst, SYMBOL MaxVar, |
| BOOL (*Better)(LITERAL, NAT, LITERAL, NAT)) |
| /************************************************************** |
| INPUT: A list of literals, a substitution, the maximum variable |
| from the domain of the substitution, and a comparison |
| function. The function <Better> will be called with two |
| literals L1 and L2 and two number S1 and S2, where Si is |
| the size of the atom of Li with respect to variable bindings |
| in <Subst>. |
| RETURNS: The same list. |
| EFFECT: This function moves the first literal L to the front of the |
| list, so that no other literal L' is better than L with respect |
| to the function <Better>. |
| The function exchanges only the literals, the order of list |
| items within the list is not changed. |
| ***************************************************************/ |
| { |
| NAT *Map, MapSize, BestSize, Size; |
| LIST Best, Scan; |
| |
| #ifdef CHECK |
| if (!list_IsSetOfPointers(Literals)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_MoveBestLiteralToFront: List contains duplicates"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (list_Empty(Literals) || list_Empty(list_Cdr(Literals))) |
| /* < 2 list items, so nothing to do */ |
| return Literals; |
| |
| Map = NULL; |
| MapSize = 0; |
| |
| if (!subst_Empty(Subst)) { |
| MapSize = symbol_VarIndex(MaxVar) + 1; |
| Map = memory_Malloc(sizeof(NAT)*MapSize); |
| clause_VarToSizeMap(Subst, Map, MapSize-1); |
| } |
| Best = Literals; /* Remember list item, not literal itself */ |
| BestSize = clause_ComputeTermSize(clause_LiteralAtom(list_Car(Best)), Map); |
| for (Scan = list_Cdr(Literals); !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| Size = clause_ComputeTermSize(clause_LiteralAtom(list_Car(Scan)), Map); |
| if (Better(list_Car(Scan), Size, list_Car(Best), BestSize)) { |
| /* Actual literal is better than the best encountered so far */ |
| BestSize = Size; |
| Best = Scan; |
| } |
| } |
| if (Best != Literals) { |
| /* Move best literal to the front. We just exchange the literals. */ |
| LITERAL h = list_Car(Literals); |
| list_Rplaca(Literals, list_Car(Best)); |
| list_Rplaca(Best, h); |
| } |
| /* cleanup */ |
| if (Map != NULL) |
| memory_Free(Map, sizeof(NAT)*MapSize); |
| |
| return Literals; |
| } |
| |
| |
| /**************************************************************/ |
| /* Literal Output Functions */ |
| /**************************************************************/ |
| |
| void clause_LiteralPrint(LITERAL Literal) |
| /************************************************************** |
| INPUT: A Literal. |
| RETURNS: Nothing. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralPrint:"); |
| misc_ErrorReport("\n Illegal input. Input not a literal."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_PrintPrefix(clause_LiteralSignedAtom(Literal)); |
| } |
| |
| |
| void clause_LiteralListPrint(LIST LitList) |
| /************************************************************** |
| INPUT: A list of literals. |
| RETURNS: Nothing. |
| SUMMARY: Prints the literals to stdout. |
| ***************************************************************/ |
| { |
| while (!(list_Empty(LitList))) { |
| clause_LiteralPrint(list_First(LitList)); |
| LitList = list_Cdr(LitList); |
| |
| if (!list_Empty(LitList)) |
| putchar(' '); |
| } |
| } |
| |
| |
| void clause_LiteralPrintUnsigned(LITERAL Literal) |
| /************************************************************** |
| INPUT: A Literal. |
| RETURNS: Nothing. |
| SUMMARY: |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralPrintUnsigned:"); |
| misc_ErrorReport("\n Illegal input. Input not a literal."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_PrintPrefix(clause_LiteralAtom(Literal)); |
| fflush(stdout); |
| } |
| |
| |
| void clause_LiteralPrintSigned(LITERAL Literal) |
| /************************************************************** |
| INPUT: A Literal. |
| RETURNS: Nothing. |
| SUMMARY: |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralPrintSigned:"); |
| misc_ErrorReport("\n Illegal input. Input not a literal."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_PrintPrefix(clause_LiteralSignedAtom(Literal)); |
| fflush(stdout); |
| } |
| |
| |
| void clause_LiteralFPrint(FILE* File, LITERAL Lit) |
| /************************************************************** |
| INPUT: A file and a literal. |
| RETURNS: Nothing. |
| ************************************************************/ |
| { |
| term_FPrintPrefix(File, clause_LiteralSignedAtom(Lit)); |
| } |
| |
| |
| LIST clause_GetLiteralSubSetList(CLAUSE Clause, int StartIndex, int EndIndex, |
| FLAGSTORE FlagStore, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a start literal index, an end index, a |
| flag store and a precedence. |
| RETURNS: The list of literals between the start and the end |
| index. |
| It is a list of pointers, not a list of indices. |
| **************************************************************/ |
| { |
| |
| LIST Result; |
| int i; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, FlagStore, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| if ((StartIndex < clause_FirstLitIndex()) |
| || (EndIndex > clause_LastLitIndex(Clause))) { |
| misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_ErrorReport("\n Index out of range."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| |
| for (i=StartIndex; |
| i<=EndIndex; |
| i++) { |
| Result = list_Cons(clause_GetLiteral(Clause, i), Result); |
| } |
| |
| return Result; |
| } |
| |
| |
| void clause_ReplaceLiteralSubSet(CLAUSE Clause, int StartIndex, |
| int EndIndex, LIST Replacement, |
| FLAGSTORE FlagStore, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a start literal index, an end literal |
| index, a flag store and a precedence. |
| RETURNS: None. |
| EFFECT: Replaces the subset of literals in <Clause> with |
| indices between (and including) <StartIndex> and |
| <EndIndex> with literals from the <Replacement> |
| list. |
| **************************************************************/ |
| { |
| |
| int i; |
| LIST Scan; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, FlagStore, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| if ((StartIndex < clause_FirstLitIndex()) |
| || (EndIndex > clause_LastLitIndex(Clause))) { |
| misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_ErrorReport("\n Index out of range."); |
| misc_FinishErrorReport(); |
| } |
| if (list_Length(Replacement) != (EndIndex - StartIndex + 1)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:"); |
| misc_ErrorReport("\n Illegal input. Replacement list size"); |
| misc_ErrorReport("\n and set size don't match"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| for (i = StartIndex, Scan = Replacement; |
| i <= EndIndex; |
| i++, Scan = list_Cdr(Scan)) { |
| clause_SetLiteral(Clause, i, list_Car(Scan)); |
| } |
| } |
| |
| static __inline__ BOOL clause_LiteralsCompare(LITERAL Left, LITERAL Right) |
| /************************************************************** |
| INPUT: Two literals. |
| RETURNS: TRUE if Left <= Right, FALSE otherwise. |
| EFFECT: Compares literals by comparing their terms' arities. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!(clause_LiteralIsLiteral(Left) && clause_LiteralIsLiteral(Right))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_LiteralsCompare:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| return term_CompareAbstractLEQ(clause_LiteralSignedAtom(Left), |
| clause_LiteralSignedAtom(Right)); |
| } |
| |
| static __inline__ void clause_FixLiteralSubsetOrder(CLAUSE Clause, |
| int StartIndex, |
| int EndIndex, |
| FLAGSTORE FlagStore, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a start index, an end index a flag store |
| and a precedence. |
| RETURNS: None. |
| EFFECT: Sorts literals with indices between (and including) |
| <StartIndex> and <EndIndex> with respect to an abstract |
| list representation of terms that identifies function |
| symbols with their arity. |
| ***************************************************************/ |
| { |
| |
| LIST literals; |
| |
| #ifdef CHECK |
| if ((StartIndex < clause_FirstLitIndex()) |
| || (EndIndex > clause_LastLitIndex(Clause))) { |
| misc_ErrorReport("\n In clause_FixLiteralSubSetOrder:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_ErrorReport("\n Index out of range."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| /* Get the literals */ |
| literals = clause_GetLiteralSubSetList(Clause, StartIndex, EndIndex, FlagStore, Precedence); |
| |
| /* Sort them */ |
| literals = list_Sort(literals, (BOOL (*) (POINTER, POINTER)) clause_LiteralsCompare); |
| |
| /* Replace clause literals in subset with sorted literals */ |
| clause_ReplaceLiteralSubSet(Clause, StartIndex, EndIndex, literals, FlagStore, Precedence); |
| |
| list_Delete(literals); |
| } |
| |
| void clause_FixLiteralOrder(CLAUSE Clause, FLAGSTORE FlagStore, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a flag store, and a precedence. |
| RETURNS: None. |
| EFFECT: Fixes literal order in a <Clause>. Different literal |
| types are ordered separately. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, FlagStore, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_FixLiteralOrder:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| /* Fix antecedent literal order */ |
| clause_FixLiteralSubsetOrder(Clause, |
| clause_FirstAntecedentLitIndex(Clause), |
| clause_LastAntecedentLitIndex(Clause), |
| FlagStore, Precedence); |
| |
| /* Fix succedent literal order */ |
| clause_FixLiteralSubsetOrder(Clause, |
| clause_FirstSuccedentLitIndex(Clause), |
| clause_LastSuccedentLitIndex(Clause), |
| FlagStore, Precedence); |
| |
| /* Fix constraint literal order */ |
| clause_FixLiteralSubsetOrder(Clause, |
| clause_FirstConstraintLitIndex(Clause), |
| clause_LastConstraintLitIndex(Clause), |
| FlagStore, Precedence); |
| |
| /* Normalize clause, to get variable names right. */ |
| clause_Normalize(Clause); |
| } |
| |
| static int clause_CompareByWeight(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by their weight. |
| ***************************************************************/ |
| { |
| NAT lweight, rweight; |
| int result; |
| |
| lweight = clause_Weight(Left); |
| rweight = clause_Weight(Right); |
| |
| if (lweight < rweight) { |
| result = -1; |
| } |
| else if (lweight > rweight) { |
| result = 1; |
| } |
| else { |
| result = 0; |
| } |
| |
| return result; |
| } |
| |
| static int clause_CompareByClausePartSize(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by the number of literals in |
| the antecedent, succedent and constraint. |
| ***************************************************************/ |
| { |
| int lsize, rsize; |
| |
| lsize = clause_NumOfAnteLits(Left); |
| rsize = clause_NumOfAnteLits(Right); |
| if (lsize < rsize) |
| return -1; |
| else if (lsize > rsize) |
| return 1; |
| |
| lsize = clause_NumOfSuccLits(Left); |
| rsize = clause_NumOfSuccLits(Right); |
| |
| if (lsize < rsize) |
| return -1; |
| else if (lsize > rsize) |
| return 1; |
| |
| lsize = clause_NumOfConsLits(Left); |
| rsize = clause_NumOfConsLits(Right); |
| |
| if (lsize < rsize) |
| return -1; |
| else if (lsize > rsize) |
| return 1; |
| |
| return 0; |
| } |
| |
| void clause_CountSymbols(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: None. |
| EFFECT: Counts the non-variable symbols in the clause, and |
| increases their counts accordingly. |
| ***************************************************************/ |
| { |
| int i; |
| |
| for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) { |
| LITERAL l; |
| TERM t; |
| |
| l = clause_GetLiteral(Clause, i); |
| if (clause_LiteralIsPredicate(l)) { |
| SYMBOL S; |
| |
| S = clause_LiteralPredicate(l); |
| symbol_SetCount(S, symbol_GetCount(S) + 1); |
| } |
| |
| t = clause_GetLiteralAtom(Clause, i); |
| |
| term_CountSymbols(t); |
| } |
| } |
| |
| |
| LIST clause_ListOfPredicates(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: A list of symbols. |
| EFFECT: Creates a list of predicates occurring in the clause. |
| A predicate occurs several times in the list, if |
| it does so in the clause. |
| ***************************************************************/ |
| { |
| LIST preds; |
| int i; |
| |
| preds = list_Nil(); |
| |
| for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) { |
| LITERAL l; |
| |
| l = clause_GetLiteral(Clause, i); |
| if (clause_LiteralIsPredicate(l)) { |
| preds = list_Cons((POINTER) clause_LiteralPredicate(l), preds); |
| } |
| } |
| |
| return preds; |
| } |
| |
| LIST clause_ListOfConstants(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: A list of symbols. |
| EFFECT: Creates a list of constants occurring in the clause. |
| A constant occurs several times in the list, if |
| it does so in the clause. |
| ***************************************************************/ |
| { |
| LIST consts; |
| int i; |
| |
| consts = list_Nil(); |
| |
| for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) { |
| TERM t; |
| |
| t = clause_GetLiteralAtom(Clause, i); |
| |
| consts = list_Nconc(term_ListOfConstants(t), consts); |
| } |
| |
| return consts; |
| } |
| |
| LIST clause_ListOfVariables(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: A list of variables. |
| EFFECT: Creates a list of variables occurring in the clause. |
| A variable occurs several times in the list, if |
| it does so in the clause. |
| ***************************************************************/ |
| { |
| LIST vars; |
| int i; |
| |
| vars = list_Nil(); |
| |
| for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) { |
| TERM t; |
| |
| t = clause_GetLiteralAtom(Clause, i); |
| |
| vars = list_Nconc(term_ListOfVariables(t), vars); |
| } |
| |
| return vars; |
| } |
| |
| LIST clause_ListOfFunctions(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: A list of symbols. |
| EFFECT: Creates a list of functions occurring in the clause. |
| A function occurs several times in the list, if |
| it does so in the clause. |
| ***************************************************************/ |
| { |
| LIST funs; |
| int i; |
| |
| funs = list_Nil(); |
| |
| for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) { |
| TERM t; |
| |
| t = clause_GetLiteralAtom(Clause, i); |
| |
| funs = list_Nconc(term_ListOfFunctions(t), funs); |
| } |
| |
| return funs; |
| } |
| |
| static int clause_CompareByPredicateDistribution(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by the frequency of predicates. |
| ***************************************************************/ |
| { |
| LIST lpreds, rpreds; |
| int result; |
| |
| lpreds = clause_ListOfPredicates(Left); |
| rpreds = clause_ListOfPredicates(Right); |
| |
| result = list_CompareMultisetsByElementDistribution(lpreds, rpreds); |
| |
| list_Delete(lpreds); |
| list_Delete(rpreds); |
| |
| return result; |
| } |
| |
| static int clause_CompareByConstantDistribution(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by the frequency of constants. |
| ***************************************************************/ |
| { |
| LIST lconsts, rconsts; |
| int result; |
| |
| lconsts = clause_ListOfConstants(Left); |
| rconsts = clause_ListOfConstants(Right); |
| |
| result = list_CompareMultisetsByElementDistribution(lconsts, rconsts); |
| |
| list_Delete(lconsts); |
| list_Delete(rconsts); |
| |
| return result; |
| } |
| |
| static int clause_CompareByVariableDistribution(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by the frequency of variables. |
| ***************************************************************/ |
| { |
| LIST lvars, rvars; |
| int result; |
| |
| lvars = clause_ListOfVariables(Left); |
| rvars = clause_ListOfVariables(Right); |
| |
| result = list_CompareMultisetsByElementDistribution(lvars, rvars); |
| |
| list_Delete(lvars); |
| list_Delete(rvars); |
| |
| return result; |
| } |
| |
| static int clause_CompareByFunctionDistribution(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by the frequency of functions. |
| ***************************************************************/ |
| { |
| LIST lfuns, rfuns; |
| int result; |
| |
| lfuns = clause_ListOfFunctions(Left); |
| rfuns = clause_ListOfFunctions(Right); |
| |
| result = list_CompareMultisetsByElementDistribution(lfuns, rfuns); |
| |
| list_Delete(lfuns); |
| list_Delete(rfuns); |
| |
| return result; |
| } |
| |
| static int clause_CompareByDepth(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by their depth. |
| ***************************************************************/ |
| { |
| if (clause_Depth(Left) < clause_Depth(Right)) |
| return -1; |
| else if (clause_Depth(Left) > clause_Depth(Right)) |
| return 1; |
| |
| return 0; |
| } |
| |
| static int clause_CompareByMaxVar(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by their maximal variable. |
| ***************************************************************/ |
| { |
| if (clause_MaxVar(Left) < clause_MaxVar(Right)) |
| return -1; |
| else if (clause_MaxVar(Left) > clause_MaxVar(Right)) |
| return 1; |
| |
| return 0; |
| } |
| |
| static int clause_CompareByLiterals(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by comparing their literals |
| from left to right. |
| ***************************************************************/ |
| { |
| int firstlitleft, lastlitleft; |
| int firstlitright, lastlitright; |
| int i, j; |
| int result; |
| |
| result = 0; |
| |
| /* Compare sorted literals from right to left */ |
| |
| firstlitleft = clause_FirstLitIndex(); |
| lastlitleft = clause_LastLitIndex(Left); |
| firstlitright = clause_FirstLitIndex(); |
| lastlitright = clause_LastLitIndex(Right); |
| |
| for (i = lastlitleft, j = lastlitright; |
| i >= firstlitleft && j >= firstlitright; |
| --i, --j) { |
| TERM lterm, rterm; |
| |
| lterm = clause_GetLiteralTerm(Left, i); |
| rterm = clause_GetLiteralTerm(Right, j); |
| |
| result = term_CompareAbstract(lterm, rterm); |
| |
| if (result != 0) |
| break; |
| } |
| |
| if (result == 0) { |
| /* All literals compared equal, so check if someone has |
| uncompared literals left over. |
| */ |
| if ( i > j) { |
| /* Left clause has uncompared literals left over. */ |
| result = 1; |
| } |
| else if (i < j) { |
| /* Right clause has uncompared literals left over. */ |
| result = -1; |
| } |
| } |
| |
| return result; |
| } |
| |
| static int clause_CompareBySymbolOccurences(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by comparing the occurrences of |
| symbols in their respective literals from left to |
| right. If a symbol occurs less frequently than |
| its positional equivalent in the other clause, |
| then the first clause is smaller. |
| ***************************************************************/ |
| { |
| int firstlitleft, lastlitleft; |
| int firstlitright, lastlitright; |
| int i, j; |
| int result; |
| |
| result = 0; |
| |
| /* Compare sorted literals from right to left */ |
| |
| firstlitleft = clause_FirstLitIndex(); |
| lastlitleft = clause_LastLitIndex(Left); |
| firstlitright = clause_FirstLitIndex(); |
| lastlitright = clause_LastLitIndex(Right); |
| |
| for (i = lastlitleft, j = lastlitright; |
| i >= firstlitleft && j >= firstlitright; |
| --i, --j) { |
| TERM lterm, rterm; |
| LITERAL llit, rlit; |
| |
| llit = clause_GetLiteral(Left, i); |
| rlit = clause_GetLiteral(Right, j); |
| |
| if (clause_LiteralIsPredicate(llit)) { |
| if (clause_LiteralIsPredicate(rlit)) { |
| if (symbol_GetCount(clause_LiteralPredicate(llit)) |
| < symbol_GetCount(clause_LiteralPredicate(rlit))) { |
| return -1; |
| } |
| else if (symbol_GetCount(clause_LiteralPredicate(llit)) |
| > symbol_GetCount(clause_LiteralPredicate(rlit))) { |
| return 1; |
| } |
| } |
| } |
| |
| lterm = clause_GetLiteralTerm(Left, i); |
| rterm = clause_GetLiteralTerm(Right, j); |
| |
| result = term_CompareBySymbolOccurences(lterm, rterm); |
| |
| if (result != 0) |
| break; |
| } |
| |
| return result; |
| } |
| |
| int clause_CompareAbstract(CLAUSE Left, CLAUSE Right) |
| /************************************************************** |
| INPUT: Two clauses. |
| RETURNS: 1 if left > right, -1 if left < right, 0 otherwise. |
| EFFECT: Compares two clauses by their weight. If the weight |
| is equal, it compares the clauses by the arity of |
| their literals from right to left. |
| CAUTION: Expects clause literal order to be fixed. |
| ***************************************************************/ |
| { |
| |
| typedef int (*CLAUSE_COMPARE_FUNCTION) (CLAUSE, CLAUSE); |
| |
| static const CLAUSE_COMPARE_FUNCTION clause_compare_functions [] = { |
| clause_CompareByWeight, |
| clause_CompareByDepth, |
| clause_CompareByMaxVar, |
| clause_CompareByClausePartSize, |
| clause_CompareByLiterals, |
| clause_CompareBySymbolOccurences, |
| clause_CompareByPredicateDistribution, |
| clause_CompareByConstantDistribution, |
| clause_CompareByFunctionDistribution, |
| clause_CompareByVariableDistribution, |
| }; |
| |
| int result; |
| int i; |
| int functions; |
| |
| result = 0; |
| functions = sizeof(clause_compare_functions)/sizeof(CLAUSE_COMPARE_FUNCTION); |
| |
| for (i = 0; i < functions; i++) { |
| result = clause_compare_functions[i](Left, Right); |
| |
| if ( result != 0) { |
| return result; |
| } |
| } |
| |
| return 0; |
| } |
| |
| |
| /**************************************************************/ |
| /* Clause functions */ |
| /**************************************************************/ |
| |
| void clause_Init(void) |
| /************************************************************** |
| INPUT: None. |
| RETURNS: Nothing. |
| SUMMARY: Initializes the clause counter and other variables |
| from this module. |
| ***************************************************************/ |
| { |
| int i; |
| clause_SetCounter(1); |
| clause_STAMPID = term_GetStampID(); |
| for (i = 0; i <= clause_MAXWEIGHT; i++) |
| clause_SORT[i] = list_Nil(); |
| } |
| |
| |
| CLAUSE clause_CreateBody(int ClauseLength) |
| /************************************************************** |
| INPUT: The number of literals as integer. |
| RETURNS: A new generated clause node for 'ClauseLength' |
| MEMORY: Allocates a CLAUSE_NODE and the needed array for LITERALs. |
| *************************************************************/ |
| { |
| CLAUSE Result; |
| |
| Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE)); |
| |
| Result->clausenumber = clause_IncreaseCounter(); |
| Result->maxVar = symbol_GetInitialStandardVarCounter(); |
| Result->flags = 0; |
| Result->depth = 0; |
| clause_InitSplitData(Result); |
| Result->weight = clause_WEIGHTUNDEFINED; |
| Result->parentCls = list_Nil(); |
| Result->parentLits = list_Nil(); |
| |
| Result->c = 0; |
| Result->a = 0; |
| Result->s = 0; |
| |
| if (ClauseLength != 0) |
| Result->literals = |
| (LITERAL *)memory_Malloc((ClauseLength) * sizeof(LITERAL)); |
| |
| clause_SetFromInput(Result); |
| |
| return Result; |
| } |
| |
| |
| CLAUSE clause_Create(LIST Constraint, LIST Antecedent, LIST Succedent, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: Three lists of pointers to atoms, a flag store and |
| a precedence. |
| RETURNS: The new generated clause. |
| MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs, |
| uses the terms from the lists, additionally allocates |
| termnodes for the fol_Not() in Const. and Ante. |
| *************************************************************/ |
| { |
| CLAUSE Result; |
| int i, c, a, s; |
| |
| Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE)); |
| |
| Result->clausenumber = clause_IncreaseCounter(); |
| Result->flags = 0; |
| Result->depth = 0; |
| Result->weight = clause_WEIGHTUNDEFINED; |
| clause_InitSplitData(Result); |
| Result->parentCls = list_Nil(); |
| Result->parentLits = list_Nil(); |
| |
| Result->c = (c = list_Length(Constraint)); |
| Result->a = (a = list_Length(Antecedent)); |
| Result->s = (s = list_Length(Succedent)); |
| |
| if (!clause_IsEmptyClause(Result)) |
| Result->literals = |
| (LITERAL *) memory_Malloc((c+a+s) * sizeof(LITERAL)); |
| |
| for (i = 0; i < c; i++) { |
| Result->literals[i] = |
| clause_LiteralCreate(term_Create(fol_Not(), |
| list_List((TERM)list_Car(Constraint))),Result); |
| Constraint = list_Cdr(Constraint); |
| } |
| |
| a += c; |
| for ( ; i < a; i++) { |
| Result->literals[i] = |
| clause_LiteralCreate(term_Create(fol_Not(), |
| list_List((TERM)list_Car(Antecedent))), Result); |
| Antecedent = list_Cdr(Antecedent); |
| } |
| |
| s += a; |
| for ( ; i < s; i++) { |
| Result->literals[i] = |
| clause_LiteralCreate((TERM) list_Car(Succedent), Result); |
| Succedent = list_Cdr(Succedent); |
| } |
| |
| clause_OrientAndReInit(Result, Flags, Precedence); |
| clause_SetFromInput(Result); |
| |
| return Result; |
| } |
| |
| |
| CLAUSE clause_CreateCrude(LIST Constraint, LIST Antecedent, LIST Succedent, |
| BOOL Con) |
| /************************************************************** |
| INPUT: Three lists of pointers to literals (!) and a Flag indicating |
| whether the clause comes from the conjecture part of of problem. |
| It is assumed that Constraint and Antecedent literals are negative, |
| whereas Succedent literals are positive. |
| RETURNS: The new generated clause, where a clause_OrientAndReInit has still |
| to be performed, i.e., variables are not normalized, maximal literal |
| flags not set, equations not oriented, the weight is not set. |
| MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs, |
| uses the terms from the lists, additionally allocates |
| termnodes for the fol_Not() in Const. and Ante. |
| ****************************************************************/ |
| { |
| CLAUSE Result; |
| int i,c,a,s; |
| |
| Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE)); |
| |
| Result->clausenumber = clause_IncreaseCounter(); |
| Result->flags = 0; |
| if (Con) |
| clause_SetFlag(Result, CONCLAUSE); |
| |
| Result->depth = 0; |
| Result->weight = clause_WEIGHTUNDEFINED; |
| clause_InitSplitData(Result); |
| Result->parentCls = list_Nil(); |
| Result->parentLits = list_Nil(); |
| |
| Result->c = (c = list_Length(Constraint)); |
| Result->a = (a = list_Length(Antecedent)); |
| Result->s = (s = list_Length(Succedent)); |
| |
| if (!clause_IsEmptyClause(Result)) |
| Result->literals = (LITERAL *)memory_Malloc((c+a+s) * sizeof(LITERAL)); |
| |
| for (i = 0; i < c; i++) { |
| Result->literals[i] = |
| clause_LiteralCreate(list_Car(Constraint),Result); |
| Constraint = list_Cdr(Constraint); |
| } |
| |
| a += c; |
| for ( ; i < a; i++) { |
| Result->literals[i] = |
| clause_LiteralCreate(list_Car(Antecedent), Result); |
| Antecedent = list_Cdr(Antecedent); |
| } |
| |
| s += a; |
| for ( ; i < s; i++) { |
| Result->literals[i] = clause_LiteralCreate(list_Car(Succedent), Result); |
| Succedent = list_Cdr(Succedent); |
| } |
| |
| clause_SetFromInput(Result); |
| |
| return Result; |
| } |
| |
| |
| CLAUSE clause_CreateUnnormalized(LIST Constraint, LIST Antecedent, |
| LIST Succedent) |
| /************************************************************** |
| INPUT: Three lists of pointers to atoms. |
| RETURNS: The new generated clause. |
| MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs, |
| uses the terms from the lists, additionally allocates |
| termnodes for the fol_Not() in Const. and Ante. |
| CAUTION: The weight of the clause is not set correctly and |
| equations are not oriented! |
| ****************************************************************/ |
| { |
| CLAUSE Result; |
| int i,c,a,s; |
| |
| Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE)); |
| |
| Result->clausenumber = clause_IncreaseCounter(); |
| Result->flags = 0; |
| Result->depth = 0; |
| Result->weight = clause_WEIGHTUNDEFINED; |
| clause_InitSplitData(Result); |
| Result->parentCls = list_Nil(); |
| Result->parentLits = list_Nil(); |
| |
| Result->c = (c = list_Length(Constraint)); |
| Result->a = (a = list_Length(Antecedent)); |
| Result->s = (s = list_Length(Succedent)); |
| |
| if (!clause_IsEmptyClause(Result)) { |
| Result->literals = (LITERAL *)memory_Malloc((c+a+s) * sizeof(LITERAL)); |
| |
| for (i = 0; i < c; i++) { |
| Result->literals[i] = |
| clause_LiteralCreate(term_Create(fol_Not(), |
| list_List(list_Car(Constraint))), |
| Result); |
| Constraint = list_Cdr(Constraint); |
| } |
| |
| a += c; |
| for ( ; i < a; i++) { |
| Result->literals[i] = |
| clause_LiteralCreate(term_Create(fol_Not(), |
| list_List(list_Car(Antecedent))), |
| Result); |
| Antecedent = list_Cdr(Antecedent); |
| } |
| |
| s += a; |
| for ( ; i < s; i++) { |
| Result->literals[i] = |
| clause_LiteralCreate((TERM)list_Car(Succedent), Result); |
| Succedent = list_Cdr(Succedent); |
| } |
| clause_UpdateMaxVar(Result); |
| } |
| |
| return Result; |
| } |
| |
| |
| CLAUSE clause_CreateFromLiterals(LIST LitList, BOOL Sorts, BOOL Conclause, |
| BOOL Ordering, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A list of literals, three boolean flags indicating whether |
| sort constraint literals should be generated, whether the |
| clause is a conjecture clause, whether the ordering information |
| should be established, a flag store and a precedence. |
| RETURNS: The new generated clause. |
| EFFECT: The result clause will be normalized and the maximal |
| variable will be set. If <Ordering> is FALSE no additional |
| initializations will be done. This mode is intended for |
| the parser for creating clauses at a time when the ordering |
| and weight flags aren't determined finally. |
| Only if <Ordering> is TRUE the equations will be oriented, |
| the maximal literals will be marked and the clause weight |
| will be set correctly. |
| MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs, |
| uses the terms from the lists. |
| ****************************************************************/ |
| { |
| CLAUSE Result; |
| LIST Antecedent,Succedent,Constraint; |
| TERM Atom; |
| |
| Antecedent = list_Nil(); |
| Succedent = list_Nil(); |
| Constraint = list_Nil(); |
| |
| while (!list_Empty(LitList)) { |
| if (term_TopSymbol(list_Car(LitList)) == fol_Not()) { |
| Atom = term_FirstArgument(list_Car(LitList)); |
| if (Sorts && symbol_IsBaseSort(term_TopSymbol(Atom)) && term_IsVariable(term_FirstArgument(Atom))) |
| Constraint = list_Cons(list_Car(LitList),Constraint); |
| else |
| Antecedent = list_Cons(list_Car(LitList),Antecedent); |
| } |
| else |
| Succedent = list_Cons(list_Car(LitList),Succedent); |
| LitList = list_Cdr(LitList); |
| } |
| |
| Constraint = list_NReverse(Constraint); |
| Antecedent = list_NReverse(Antecedent); |
| Succedent = list_NReverse(Succedent); |
| Result = clause_CreateCrude(Constraint, Antecedent, Succedent, Conclause); |
| |
| list_Delete(Constraint); |
| list_Delete(Antecedent); |
| list_Delete(Succedent); |
| |
| if (Ordering) |
| clause_OrientAndReInit(Result, Flags, Precedence); |
| else { |
| clause_Normalize(Result); |
| clause_UpdateMaxVar(Result); |
| } |
| |
| return Result; |
| } |
| |
| void clause_SetSortConstraint(CLAUSE Clause, BOOL Strong, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a flag indicating whether also negative |
| monadic literals with a real term argument should be |
| put in the sort constraint, a flag store and a precedence. |
| RETURNS: Nothing. |
| EFFECT: Negative monadic literals are put in the sort constraint. |
| ****************************************************************/ |
| { |
| LITERAL ActLit,Help; |
| TERM ActAtom; |
| int i,k,NewConLits; |
| |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_SetSortConstraint:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| i = clause_LastConstraintLitIndex(Clause); |
| NewConLits = 0; |
| |
| for (k=clause_FirstAntecedentLitIndex(Clause);k<=clause_LastAntecedentLitIndex(Clause);k++) { |
| ActLit = clause_GetLiteral(Clause,k); |
| ActAtom = clause_LiteralAtom(ActLit); |
| if (symbol_IsBaseSort(term_TopSymbol(ActAtom)) && |
| (Strong || term_IsVariable(term_FirstArgument(ActAtom)))) { |
| if (++i != k) { |
| Help = clause_GetLiteral(Clause,i); |
| clause_SetLiteral(Clause,i,ActLit); |
| clause_SetLiteral(Clause,k,Help); |
| } |
| NewConLits++; |
| } |
| } |
| |
| clause_SetNumOfConsLits(Clause, clause_NumOfConsLits(Clause) + NewConLits); |
| clause_SetNumOfAnteLits(Clause, clause_NumOfAnteLits(Clause) - NewConLits); |
| clause_ReInit(Clause, Flags, Precedence); |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_SetSortConstraint:"); |
| misc_ErrorReport("\n Illegal computations."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| } |
| |
| |
| |
| void clause_Delete(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause. |
| RETURNS: Nothing. |
| MEMORY: Frees the memory of the clause. |
| ***************************************************************/ |
| { |
| int i, n; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { /* Clause may be a byproduct of some hyper rule */ |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_Delete:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| n = clause_Length(Clause); |
| |
| for (i = 0; i < n; i++) |
| clause_LiteralDelete(clause_GetLiteral(Clause,i)); |
| |
| clause_FreeLitArray(Clause); |
| |
| list_Delete(clause_ParentClauses(Clause)); |
| list_Delete(clause_ParentLiterals(Clause)); |
| #ifdef CHECK |
| if ((Clause->splitfield != NULL) && (Clause->splitfield_length == 0)) |
| { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_Delete:"); |
| misc_ErrorReport("\n Illegal splitfield_length."); |
| misc_FinishErrorReport(); |
| } |
| if ((Clause->splitfield == NULL) && (Clause->splitfield_length != 0)) |
| { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_Delete:"); |
| misc_ErrorReport("\n Illegal splitfield."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| if (Clause->splitfield != NULL) { |
| |
| memory_Free(Clause->splitfield, |
| sizeof(SPLITFIELDENTRY) * Clause->splitfield_length); |
| } |
| clause_Free(Clause); |
| } |
| |
| |
| /**************************************************************/ |
| /* Functions to use the sharing for clauses. */ |
| /**************************************************************/ |
| |
| void clause_InsertIntoSharing(CLAUSE Clause, SHARED_INDEX ShIndex, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, an index, a flag store and a precedence. |
| RETURNS: Nothing. |
| SUMMARY: Inserts the unsigned atoms of 'Clause' into the sharing index. |
| ***************************************************************/ |
| { |
| int i, litnum; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_Delete:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| clause_Check(Clause, Flags, Precedence); |
| #endif |
| |
| litnum = clause_Length(Clause); |
| |
| for (i = 0; i < litnum; i++) { |
| clause_LiteralInsertIntoSharing(clause_GetLiteral(Clause,i), ShIndex); |
| } |
| } |
| |
| |
| void clause_DeleteFromSharing(CLAUSE Clause, SHARED_INDEX ShIndex, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, an Index, a flag store and a precedence. |
| RETURNS: Nothing. |
| SUMMARY: Deletes 'Clause' and all its literals from the sharing, |
| frees the memory of 'Clause'. |
| ***************************************************************/ |
| { |
| int i, length; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_DeleteFromSharing:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| length = clause_Length(Clause); |
| |
| for (i = 0; i < length; i++) |
| clause_LiteralDeleteFromSharing(clause_GetLiteral(Clause,i),ShIndex); |
| |
| clause_FreeLitArray(Clause); |
| |
| list_Delete(clause_ParentClauses(Clause)); |
| list_Delete(clause_ParentLiterals(Clause)); |
| #ifdef CHECK |
| if ((Clause->splitfield != NULL) && (Clause->splitfield_length == 0)) |
| { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_DeleteFromSharing:"); |
| misc_ErrorReport("\n Illegal splitfield_length."); |
| misc_FinishErrorReport(); |
| } |
| if ((Clause->splitfield == NULL) && (Clause->splitfield_length != 0)) |
| { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_DeleteFromSharing:"); |
| misc_ErrorReport("\n Illegal splitfield."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| if (Clause->splitfield != NULL) { |
| memory_Free(Clause->splitfield, |
| sizeof(SPLITFIELDENTRY) * Clause->splitfield_length); |
| } |
| clause_Free(Clause); |
| } |
| |
| |
| void clause_MakeUnshared(CLAUSE Clause, SHARED_INDEX ShIndex) |
| /************************************************************** |
| INPUT: A Clause and an Index. |
| RETURNS: Nothing. |
| SUMMARY: Deletes the clauses literals from the sharing and |
| replaces them by unshared copies. |
| ***************************************************************/ |
| { |
| LITERAL ActLit; |
| TERM SharedAtom, AtomCopy; |
| int i,LastAnte,length; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_MakeUnshared:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| LastAnte = clause_LastAntecedentLitIndex(Clause); |
| length = clause_Length(Clause); |
| |
| for (i = clause_FirstLitIndex(); i <= LastAnte; i++) { |
| ActLit = clause_GetLiteral(Clause, i); |
| SharedAtom = clause_LiteralAtom(ActLit); |
| AtomCopy = term_Copy(SharedAtom); |
| sharing_Delete(ActLit, SharedAtom, ShIndex); |
| clause_LiteralSetNegAtom(ActLit, AtomCopy); |
| } |
| |
| for ( ; i < length; i++) { |
| ActLit = clause_GetLiteral(Clause, i); |
| SharedAtom = clause_LiteralSignedAtom(ActLit); |
| AtomCopy = term_Copy(SharedAtom); |
| sharing_Delete(ActLit, SharedAtom, ShIndex); |
| clause_LiteralSetPosAtom(ActLit, AtomCopy); |
| } |
| } |
| |
| void clause_MoveSharedClause(CLAUSE Clause, SHARED_INDEX Source, |
| SHARED_INDEX Destination, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, two indexes, a flag store, and a precedence. |
| RETURNS: Nothing. |
| EFFECT: Deletes <Clause> from <Source> and inserts it into |
| <Destination>. |
| ***************************************************************/ |
| { |
| LITERAL Lit; |
| TERM Atom,Copy; |
| int i,length; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_MoveSharedClause:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| length = clause_Length(Clause); |
| |
| for (i = clause_FirstLitIndex(); i < length; i++) { |
| Lit = clause_GetLiteral(Clause, i); |
| Atom = clause_LiteralAtom(Lit); |
| Copy = term_Copy(Atom); /* sharing_Insert works destructively on <Copy>'s superterms */ |
| clause_LiteralSetAtom(Lit, sharing_Insert(Lit, Copy, Destination)); |
| sharing_Delete(Lit, Atom, Source); |
| term_Delete(Copy); |
| } |
| } |
| |
| |
| void clause_DeleteSharedLiteral(CLAUSE Clause, int Indice, SHARED_INDEX ShIndex, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, a literals indice, an Index, a flag store |
| and a precedence. |
| RETURNS: Nothing. |
| SUMMARY: Deletes the shared literal from the clause. |
| MEMORY: Various. |
| ***************************************************************/ |
| { |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_DeleteSharedLiteral:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| clause_MakeUnshared(Clause, ShIndex); |
| clause_DeleteLiteral(Clause, Indice, Flags, Precedence); |
| clause_InsertIntoSharing(Clause, ShIndex, Flags, Precedence); |
| } |
| |
| |
| void clause_DeleteClauseList(LIST ClauseList) |
| /************************************************************** |
| INPUT: A list of unshared clauses. |
| RETURNS: Nothing. |
| SUMMARY: Deletes all clauses in the list and the list. |
| MEMORY: Frees the lists and the clauses' memory. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| for (Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| if (clause_Exists(list_Car(Scan))) |
| clause_Delete(list_Car(Scan)); |
| |
| list_Delete(ClauseList); |
| } |
| |
| |
| void clause_DeleteSharedClauseList(LIST ClauseList, SHARED_INDEX ShIndex, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A list of clauses, an index, a flag store and |
| a precedence. |
| RETURNS: Nothing. |
| SUMMARY: Deletes all clauses in the list from the sharing. |
| MEMORY: Frees the lists and the clauses' memory. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| for (Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| clause_DeleteFromSharing(list_Car(Scan), ShIndex, Flags, Precedence); |
| |
| list_Delete(ClauseList); |
| } |
| |
| |
| void clause_DeleteAllIndexedClauses(SHARED_INDEX ShIndex, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An Index, a flag store and a precedence. |
| RETURNS: Nothing. |
| SUMMARY: Deletes all clauses' terms from the sharing, frees their |
| memory. |
| MEMORY: Frees the memory of all clauses with terms in the index. |
| ***************************************************************/ |
| { |
| LIST TermList,DelList,Scan; |
| TERM NewVar; |
| SYMBOL NewVarSymbol; |
| |
| NewVar = term_CreateStandardVariable(); |
| NewVarSymbol = term_TopSymbol(NewVar); |
| |
| TermList = st_GetInstance(cont_LeftContext(), sharing_Index(ShIndex), NewVar); |
| /* This should yield a list of all terms in the index |
| and thus the sharing. */ |
| |
| while (!list_Empty(TermList)) { |
| |
| DelList = sharing_GetDataList(list_Car(TermList), ShIndex); |
| |
| for (Scan = DelList; |
| !list_Empty(Scan); |
| Scan = list_Cdr(Scan)) |
| list_Rplaca(Scan, clause_LiteralOwningClause(list_Car(Scan))); |
| |
| DelList = list_PointerDeleteDuplicates(DelList); |
| |
| for (Scan = DelList; |
| !list_Empty(Scan); |
| Scan = list_Cdr(Scan)) |
| clause_DeleteFromSharing(list_Car(Scan), ShIndex, Flags, Precedence); |
| |
| list_Delete(TermList); |
| |
| TermList = st_GetInstance(cont_LeftContext(), sharing_Index(ShIndex), NewVar); |
| |
| list_Delete(DelList); |
| } |
| term_Delete(NewVar); |
| symbol_Delete(NewVarSymbol); |
| } |
| |
| |
| void clause_PrintAllIndexedClauses(SHARED_INDEX ShIndex) |
| /************************************************************** |
| INPUT: An Index. |
| RETURNS: Nothing. |
| SUMMARY: Prints all indexed clauses to stdout. |
| ***************************************************************/ |
| { |
| LIST TermList,ClList,PrintList,Scan; |
| TERM NewVar; |
| SYMBOL NewVarSymbol; |
| |
| NewVar = term_CreateStandardVariable(); |
| NewVarSymbol = term_TopSymbol(NewVar); |
| |
| TermList = st_GetInstance(cont_LeftContext(), sharing_Index(ShIndex), NewVar); |
| /* This should yield a list of all terms in the index |
| and thus the sharing. */ |
| |
| PrintList = list_Nil(); |
| |
| while (!list_Empty(TermList)) { |
| |
| ClList = sharing_GetDataList(list_Car(TermList), ShIndex); |
| |
| for (Scan = ClList; |
| !list_Empty(Scan); |
| Scan = list_Cdr(Scan)) |
| list_Rplaca(Scan, clause_LiteralOwningClause(list_Car(Scan))); |
| |
| PrintList = list_NPointerUnion(ClList, PrintList); |
| |
| Scan = TermList; |
| TermList = list_Cdr(TermList); |
| list_Free(Scan); |
| } |
| clause_ListPrint(PrintList); |
| |
| list_Delete(PrintList); |
| |
| term_Delete(NewVar); |
| symbol_Delete(NewVarSymbol); |
| } |
| |
| |
| LIST clause_AllIndexedClauses(SHARED_INDEX ShIndex) |
| /************************************************************** |
| INPUT: An index |
| RETURNS: A list of all the clauses in the index |
| MEMORY: Memory is allocated for the list nodes |
| ***************************************************************/ |
| { |
| LIST clauselist, scan; |
| clauselist = sharing_GetAllSuperTerms(ShIndex); |
| for (scan = clauselist; scan != list_Nil(); scan = list_Cdr(scan)) |
| list_Rplaca(scan, clause_LiteralOwningClause(list_Car(scan))); |
| clauselist = list_PointerDeleteDuplicates(clauselist); |
| return clauselist; |
| } |
| |
| |
| /**************************************************************/ |
| /* Clause Access Functions */ |
| /**************************************************************/ |
| |
| void clause_DeleteLiteralNN(CLAUSE Clause, int Indice) |
| /************************************************************** |
| INPUT: An unshared clause, and a literal index. |
| RETURNS: Nothing. |
| EFFECT: The literal is position <Indice> is deleted from <Clause>. |
| The clause isn't reinitialized afterwards. |
| MEMORY: The memory of the literal with the 'Indice' and |
| memory of its atom is freed. |
| ***************************************************************/ |
| { |
| int i, lc, la, length, shift; |
| LITERAL *Literals; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause) || (clause_Length(Clause) <= Indice) || |
| Indice < 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_DeleteLiteral:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| lc = clause_LastConstraintLitIndex(Clause); |
| la = clause_LastAntecedentLitIndex(Clause); |
| length = clause_Length(Clause); |
| |
| /* Create a new literal array */ |
| if (length > 1) |
| Literals = (LITERAL*) memory_Malloc(sizeof(LITERAL) * (length-1)); |
| else |
| Literals = (LITERAL*) NULL; |
| |
| /* Copy literals to the new array */ |
| shift = 0; |
| length--; /* The loop iterates over the new array */ |
| for (i = 0; i < length; i++) { |
| if (i == Indice) |
| shift = 1; |
| Literals[i] = Clause->literals[i+shift]; |
| } |
| |
| /* Free literal and old array and set new one */ |
| clause_LiteralDelete(clause_GetLiteral(Clause, Indice)); |
| clause_FreeLitArray(Clause); |
| Clause->literals = Literals; |
| |
| /* Update clause */ |
| if (Indice <= lc) |
| clause_SetNumOfConsLits(Clause, clause_NumOfConsLits(Clause) - 1); |
| else if (Indice <= la) |
| clause_SetNumOfAnteLits(Clause, clause_NumOfAnteLits(Clause) - 1); |
| else |
| clause_SetNumOfSuccLits(Clause, clause_NumOfSuccLits(Clause) - 1); |
| /* Mark the weight as undefined */ |
| Clause->weight = clause_WEIGHTUNDEFINED; |
| } |
| |
| |
| void clause_DeleteLiteral(CLAUSE Clause, int Indice, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An unshared clause, a literals index, a flag store, |
| and a precedence. |
| RETURNS: Nothing. |
| EFFECT: The literal at position <Indice> is deleted from <Clause>. |
| In contrast to the function clause_DeleteLiteralNN |
| the clause is reinitialized afterwards. |
| MEMORY: The memory of the literal with the 'Indice' and memory |
| of its atom is freed. |
| ***************************************************************/ |
| { |
| clause_DeleteLiteralNN(Clause, Indice); |
| clause_ReInit(Clause, Flags, Precedence); |
| } |
| |
| |
| void clause_DeleteLiterals(CLAUSE Clause, LIST Indices, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An unshared clause, a list of literal indices a |
| flag store and a precedence. |
| RETURNS: Nothing. |
| EFFECT: The literals given by <Indices> are deleted. |
| The clause is reinitialized afterwards. |
| MEMORY: The memory of the literals with the 'Indice' and |
| memory of its atom is freed. |
| ***************************************************************/ |
| { |
| LITERAL *NewLits; |
| int i, j, nc, na, ns, lc, la, olength, nlength; |
| |
| #ifdef CHECK |
| LIST Scan; |
| if (!list_IsSetOfPointers(Indices)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_DeleteLiterals:"); |
| misc_ErrorReport(" list contains duplicate indices."); |
| misc_FinishErrorReport(); |
| } |
| /* check the literal indices */ |
| for (Scan = Indices; !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| i = (int) list_Car(Scan); |
| if (i < 0 || i > clause_LastLitIndex(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_DeleteLiterals:"); |
| misc_ErrorReport(" literal index %d is out ", i); |
| misc_ErrorReport(" of bounds"); |
| misc_FinishErrorReport(); |
| } |
| } |
| #endif |
| |
| nc = 0; |
| na = 0; |
| ns = 0; |
| lc = clause_LastConstraintLitIndex(Clause); |
| la = clause_LastAntecedentLitIndex(Clause); |
| |
| olength = clause_Length(Clause); |
| nlength = olength - list_Length(Indices); |
| |
| if (nlength != 0) |
| NewLits = (LITERAL*) memory_Malloc(sizeof(LITERAL) * nlength); |
| else |
| NewLits = (LITERAL*) NULL; |
| |
| for (i=clause_FirstLitIndex(), j=clause_FirstLitIndex(); i < olength; i++) |
| |
| if (list_PointerMember(Indices, (POINTER) i)) |
| clause_LiteralDelete(clause_GetLiteral(Clause,i)); |
| else { |
| |
| NewLits[j++] = clause_GetLiteral(Clause,i); |
| |
| if (i <= lc) |
| nc++; |
| else if (i <= la) |
| na++; |
| else |
| ns++; |
| } |
| clause_FreeLitArray(Clause); |
| Clause->literals = NewLits; |
| |
| clause_SetNumOfConsLits(Clause, nc); |
| clause_SetNumOfAnteLits(Clause, na); |
| clause_SetNumOfSuccLits(Clause, ns); |
| |
| clause_ReInit(Clause, Flags, Precedence); |
| } |
| |
| |
| /**************************************************************/ |
| /* Clause Comparisons */ |
| /**************************************************************/ |
| |
| BOOL clause_IsHornClause(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: The boolean value TRUE if 'Clause' is a hornclause |
| FALSE else. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_IsHornClause:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| return (clause_NumOfSuccLits(Clause) <= 1); |
| } |
| |
| |
| BOOL clause_HasTermSortConstraintLits(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause, |
| RETURNS: TRUE iff there is at least one sort constraint atom having |
| a term as its argument |
| ***************************************************************/ |
| { |
| int i,n; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_HasTermSortConstraintLits:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| n = clause_LastConstraintLitIndex(Clause); |
| |
| for (i = clause_FirstConstraintLitIndex(Clause); i <= n; i++) |
| if (!term_AllArgsAreVar(clause_GetLiteralAtom(Clause,i))) |
| return TRUE; |
| |
| return FALSE; |
| } |
| |
| |
| BOOL clause_HasSolvedConstraint(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: The boolean value TRUE if 'Clause' has a solved |
| constraint, i.e. only variables as sort arguments, |
| FALSE else. |
| ***************************************************************/ |
| { |
| int i,c; |
| LIST CVars, LitVars; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_HasSolvedConstraint:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| CVars = list_Nil(); |
| c = clause_NumOfConsLits(Clause); |
| |
| if (c == 0) |
| return TRUE; |
| |
| if (clause_HasTermSortConstraintLits(Clause)) |
| return FALSE; |
| |
| for (i = 0; i < c; i++) |
| CVars = list_NPointerUnion(term_VariableSymbols(clause_GetLiteralAtom(Clause, i)), CVars); |
| |
| if (i == c) { |
| c = clause_Length(Clause); |
| LitVars = list_Nil(); |
| |
| for ( ; i < c; i++) |
| LitVars = list_NPointerUnion(LitVars, term_VariableSymbols(clause_GetLiteralAtom(Clause, i))); |
| |
| if (list_Empty(CVars = list_NPointerDifference(CVars, LitVars))) { |
| list_Delete(LitVars); |
| return TRUE; |
| } |
| list_Delete(LitVars); |
| } |
| |
| list_Delete(CVars); |
| |
| return FALSE; |
| } |
| |
| |
| BOOL clause_HasSelectedLiteral(CLAUSE Clause, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, a flag store and a precedence. |
| RETURNS: The boolean value TRUE iff <Clause> has a selected literal |
| ***************************************************************/ |
| { |
| int i,negs; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_HasSelectedLiteral:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| negs = clause_LastAntecedentLitIndex(Clause); |
| |
| for (i=clause_FirstAntecedentLitIndex(Clause); i <= negs; i++) |
| if (clause_LiteralGetFlag(clause_GetLiteral(Clause,i), LITSELECT)) |
| return TRUE; |
| |
| return FALSE; |
| } |
| |
| |
| BOOL clause_IsDeclarationClause(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: The boolean value TRUE, if 'Clause' has only variables |
| as arguments in constraint literals. |
| ***************************************************************/ |
| { |
| int i,length; |
| LITERAL Lit; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_IsDeclarationClause:"); |
| misc_ErrorReport("\n Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (!clause_HasSolvedConstraint(Clause)) |
| return FALSE; |
| |
| length = clause_Length(Clause); |
| |
| for (i=clause_FirstSuccedentLitIndex(Clause);i<length;i++) { |
| Lit = clause_GetLiteral(Clause,i); |
| if (clause_LiteralIsMaximal(Lit) && |
| symbol_IsBaseSort(term_TopSymbol(clause_LiteralSignedAtom(Lit)))) |
| return TRUE; |
| } |
| |
| return FALSE; |
| } |
| |
| |
| BOOL clause_IsSortTheoryClause(CLAUSE Clause, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, a flag store and a precedence. |
| RETURNS: The boolean value TRUE, if 'Clause' has only variables |
| as arguments in constraint literals, no antecedent literals |
| and exactly one monadic succedent literal. |
| ***************************************************************/ |
| { |
| LITERAL Lit; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_IsSortTheoryClause:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (clause_NumOfAnteLits(Clause) > 0 || |
| clause_NumOfSuccLits(Clause) > 1 || |
| !clause_HasSolvedConstraint(Clause)) |
| return FALSE; |
| |
| Lit = clause_GetLiteral(Clause,clause_FirstSuccedentLitIndex(Clause)); |
| if (symbol_IsBaseSort(term_TopSymbol(clause_LiteralSignedAtom(Lit)))) |
| return TRUE; |
| |
| return FALSE; |
| } |
| |
| BOOL clause_IsPotentialSortTheoryClause(CLAUSE Clause, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, a flag store and a precedence. |
| RETURNS: The boolean value TRUE, if 'Clause' has monadic literals |
| only variables as arguments in antecedent/constraint literals, |
| no other antecedent literals and exactly one monadic succedent |
| literal. |
| ***************************************************************/ |
| { |
| LITERAL Lit; |
| int i; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_IsPotentialSortTheoryClause:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (clause_NumOfSuccLits(Clause) != 1) |
| return FALSE; |
| |
| for (i=clause_FirstLitIndex();i<clause_FirstSuccedentLitIndex(Clause);i++) { |
| Lit = clause_GetLiteral(Clause,i); |
| if (!symbol_IsBaseSort(term_TopSymbol(clause_LiteralAtom(Lit))) || |
| !term_IsVariable(term_FirstArgument(clause_LiteralAtom(Lit)))) |
| return FALSE; |
| } |
| |
| Lit = clause_GetLiteral(Clause,clause_FirstSuccedentLitIndex(Clause)); |
| if (symbol_IsBaseSort(term_TopSymbol(clause_LiteralSignedAtom(Lit)))) |
| return TRUE; |
| |
| return FALSE; |
| } |
| |
| |
| BOOL clause_HasOnlyVarsInConstraint(CLAUSE Clause, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, a flag store and a precedence. |
| RETURNS: The boolean value TRUE, if 'Clause' has only variables |
| as arguments in constraint literals. |
| ***************************************************************/ |
| { |
| int i,nc; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_HasOnlyVarsInConstraint:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| nc = clause_NumOfConsLits(Clause); |
| |
| for (i = 0; i < nc && term_AllArgsAreVar(clause_GetLiteralAtom(Clause,i)); i++) |
| /* empty */; |
| |
| return (i == nc); |
| } |
| |
| |
| BOOL clause_HasSortInSuccedent(CLAUSE Clause, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, a flag store and a precedence. |
| RETURNS: The boolean value TRUE, if 'Clause' has a maximal succedent |
| sort literal; FALSE, else. |
| ***************************************************************/ |
| { |
| LITERAL Lit; |
| int i,l; |
| BOOL result = FALSE; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_HasSortInSuccedent:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| l = clause_Length(Clause); |
| |
| for (i = clause_FirstSuccedentLitIndex(Clause); i < l && !result ; i++) { |
| Lit = clause_GetLiteral(Clause, i); |
| result = (symbol_Arity(term_TopSymbol(clause_LiteralAtom(Lit))) == 1); |
| } |
| return result; |
| } |
| |
| |
| BOOL clause_LitsHaveCommonVar(LITERAL Lit1, LITERAL Lit2) |
| /************************************************************** |
| INPUT: Two literals. |
| RETURNS: The boolean value TRUE, if 'Lit1' and 'Lit2' have |
| common variables, FALSE, else. |
| ***************************************************************/ |
| { |
| LIST Vars1, Vars2; |
| BOOL Result; |
| |
| Vars1 = term_VariableSymbols(clause_LiteralAtom(Lit1)); |
| Vars2 = term_VariableSymbols(clause_LiteralAtom(Lit2)); |
| Result = list_HasIntersection(Vars1, Vars2); |
| list_Delete(Vars1); |
| list_Delete(Vars2); |
| |
| return Result; |
| } |
| |
| |
| /**************************************************************/ |
| /* Clause Input and Output Functions */ |
| /**************************************************************/ |
| |
| void clause_Print(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause. |
| RETURNS: Nothing. |
| SUMMARY: The clause is printed to stdout. |
| ***************************************************************/ |
| { |
| RULE Origin; |
| LITERAL Lit; |
| int i,c,a,s; |
| |
| #ifdef CHECK |
| if (!clause_IsUnorderedClause(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_Print:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (!clause_Exists(Clause)) |
| fputs("(CLAUSE)NULL", stdout); |
| else { |
| printf("%d",clause_Number(Clause)); |
| |
| Origin = clause_Origin(Clause); |
| printf("[%d:", clause_SplitLevel(Clause)); |
| |
| #ifdef CHECK |
| if (Clause->splitfield_length <= 1) |
| fputs("0.", stdout); |
| else |
| for (i=Clause->splitfield_length-1; i > 0; i--) |
| printf("%lu.", Clause->splitfield[i]); |
| if (Clause->splitfield_length == 0) |
| putchar('1'); |
| else |
| printf("%lu", (Clause->splitfield[0] | 1)); |
| printf(":%c%c:%c:%d:%d:", clause_GetFlag(Clause, CONCLAUSE) ? 'C' : 'A', |
| clause_GetFlag(Clause, WORKEDOFF) ? 'W' : 'U', |
| clause_GetFlag(Clause, NOPARAINTO) ? 'N' : 'P', |
| clause_Weight(Clause), clause_Depth(Clause)); |
| #endif |
| |
| clause_PrintOrigin(Clause); |
| |
| if (Origin == INPUT) { |
| ; |
| } else { |
| putchar(':'); |
| clause_PrintParentClauses(Clause); |
| } |
| putchar(']'); |
| |
| c = clause_NumOfConsLits(Clause); |
| a = clause_NumOfAnteLits(Clause); |
| s = clause_NumOfSuccLits(Clause); |
| |
| for (i = 0; i < c; i++) { |
| putchar(' '); |
| Lit = clause_GetLiteral(Clause, i); |
| clause_LiteralPrintUnsigned(Lit); |
| } |
| fputs(" || ", stdout); |
| |
| a += c; |
| for ( ; i < a; i++) { |
| |
| Lit = clause_GetLiteral(Clause, i); |
| clause_LiteralPrintUnsigned(Lit); |
| if (clause_LiteralIsMaximal(Lit)) { |
| putchar('*'); |
| if (clause_LiteralIsOrientedEquality(Lit)) |
| putchar('*'); |
| } |
| if (clause_LiteralGetFlag(Lit,LITSELECT)) |
| putchar('+'); |
| if (i+1 < a) |
| putchar(' '); |
| } |
| fputs(" -> ",stdout); |
| |
| s += a; |
| for ( ; i < s; i++) { |
| |
| Lit = clause_GetLiteral(Clause, i); |
| clause_LiteralPrintUnsigned(Lit); |
| if (clause_LiteralIsMaximal(Lit)) { |
| putchar('*'); |
| if (clause_LiteralIsOrientedEquality(Lit)) |
| putchar('*'); |
| } |
| #ifdef CHECK |
| if (clause_LiteralGetFlag(Lit,LITSELECT)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_Print: Clause has selected positive literal.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| if (i+1 < s) |
| putchar(' '); |
| } |
| putchar('.'); |
| } |
| } |
| |
| |
| void clause_PrintMaxLitsOnly(CLAUSE Clause, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, a flag store and a precedence. |
| RETURNS: Nothing. |
| SUMMARY: |
| ***************************************************************/ |
| { |
| int i,c,a,s; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_PrinMaxLitsOnly:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| c = clause_NumOfConsLits(Clause); |
| a = clause_NumOfAnteLits(Clause); |
| s = clause_NumOfSuccLits(Clause); |
| |
| for (i = 0; i < c; i++) { |
| if (clause_LiteralIsMaximal(clause_GetLiteral(Clause, i))) |
| clause_LiteralPrint(clause_GetLiteral(Clause, i)); |
| if (clause_LiteralGetFlag(clause_GetLiteral(Clause, i),STRICTMAXIMAL)) { |
| clause_LiteralPrint(clause_GetLiteral(Clause, i)); |
| fputs("(strictly)", stdout); |
| } |
| } |
| fputs(" || ", stdout); |
| |
| a += c; |
| for ( ; i < a; i++) { |
| if (clause_LiteralIsMaximal(clause_GetLiteral(Clause, i))) |
| clause_LiteralPrint(clause_GetLiteral(Clause, i)); |
| if (clause_LiteralGetFlag(clause_GetLiteral(Clause, i),STRICTMAXIMAL)) { |
| clause_LiteralPrint(clause_GetLiteral(Clause, i)); |
| fputs("(strictly)", stdout); |
| } |
| } |
| fputs(" -> ", stdout); |
| |
| s += a; |
| for ( ; i < s; i++) { |
| if (clause_LiteralIsMaximal(clause_GetLiteral(Clause, i))) |
| clause_LiteralPrint(clause_GetLiteral(Clause, i)); |
| if (clause_LiteralGetFlag(clause_GetLiteral(Clause, i),STRICTMAXIMAL)) { |
| clause_LiteralPrint(clause_GetLiteral(Clause, i)); |
| fputs("(strictly)", stdout); |
| } |
| } |
| puts("."); /* with newline */ |
| } |
| |
| |
| void clause_FPrint(FILE* File, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A file and a clause. |
| RETURNS: Nothing. |
| SUMMARY: Prints any clause to the file 'File'. |
| CAUTION: Uses the term_Output functions. |
| ***************************************************************/ |
| { |
| int i, c, a, s; |
| |
| c = clause_NumOfConsLits(Clause); |
| a = clause_NumOfAnteLits(Clause); |
| s = clause_NumOfSuccLits(Clause); |
| |
| for (i = 0; i < c; i++) |
| term_FPrint(File, clause_GetLiteralAtom(Clause, i)); |
| |
| fputs(" || ", stdout); |
| |
| a += c; |
| for ( ; i < a; i++) |
| term_FPrint(File, clause_GetLiteralAtom(Clause, i)); |
| |
| fputs(" -> ", stdout); |
| |
| s += a; |
| for ( ; i < s; i++) |
| term_FPrint(File, clause_GetLiteralAtom(Clause, i)); |
| |
| putc('.', File); |
| } |
| |
| |
| void clause_ListPrint(LIST ClauseList) |
| /************************************************************** |
| INPUT: A list of clauses. |
| RETURNS: Nothing. |
| SUMMARY: Prints the clauses to stdout. |
| CAUTION: Uses the clause_Print function. |
| ***************************************************************/ |
| { |
| while (!(list_Empty(ClauseList))) { |
| clause_Print(list_First(ClauseList)); |
| ClauseList = list_Cdr(ClauseList); |
| if (!list_Empty(ClauseList)) |
| putchar('\n'); |
| } |
| } |
| |
| |
| void clause_PrintParentClauses(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause. |
| RETURNS: Nothing. |
| SUMMARY: Prints the clauses parentclauses and -literals to stdout. |
| ***************************************************************/ |
| { |
| LIST Scan1,Scan2; |
| |
| if (!list_Empty(clause_ParentClauses(Clause))) { |
| |
| Scan1 = clause_ParentClauses(Clause); |
| Scan2 = clause_ParentLiterals(Clause); |
| printf("%d.%d", (int)list_Car(Scan1), (int)list_Car(Scan2)); |
| |
| for (Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2); |
| !list_Empty(Scan1); |
| Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2)) |
| printf(",%d.%d", (int)list_Car(Scan1), (int)list_Car(Scan2)); |
| } |
| } |
| |
| |
| RULE clause_GetOriginFromString(const char* RuleName) |
| /************************************************************** |
| INPUT: A string containing the abbreviated name of a rule. |
| RETURNS: The RULE corresponding to the <RuleName>. |
| ***************************************************************/ |
| { |
| if (string_Equal(RuleName, "App")) return CLAUSE_DELETION; |
| else if (string_Equal(RuleName, "EmS")) return EMPTY_SORT; |
| else if (string_Equal(RuleName, "SoR")) return SORT_RESOLUTION; |
| else if (string_Equal(RuleName, "EqR")) return EQUALITY_RESOLUTION; |
| else if (string_Equal(RuleName, "EqF")) return EQUALITY_FACTORING; |
| else if (string_Equal(RuleName, "MPm")) return MERGING_PARAMODULATION; |
| else if (string_Equal(RuleName, "SpR")) return SUPERPOSITION_RIGHT; |
| else if (string_Equal(RuleName, "SPm")) return PARAMODULATION; |
| else if (string_Equal(RuleName, "OPm")) return ORDERED_PARAMODULATION; |
| else if (string_Equal(RuleName, "SpL")) return SUPERPOSITION_LEFT; |
| else if (string_Equal(RuleName, "Res")) return GENERAL_RESOLUTION; |
| else if (string_Equal(RuleName, "SHy")) return SIMPLE_HYPER; |
| else if (string_Equal(RuleName, "OHy")) return ORDERED_HYPER; |
| else if (string_Equal(RuleName, "URR")) return UR_RESOLUTION; |
| else if (string_Equal(RuleName, "Fac")) return GENERAL_FACTORING; |
| else if (string_Equal(RuleName, "Spt")) return SPLITTING; |
| else if (string_Equal(RuleName, "Inp")) return INPUT; |
| else if (string_Equal(RuleName, "Rew")) return REWRITING; |
| else if (string_Equal(RuleName, "CRw")) return CONTEXTUAL_REWRITING; |
| else if (string_Equal(RuleName, "Con")) return CONDENSING; |
| else if (string_Equal(RuleName, "AED")) return ASSIGNMENT_EQUATION_DELETION; |
| else if (string_Equal(RuleName, "Obv")) return OBVIOUS_REDUCTIONS; |
| else if (string_Equal(RuleName, "SSi")) return SORT_SIMPLIFICATION; |
| else if (string_Equal(RuleName, "MRR")) return MATCHING_REPLACEMENT_RESOLUTION; |
| else if (string_Equal(RuleName, "UnC")) return UNIT_CONFLICT; |
| else if (string_Equal(RuleName, "Def")) return DEFAPPLICATION; |
| else if (string_Equal(RuleName, "Ter")) return TERMINATOR; |
| else { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\nIn clause_GetOriginFromString: Unknown clause origin."); |
| misc_FinishErrorReport(); |
| return CLAUSE_DELETION; /* Just for the compiler, code is not reachable */ |
| } |
| } |
| |
| void clause_FPrintOrigin(FILE* File, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause. |
| RETURNS: Nothing. |
| SUMMARY: Prints the clause's origin to the file. |
| ***************************************************************/ |
| { |
| RULE Result; |
| |
| Result = clause_Origin(Clause); |
| |
| switch(Result) { |
| case CLAUSE_DELETION: fputs("App", File); break; |
| case EMPTY_SORT: fputs("EmS", File); break; |
| case SORT_RESOLUTION: fputs("SoR", File); break; |
| case EQUALITY_RESOLUTION: fputs("EqR", File); break; |
| case EQUALITY_FACTORING: fputs("EqF", File); break; |
| case MERGING_PARAMODULATION: fputs("MPm", File); break; |
| case SUPERPOSITION_RIGHT: fputs("SpR", File); break; |
| case PARAMODULATION: fputs("SPm", File); break; |
| case ORDERED_PARAMODULATION: fputs("OPm", File); break; |
| case SUPERPOSITION_LEFT: fputs("SpL", File); break; |
| case GENERAL_RESOLUTION: fputs("Res", File); break; |
| case SIMPLE_HYPER: fputs("SHy", File); break; |
| case ORDERED_HYPER: fputs("OHy", File); break; |
| case UR_RESOLUTION: fputs("URR", File); break; |
| case GENERAL_FACTORING: fputs("Fac", File); break; |
| case SPLITTING: fputs("Spt", File); break; |
| case INPUT: fputs("Inp", File); break; |
| case REWRITING: fputs("Rew", File); break; |
| case CONTEXTUAL_REWRITING: fputs("CRw", File); break; |
| case CONDENSING: fputs("Con", File); break; |
| case ASSIGNMENT_EQUATION_DELETION: fputs("AED", File); break; |
| case OBVIOUS_REDUCTIONS: fputs("Obv", File); break; |
| case SORT_SIMPLIFICATION: fputs("SSi", File); break; |
| case MATCHING_REPLACEMENT_RESOLUTION: fputs("MRR", File); break; |
| case UNIT_CONFLICT: fputs("UnC", File); break; |
| case DEFAPPLICATION: fputs("Def", File); break; |
| case TERMINATOR: fputs("Ter", File); break; |
| case TEMPORARY: fputs("Temporary", File); break; |
| default: |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_FPrintOrigin: Clause has no origin."); |
| misc_FinishErrorReport(); |
| } |
| } |
| |
| |
| void clause_PrintOrigin(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A Clause. |
| RETURNS: Nothing. |
| SUMMARY: Prints the clauses origin to stdout. |
| ***************************************************************/ |
| { |
| clause_FPrintOrigin(stdout, Clause); |
| } |
| |
| |
| void clause_PrintVerbose(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A Clause, a flag store and a precedence. |
| RETURNS: Nothing. |
| SUMMARY: Prints almost all the information kept in the |
| clause structure. |
| ***************************************************************/ |
| { |
| int c,a,s; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_PrintVerbose:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| c = clause_NumOfConsLits(Clause); |
| a = clause_NumOfAnteLits(Clause); |
| s = clause_NumOfSuccLits(Clause); |
| |
| printf(" c = %d a = %d s = %d", c,a,s); |
| printf(" Weight : %d", clause_Weight(Clause)); |
| printf(" Depth : %d", clause_Depth(Clause)); |
| printf(" %s %s ", |
| (clause_GetFlag(Clause,WORKEDOFF) ? "WorkedOff" : "Usable"), |
| (clause_GetFlag(Clause,CLAUSESELECT) ? "Selected" : "NotSelected")); |
| |
| clause_Print(Clause); |
| } |
| |
| |
| CLAUSE clause_GetNumberedCl(int number, LIST ClList) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| CAUTION: |
| ***************************************************************/ |
| { |
| while (!list_Empty(ClList) && |
| clause_Number((CLAUSE)list_Car(ClList)) != number) |
| ClList = list_Cdr(ClList); |
| |
| if (list_Empty(ClList)) |
| return NULL; |
| else |
| return list_Car(ClList); |
| } |
| |
| static __inline__ BOOL clause_NumberLower(CLAUSE A, CLAUSE B) |
| { |
| return (BOOL) (clause_Number(A) < clause_Number(B)); |
| } |
| |
| LIST clause_NumberSort(LIST List) |
| /************************************************************** |
| INPUT: A list of clauses. |
| RETURNS: The same list where the elements are sorted wrt their number. |
| CAUTION: Destructive. |
| ***************************************************************/ |
| { |
| return list_Sort(List, (BOOL (*) (POINTER, POINTER)) clause_NumberLower); |
| } |
| |
| |
| LIST clause_NumberDelete(LIST List, int Number) |
| /************************************************************** |
| INPUT: A list of clauses and an integer. |
| RETURNS: The same list where the clauses with <Number> are deleted. |
| CAUTION: Destructive. |
| ***************************************************************/ |
| { |
| LIST Scan1,Scan2; |
| |
| for (Scan1 = List; !list_Empty(Scan1); ) |
| if (clause_Number(list_Car(Scan1))==Number) { |
| |
| Scan2 = Scan1; |
| Scan1 = list_Cdr(Scan1); |
| List = list_PointerDeleteOneElement(List, list_Car(Scan2)); |
| } else |
| Scan1 = list_Cdr(Scan1); |
| |
| return List; |
| } |
| |
| |
| static NAT clause_NumberOfMaxLits(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: The number of maximal literals in a clause. |
| ***************************************************************/ |
| { |
| NAT Result,i,n; |
| |
| Result = 0; |
| n = clause_Length(Clause); |
| |
| for (i = clause_FirstAntecedentLitIndex(Clause); i < n; i++) |
| if (clause_LiteralIsMaximal(clause_GetLiteral(Clause,i))) |
| Result++; |
| |
| return Result; |
| } |
| |
| /* Unused ! */ |
| NAT clause_NumberOfMaxAntecedentLits(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: The number of maximal antecedent literals in a clause. |
| ***************************************************************/ |
| { |
| NAT Result,i,n; |
| |
| Result = 0; |
| n = clause_LastAntecedentLitIndex(Clause); |
| |
| for (i = clause_FirstAntecedentLitIndex(Clause); i <= n; i++) |
| if (clause_LiteralIsMaximal(clause_GetLiteral(Clause,i))) |
| Result++; |
| |
| return Result; |
| } |
| |
| |
| void clause_SelectLiteral(CLAUSE Clause, FLAGSTORE Flags) |
| /************************************************************** |
| INPUT: A clause and a flag store. |
| RETURNS: Nothing. |
| EFFECT: If the clause contains more than 2 maximal literals, |
| at least one antecedent literal, the literal with |
| the highest weight is selected. |
| ***************************************************************/ |
| { |
| if (clause_HasSolvedConstraint(Clause) && |
| !clause_GetFlag(Clause,CLAUSESELECT) && |
| clause_NumOfAnteLits(Clause) > 0 && |
| (flag_GetFlagValue(Flags, flag_SELECT) == flag_SELECTALWAYS || |
| (flag_GetFlagValue(Flags, flag_SELECT) == flag_SELECTIFSEVERALMAXIMAL && |
| clause_NumberOfMaxLits(Clause) > 1))) { |
| NAT i,n; |
| LITERAL Lit; |
| |
| n = clause_LastAntecedentLitIndex(Clause); |
| i = clause_FirstAntecedentLitIndex(Clause); |
| Lit = clause_GetLiteral(Clause,i); |
| i++; |
| |
| for ( ; i <= n; i++) |
| if (clause_LiteralWeight(Lit) |
| < clause_LiteralWeight(clause_GetLiteral(Clause,i))) |
| Lit = clause_GetLiteral(Clause,i); |
| |
| clause_LiteralSetFlag(Lit,LITSELECT); |
| clause_SetFlag(Clause,CLAUSESELECT); |
| } |
| } |
| |
| |
| void clause_SetSpecialFlags(CLAUSE Clause, BOOL SortDecreasing, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a flag indicating whether all equations are |
| sort decreasing, a flag store and a precedence. |
| RETURNS: void. |
| EFFECT: If the clause is a sort theory clause and its declaration |
| top symbol is a set declaration sort, i.e., it occurred in a |
| declaration right from the beginning, the paramodulation/superposition |
| steps into the clause are forbidden by setting the |
| NOPARAINTO clause flag |
| ***************************************************************/ |
| { |
| if (SortDecreasing && |
| clause_IsSortTheoryClause(Clause, Flags, Precedence) && |
| symbol_HasProperty(term_TopSymbol(clause_GetLiteralTerm(Clause,clause_FirstSuccedentLitIndex(Clause))), |
| DECLSORT)) |
| clause_SetFlag(Clause,NOPARAINTO); |
| } |
| |
| |
| BOOL clause_ContainsPotPredDef(CLAUSE Clause, FLAGSTORE Flags, |
| PRECEDENCE Precedence, NAT* Index, LIST* Pair) |
| /************************************************************** |
| INPUT: A clause, a flag store, a precedence and a pointer to an index. |
| RETURNS: TRUE iff a succedent literal of the clause is a predicate |
| having only variables as arguments, the predicate occurs only |
| once in the clause and no other variables but the predicates' |
| occur. |
| In that case Index is set to the index of the predicate and |
| Pair contains two lists : the literals for which positive |
| occurrences must be found and a list of literals for which negative |
| occurrences must be found for a complete definition. |
| ***************************************************************/ |
| { |
| NAT i; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_ContainsPotPredDef:"); |
| misc_ErrorReport("\n Illegal input. Input not a clause."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| /* Iterate over all succedent literals */ |
| for (i=clause_FirstSuccedentLitIndex(Clause); i < clause_Length(Clause); i++) { |
| LITERAL lit; |
| TERM atom; |
| LIST pair; |
| |
| lit = clause_GetLiteral(Clause, i); |
| atom = clause_LiteralSignedAtom(lit); |
| if (symbol_IsPredicate(term_TopSymbol(atom))) { |
| LIST l; |
| BOOL ok; |
| ok = TRUE; |
| pair = list_PairCreate(list_Nil(), list_Nil()); |
| |
| /* Make sure all arguments of predicate are variables */ |
| for (l=term_ArgumentList(atom); !list_Empty(l); l=list_Cdr(l)) { |
| if (!term_IsStandardVariable((TERM) list_Car(l))) { |
| ok = FALSE; |
| break; |
| } |
| } |
| if (ok) { |
| /* Make sure predicate occurs only once in clause */ |
| NAT j, count; |
| count = 0; |
| for (j=0; (j < clause_Length(Clause)) && (count < 2); j++) { |
| TERM t; |
| t = clause_GetLiteralAtom(Clause, j); |
| if (symbol_Equal(term_TopSymbol(t), term_TopSymbol(atom))) |
| count++; |
| } |
| if (count > 1) |
| ok = FALSE; |
| } |
| if (ok) { |
| /* Build lists of positive and negative literals */ |
| /* At the same time check if other variables than those among |
| the predicates arguments are found */ |
| NAT j; |
| LIST predvars, vars; |
| predvars = fol_FreeVariables(atom); |
| |
| /* Build list of literals for which positive occurrences are required */ |
| for (j=0; (j < clause_FirstSuccedentLitIndex(Clause)) && ok; j++) { |
| list_Rplaca(pair, list_Cons(clause_GetLiteralAtom(Clause, j), list_PairFirst(pair))); |
| vars = fol_FreeVariables(clause_GetLiteralTerm(Clause, j)); |
| for (l = vars; !list_Empty(l); l = list_Cdr(l)) { |
| if (!term_ListContainsTerm(predvars, list_Car(l))) { |
| ok = FALSE; |
| break; |
| } |
| } |
| list_Delete(vars); |
| } |
| |
| /* Build list of literals for which negative occurrences are required */ |
| for (j = clause_FirstSuccedentLitIndex(Clause); |
| (j < clause_Length(Clause)) && ok; j++) { |
| if (j != i) { |
| list_Rplacd(pair, list_Cons(clause_GetLiteralAtom(Clause, j), list_PairSecond(pair))); |
| vars = fol_FreeVariables(clause_GetLiteralAtom(Clause, j)); |
| for (l=vars; !list_Empty(l); l=list_Cdr(l)) { |
| if (!term_ListContainsTerm(predvars, list_Car(l))) { |
| ok = FALSE; |
| break; |
| } |
| } |
| list_Delete(vars); |
| } |
| } |
| list_Delete(predvars); |
| } |
| |
| if (ok) { |
| *Index = i; |
| *Pair = pair; |
| return TRUE; |
| } |
| else { |
| list_Delete(list_PairFirst(pair)); |
| list_Delete(list_PairSecond(pair)); |
| list_PairFree(pair); |
| } |
| } |
| } |
| return FALSE; |
| } |
| |
| BOOL clause_IsPartOfDefinition(CLAUSE Clause, TERM Predicate, int *Index, |
| LIST Pair) |
| /************************************************************** |
| INPUT: A clause, a term, a pointer to an int and a pair of term lists. |
| RETURNS: TRUE iff the predicate occurs among the negative literals of |
| the clause and the other negative and positive literals are found |
| in the pairs' lists. |
| In that case they are removed from the lists. |
| Index is set to the index of the defined predicate in Clause. |
| ***************************************************************/ |
| { |
| NAT predindex, i; |
| BOOL ok; |
| |
| ok = TRUE; |
| |
| /* Check whether Predicate is among antecedent or constraint literals */ |
| for (predindex=clause_FirstLitIndex(); |
| predindex < clause_FirstSuccedentLitIndex(Clause); |
| predindex++) |
| if (term_Equal(Predicate, clause_GetLiteralAtom(Clause, predindex))) |
| break; |
| if (predindex == clause_FirstSuccedentLitIndex(Clause)) |
| return FALSE; |
| *Index = predindex; |
| |
| /* Check if other negative literals are required for definition */ |
| for (i=clause_FirstLitIndex(); |
| (i < clause_FirstSuccedentLitIndex(Clause)) && ok; i++) { |
| if (i != predindex) |
| if (!term_ListContainsTerm((LIST) list_PairSecond(Pair), |
| clause_GetLiteralAtom(Clause, i))) |
| ok = FALSE; |
| } |
| |
| /* Check if positive literals are required for definition */ |
| for (i=clause_FirstSuccedentLitIndex(Clause); |
| (i < clause_Length(Clause)) && ok; i++) |
| if (!term_ListContainsTerm((LIST) list_PairFirst(Pair), |
| clause_GetLiteralAtom(Clause, i))) |
| ok = FALSE; |
| |
| if (!ok) |
| return FALSE; |
| else { |
| /* Complement for definition found, remove literals from pair lists */ |
| for (i=0; i < clause_FirstSuccedentLitIndex(Clause); i++) |
| if (i != predindex) |
| list_Rplacd(Pair, |
| list_DeleteElement((LIST) list_PairSecond(Pair), |
| clause_GetLiteralAtom(Clause, i), |
| (BOOL (*)(POINTER, POINTER)) term_Equal)); |
| for (i=clause_FirstSuccedentLitIndex(Clause); i < clause_Length(Clause); i++) |
| list_Rplaca(Pair, |
| list_DeleteElement((LIST) list_PairFirst(Pair), |
| clause_GetLiteralAtom(Clause, i), |
| (BOOL (*)(POINTER, POINTER)) term_Equal)); |
| return TRUE; |
| } |
| } |
| |
| void clause_FPrintRule(FILE* File, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A file and a clause. |
| RETURNS: Nothing. |
| SUMMARY: Prints any term of the clause to file in rule format. |
| CAUTION: Uses the term_Output functions. |
| ***************************************************************/ |
| { |
| int i,n; |
| TERM Literal; |
| LIST scan,antecedent,succedent,constraints; |
| |
| n = clause_Length(Clause); |
| |
| constraints = list_Nil(); |
| antecedent = list_Nil(); |
| succedent = list_Nil(); |
| |
| for (i = 0; i < n; i++) { |
| Literal = clause_GetLiteralTerm(Clause,i); |
| if (symbol_Equal(term_TopSymbol(Literal),fol_Not())) { |
| if (symbol_Arity(term_TopSymbol(fol_Atom(Literal))) == 1 && |
| symbol_IsVariable(term_TopSymbol(term_FirstArgument(fol_Atom(Literal))))) |
| constraints = list_Cons(Literal,constraints); |
| else |
| antecedent = list_Cons(Literal,antecedent); |
| } |
| else |
| succedent = list_Cons(Literal,succedent); |
| } |
| |
| for (scan = constraints; !list_Empty(scan); scan = list_Cdr(scan)) { |
| term_FPrint(File, fol_Atom(list_Car(scan))); |
| putc(' ', File); |
| } |
| fputs("||", File); |
| for (scan = antecedent; !list_Empty(scan); scan = list_Cdr(scan)) { |
| putc(' ', File); |
| term_FPrint(File,fol_Atom(list_Car(scan))); |
| if (list_Empty(list_Cdr(scan))) |
| putc(' ', File); |
| } |
| fputs("->", File); |
| for (scan = succedent; !list_Empty(scan); scan = list_Cdr(scan)) { |
| putc(' ', File); |
| term_FPrint(File,list_Car(scan)); |
| } |
| fputs(".\n", File); |
| |
| list_Delete(antecedent); |
| list_Delete(succedent); |
| list_Delete(constraints); |
| } |
| |
| |
| void clause_FPrintOtter(FILE* File, CLAUSE clause) |
| /************************************************************** |
| INPUT: A file and a clause. |
| RETURNS: Nothing. |
| SUMMARY: Prints any clause to File. |
| CAUTION: Uses the other clause_Output functions. |
| ***************************************************************/ |
| { |
| int n,j; |
| LITERAL Lit; |
| TERM Atom; |
| |
| n = clause_Length(clause); |
| |
| if (n == 0) |
| fputs(" $F ", File); |
| else { |
| for (j = 0; j < n; j++) { |
| Lit = clause_GetLiteral(clause,j); |
| Atom = clause_LiteralAtom(Lit); |
| if (clause_LiteralIsNegative(Lit)) |
| putc('-', File); |
| if (fol_IsEquality(Atom)) { |
| if (clause_LiteralIsNegative(Lit)) |
| putc('(', File); |
| term_FPrintOtterPrefix(File,term_FirstArgument(Atom)); |
| fputs(" = ", File); |
| term_FPrintOtterPrefix(File,term_SecondArgument(Atom)); |
| if (clause_LiteralIsNegative(Lit)) |
| putc(')', File); |
| } |
| else |
| term_FPrintOtterPrefix(File,Atom); |
| if (j <= (n-2)) |
| fputs(" | ", File); |
| } |
| } |
| |
| fputs(".\n", File); |
| } |
| |
| |
| void clause_FPrintCnfDFG(FILE* File, BOOL OnlyProductive, LIST Axioms, |
| LIST Conjectures, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A file, a list of axiom clauses and a list of conjecture clauses. |
| A flag indicating whether only potentially productive clauses should |
| be printed. |
| A flag store. |
| A precedence. |
| RETURNS: Nothing. |
| SUMMARY: Prints a the respective clause lists to <File> dependent |
| on <OnlyProductive>. |
| ***************************************************************/ |
| { |
| LIST scan; |
| CLAUSE Clause; |
| |
| if (Axioms) { |
| fputs("list_of_clauses(axioms, cnf).\n", File); |
| for (scan=Axioms;!list_Empty(scan);scan=list_Cdr(scan)) { |
| Clause = (CLAUSE)list_Car(scan); |
| if (!OnlyProductive || |
| (clause_HasSolvedConstraint(Clause) && |
| !clause_HasSelectedLiteral(Clause, Flags, Precedence))) |
| clause_FPrintDFG(File,Clause,FALSE); |
| } |
| fputs("end_of_list.\n\n", File); |
| } |
| |
| if (Conjectures) { |
| fputs("list_of_clauses(conjectures, cnf).\n", File); |
| for (scan=Conjectures;!list_Empty(scan);scan=list_Cdr(scan)) { |
| Clause = (CLAUSE)list_Car(scan); |
| if (!OnlyProductive || |
| (clause_HasSolvedConstraint(Clause) && |
| !clause_HasSelectedLiteral(Clause, Flags, Precedence))) |
| clause_FPrintDFG(File,Clause,FALSE); |
| } |
| fputs("end_of_list.\n\n", File); |
| } |
| } |
| |
| |
| static void clause_FPrintDescription(FILE* File, const char* Name, |
| const char* Author, const char* Status, |
| const char* Description) |
| { |
| fputs("list_of_descriptions.\n", File); |
| fprintf(File, "name(%s).\n", Name); |
| fprintf(File, "author(%s).\n", Author); |
| fprintf(File, "status(%s).\n", Status); |
| fprintf(File, "description(%s).\n", Description); |
| fputs("end_of_list.\n", File); |
| } |
| |
| void clause_FPrintCnfDFGProblem(FILE* File, const char* Name, |
| const char* Author, const char* Status, |
| const char* Description, LIST Clauses) |
| /************************************************************** |
| INPUT: A file, the problems name, author, status and description |
| to be included in the description block given as strings |
| and a list of clauses. |
| RETURNS: Nothing. |
| SUMMARY: Prints a complete DFG problem clause file to <File>. |
| ***************************************************************/ |
| { |
| LIST Scan; |
| |
| fputs("begin_problem(Unknown).\n\n", File); |
| clause_FPrintDescription(File, Name, Author, Status, Description); |
| putc('\n', File); |
| fputs("list_of_symbols.\n", File); |
| fol_FPrintDFGSignature(File); |
| fputs("end_of_list.\n\n", File); |
| fputs("list_of_clauses(axioms, cnf).\n", File); |
| |
| for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| if (!clause_GetFlag(list_Car(Scan),CONCLAUSE)) |
| clause_FPrintDFG(File,list_Car(Scan),FALSE); |
| |
| fputs("end_of_list.\n\n", File); |
| fputs("list_of_clauses(conjectures, cnf).\n", File); |
| |
| for (Scan=Clauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| if (clause_GetFlag(list_Car(Scan),CONCLAUSE)) |
| clause_FPrintDFG(File,list_Car(Scan),FALSE); |
| |
| fputs("end_of_list.\n\n", File); |
| fputs("\nend_problem.\n\n", File); |
| } |
| |
| |
| void clause_FPrintCnfFormulasDFGProblem(FILE* File, BOOL OnlyProductive, |
| const char* Name, const char* Author, |
| const char* Status, |
| const char* Description, LIST Axioms, |
| LIST Conjectures, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A file, a list of axiom clauses and a list of conjecture clauses. |
| A flag indicating whether only potentially productive clauses should |
| be printed. |
| A bunch of strings that are printed to the description. |
| A flag store. |
| A precedence. |
| RETURNS: Nothing. |
| SUMMARY: Prints the respective clause lists as a complete DFG formulae output |
| to <File>. |
| ***************************************************************/ |
| { |
| LIST scan; |
| CLAUSE Clause; |
| |
| fputs("begin_problem(Unknown).\n\n", File); |
| clause_FPrintDescription(File, Name, Author, Status, Description); |
| fputs("\nlist_of_symbols.\n", File); |
| fol_FPrintDFGSignature(File); |
| fputs("end_of_list.\n\n", File); |
| |
| if (Axioms) { |
| fputs("list_of_formulae(axioms).\n", File); |
| for (scan=Axioms; !list_Empty(scan); scan=list_Cdr(scan)) { |
| Clause = (CLAUSE)list_Car(scan); |
| if (!OnlyProductive || |
| (clause_HasSolvedConstraint(Clause) && |
| !clause_HasSelectedLiteral(Clause, Flags, Precedence))) |
| clause_FPrintFormulaDFG(File,Clause,FALSE); |
| } |
| fputs("end_of_list.\n\n", File); |
| } |
| |
| if (Conjectures) { |
| fputs("list_of_formulae(conjectures).\n", File); |
| for (scan=Conjectures; !list_Empty(scan); scan=list_Cdr(scan)) { |
| Clause = (CLAUSE)list_Car(scan); |
| if (!OnlyProductive || |
| (clause_HasSolvedConstraint(Clause) && |
| !clause_HasSelectedLiteral(Clause, Flags, Precedence))) |
| clause_FPrintFormulaDFG(File,Clause,FALSE); |
| } |
| fputs("end_of_list.\n\n", File); |
| } |
| |
| fputs("list_of_settings(SPASS).\n{*\n", File); |
| fol_FPrintPrecedence(File, Precedence); |
| fputs("\n*}\nend_of_list.\n\nend_problem.\n\n", File); |
| } |
| |
| void clause_FPrintCnfOtter(FILE* File, LIST Clauses, FLAGSTORE Flags) |
| /************************************************************** |
| INPUT: A file, a list of clauses and a flag store. |
| RETURNS: Nothing. |
| SUMMARY: Prints the clauses to <File> in a format readable by Otter. |
| ***************************************************************/ |
| { |
| LIST scan; |
| int i; |
| BOOL Equality; |
| CLAUSE Clause; |
| |
| Equality = FALSE; |
| |
| for (scan=Clauses;!list_Empty(scan) && !Equality; scan=list_Cdr(scan)) { |
| Clause = (CLAUSE)list_Car(scan); |
| for (i=clause_FirstAntecedentLitIndex(Clause);i<clause_Length(Clause);i++) |
| if (fol_IsEquality(clause_GetLiteralAtom(Clause,i))) { |
| Equality = TRUE; |
| i = clause_Length(Clause); |
| } |
| } |
| |
| fol_FPrintOtterOptions(File, Equality, |
| flag_GetFlagValue(Flags, flag_TDFG2OTTEROPTIONS)); |
| |
| if (Clauses) { |
| fputs("list(usable).\n", File); |
| if (Equality) |
| fputs("x=x.\n", File); |
| for (scan=Clauses;!list_Empty(scan);scan=list_Cdr(scan)) |
| clause_FPrintOtter(File,list_Car(scan)); |
| fputs("end_of_list.\n\n", File); |
| } |
| } |
| |
| |
| void clause_FPrintCnfDFGDerivables(FILE* File, LIST Clauses, BOOL Type) |
| /************************************************************** |
| INPUT: A file, a list of clauses and a bool flag Type. |
| RETURNS: Nothing. |
| SUMMARY: If <Type> is true then all axiom clauses in <Clauses> are |
| written to <File>. Otherwise all conjecture clauses in |
| <Clauses> are written to <File>. |
| ***************************************************************/ |
| { |
| CLAUSE Clause; |
| |
| while (Clauses) { |
| Clause = (CLAUSE)list_Car(Clauses); |
| if ((Type && !clause_GetFlag(Clause,CONCLAUSE)) || |
| (!Type && clause_GetFlag(Clause,CONCLAUSE))) |
| clause_FPrintDFG(File,Clause,FALSE); |
| Clauses = list_Cdr(Clauses); |
| } |
| } |
| |
| |
| void clause_FPrintDFGStep(FILE* File, CLAUSE Clause, BOOL Justif) |
| /************************************************************** |
| INPUT: A file, a clause and a boolean value. |
| RETURNS: Nothing. |
| SUMMARY: Prints any clause together with a label (the clause number) |
| to File. If <Justif> is TRUE also the labels of the parent |
| clauses are printed. |
| CAUTION: Uses the other clause_Output functions. |
| ***************************************************************/ |
| { |
| int n,j; |
| LITERAL Lit; |
| TERM Atom; |
| LIST Variables,Iter; |
| |
| n = clause_Length(Clause); |
| |
| fputs(" step(", File); |
| fprintf(File, "%d,", clause_Number(Clause)); |
| |
| Variables = list_Nil(); |
| |
| for (j = 0; j < n; j++) |
| Variables = |
| list_NPointerUnion(Variables, |
| term_VariableSymbols(clause_GetLiteralAtom(Clause,j))); |
| |
| if (!list_Empty(Variables)) { |
| symbol_FPrint(File, fol_All()); |
| fputs("([", File); |
| for (Iter = Variables; !list_Empty(Iter); Iter = list_Cdr(Iter)) { |
| symbol_FPrint(File, (SYMBOL) list_Car(Iter)); |
| if (!list_Empty(list_Cdr(Iter))) |
| putc(',', File); |
| } |
| fputs("],", File); |
| } |
| |
| symbol_FPrint(File, fol_Or()); |
| putc('(', File); |
| |
| for (j = 0; j < n; j++) { |
| Lit = clause_GetLiteral(Clause,j); |
| Atom = clause_LiteralSignedAtom(Lit); |
| term_FPrintPrefix(File,Atom); |
| if (j+1 < n) |
| putc(',', File); |
| } |
| if (n==0) |
| symbol_FPrint(File,fol_False()); |
| |
| if (!list_Empty(Variables)) { |
| list_Delete(Variables); |
| putc(')', File); |
| } |
| fputs("),", File); |
| clause_FPrintOrigin(File, Clause); |
| |
| fputs(",[", File); |
| for (Iter = clause_ParentClauses(Clause); |
| !list_Empty(Iter); |
| Iter = list_Cdr(Iter)) { |
| fprintf(File, "%d", (int)list_Car(Iter)); |
| if (!list_Empty(list_Cdr(Iter))) |
| putc(',', File); |
| } |
| putc(']', File); |
| fprintf(File, ",[splitlevel:%d]", clause_SplitLevel(Clause)); |
| |
| fputs(").\n", File); |
| } |
| |
| void clause_FPrintDFG(FILE* File, CLAUSE Clause, BOOL Justif) |
| /************************************************************** |
| INPUT: A file, a clause and a boolean value. |
| RETURNS: Nothing. |
| SUMMARY: Prints any clause together with a label (the clause number) |
| to File. If Justif is TRUE also the labels of the parent |
| clauses are printed. |
| CAUTION: Uses the other clause_Output functions. |
| ***************************************************************/ |
| { |
| int n,j; |
| LITERAL Lit; |
| TERM Atom; |
| LIST Variables,Iter; |
| |
| n = clause_Length(Clause); |
| |
| fputs(" clause(", File); |
| Variables = list_Nil(); |
| |
| for (j = 0; j < n; j++) |
| Variables = |
| list_NPointerUnion(Variables, |
| term_VariableSymbols(clause_GetLiteralAtom(Clause,j))); |
| |
| if (!list_Empty(Variables)) { |
| symbol_FPrint(File, fol_All()); |
| fputs("([", File); |
| for (Iter = Variables; !list_Empty(Iter); Iter = list_Cdr(Iter)) { |
| symbol_FPrint(File, (SYMBOL) list_Car(Iter)); |
| if (!list_Empty(list_Cdr(Iter))) |
| putc(',', File); |
| } |
| fputs("],", File); |
| } |
| |
| symbol_FPrint(File, fol_Or()); |
| putc('(', File); |
| |
| for (j = 0; j < n; j++) { |
| Lit = clause_GetLiteral(Clause,j); |
| Atom = clause_LiteralSignedAtom(Lit); |
| term_FPrintPrefix(File,Atom); |
| if (j+1 < n) |
| putc(',', File); |
| } |
| if (n==0) |
| symbol_FPrint(File,fol_False()); |
| |
| if (!list_Empty(Variables)) { |
| list_Delete(Variables); |
| putc(')', File); |
| } |
| fprintf(File, "),%d", clause_Number(Clause)); |
| |
| if (Justif) { |
| putc(',', File); |
| clause_FPrintOrigin(File, Clause); |
| fputs(",[", File); |
| for (Iter = clause_ParentClauses(Clause); |
| !list_Empty(Iter); |
| Iter = list_Cdr(Iter)) { |
| fprintf(File, "%d", (int)list_Car(Iter)); |
| if (!list_Empty(list_Cdr(Iter))) |
| putc(',', File); |
| } |
| putc(']', File); |
| fprintf(File, ",%d", clause_SplitLevel(Clause)); |
| } |
| |
| fputs(").\n", File); |
| } |
| |
| void clause_FPrintFormulaDFG(FILE* File, CLAUSE Clause, BOOL Justif) |
| /************************************************************** |
| INPUT: A file, a clause and a boolean value. |
| RETURNS: Nothing. |
| SUMMARY: Prints any clause together with a label (the clause number) |
| as DFG Formula to File. If Justif is TRUE also the labels of the |
| parent clauses are printed. |
| CAUTION: Uses the other clause_Output functions. |
| ***************************************************************/ |
| { |
| int n,j; |
| LITERAL Lit; |
| TERM Atom; |
| LIST Variables,Iter; |
| |
| n = clause_Length(Clause); |
| |
| fputs(" formula(", File); |
| Variables = list_Nil(); |
| |
| for (j = 0; j < n; j++) |
| Variables = |
| list_NPointerUnion(Variables, |
| term_VariableSymbols(clause_GetLiteralAtom(Clause,j))); |
| |
| if (!list_Empty(Variables)) { |
| symbol_FPrint(File, fol_All()); |
| fputs("([", File); |
| for (Iter = Variables; !list_Empty(Iter); Iter = list_Cdr(Iter)) { |
| symbol_FPrint(File, (SYMBOL) list_Car(Iter)); |
| if (!list_Empty(list_Cdr(Iter))) |
| putc(',', File); |
| } |
| fputs("],", File); |
| } |
| |
| if (n>1) { |
| symbol_FPrint(File, fol_Or()); |
| putc('(', File); |
| } |
| |
| for (j = 0; j < n; j++) { |
| Lit = clause_GetLiteral(Clause,j); |
| Atom = clause_LiteralSignedAtom(Lit); |
| term_FPrintPrefix(File,Atom); |
| if (j+1 < n) |
| putc(',', File); |
| } |
| if (n==0) |
| symbol_FPrint(File,fol_False()); |
| |
| if (!list_Empty(Variables)) { |
| list_Delete(Variables); |
| putc(')', File); |
| } |
| |
| if (n>1) |
| fprintf(File, "),%d", clause_Number(Clause)); |
| else |
| fprintf(File, ",%d", clause_Number(Clause)); |
| |
| if (Justif) { |
| putc(',', File); |
| clause_FPrintOrigin(File, Clause); |
| fputs(",[", File); |
| for (Iter = clause_ParentClauses(Clause); |
| !list_Empty(Iter); |
| Iter = list_Cdr(Iter)) { |
| fprintf(File, "%d", (int)list_Car(Iter)); |
| if (!list_Empty(list_Cdr(Iter))) |
| putc(',', File); |
| } |
| putc(']', File); |
| fprintf(File, ",%d", clause_SplitLevel(Clause)); |
| } |
| |
| fputs(").\n", File); |
| } |
| |
| |
| void clause_Check(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a flag store and a precedence. |
| RETURNS: Nothing. |
| EFFECT: Checks whether the clause is in a proper state. If |
| not, a core is dumped. |
| ***************************************************************/ |
| { |
| CLAUSE Copy; |
| if (!clause_Exists(Clause)) |
| return; |
| |
| if (!clause_IsClause(Clause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_Check: Clause not consistent !\n"); |
| misc_FinishErrorReport(); |
| } |
| |
| Copy = clause_Copy(Clause); |
| clause_OrientAndReInit(Copy, Flags, Precedence); |
| if ((clause_Weight(Clause) != clause_Weight(Copy)) || |
| (clause_MaxVar(Clause) != clause_MaxVar(Copy))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_Check: Weight or maximal variable not properly set.\n"); |
| misc_FinishErrorReport(); |
| } |
| clause_Delete(Copy); |
| } |
| |
| /* The following are output procedures for clauses with parent pointers */ |
| |
| |
| void clause_PParentsFPrintParentClauses(FILE* File, CLAUSE Clause, BOOL ParentPts) |
| /************************************************************** |
| INPUT: A file, a clause and a boolean flag indicating whether |
| the clause's parents are given by numbers or pointers. |
| RETURNS: Nothing. |
| SUMMARY: Prints the clauses parent clauses and -literals to the file. |
| If <ParentPts> is TRUE the parent clauses are defined |
| by pointers, else by numbers. |
| ***************************************************************/ |
| { |
| LIST Scan1,Scan2; |
| int length; |
| int ParentNum; |
| |
| if (!list_Empty(clause_ParentClauses(Clause))) { |
| |
| Scan1 = clause_ParentClauses(Clause); |
| Scan2 = clause_ParentLiterals(Clause); |
| |
| if (ParentPts) |
| ParentNum = clause_Number(list_Car(Scan1)); |
| else |
| ParentNum = (int)list_Car(Scan1); |
| |
| fprintf(File, "%d.%d", ParentNum, (int)list_Car(Scan2)); |
| |
| if (!list_Empty(list_Cdr(Scan1))) { |
| |
| length = list_Length(Scan1) - 2; |
| putc(',', File); |
| Scan1 = list_Cdr(Scan1); |
| Scan2 = list_Cdr(Scan2); |
| |
| if (ParentPts) |
| ParentNum = clause_Number(list_Car(Scan1)); |
| else |
| ParentNum = (int)list_Car(Scan1); |
| |
| fprintf(File, "%d.%d", ParentNum, (int)list_Car(Scan2)); |
| |
| for (Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2); |
| !list_Empty(Scan1); |
| Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2)) { |
| |
| length -= 2; |
| |
| if (ParentPts) |
| ParentNum = clause_Number(list_Car(Scan1)); |
| else |
| ParentNum = (int)list_Car(Scan1); |
| |
| fprintf(File, ",%d.%d", ParentNum, (int)list_Car(Scan2)); |
| } |
| } |
| } |
| } |
| |
| void clause_PParentsLiteralFPrintUnsigned(FILE* File, LITERAL Literal) |
| /************************************************************** |
| INPUT: A Literal. |
| RETURNS: Nothing. |
| SUMMARY: |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_PParentsLiteralFPrintUnsigned:"); |
| misc_ErrorReport("\n Illegal input. Input not a literal."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_FPrintPrefix(File, clause_LiteralAtom(Literal)); |
| fflush(stdout); |
| } |
| |
| void clause_PParentsFPrintGen(FILE* File, CLAUSE Clause, BOOL ParentPts) |
| /************************************************************** |
| INPUT: A file, a clause, a boolean flag. |
| RETURNS: Nothing. |
| EFFECTS: Prints the clause to file in SPASS format. If <ParentPts> |
| is TRUE, the parents of <Clause> are interpreted as pointers. |
| ***************************************************************/ |
| { |
| LITERAL Lit; |
| int i,c,a,s; |
| |
| if (!clause_Exists(Clause)) |
| fputs("(CLAUSE)NULL", File); |
| else { |
| fprintf(File, "%d",clause_Number(Clause)); |
| |
| fprintf(File, "[%d:", clause_SplitLevel(Clause)); |
| |
| #ifdef CHECK |
| if (Clause->splitfield_length <= 1) |
| fputs("0.", File); |
| else |
| for (i=Clause->splitfield_length-1; i > 0; i--) |
| fprintf(File, "%lu.", Clause->splitfield[i]); |
| if (Clause->splitfield_length == 0) |
| putc('1', File); |
| else |
| fprintf(File, "%lu", (Clause->splitfield[0] | 1)); |
| fprintf(File,":%c%c:%c:%d:%d:", clause_GetFlag(Clause, CONCLAUSE) ? 'C' : 'A', |
| clause_GetFlag(Clause, WORKEDOFF) ? 'W' : 'U', |
| clause_GetFlag(Clause, NOPARAINTO) ? 'N' : 'P', |
| clause_Weight(Clause), clause_Depth(Clause)); |
| #endif |
| |
| clause_FPrintOrigin(File, Clause); |
| |
| if (!list_Empty(clause_ParentClauses(Clause))) { |
| putc(':', File); |
| clause_PParentsFPrintParentClauses(File, Clause, ParentPts); |
| } |
| putc(']', File); |
| |
| c = clause_NumOfConsLits(Clause); |
| a = clause_NumOfAnteLits(Clause); |
| s = clause_NumOfSuccLits(Clause); |
| |
| for (i = 0; i < c; i++) { |
| Lit = clause_GetLiteral(Clause, i); |
| clause_PParentsLiteralFPrintUnsigned(File, Lit); |
| if (i+1 < c) |
| putc(' ', File); |
| } |
| fputs(" || ", File); |
| |
| a += c; |
| for ( ; i < a; i++) { |
| |
| Lit = clause_GetLiteral(Clause, i); |
| clause_PParentsLiteralFPrintUnsigned(File, Lit); |
| if (clause_LiteralIsMaximal(Lit)) { |
| putc('*', File); |
| if (clause_LiteralIsOrientedEquality(Lit)) |
| putc('*', File); |
| } |
| if (clause_LiteralGetFlag(Lit,LITSELECT)) |
| putc('+', File); |
| if (i+1 < a) |
| putc(' ', File); |
| } |
| fputs(" -> ",File); |
| |
| s += a; |
| for ( ; i < s; i++) { |
| |
| Lit = clause_GetLiteral(Clause, i); |
| clause_PParentsLiteralFPrintUnsigned(File, Lit); |
| if (clause_LiteralIsMaximal(Lit)) { |
| putc('*', File); |
| if (clause_LiteralIsOrientedEquality(Lit)) |
| putc('*', File); |
| } |
| #ifdef CHECK |
| if (clause_LiteralGetFlag(Lit, LITSELECT)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In clause_PParentsFPrintGen: Clause has selected positive literal.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| if (i+1 < s) |
| putc(' ', File); |
| } |
| putc('.', File); |
| } |
| } |
| |
| void clause_PParentsFPrint(FILE* File, CLAUSE Clause) |
| /************************************************************** |
| INPUT: A file handle and a clause. |
| RETURNS: Nothing. |
| EFFECTS: Prints out the clause to file in SPASS output format |
| ***************************************************************/ |
| { |
| clause_PParentsFPrintGen(File, Clause, TRUE); |
| } |
| |
| void clause_PParentsListFPrint(FILE* File, LIST L) |
| /************************************************************** |
| INPUT: A file handle, a list of clauses with parent pointers |
| RETURNS: Nothing. |
| EFFECTS: Print the list to <file>. |
| ***************************************************************/ |
| { |
| while (!list_Empty(L)) { |
| clause_PParentsFPrint(File, list_Car(L)); |
| putc('\n', File); |
| L = list_Cdr(L); |
| } |
| } |
| |
| |
| void clause_PParentsPrint(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause with parent pointers |
| RETURNS: Nothing. |
| EFFECTS: The clause is printed to stdout. |
| ***************************************************************/ |
| { |
| clause_PParentsFPrint(stdout, Clause); |
| } |
| |
| void clause_PParentsListPrint(LIST L) |
| /************************************************************** |
| INPUT: A file handle, a list of clauses with parent pointers |
| RETURNS: Nothing. |
| EFFECTS: Print the clause list to stdout. |
| ***************************************************************/ |
| { |
| clause_PParentsListFPrint(stdout, L); |
| } |