| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * UR-RESOLUTION * */ |
| /* * * */ |
| /* * $Module: INFERENCE RULES * */ |
| /* * * */ |
| /* * Copyright (C) 1999, 2000, 2001 MPI fuer Informatik * */ |
| /* * * */ |
| /* * This program is free software; you can redistribute * */ |
| /* * it and/or modify it under the terms of the GNU * */ |
| /* * General Public License as published by the Free * */ |
| /* * Software Foundation; either version 2 of the License, * */ |
| /* * or (at your option) any later version. * */ |
| /* * * */ |
| /* * This program is distributed in the hope that it will * */ |
| /* * be useful, but WITHOUT ANY WARRANTY; without even * */ |
| /* * the implied warranty of MERCHANTABILITY or FITNESS * */ |
| /* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ |
| /* * License for more details. * */ |
| /* * * */ |
| /* * You should have received a copy of the GNU General * */ |
| /* * Public License along with this program; if not, write * */ |
| /* * to the Free Software Foundation, Inc., 59 Temple * */ |
| /* * Place, Suite 330, Boston, MA 02111-1307 USA * */ |
| /* * * */ |
| /* * * */ |
| /* $Revision$ * */ |
| /* $State$ * */ |
| /* $Date$ * */ |
| /* $Author$ * */ |
| /* * * */ |
| /* * Contact: * */ |
| /* * Christoph Weidenbach * */ |
| /* * MPI fuer Informatik * */ |
| /* * Stuhlsatzenhausweg 85 * */ |
| /* * 66123 Saarbruecken * */ |
| /* * Email: weidenb@mpi-sb.mpg.de * */ |
| /* * Germany * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| /* $RCSfile$ */ |
| |
| /**************************************************************/ |
| /* Includes */ |
| /**************************************************************/ |
| |
| #include "rules-ur.h" |
| #include "list.h" |
| |
| |
| static LIST inf_GetURPartnerLits(TERM Atom, LITERAL Lit, |
| BOOL Unit, SHARED_INDEX Index) |
| /************************************************************** |
| INPUT: An atom, a literal, a boolean flag and a SHARED_INDEX. |
| RETURNS: A list of literals with sign complementary to <Lit> |
| that are unifiable with <Atom>. If <Unit> is true, |
| only literals from unit clauses are returned, if <Unit> |
| is false, only literals from non-unit clauses are |
| returned. |
| EFFECT: <Atom> is a copy of <Lit>'s atom where some substitution |
| was applied and equality literals might have been swapped. |
| <Lit> is just needed to check whether the unifiable |
| literals are complementary. |
| ***************************************************************/ |
| { |
| LIST Result, Unifiers, LitScan; |
| LITERAL PLit; |
| int length; |
| |
| Result = list_Nil(); |
| Unifiers = st_GetUnifier(cont_LeftContext(), sharing_Index(Index), |
| cont_RightContext(), Atom); |
| for ( ; !list_Empty(Unifiers); Unifiers = list_Pop(Unifiers)) { |
| if (!term_IsVariable(list_Car(Unifiers))) { |
| for (LitScan = sharing_NAtomDataList(list_Car(Unifiers)); |
| !list_Empty(LitScan); LitScan = list_Cdr(LitScan)) { |
| PLit = list_Car(LitScan); |
| length = clause_Length(clause_LiteralOwningClause(PLit)); |
| if (clause_LiteralsAreComplementary(Lit, PLit) && |
| ((Unit && length==1) || (!Unit && length!=1))) |
| /* The partner literals must have complementary sign and |
| if <Unit> == TRUE they must be from unit clauses, |
| if <Unit> == FALSE they must be from non-unit clauses. */ |
| Result = list_Cons(PLit, Result); |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| static CLAUSE inf_CreateURUnitResolvent(CLAUSE Clause, int i, SUBST Subst, |
| LIST FoundMap, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A non-unit clause, a literal index from the clause, |
| a substitution, a list of pairs (l1, l2) of literals, |
| where l1 is from the non-unit clause and l2 is from a |
| unit clause, a flag store and a precedence. |
| RETURNS: The resolvent of this UR resolution inference. The |
| clause consists of the literal at index <i> in <Clause> |
| after application of <Subst>. |
| EFFECT: The flag store and the precedence are needed to create |
| the new clause. |
| ***************************************************************/ |
| { |
| CLAUSE Result, PClause; |
| LITERAL Lit; |
| TERM Atom; |
| LIST Parents; |
| NAT depth; |
| |
| /* Create atom for resolvent */ |
| Atom = subst_Apply(Subst, term_Copy(clause_GetLiteralAtom(Clause, i))); |
| /* Create clause */ |
| Parents = list_List(Atom); |
| if (i <= clause_LastConstraintLitIndex(Clause)) |
| Result = clause_Create(Parents, list_Nil(), list_Nil(), Flags, Precedence); |
| else if (i <= clause_LastAntecedentLitIndex(Clause)) |
| Result = clause_Create(list_Nil(), Parents, list_Nil(), Flags, Precedence); |
| else |
| Result = clause_Create(list_Nil(), list_Nil(), Parents, Flags, Precedence); |
| list_Delete(Parents); |
| |
| /* Get parent clauses and literals, calculate depth of resolvent */ |
| Parents = list_List(Clause); |
| depth = clause_Depth(Clause); |
| for ( ; !list_Empty(FoundMap); FoundMap = list_Cdr(FoundMap)) { |
| Lit = list_PairSecond(list_Car(FoundMap)); /* Literal from unit */ |
| PClause = clause_LiteralOwningClause(Lit); |
| Parents = list_Cons(PClause, Parents); |
| depth = misc_Max(depth, clause_Depth(PClause)); |
| clause_AddParentClause(Result, clause_Number(PClause)); |
| clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit)); |
| |
| Lit = list_PairFirst(list_Car(FoundMap)); /* Is from <Clause> */ |
| clause_AddParentClause(Result, clause_Number(Clause)); |
| clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit)); |
| } |
| clause_SetFromURResolution(Result); |
| clause_SetDepth(Result, depth+1); |
| clause_SetSplitDataFromList(Result, Parents); |
| list_Delete(Parents); |
| |
| return Result; |
| } |
| |
| |
| static LIST inf_SearchURResolvents(CLAUSE Clause, int i, LIST FoundMap, |
| LIST RestLits, SUBST Subst, |
| SYMBOL GlobalMaxVar, SHARED_INDEX Index, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A non-unit clause, a literal index from <Clause>. |
| <FoundMap> is a list of pairs (l1,l2) of unifiable literals, |
| where l1 is from <Clause> and l2 is from a unit clause. |
| <RestLits> is a list of literals from <Clause> where |
| we haven't found unifiable literals from unit clauses |
| so far. |
| <Subst> is the overall substitution for <Clause> |
| (not for the unit-clauses!). |
| <GlobalMaxVar> is the maximal variable encountered so far. |
| <Index> is used to search unifiable literals. |
| The flag store and the precedence are needed to create |
| the new clauses. |
| RETURNS: A list of UR resolution resolvents. |
| ***************************************************************/ |
| { |
| if (list_Empty(RestLits)) { |
| /* Stop the recursion */ |
| return list_List(inf_CreateURUnitResolvent(Clause, i, Subst, FoundMap, |
| Flags, Precedence)); |
| } else { |
| LITERAL Lit, PLit; |
| SYMBOL NewMaxVar; |
| SUBST NewSubst, RightSubst; |
| TERM AtomCopy, PAtom; |
| LIST Result, Partners; |
| BOOL Swapped; |
| |
| Result = list_Nil(); |
| Swapped = FALSE; |
| /* Choose the unmatched literal with the most symbols */ |
| RestLits = clause_MoveBestLiteralToFront(list_Copy(RestLits), Subst, |
| GlobalMaxVar, |
| clause_HyperLiteralIsBetter); |
| Lit = list_Car(RestLits); |
| RestLits = list_Pop(RestLits); |
| AtomCopy = subst_Apply(Subst, term_Copy(clause_LiteralAtom(Lit))); |
| |
| /* The following 'endless' loop runs twice for equality literals */ |
| /* and only once for other literals. */ |
| while (TRUE) { |
| Partners = inf_GetURPartnerLits(AtomCopy, Lit, TRUE, Index); |
| for ( ; !list_Empty(Partners); Partners = list_Pop(Partners)) { |
| PLit = list_Car(Partners); |
| |
| /* Rename the atom */ |
| PAtom = term_Copy(clause_LiteralAtom(PLit)); |
| term_StartMaxRenaming(GlobalMaxVar); |
| term_Rename(PAtom); |
| /* Get the new global maximal variable */ |
| NewMaxVar = term_MaxVar(PAtom); |
| if (symbol_GreaterVariable(GlobalMaxVar, NewMaxVar)) |
| NewMaxVar = GlobalMaxVar; |
| |
| /* Get the substitution */ |
| cont_Check(); |
| if (!unify_UnifyNoOC(cont_LeftContext(), AtomCopy, |
| cont_RightContext(), PAtom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_SearchURResolvents: Unification failed."); |
| misc_FinishErrorReport(); |
| } |
| subst_ExtractUnifier(cont_LeftContext(), &NewSubst, |
| cont_RightContext(), &RightSubst); |
| cont_Reset(); |
| subst_Delete(RightSubst); /* Forget substitution for unit clause */ |
| term_Delete(PAtom); /* Was just needed to get the substitution */ |
| |
| /* Build the composition of the substitutions */ |
| RightSubst = NewSubst; |
| NewSubst = subst_Compose(NewSubst, subst_Copy(Subst)); |
| subst_Delete(RightSubst); |
| |
| FoundMap = list_Cons(list_PairCreate(Lit, PLit), FoundMap); |
| |
| Result = list_Nconc(inf_SearchURResolvents(Clause,i,FoundMap,RestLits, |
| NewSubst,NewMaxVar,Index, |
| Flags, Precedence), |
| Result); |
| |
| list_PairFree(list_Car(FoundMap)); |
| FoundMap = list_Pop(FoundMap); |
| subst_Delete(NewSubst); |
| } |
| /* loop control */ |
| if (!fol_IsEquality(AtomCopy) || Swapped) |
| break; |
| else { |
| term_EqualitySwap(AtomCopy); |
| Swapped = TRUE; |
| } |
| } |
| /* cleanup */ |
| term_Delete(AtomCopy); |
| list_Delete(RestLits); |
| |
| return Result; |
| } |
| } |
| |
| |
| static LIST inf_NonUnitURResolution(CLAUSE Clause, int SpecialLitIndex, |
| LIST FoundMap, SUBST Subst, |
| SYMBOL GlobalMaxVar, SHARED_INDEX Index, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A non-unit clause, a literal index from <Clause>. |
| <FoundMap> is a list of pairs (l1,l2) of unifiable literals, |
| where l1 is from <Clause> and l2 is from a unit clause. |
| At this point the list has at most one element. |
| <Subst> is the substitution for <Clause>. |
| <GlobalMaxVar> is the maximal variable encountered so far. |
| <Index> is used to search unifiable literals. |
| The flag store and the precedence are needed to create |
| the new clauses. |
| RETURNS: The list of UR resolution resolvents. |
| EFFECT: If inf_URResolution was called with a unit clause, |
| <SpecialLitIndex> is the index of a literal from a non-unit |
| clause, that is unifiable with the unit clause's literal, |
| otherwise it is set to -1. |
| ***************************************************************/ |
| { |
| LIST Result, RestLits; |
| int i, last; |
| |
| Result = list_Nil(); |
| RestLits = clause_GetLiteralListExcept(Clause, SpecialLitIndex); |
| last = clause_LastLitIndex(Clause); |
| for (i = clause_FirstLitIndex(); i <= last; i++) { |
| /* <i> is the index of the literal that remains in the resolvent */ |
| if (i != SpecialLitIndex) { |
| RestLits = list_PointerDeleteOneElement(RestLits, |
| clause_GetLiteral(Clause,i)); |
| |
| Result = list_Nconc(inf_SearchURResolvents(Clause, i, FoundMap, RestLits, |
| Subst, GlobalMaxVar, Index, |
| Flags, Precedence), |
| Result); |
| |
| RestLits = list_Cons(clause_GetLiteral(Clause, i), RestLits); |
| } |
| } |
| list_Delete(RestLits); |
| return Result; |
| } |
| |
| |
| LIST inf_URResolution(CLAUSE Clause, SHARED_INDEX Index, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a shared index, a flag store and a precedence. |
| RETURNS: The list of UR resolution resolvents. |
| EFFECT: The flag store and the precedence are needed to create |
| the resolvents. |
| ***************************************************************/ |
| { |
| LIST Result; |
| |
| if (clause_Length(Clause) != 1) { |
| /* Clause isn't unit clause */ |
| Result = inf_NonUnitURResolution(Clause, -1, list_Nil(), subst_Nil(), |
| clause_MaxVar(Clause), Index, Flags, |
| Precedence); |
| } |
| else { |
| /* Clause is unit clause, so search partner literals in non-unit clauses */ |
| LITERAL Lit, PLit; |
| TERM Atom; |
| LIST Partners, FoundMap; |
| SYMBOL MaxVar, PMaxVar; |
| SUBST LeftSubst, RightSubst; |
| CLAUSE PClause; |
| int PLitInd; |
| BOOL Swapped; |
| |
| Result = list_Nil(); |
| Lit = clause_GetLiteral(Clause, clause_FirstLitIndex()); |
| Atom = term_Copy(clause_LiteralAtom(Lit)); |
| Swapped = FALSE; |
| |
| /* The following 'endless' loop runs twice for equality literals */ |
| /* and only once for other literals. */ |
| while (TRUE) { |
| /* Get complementary literals from non-unit clauses */ |
| Partners = inf_GetURPartnerLits(Atom, Lit, FALSE, Index); |
| |
| for ( ; !list_Empty(Partners); Partners = list_Pop(Partners)) { |
| PLit = list_Car(Partners); |
| PLitInd = clause_LiteralGetIndex(PLit); |
| PClause = clause_LiteralOwningClause(PLit); /* non-unit clause */ |
| |
| PMaxVar = clause_MaxVar(PClause); |
| term_StartMaxRenaming(PMaxVar); |
| term_Rename(Atom); /* Rename atom from unit clause */ |
| MaxVar = term_MaxVar(Atom); |
| if (symbol_GreaterVariable(PMaxVar, MaxVar)) |
| MaxVar = PMaxVar; |
| |
| /* Get the substitution */ |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), clause_LiteralAtom(PLit), |
| cont_RightContext(), Atom); |
| subst_ExtractUnifier(cont_LeftContext(), &LeftSubst, |
| cont_RightContext(), &RightSubst); |
| cont_Reset(); |
| /* We don't need the substitution for the unit clause */ |
| subst_Delete(RightSubst); |
| |
| FoundMap = list_List(list_PairCreate(PLit, Lit)); |
| |
| Result = list_Nconc(inf_NonUnitURResolution(PClause, PLitInd, FoundMap, |
| LeftSubst, MaxVar, Index, |
| Flags, Precedence), |
| Result); |
| |
| list_DeletePairList(FoundMap); |
| subst_Delete(LeftSubst); |
| } |
| /* loop control */ |
| if (!fol_IsEquality(Atom) || Swapped) |
| break; |
| else { |
| term_EqualitySwap(Atom); |
| Swapped = TRUE; |
| } |
| } /* end of endless loop */ |
| term_Delete(Atom); |
| } |
| return Result; |
| } |