| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * TERMINATOR * */ |
| /* * * */ |
| /* * $Module: REDRULES * */ |
| /* * * */ |
| /* * Copyright (C) 1999, 2000, 2001 MPI fuer Informatik * */ |
| /* * * */ |
| /* * This program is free software; you can redistribute * */ |
| /* * it and/or modify it under the terms of the GNU * */ |
| /* * General Public License as published by the Free * */ |
| /* * Software Foundation; either version 2 of the License, * */ |
| /* * or (at your option) any later version. * */ |
| /* * * */ |
| /* * This program is distributed in the hope that it will * */ |
| /* * be useful, but WITHOUT ANY WARRANTY; without even * */ |
| /* * the implied warranty of MERCHANTABILITY or FITNESS * */ |
| /* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ |
| /* * License for more details. * */ |
| /* * * */ |
| /* * You should have received a copy of the GNU General * */ |
| /* * Public License along with this program; if not, write * */ |
| /* * to the Free Software Foundation, Inc., 59 Temple * */ |
| /* * Place, Suite 330, Boston, MA 02111-1307 USA * */ |
| /* * * */ |
| /* * * */ |
| /* $Revision$ * */ |
| /* $State$ * */ |
| /* $Date$ * */ |
| /* $Author$ * */ |
| /* * * */ |
| /* * Contact: * */ |
| /* * Christoph Weidenbach * */ |
| /* * MPI fuer Informatik * */ |
| /* * Stuhlsatzenhausweg 85 * */ |
| /* * 66123 Saarbruecken * */ |
| /* * Email: weidenb@mpi-sb.mpg.de * */ |
| /* * Germany * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| /* $RCSfile$ */ |
| |
| /**************************************************************/ |
| /* Includes */ |
| /**************************************************************/ |
| |
| #include "terminator.h" |
| #include "list.h" |
| |
| |
| static LIST red_GetTerminatorPartnerLits(TERM Atom, LITERAL Lit, |
| BOOL UnitsOnly, LIST IndexList) |
| /************************************************************** |
| INPUT: An atom, a literal, a boolean flag and a list of SHARED_INDEXes. |
| RETURNS: A list of literals with sign complementary to <Lit> |
| that are unifiable with <Atom>. The literals are searched |
| in all SHARED_INDEXes from <IndexList>. Additionally, |
| if <Unitsonly> is true, only literals from unit clauses |
| are returned. |
| EFFECT: <Atom> is a copy of <Lit> where some substitution |
| was applied and equality literals might have been swapped. |
| <Lit> is just needed to check whether the unifiable |
| literals are complementary. |
| ***************************************************************/ |
| { |
| LIST Result, Unifiers, LitScan; |
| LITERAL NextLit; |
| |
| Result = list_Nil(); |
| for ( ; !list_Empty(IndexList); IndexList = list_Cdr(IndexList)) { |
| Unifiers = st_GetUnifier(cont_LeftContext(), |
| sharing_Index(list_Car(IndexList)), |
| cont_RightContext(), Atom); |
| for ( ; !list_Empty(Unifiers); Unifiers = list_Pop(Unifiers)) { |
| if (!term_IsVariable(list_Car(Unifiers))) { |
| for (LitScan = sharing_NAtomDataList(list_Car(Unifiers)); |
| !list_Empty(LitScan); LitScan = list_Cdr(LitScan)) { |
| NextLit = list_Car(LitScan); |
| if (clause_LiteralsAreComplementary(Lit, NextLit) && |
| (!UnitsOnly || clause_Length(clause_LiteralOwningClause(NextLit))==1)) |
| /* The partner literals must have complementary sign and |
| if <UnitsOnly> == TRUE they must be from unit clauses. */ |
| Result = list_Cons(NextLit, Result); |
| } |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| static CLAUSE red_CreateTerminatorEmptyClause(LIST FoundMap, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A list of pairs (l1, l2), where l1 and l2 are unifiable |
| literals with complementary sign and a flag store. |
| More accurately, a substitution s exists, |
| such that l1 s = l2 s for all pairs (l1,l2) in |
| <FoundMap>. |
| For all literals l from the involved clauses |
| there exists one pair (l1,l2) in <FoundMap> |
| with l1=l or l2=l. |
| The flags store and the precedence are needed to create |
| the new clause. |
| RETURNS: A newly created empty clause, where the data |
| (parents,...) is set according to <FoundMap>. |
| ***************************************************************/ |
| { |
| CLAUSE Result, PClause; |
| LITERAL Lit; |
| LIST Parents; |
| NAT depth; |
| |
| Result = clause_Create(list_Nil(), list_Nil(), list_Nil(), Flags, Precedence); |
| Parents = list_Nil(); |
| depth = 0; |
| for (; !list_Empty(FoundMap); FoundMap = list_Cdr(FoundMap)) { |
| Lit = list_PairSecond(list_Car(FoundMap)); |
| PClause = clause_LiteralOwningClause(Lit); |
| Parents = list_Cons(PClause, Parents); |
| depth = misc_Max(depth, clause_Depth(PClause)); |
| clause_AddParentClause(Result, clause_Number(PClause)); |
| clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit)); |
| |
| Lit = list_PairFirst(list_Car(FoundMap)); |
| PClause = clause_LiteralOwningClause(Lit); |
| Parents = list_Cons(PClause, Parents); |
| depth = misc_Max(depth, clause_Depth(PClause)); |
| clause_AddParentClause(Result, clause_Number(PClause)); |
| clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit)); |
| } |
| clause_SetFromTerminator(Result); |
| clause_SetDepth(Result, depth+1); |
| clause_SetSplitDataFromList(Result, Parents); |
| list_Delete(Parents); |
| return Result; |
| } |
| |
| |
| static BOOL red_TerminatorLitIsBetter(LITERAL L1, NAT S1, LITERAL L2, NAT S2) |
| /************************************************************** |
| INPUT: Two literals and its sizes wrt. some substitution. |
| RETURNS: TRUE, if <L1> is 'better' than <L2>, FALSE otherwise. |
| EFFECT: 1. Positive literals are 'better' than negative literals |
| 2. If both literals have the same sign, the bigger literal |
| is better. |
| This is an heuristic that has shown to be useful in practice. |
| This function is used as parameter for the function |
| clause_MoveBestLiteralToFront. |
| ***************************************************************/ |
| { |
| if ((clause_LiteralIsNegative(L2) && clause_LiteralIsPositive(L1)) || |
| /* The following conditions do the same as this condition: */ |
| /* (!clause_LiteralsAreComplementary(L1, L2) && S1 > S2) */ |
| (clause_LiteralIsPositive(L1) && S1 > S2) || |
| (clause_LiteralIsNegative(L2) && S1 > S2)) |
| return TRUE; |
| else |
| return FALSE; |
| } |
| |
| |
| static CLAUSE red_SearchTerminator(NAT n, LIST RestLits, LIST FoundMap, |
| SUBST Subst, SYMBOL GlobalMaxVar, |
| LIST IndexList, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A natural number, a list of literals, a list of pairs, |
| a substitution, the maximum variable occurring in all |
| involved clauses, a list of SHARED_INDEXes, a flag store |
| and a precedence. |
| RETURNS: An empty clause, if a terminator situation was found, |
| NULL otherwise. |
| EFFECT: This recursive function implements the search for |
| a terminator situation with at most <n> non-unit clauses. |
| <RestLits> is the lists of literals actually missing |
| a complementary partner literal. |
| <FoundMap> is a list of pairs (l1,l2), where l1 and l2 |
| are complementary, unifiable literals. |
| <Subst> is the common substitution of all those pairs. |
| <GlobalMaxVar> is the maximum variable from all |
| involved clauses. |
| To enable the search all involved clauses are made |
| variable-disjoint. |
| At the moment the function stops, if ANY terminator |
| situation occurred. This might not be desirable |
| if splitting is enabled, since there might be other |
| terminator situations resulting in an empty clause |
| of lower split level. |
| The flag store and the precedence are needed to create |
| the new clause. |
| ***************************************************************/ |
| { |
| if (list_Empty(RestLits)) { |
| /* We found a terminator situation, so stop the recursion */ |
| return red_CreateTerminatorEmptyClause(FoundMap, Flags, Precedence); |
| } else { |
| CLAUSE Result, PClauseCopy; |
| LITERAL Lit, PLit; |
| SYMBOL NewMaxVar; |
| SUBST NewSubst, RightSubst; |
| TERM AtomCopy; |
| LIST ClashList, ToDoList; |
| BOOL Swapped; |
| NAT Limit; |
| int PLitInd; |
| |
| Swapped = FALSE; |
| Result = clause_Null(); |
| clause_MoveBestLiteralToFront(RestLits, Subst, GlobalMaxVar, |
| red_TerminatorLitIsBetter); |
| Lit = list_Car(RestLits); |
| RestLits = list_Cdr(RestLits); |
| AtomCopy = subst_Apply(Subst, term_Copy(clause_LiteralAtom(Lit))); |
| |
| /* The following 'endless' loop runs twice for equality literals */ |
| /* and only once for other literals. */ |
| while (TRUE) { |
| ClashList = red_GetTerminatorPartnerLits(AtomCopy, Lit, n==0, IndexList); |
| for (; !list_Empty(ClashList) && Result==NULL; |
| ClashList = list_Pop(ClashList)) { |
| PLit = list_Car(ClashList); |
| PLitInd = clause_LiteralGetIndex(PLit); |
| PClauseCopy = clause_Copy(clause_LiteralOwningClause(PLit)); |
| Limit = clause_Length(PClauseCopy) == 1 ? n : n-1; |
| |
| clause_RenameVarsBiggerThan(PClauseCopy, GlobalMaxVar); |
| |
| PLit = clause_GetLiteral(PClauseCopy, PLitInd); |
| FoundMap = list_Cons(list_PairCreate(Lit, PLit), FoundMap); |
| ToDoList = clause_GetLiteralListExcept(PClauseCopy, PLitInd); |
| ToDoList = list_Nconc(ToDoList, list_Copy(RestLits)); |
| |
| NewMaxVar = clause_SearchMaxVar(PClauseCopy); |
| if (symbol_GreaterVariable(GlobalMaxVar, NewMaxVar)) |
| NewMaxVar = GlobalMaxVar; |
| |
| cont_Check(); |
| if (!unify_UnifyNoOC(cont_LeftContext(), AtomCopy, |
| cont_RightContext(), clause_LiteralAtom(PLit))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In red_SearchTerminator: Unification failed."); |
| misc_FinishErrorReport(); |
| } |
| subst_ExtractUnifier(cont_LeftContext(), &NewSubst, |
| cont_RightContext(), &RightSubst); |
| cont_Reset(); |
| |
| /* The domains of both substitutions are disjoint */ |
| /* so we do just a simple union operation. */ |
| NewSubst = subst_NUnion(NewSubst, RightSubst); |
| RightSubst = NewSubst; |
| NewSubst = subst_Compose(NewSubst, subst_Copy(Subst)); |
| subst_Delete(RightSubst); |
| |
| Result = red_SearchTerminator(Limit, ToDoList, FoundMap, NewSubst, |
| NewMaxVar, IndexList, Flags, Precedence); |
| |
| clause_Delete(PClauseCopy); |
| subst_Delete(NewSubst); |
| list_Delete(ToDoList); |
| list_PairFree(list_Car(FoundMap)); |
| FoundMap = list_Pop(FoundMap); |
| } |
| /* loop control */ |
| if (!fol_IsEquality(AtomCopy) || Swapped || Result!=NULL) |
| break; |
| else { |
| list_Delete(ClashList); |
| term_EqualitySwap(AtomCopy); |
| Swapped = TRUE; |
| } |
| } |
| /* cleanup */ |
| term_Delete(AtomCopy); |
| /* <ClashList> may be non-empty since the loop stops */ |
| /* if a terminator was found. */ |
| list_Delete(ClashList); |
| |
| return Result; |
| } |
| } |
| |
| |
| CLAUSE red_Terminator(CLAUSE RedClause, NAT n, SHARED_INDEX WoIndex, |
| SHARED_INDEX UsIndex, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, two shared indexes, a number <n> |
| restricting the number of non-unit clauses in |
| a possible terminator situation, a flag store |
| and a precedence. |
| RETURNS: An empty clause if a terminator with at most <n> |
| non-unit clauses is found, NULL otherwise. |
| EFFECT: See also description of red_SearchTerminator. |
| ***************************************************************/ |
| { |
| LIST Rest, IndexList; |
| CLAUSE Result; |
| |
| if (clause_Length(RedClause) > 1) /* non-unit clause */ |
| n--; |
| |
| /* Pass the indexes as a list to sub-functions */ |
| IndexList = list_Cons(WoIndex, list_List(UsIndex)); |
| Rest = clause_GetLiteralList(RedClause); |
| Result = red_SearchTerminator(n, Rest, list_Nil(), subst_Nil(), |
| clause_MaxVar(RedClause), IndexList, Flags, |
| Precedence); |
| |
| /* cleanup */ |
| list_Delete(IndexList); |
| list_Delete(Rest); |
| |
| return Result; |
| } |