| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * INFERENCE RULES FOR SORTS * */ |
| /* * * */ |
| /* * $Module: SORTRULES * */ |
| /* * * */ |
| /* * 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$ */ |
| |
| /**************************************************************/ |
| /* Includes */ |
| /**************************************************************/ |
| |
| #include "rules-sort.h" |
| |
| |
| /**************************************************************/ |
| /* Functions */ |
| /**************************************************************/ |
| |
| static LIST inf_GetForwardPartnerLits(LITERAL, st_INDEX); |
| static SORT inf_GetSortFromLits(LIST, SORTTHEORY); |
| |
| |
| static BOOL inf_SubsortPrecheck(CLAUSE Clause, LIST TLits, LITERAL Special, |
| st_INDEX Index, SORTTHEORY SortTheory) |
| /************************************************************** |
| INPUT: A clause, a list of constraint literal indices in |
| that clause, a special literal, an index of clauses, |
| and the actual sort theory. |
| RETURNS: TRUE, if there exists any subsort of the <TLits> sort. |
| ***************************************************************/ |
| { |
| SORT tSort, unifierSort; |
| LIST unifiers; |
| BOOL result; |
| |
| unifiers = inf_GetForwardPartnerLits(clause_GetLiteral(Clause,(int)list_Car(TLits)), |
| Index); |
| unifierSort = inf_GetSortFromLits(unifiers, SortTheory); |
| list_Delete(unifiers); |
| |
| tSort = sort_TopSort(); |
| for (; !list_Empty(TLits); TLits = list_Cdr(TLits)) { |
| TERM actAtom = clause_GetLiteralAtom(Clause, (int)list_Car(TLits)); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(actAtom)), |
| tSort); |
| } |
| tSort = list_PointerDeleteDuplicates(tSort); |
| |
| if (Special == NULL) |
| result = sort_TheoryIsSubsortOf(SortTheory, unifierSort, tSort); |
| else { |
| SORT extraSort; |
| extraSort = sort_TheorySortOfSymbol(SortTheory, clause_LiteralPredicate(Special)); |
| result = sort_TheoryIsSubsortOfExtra(SortTheory, extraSort, unifierSort, tSort); |
| sort_Delete(extraSort); |
| } |
| |
| sort_Delete(tSort); |
| sort_Delete(unifierSort); |
| |
| return result; |
| } |
| |
| static LIST inf_GetSortResolutionPartnerLits(TERM Atom, st_INDEX Index) |
| /************************************************************** |
| INPUT: A clause, and an Index of clauses. |
| RETURNS: A list of literals with which sortresolution is possible. |
| MEMORY: Allocates memory for the list. |
| ***************************************************************/ |
| { |
| LIST Result, TermList, LitScan; |
| LITERAL NextLit; |
| CLAUSE Clause; |
| |
| #ifdef CHECK |
| if (!term_IsAtom(Atom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GetSortResolutionPartnerLits: Variable as atom input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| TermList = st_GetUnifier(cont_LeftContext(), Index, cont_RightContext(), Atom); |
| |
| for ( ; !list_Empty(TermList); TermList = list_Pop(TermList)) { |
| |
| if (term_IsAtom(list_Car(TermList))) { |
| |
| for (LitScan = sharing_NAtomDataList(list_Car(TermList)); |
| !list_Empty(LitScan); |
| LitScan = list_Cdr(LitScan)){ |
| NextLit = list_Car(LitScan); |
| Clause = clause_LiteralOwningClause(NextLit); |
| |
| if (clause_LiteralIsPositive(NextLit) && |
| clause_LiteralGetFlag(NextLit,STRICTMAXIMAL) && |
| clause_GetFlag(Clause, WORKEDOFF) && |
| clause_HasSolvedConstraint(Clause) && |
| !list_PointerMember(Result, NextLit)) |
| Result = list_Cons(NextLit, Result); |
| } |
| } |
| } |
| |
| return Result; |
| } |
| |
| |
| static CLAUSE inf_BuildConstraintHyperResolvent(CLAUSE Clause, LIST Lits, |
| SUBST Subst, LIST Foundlits, |
| FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A <Clause> where the sort constraint is resolved, |
| a list <Lits> of constraint indices in <Clause> where |
| all corresponding constraints have the same term, |
| the overall substitution <Subst>, |
| a list <Foundlits> of literals of found partner clauses, |
| a flag store and a precedence. |
| RETURNS: A clause, the resolvent of a resolution step. |
| ***************************************************************/ |
| { |
| CLAUSE NewClause, ClauseCopy; |
| LIST Constraint, Antecedent, Succedent, ParentCls, ParentLits, Scan; |
| TERM Atom; |
| SYMBOL MaxVar,MaxCand; |
| int i,bound, depth; |
| BOOL IsFromEmptySort; |
| LIST Partners; |
| |
| ParentCls = list_Nil(); |
| ParentLits = list_Nil(); |
| Constraint = list_Nil(); |
| Antecedent = list_Nil(); |
| Succedent = list_Nil(); |
| Partners = list_Nil(); |
| depth = clause_Depth(Clause); |
| |
| for (Scan=Foundlits; !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| depth = misc_Max(depth, |
| clause_Depth(clause_LiteralOwningClause(list_Car(Scan)))); |
| |
| ClauseCopy = clause_Copy(Clause); |
| Partners = list_Cons(ClauseCopy, Partners); |
| clause_SubstApply(Subst, ClauseCopy); |
| |
| IsFromEmptySort = term_IsVariable(term_FirstArgument( |
| clause_GetLiteralAtom(Clause, (int)list_Car(Lits)))); |
| |
| bound = clause_LastConstraintLitIndex(ClauseCopy); |
| |
| for (i = clause_FirstLitIndex(); i <= bound; i++) |
| if (!list_PointerMember(Lits, (POINTER)i)) { |
| Atom = term_Copy(clause_GetLiteralAtom(ClauseCopy, i)); |
| Constraint = list_Cons(Atom, Constraint); |
| } |
| else { |
| ParentCls = list_Cons((POINTER)clause_Number(ClauseCopy), ParentCls); |
| ParentLits = list_Cons((POINTER)i, ParentLits); |
| } |
| |
| bound = clause_LastAntecedentLitIndex(ClauseCopy); |
| for ( ; i <= bound; i++) { |
| Atom = term_Copy(clause_GetLiteralAtom(ClauseCopy, i)); |
| Antecedent = list_Cons(Atom, Antecedent); |
| } |
| bound = clause_LastSuccedentLitIndex(ClauseCopy); |
| for (; i <= bound; i++) { |
| Atom = term_Copy(clause_GetLiteralAtom(ClauseCopy, i)); |
| Succedent = list_Cons(Atom, Succedent); |
| } |
| bound = clause_LastConstraintLitIndex(Clause); |
| for (i = clause_FirstLitIndex(); i <= bound; i++) { |
| /* Hier sollen die gematchten Constraintliterale dazu fuehren, dass die */ |
| /* c,a und s- literale der Partnerclauses in die Listen kommen... */ |
| |
| if (list_PointerMember(Lits, (POINTER)i)) { |
| CLAUSE PartnerCopy; |
| LITERAL PLit; |
| TERM PAtom; |
| SUBST NewSubst,RightSubst; |
| int j,lc,la,n,PLitInd; |
| |
| Atom = clause_GetLiteralAtom(ClauseCopy, i); |
| NewClause = clause_CreateUnnormalized(Constraint, Antecedent, Succedent); |
| |
| list_Delete(Constraint); |
| list_Delete(Antecedent); |
| list_Delete(Succedent); |
| Constraint = list_Nil(); |
| Antecedent = list_Nil(); |
| Succedent = list_Nil(); |
| |
| /* Find corresponding Foundlit: */ |
| for (Scan = Foundlits; |
| term_TopSymbol(Atom) != |
| term_TopSymbol(clause_LiteralAtom(list_Car(Scan))); |
| Scan = list_Cdr(Scan)); |
| PLit = list_Car(Scan); |
| PLitInd = clause_LiteralGetIndex(PLit); |
| PartnerCopy = clause_Copy(clause_LiteralOwningClause(PLit)); |
| Partners = list_Cons(PartnerCopy, Partners); |
| ParentCls = list_Cons((POINTER)clause_Number(PartnerCopy), ParentCls); |
| ParentLits = list_Cons((POINTER)PLitInd, ParentLits); |
| MaxVar = clause_SearchMaxVar(ClauseCopy); |
| MaxCand = clause_SearchMaxVar(NewClause); |
| MaxVar = ((MaxVar > MaxCand) ? MaxVar : MaxCand); |
| /* MaxVar is the maximal variable in the new clause or the ClauseCopy, */ |
| /* the latter to guarantee the stability of variable names. */ |
| |
| clause_RenameVarsBiggerThan(PartnerCopy, MaxVar); |
| PLit = clause_GetLiteral(PartnerCopy, PLitInd); |
| PAtom = clause_LiteralAtom(PLit); |
| |
| cont_Check(); |
| if (!unify_UnifyNoOC(cont_LeftContext(), PAtom, cont_RightContext(), Atom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BuildConstraintHyperResolvent: Unification failed."); |
| misc_FinishErrorReport(); |
| } |
| subst_ExtractUnifier(cont_LeftContext(), &RightSubst, cont_RightContext(), &NewSubst); |
| cont_Reset(); |
| |
| clause_SubstApply(NewSubst, NewClause); |
| clause_SubstApply(NewSubst, ClauseCopy); |
| subst_Delete(NewSubst); |
| |
| n = clause_Length(PartnerCopy); |
| lc = clause_LastConstraintLitIndex(PartnerCopy); |
| la = clause_LastAntecedentLitIndex(PartnerCopy); |
| for (j = clause_FirstLitIndex(); j < n; j++) { |
| if (j <= lc) |
| Constraint = list_Cons(subst_Apply(RightSubst, |
| term_Copy(clause_GetLiteralAtom(PartnerCopy, j))), |
| Constraint); |
| else if (j <= la) |
| Antecedent = list_Cons(subst_Apply(RightSubst, |
| term_Copy(clause_GetLiteralAtom(PartnerCopy, j))), |
| Antecedent); |
| else if (j != PLitInd) |
| Succedent = list_Cons(subst_Apply(RightSubst, |
| term_Copy(clause_GetLiteralAtom(PartnerCopy, j))), |
| Succedent); |
| } |
| |
| subst_Delete(RightSubst); |
| |
| n = clause_Length(NewClause); |
| lc = clause_LastConstraintLitIndex(NewClause); |
| la = clause_LastAntecedentLitIndex(NewClause); |
| |
| for (j = clause_FirstLitIndex(); j < n; j++) { |
| if (j <= lc) |
| Constraint = list_Cons(term_Copy(clause_GetLiteralAtom(NewClause, j)), |
| Constraint); |
| else if (j <= la) |
| Antecedent = list_Cons(term_Copy(clause_GetLiteralAtom(NewClause, j)), |
| Antecedent); |
| else |
| Succedent = list_Cons(term_Copy(clause_GetLiteralAtom(NewClause, j)), |
| Succedent); |
| } |
| clause_Delete(NewClause); |
| clause_DecreaseCounter(); |
| } |
| } |
| NewClause = clause_Create(Constraint, Antecedent, Succedent, Flags,Precedence); |
| |
| list_Delete(Constraint); |
| list_Delete(Antecedent); |
| list_Delete(Succedent); |
| |
| if (IsFromEmptySort) |
| clause_SetFromEmptySort(NewClause); |
| else |
| clause_SetFromSortResolution(NewClause); |
| |
| clause_SetDepth(NewClause, depth + 1); |
| |
| clause_SetSplitDataFromList(NewClause, Partners); |
| clause_DeleteClauseList(Partners); |
| |
| clause_SetParentClauses(NewClause, list_NReverse(ParentCls)); |
| clause_SetParentLiterals(NewClause, list_NReverse(ParentLits)); |
| |
| return NewClause; |
| } |
| |
| |
| static LIST inf_ConstraintHyperResolvents(CLAUSE Clause, LIST Lits, |
| SUBST Subst, LIST Restlits, |
| LIST Foundlits, st_INDEX Index, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A <Clause> where the sort constraint is resolved, |
| a list <Lits> of constraint indices in <Clause> where |
| all corresponding constraints have the same term, |
| the overall substitution <Subst>, |
| a list <Restlits> of constraint indeces for which |
| a partner clause is searched with respect to <Index>, |
| a list <Foundlits> of literals of already found partner clauses, |
| a flag store and a precedence. |
| RETURNS: The list of possible resolvents. |
| ***************************************************************/ |
| { |
| if (list_Empty(Restlits)) |
| return list_List(inf_BuildConstraintHyperResolvent(Clause,Lits,Subst, |
| Foundlits, Flags, |
| Precedence)); |
| else { |
| CLAUSE PartnerCopy; |
| LITERAL Lit, PLit; |
| LIST Result, NextLits; |
| TERM AtomCopy; |
| SUBST NewSubst, RightSubst, HelpSubst; |
| SYMBOL MaxVar, MaxCand; |
| int PLitInd; |
| |
| Result = list_Nil(); |
| Lit = clause_GetLiteral(Clause, (int) list_Car(Restlits)); |
| AtomCopy = subst_Apply(Subst, term_Copy(clause_LiteralAtom(Lit))); |
| NextLits = inf_GetSortResolutionPartnerLits(AtomCopy,Index); |
| MaxVar = clause_MaxVar(Clause); |
| MaxCand = clause_AtomMaxVar(AtomCopy); |
| MaxVar = (symbol_GreaterVariable(MaxVar, MaxCand) ? MaxVar : MaxCand); |
| |
| for ( ; !list_Empty(NextLits); NextLits = list_Pop(NextLits)) { |
| PLit = list_Car(NextLits); |
| PLitInd = clause_LiteralGetIndex(PLit); |
| Foundlits = list_Cons(PLit, Foundlits); |
| PartnerCopy = clause_Copy(clause_LiteralOwningClause(PLit)); |
| |
| clause_RenameVarsBiggerThan(PartnerCopy, MaxVar); |
| PLit = clause_GetLiteral(PartnerCopy, PLitInd); |
| |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), AtomCopy, |
| cont_RightContext(), clause_LiteralAtom(PLit)); |
| subst_ExtractUnifier(cont_LeftContext(), &NewSubst, cont_RightContext(), &RightSubst); |
| cont_Reset(); |
| |
| subst_Delete(RightSubst); |
| HelpSubst = NewSubst; |
| NewSubst = subst_Compose(NewSubst, subst_Copy(Subst)); |
| |
| Result = list_Nconc(inf_ConstraintHyperResolvents(Clause, Lits, NewSubst, |
| list_Cdr(Restlits), |
| Foundlits, Index, Flags, |
| Precedence), |
| Result); |
| subst_Delete(NewSubst); |
| subst_Delete(HelpSubst); |
| clause_Delete(PartnerCopy); |
| |
| Foundlits = list_Pop(Foundlits); |
| } |
| term_Delete(AtomCopy); |
| |
| return Result; |
| } |
| } |
| |
| |
| LIST inf_BackwardSortResolution(CLAUSE GivenClause, st_INDEX Index, |
| SORTTHEORY SortTheory, BOOL Precheck, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with a solved sort constraint, an index of clauses, |
| a sort theory, a boolean flag indicating whether the subsort |
| precheck can be applied, a flag store and a precedence. |
| RETURNS: A list of clauses inferred from the GivenClause by |
| SortResolution with the given clause. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST result; |
| int i, ls; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence) || |
| !clause_HasSolvedConstraint(GivenClause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BackwardSortResolution: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| result = list_Nil(); |
| ls = clause_LastSuccedentLitIndex(GivenClause); |
| |
| for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= ls; i++) { |
| LITERAL pLit; |
| TERM pAtom; |
| |
| pLit = clause_GetLiteral(GivenClause, i); |
| pAtom = clause_LiteralAtom(pLit); |
| |
| if (clause_LiteralGetFlag(pLit,STRICTMAXIMAL) && |
| clause_LiteralIsSort(pLit)) { |
| LIST termList; |
| termList = st_GetUnifier(cont_LeftContext(),Index,cont_RightContext(),pAtom); |
| |
| for ( ; !list_Empty(termList); termList = list_Pop(termList)){ |
| if (term_IsAtom(list_Car(termList)) && |
| !term_IsVariable(term_FirstArgument(list_Car(termList)))) { |
| |
| LIST litScan; |
| litScan = sharing_NAtomDataList(list_Car(termList)); |
| for ( ; !list_Empty(litScan); litScan = list_Cdr(litScan)) { |
| LITERAL gLit; |
| CLAUSE gClause; |
| gLit = list_Car(litScan); |
| gClause = clause_LiteralOwningClause(gLit); |
| if (clause_LiteralGetIndex(gLit) < clause_FirstAntecedentLitIndex(gClause) && |
| clause_GetFlag(gClause,WORKEDOFF)) { |
| TERM gAtom; |
| int lc, gi, j; |
| LIST tLits, restLits; |
| gAtom = clause_LiteralAtom(gLit); |
| lc = clause_LastConstraintLitIndex(gClause); |
| gi = clause_LiteralGetIndex(gLit); |
| tLits = list_List((POINTER)gi); |
| restLits = list_Nil(); |
| for (j = clause_FirstLitIndex(); j <= lc; j++) { |
| LITERAL tCand; |
| tCand = clause_GetLiteral(gClause, j); |
| if (j != gi && |
| term_FirstArgument(clause_LiteralAtom(tCand)) |
| == term_FirstArgument(gAtom)) { |
| tLits = list_Cons((POINTER)j, tLits); |
| restLits = list_Cons((POINTER)j, restLits); |
| } |
| } |
| |
| if (!Precheck || |
| inf_SubsortPrecheck(gClause,tLits,pLit,Index,SortTheory)) { |
| CLAUSE pClauseCopy; |
| SYMBOL minVar; |
| LIST foundLits; |
| SUBST leftSubst, rightSubst; |
| pClauseCopy = clause_Copy(GivenClause); |
| minVar = clause_MaxVar(gClause); |
| foundLits = list_List(pLit); |
| |
| clause_RenameVarsBiggerThan(pClauseCopy, minVar); |
| pAtom = clause_GetLiteralAtom(pClauseCopy, i); |
| /* set, to unify correctly! */ |
| |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), gAtom, cont_RightContext(), pAtom); |
| subst_ExtractUnifier(cont_LeftContext(), &leftSubst, |
| cont_RightContext(), &rightSubst); |
| cont_Reset(); |
| |
| subst_Delete(rightSubst); |
| |
| result = |
| list_Nconc(inf_ConstraintHyperResolvents(gClause, tLits, |
| leftSubst, restLits, |
| foundLits, Index, |
| Flags, Precedence), |
| result); |
| |
| pAtom = clause_LiteralAtom(pLit); |
| |
| subst_Delete(leftSubst); |
| list_Delete(foundLits); |
| clause_Delete(pClauseCopy); |
| } /* if Precheck */ |
| list_Delete(tLits); |
| list_Delete(restLits); |
| } |
| } |
| } |
| } |
| } |
| } |
| return result; |
| } |
| |
| |
| LIST inf_ForwardSortResolution(CLAUSE GivenClause, st_INDEX Index, |
| SORTTHEORY SortTheory, BOOL Precheck, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with an unsolved sort constraint, an index of clauses, |
| a sort theory, a boolean flag indicating whether the subsort |
| precheck can be applied, a flag store and a precedence. |
| RETURNS: A list of clauses inferred from the GivenClause by |
| SortResolution on the given clause. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, TLits, RestLits; |
| int i, j, lc; |
| BOOL Hit; |
| TERM TAtom; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence) || |
| !clause_HasTermSortConstraintLits(GivenClause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_ForwardSortResolution: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| lc = clause_LastConstraintLitIndex(GivenClause); |
| Hit = FALSE; |
| |
| i = clause_FirstLitIndex(); |
| while (i <= lc && !Hit) { |
| TAtom = clause_GetLiteralAtom(GivenClause, i); |
| if (!term_IsVariable(term_FirstArgument(TAtom))) |
| Hit = TRUE; |
| else |
| i++; |
| } |
| |
| if (!Hit) |
| return list_Nil(); |
| |
| /* added because of compiler warnings */ |
| TAtom = clause_GetLiteralAtom(GivenClause, i); |
| |
| /* Search the other T_i from <GivenClause> */ |
| TLits = list_List((POINTER)i); |
| for (j = i+1; j <= lc; j++) { |
| if (term_FirstArgument(clause_GetLiteralAtom(GivenClause, j)) |
| == term_FirstArgument(TAtom)) |
| TLits = list_Cons((POINTER)j, TLits); |
| } |
| RestLits = list_Copy(TLits); |
| |
| if (!Precheck || |
| inf_SubsortPrecheck(GivenClause, TLits, NULL, Index, SortTheory)) { |
| |
| Result = inf_ConstraintHyperResolvents(GivenClause, TLits, subst_Nil(), |
| RestLits, list_Nil(), Index, Flags, |
| Precedence); |
| |
| } |
| list_Delete(RestLits); |
| list_Delete(TLits); |
| |
| return Result; |
| } |
| |
| |
| LIST inf_BackwardEmptySort(CLAUSE GivenClause, st_INDEX Index, |
| SORTTHEORY SortTheory, BOOL Precheck, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with a solved sort constraint, an 'Index' of clauses, |
| a sort theory, a boolean flag indicating whether the subsort |
| precheck can be applied, a flag store and a precedence. |
| RETURNS: A list of clauses inferred from the GivenClause by |
| EmptySort with the given clause. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST result; |
| int i, ls; |
| |
| #ifdef CHECK |
| if (!(clause_IsClause(GivenClause, Flags, Precedence)) || |
| !clause_HasSolvedConstraint(GivenClause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BackwardEmptySort: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| result = list_Nil(); |
| |
| ls = clause_LastSuccedentLitIndex(GivenClause); |
| |
| for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= ls; i++) { |
| LITERAL pLit = clause_GetLiteral(GivenClause, i); |
| TERM pAtom = clause_LiteralAtom(pLit); |
| |
| if (clause_LiteralGetFlag(pLit,STRICTMAXIMAL) && |
| clause_LiteralIsSort(pLit)) { |
| LIST unifiers = st_GetUnifier(cont_LeftContext(),Index,cont_RightContext(),pAtom); |
| |
| for ( ; !list_Empty(unifiers); unifiers = list_Pop(unifiers)){ |
| if (term_IsAtom(list_Car(unifiers)) && |
| term_IsVariable(term_FirstArgument(list_Car(unifiers)))) { |
| LIST litScan = sharing_NAtomDataList(list_Car(unifiers)); |
| |
| for ( ; !list_Empty(litScan); litScan = list_Cdr(litScan)){ |
| LITERAL gLit = list_Car(litScan); |
| CLAUSE gClause = clause_LiteralOwningClause(gLit); |
| |
| if (clause_LiteralGetIndex(gLit) < clause_FirstAntecedentLitIndex(gClause) && |
| clause_GetFlag(gClause,WORKEDOFF) && |
| clause_HasOnlyVarsInConstraint(gClause, Flags, Precedence)) { |
| TERM gAtom = clause_LiteralAtom(gLit); |
| SYMBOL var = term_TopSymbol(term_FirstArgument(gAtom)); |
| int lc = clause_LastConstraintLitIndex(gClause); |
| int gi = clause_LiteralGetIndex(gLit); |
| BOOL varOccursNoMore; |
| int j, bound; |
| |
| varOccursNoMore = TRUE; |
| bound = clause_LastSuccedentLitIndex(gClause); |
| |
| for (j = clause_FirstAntecedentLitIndex(gClause); |
| (j <= bound) && varOccursNoMore; |
| j++) { |
| if (term_ContainsSymbol(clause_GetLiteralAtom(gClause, j), var)) |
| varOccursNoMore = FALSE; |
| } |
| |
| if (varOccursNoMore) { |
| LIST tLits, restLits; |
| |
| /* Search the other T_i from <gClause> */ |
| tLits = list_List((POINTER)gi); |
| restLits = list_Nil(); |
| for (j = clause_FirstLitIndex(); j <= lc; j++) { |
| LITERAL tCand = clause_GetLiteral(gClause, j); |
| |
| if (j != gi && |
| term_FirstArgument(clause_LiteralAtom(tCand)) |
| == term_FirstArgument(gAtom)) { |
| tLits = list_Cons((POINTER)j, tLits); |
| restLits = list_Cons((POINTER)j, restLits); |
| } |
| } |
| |
| if (!Precheck || |
| inf_SubsortPrecheck(gClause,tLits,pLit,Index,SortTheory)) { |
| CLAUSE pCopy = clause_Copy(GivenClause); |
| SYMBOL minVar = clause_MaxVar(gClause); |
| LIST foundLits = list_List(pLit); |
| SUBST leftSubst, rightSubst; |
| |
| clause_RenameVarsBiggerThan(pCopy, minVar); |
| pAtom = clause_GetLiteralAtom(pCopy, i); |
| /* set, to adress the renamed term! */ |
| |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), gAtom, cont_RightContext(), pAtom); |
| subst_ExtractUnifier(cont_LeftContext(), &leftSubst, |
| cont_RightContext(), &rightSubst); |
| cont_Reset(); |
| |
| subst_Delete(rightSubst); |
| |
| result = |
| list_Nconc(inf_ConstraintHyperResolvents(gClause, tLits, |
| leftSubst,restLits, |
| foundLits, Index, |
| Flags, Precedence), |
| result); |
| |
| list_Delete(foundLits); |
| subst_Delete(leftSubst); |
| clause_Delete(pCopy); |
| |
| pAtom = clause_LiteralAtom(pLit); |
| /* reset to original clauses literal! */ |
| } /* if Precheck */ |
| list_Delete(tLits); |
| list_Delete(restLits); |
| } |
| } |
| } |
| } |
| } |
| } |
| } |
| return result; |
| } |
| |
| |
| LIST inf_ForwardEmptySort(CLAUSE GivenClause, st_INDEX Index, |
| SORTTHEORY SortTheory, BOOL Precheck, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, an index of clauses, a sort theory, |
| a boolean flag indicating whether the subsort |
| precheck can be applied, a flag store and a precedence. |
| The constraint of <GivenClause> is necessarily unsolved |
| RETURNS: A list of clauses inferred from the GivenClause by |
| EmptySort on the given clause. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, TLits, RestLits; |
| int i, j, lc, ls; |
| BOOL Hit; |
| TERM TAtom; |
| SYMBOL Var; |
| |
| #ifdef CHECK |
| if (clause_HasTermSortConstraintLits(GivenClause) || |
| clause_HasSolvedConstraint(GivenClause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_ForwardEmptySort: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| lc = clause_LastConstraintLitIndex(GivenClause); |
| Hit = FALSE; |
| |
| i = clause_FirstLitIndex(); |
| while (i <= lc && !Hit) { |
| TAtom = clause_GetLiteralAtom(GivenClause, i); |
| |
| if (term_IsVariable(term_FirstArgument(TAtom))) { |
| Var = term_TopSymbol(term_FirstArgument(TAtom)); |
| ls = clause_LastSuccedentLitIndex(GivenClause); |
| Hit = TRUE; |
| /* Check if the variable occurs in antecedent or succedent literals */ |
| for (j = clause_FirstAntecedentLitIndex(GivenClause); |
| j <= ls && Hit; j++) { |
| if (term_ContainsSymbol(clause_GetLiteralAtom(GivenClause,j), Var)) |
| Hit = FALSE; /* Variable occurs in antecedent/constraint literal */ |
| } |
| } |
| if (!Hit) |
| i++; |
| } |
| |
| if (!Hit) |
| return list_Nil(); |
| |
| TAtom = clause_GetLiteralAtom(GivenClause, i); |
| Var = term_TopSymbol(term_FirstArgument(TAtom)); |
| |
| /* Search the other T_i(t) literals */ |
| TLits = list_List((POINTER)i); |
| for (j = i+1; j <= lc; j++) { |
| TERM TCand; |
| |
| TCand = clause_GetLiteralAtom(GivenClause, j); |
| |
| if (symbol_Equal(term_TopSymbol(term_FirstArgument(TCand)), Var)) |
| TLits = list_Cons((POINTER)j, TLits); |
| } |
| RestLits = list_Copy(TLits); |
| |
| if (!Precheck || |
| inf_SubsortPrecheck(GivenClause, TLits, NULL, Index, SortTheory)) { |
| |
| Result = inf_ConstraintHyperResolvents(GivenClause, TLits, subst_Nil(), |
| RestLits, list_Nil(), Index, Flags, |
| Precedence); |
| |
| } |
| list_Delete(RestLits); |
| list_Delete(TLits); |
| |
| return Result; |
| } |
| |
| static LIST inf_GetForwardPartnerLits(LITERAL Literal, st_INDEX Index) |
| /************************************************************** |
| INPUT: A monadic literal, and an index of clauses. |
| RETURNS: A list of monadic succedent literals whose subterm |
| is unifiable with the (one) subterm of <Literal>. |
| The literals are strict maximal in their respective clauses, |
| the clauses are "WORKEDOFF" and either the subterm |
| is not a variable or the clause has an empty constraint. |
| MEMORY: Allocates memory for the list. |
| ***************************************************************/ |
| { |
| LIST result, unifiers, atomScan, litScan; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal) || !clause_LiteralIsSort(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GetForwardPartnerLits: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| result = list_Nil(); |
| /* Search unifiers for the literal's subterm */ |
| unifiers = st_GetUnifier(cont_LeftContext(), Index, cont_RightContext(), |
| term_FirstArgument(clause_LiteralAtom(Literal))); |
| |
| for ( ; !list_Empty(unifiers); unifiers = list_Pop(unifiers)) { |
| |
| if (!term_IsAtom(list_Car(unifiers))) { /* Can happen if arg is variable */ |
| |
| for (atomScan = term_SupertermList(list_Car(unifiers)); |
| !list_Empty(atomScan); |
| atomScan = list_Cdr(atomScan)) { |
| TERM atomCand; |
| atomCand = (TERM) list_Car(atomScan); |
| if (term_IsDeclaration(atomCand)) { |
| /* We are looking for an unary atom */ |
| |
| for (litScan = sharing_NAtomDataList(atomCand); |
| !list_Empty(litScan); |
| litScan = list_Cdr(litScan)) { |
| LITERAL nextLit; |
| CLAUSE nextClause; |
| nextLit = list_Car(litScan); |
| nextClause = clause_LiteralOwningClause(nextLit); |
| |
| if (clause_LiteralIsPositive(nextLit) && |
| clause_LiteralGetFlag(nextLit,STRICTMAXIMAL) && |
| clause_GetFlag(nextClause, WORKEDOFF) && |
| (!term_IsVariable(list_Car(unifiers)) || |
| clause_HasEmptyConstraint(nextClause)) && |
| clause_HasSolvedConstraint(nextClause)) { |
| /* Add the literal from the copied clause */ |
| result = list_Cons(nextLit, result); |
| } |
| } /* litScan */ |
| } /* if IsAtom */ |
| } /* atomScan */ |
| } /* ! variable */ |
| } /* unifiers */ |
| return result; |
| } |
| |
| static BOOL inf_LiteralsHaveSameSubtermAndAreFromSameClause(LITERAL L1, LITERAL L2) |
| /************************************************************** |
| INPUT: Two literals. |
| RETURNS: TRUE, if both literals have the same term and are |
| from the same clause, FALSE otherwise. |
| Since both literals are shared, pointer equality |
| is used to detect this. |
| This function is used by inf_GetBackwardPartnerLits(). |
| ***************************************************************/ |
| { |
| return (term_FirstArgument(clause_LiteralAtom(L1)) |
| == term_FirstArgument(clause_LiteralAtom(L2)) && |
| clause_LiteralOwningClause(L1) == clause_LiteralOwningClause(L2)); |
| } |
| |
| static void inf_GetBackwardPartnerLits(LITERAL Literal, st_INDEX Index, |
| LIST* ConstraintLits, LIST* Unifiers, |
| BOOL IsFromEmptySort, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A literal, an index of clauses, two pointers to lists, |
| a boolean value, a flag store and a precedence. |
| RETURNS: |
| MEMORY: Allocates memory for the list. |
| ***************************************************************/ |
| { |
| LIST candidates, atomScan, litScan; |
| LITERAL nextLit; |
| CLAUSE nextClause; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsLiteral(Literal) || !clause_LiteralIsSort(Literal)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GetBackwardPartnerLits: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| candidates = st_GetUnifier(cont_LeftContext(), Index, cont_RightContext(), |
| term_FirstArgument(clause_LiteralAtom(Literal))); |
| |
| for ( ; !list_Empty(candidates); candidates = list_Pop(candidates)) { |
| if (!term_IsAtom(list_Car(candidates))) { /* May happen if arg is variable */ |
| /* Consider variable unifiers only if called from BackwardEmptySort */ |
| for (atomScan = term_SupertermList(list_Car(candidates)); |
| !list_Empty(atomScan); |
| atomScan = list_Cdr(atomScan)) { |
| TERM atomCand; |
| atomCand = (TERM) list_Car(atomScan); |
| if (term_IsDeclaration(atomCand)) { |
| /* We are looking for unary atoms */ |
| |
| for (litScan = sharing_NAtomDataList(atomCand); |
| !list_Empty(litScan); |
| litScan = list_Cdr(litScan)) { |
| nextLit = list_Car(litScan); |
| nextClause = clause_LiteralOwningClause(nextLit); |
| |
| if (clause_GetFlag(nextClause, WORKEDOFF)) { |
| if (clause_LiteralIsPositive(nextLit)) { |
| if (clause_LiteralGetFlag(nextLit,STRICTMAXIMAL) && |
| (!term_IsVariable(list_Car(candidates)) || |
| clause_HasEmptyConstraint(nextClause)) && |
| clause_HasSolvedConstraint(nextClause) && |
| !symbol_Equal(clause_LiteralPredicate(Literal), |
| clause_LiteralPredicate(nextLit))) { |
| /* Don't consider literals with same top symbol as given literal */ |
| /* since the given clause must be part of any inference */ |
| *Unifiers = list_Cons(nextLit, *Unifiers); |
| } |
| } else if (clause_LiteralGetIndex(nextLit) < clause_FirstAntecedentLitIndex(nextClause) && |
| ((!term_IsVariable(list_Car(candidates)) && !IsFromEmptySort) || |
| (term_IsVariable(list_Car(candidates)) && IsFromEmptySort && |
| clause_HasOnlyVarsInConstraint(nextClause,Flags, Precedence)))) { |
| *ConstraintLits = list_Cons(nextLit, *ConstraintLits); |
| } |
| } |
| } /* litScan */ |
| } |
| } /* atomScan */ |
| } |
| } /* candidates */ |
| |
| /* We have to avoid constraint literals from the same clause with the same |
| term or variable, since those would create the same result clause. */ |
| *ConstraintLits = |
| list_DeleteDuplicates(*ConstraintLits, |
| (BOOL (*)(POINTER,POINTER)) inf_LiteralsHaveSameSubtermAndAreFromSameClause); |
| } |
| |
| static void inf_MakeClausesDisjoint(CLAUSE GClause, LIST Literals) |
| /************************************************************** |
| INPUT: A clause and a non-empty list of literals. |
| EFFECT: All input clauses, those pointed to by the literals, |
| are variable disjointly renamed. |
| ***************************************************************/ |
| { |
| SYMBOL maxVar, maxCand; |
| CLAUSE lastClause; |
| |
| maxVar = clause_MaxVar(GClause); |
| lastClause = clause_LiteralOwningClause(list_Car(Literals)); |
| clause_RenameVarsBiggerThan(lastClause, maxVar); |
| Literals = list_Cdr(Literals); |
| |
| for ( ; !list_Empty(Literals); Literals = list_Cdr(Literals)) { |
| CLAUSE actClause; |
| |
| clause_UpdateMaxVar(lastClause); |
| maxCand = clause_MaxVar(lastClause); |
| maxVar = (symbol_GreaterVariable(maxVar,maxCand)? maxVar : maxCand); |
| |
| actClause = clause_LiteralOwningClause(list_Car(Literals)); |
| clause_RenameVarsBiggerThan(actClause, maxVar); |
| } |
| } |
| |
| static void inf_CopyUnifierClauses(LIST Literals) |
| /************************************************************** |
| INPUT: A list of literals. |
| EFFECT: Replaces all literals by pointers to literals of copies |
| of the respective clauses. |
| ***************************************************************/ |
| { |
| for ( ; !list_Empty(Literals); Literals = list_Cdr(Literals)) { |
| CLAUSE actClause; |
| int i; |
| |
| actClause = clause_LiteralOwningClause(list_Car(Literals)); |
| i = clause_LiteralGetIndex(list_Car(Literals)); |
| actClause = clause_Copy(actClause); |
| list_Rplaca(Literals, clause_GetLiteral(actClause, i)); /* Set to literal from copy */ |
| } |
| } |
| |
| static void inf_DeleteUnifierClauses(LIST Literals) |
| /************************************************************** |
| INPUT: A list of literals. |
| EFFECT: Deletes all clauses the literals point to. |
| ***************************************************************/ |
| { |
| for ( ; !list_Empty(Literals); Literals = list_Cdr(Literals)) { |
| clause_Delete(clause_LiteralOwningClause(list_Car(Literals))); |
| list_Rplaca(Literals, NULL); |
| } |
| } |
| |
| static SORT inf_GetSortFromLits(LIST Literals, SORTTHEORY SortTheory) |
| /************************************************************** |
| INPUT: A list of literals and a sort theory. |
| RETURNS: The sort created from the literals' predicates. |
| ***************************************************************/ |
| { |
| SORT result = sort_TopSort(); |
| |
| for ( ; !list_Empty(Literals); Literals = list_Cdr(Literals)) { |
| SORT newSort = sort_TheorySortOfSymbol(SortTheory, |
| clause_LiteralPredicate(list_Car(Literals))); |
| |
| result = sort_Intersect(newSort, result); |
| } |
| |
| list_PointerDeleteDuplicates(result); |
| |
| return result; |
| } |
| |
| static LIST inf_ApplyWeakening(CLAUSE Clause, LIST TLits, LIST Partners, |
| CONDITION Condition, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a list of constraint indices in <Clause>, |
| a list of maximal, monadic succedent literals, |
| a subsort condition, a flag store and a precedence. |
| RETURNS: A one-element list with a clause derived from the |
| clause and the partner clauses by the Weakening or |
| Empty Sort rule. |
| The flag store is needed to create the result clause. |
| MEMORY: Memory is allocated for the returned list and the clause. |
| ***************************************************************/ |
| { |
| LIST scan, parents; |
| LIST constraint, antecedent, succedent; |
| LIST parentClauses, parentLits; /* clause numbers and literal indices */ |
| int i, bound, depth; |
| TERM tSubterm; |
| CLAUSE newClause; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence) || list_Empty(TLits) || |
| list_Empty(Partners) || Condition == NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_ApplyWeakening: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| constraint = antecedent = succedent = list_Nil(); |
| parentClauses = parentLits = list_Nil(); |
| parents = list_Nil(); /* Used to set split data */ |
| depth = clause_Depth(Clause); |
| tSubterm = term_FirstArgument(clause_GetLiteralAtom(Clause, (int)list_Car(TLits))); |
| |
| /* Now collect the literals of the new clause */ |
| /* First consider the condition atoms */ |
| for (scan=sort_ConditionConstraint(Condition); !list_Empty(scan); scan=list_Cdr(scan)) { |
| TERM termCopy; |
| |
| termCopy = term_Copy(list_Car(scan)); |
| term_ReplaceVariable(termCopy, sort_ConditionVar(Condition), tSubterm); |
| constraint = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), termCopy), |
| constraint); |
| term_Delete(termCopy); /* constraint contains a copy */ |
| } |
| for (scan=sort_ConditionAntecedent(Condition); !list_Empty(scan); scan=list_Cdr(scan)) { |
| TERM termCopy; |
| |
| termCopy = term_Copy(list_Car(scan)); |
| term_ReplaceVariable(termCopy, sort_ConditionVar(Condition), tSubterm); |
| antecedent = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), termCopy), |
| antecedent); |
| term_Delete(termCopy); /* antecedent contains a copy */ |
| } |
| for (scan=sort_ConditionSuccedent(Condition); !list_Empty(scan); scan=list_Cdr(scan)) { |
| TERM termCopy; |
| |
| termCopy = term_Copy(list_Car(scan)); |
| term_ReplaceVariable(termCopy, sort_ConditionVar(Condition), tSubterm); |
| succedent = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), termCopy), |
| succedent); |
| term_Delete(termCopy); /* succedent contains a copy */ |
| } |
| /* update parents and depth from condition clauses */ |
| for (scan=sort_ConditionClauses(Condition); !list_Empty(scan); scan=list_Cdr(scan)) { |
| CLAUSE condClause; |
| |
| condClause = list_Car(scan); |
| parents = list_Cons(condClause, parents); |
| parentClauses = list_Cons((POINTER)clause_Number(condClause), parentClauses); |
| parentLits = list_Cons((POINTER)clause_FirstSuccedentLitIndex(condClause), parentLits); |
| depth = misc_Max(depth, clause_Depth(condClause)); |
| } |
| |
| /* Now we consider the partner clauses */ |
| for (scan = Partners; !list_Empty(scan); scan = list_Cdr(scan)) { |
| LITERAL pLit; |
| CLAUSE pClause; |
| int pi; |
| |
| pLit = list_Car(scan); |
| pClause = clause_LiteralOwningClause(pLit); |
| pi = clause_LiteralGetIndex(pLit); |
| bound = clause_LastConstraintLitIndex(pClause); |
| for (i = clause_FirstLitIndex(); i <= bound; i++) { |
| constraint = list_Cons(cont_CopyAndApplyBindings(cont_RightContext(), |
| clause_GetLiteralAtom(pClause,i)), |
| constraint); |
| } |
| bound = clause_LastAntecedentLitIndex(pClause); |
| for (i = clause_FirstAntecedentLitIndex(pClause); i <= bound; i++) { |
| antecedent = list_Cons(cont_CopyAndApplyBindings(cont_RightContext(), |
| clause_GetLiteralAtom(pClause,i)), |
| antecedent); |
| } |
| bound = clause_LastSuccedentLitIndex(pClause); |
| for (i = clause_FirstSuccedentLitIndex(pClause); i <= bound; i++) { |
| if (i != pi) |
| succedent = list_Cons(cont_CopyAndApplyBindings(cont_RightContext(), |
| clause_GetLiteralAtom(pClause,i)), |
| succedent); |
| } |
| |
| parents = list_Cons(pClause, parents); |
| |
| parentClauses = list_Cons((POINTER)clause_Number(pClause), parentClauses); |
| parentLits = list_Cons((POINTER) pi, parentLits); |
| |
| depth = misc_Max(depth, clause_Depth(pClause)); |
| } |
| |
| /* Last but not least we consider the <Clause> itself */ |
| bound = clause_LastConstraintLitIndex(Clause); |
| for (i = clause_FirstLitIndex(); i <= bound; i++) { |
| if (!list_PointerMember(TLits, (POINTER)i)) |
| constraint = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), |
| clause_GetLiteralAtom(Clause,i)), |
| constraint); |
| else { |
| parentClauses = list_Cons((POINTER)clause_Number(Clause), parentClauses); |
| parentLits = list_Cons((POINTER)i, parentLits); |
| } |
| } |
| bound = clause_LastAntecedentLitIndex(Clause); |
| for (i = clause_FirstAntecedentLitIndex(Clause); i <= bound; i++) { |
| antecedent = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), |
| clause_GetLiteralAtom(Clause,i)), |
| antecedent); |
| } |
| bound = clause_LastSuccedentLitIndex(Clause); |
| for (i = clause_FirstSuccedentLitIndex(Clause); i <= bound; i++) { |
| succedent = list_Cons(cont_CopyAndApplyBindings(cont_LeftContext(), |
| clause_GetLiteralAtom(Clause,i)), |
| succedent); |
| } |
| |
| parents = list_Cons(Clause, parents); |
| |
| /* Now we've got all data we need */ |
| newClause = clause_Create(constraint, antecedent, succedent, Flags,Precedence); |
| |
| list_Delete(constraint); |
| list_Delete(antecedent); |
| list_Delete(succedent); |
| |
| if (term_IsVariable(tSubterm)) |
| clause_SetFromEmptySort(newClause); |
| else |
| clause_SetFromSortResolution(newClause); |
| |
| clause_SetDepth(newClause, depth+1); |
| clause_SetFlag(newClause, DOCCLAUSE); |
| |
| clause_SetSplitDataFromList(newClause, parents); |
| list_Delete(parents); |
| |
| clause_SetParentClauses(newClause, parentClauses); |
| clause_SetParentLiterals(newClause, parentLits); |
| |
| return list_List(newClause); |
| } |
| |
| static LIST inf_InternWeakening(CLAUSE Clause, LIST TLits, LIST Unifiers, |
| LITERAL Special, LIST SojuList, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A <Clause> with unsolved sort constraint, |
| a list <TLits> of constraint indices in <Clause> where |
| all corresponding constraints have the same term, |
| a list <Unifiers> of monadic succedent literals whose |
| subterm is unifiable with the subterm of the <TLits>, |
| and a flag store. |
| If called from a backward rule the literal <Special> |
| will be the succedent literal from the respective |
| GivenClause, that must be part of every considered |
| SOJU sort. If called from a forward rule <Special> is NULL. |
| A list <SojuList> of sort pairs. |
| A flag store and a precedence. |
| RETURNS: The list of possible resolvents. |
| EFFECT: ATTENTION: <SojuList> is deleted. |
| MEMORY: Memory is allocated for the returned list and the clauses. |
| ***************************************************************/ |
| { |
| LIST result, myUnifiers; |
| TERM searchTerm; |
| int stack; |
| |
| LIST scan; |
| #ifdef CHECK |
| if (!clause_IsClause(Clause, Flags, Precedence) || list_Empty(TLits) || |
| list_Empty(Unifiers)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_InternWeakening: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| putchar('\n'); clause_Print(Clause); |
| fputs("\nT_k = ", stdout); |
| for (scan = TLits; !list_Empty(scan); scan = list_Cdr(scan)) { |
| clause_LiteralPrint(clause_GetLiteral(Clause, (int)list_Car(scan))); |
| putchar(' '); |
| } |
| fputs("\nS_k =", stdout); |
| for (scan = Unifiers; !list_Empty(scan); scan = list_Cdr(scan)) { |
| putchar('\n'); |
| clause_LiteralPrint(list_Car(scan)); |
| fputs(" in ", stdout); |
| clause_Print(clause_LiteralOwningClause(list_Car(scan))); |
| } |
| putchar('\n'); |
| |
| if (list_Empty(SojuList)) |
| return list_Nil(); |
| |
| /*return list_Nil();*/ |
| /* Und Schluss */ |
| |
| result = list_Nil(); |
| |
| myUnifiers = list_Copy(Unifiers); |
| inf_CopyUnifierClauses(myUnifiers); |
| inf_MakeClausesDisjoint(Clause, myUnifiers); |
| |
| searchTerm = |
| term_FirstArgument(clause_GetLiteralAtom(Clause, (int)list_Car(TLits))); |
| |
| stack = stack_Bottom(); |
| |
| for ( ; !list_Empty(SojuList); SojuList = list_Pop(SojuList)) { |
| SOJU actSoju = list_Car(SojuList); |
| |
| fputs("\nSOJU: ", stdout); sort_PairPrint(actSoju); fflush(stdout); |
| |
| if (Special == NULL || |
| sort_ContainsSymbol(sort_PairSort(actSoju), |
| clause_LiteralPredicate(Special))) { |
| LIST actSortSymbols, symbolScan, unifierScan, subset; |
| |
| actSortSymbols = sort_GetSymbolsFromSort(sort_PairSort(actSoju)); |
| subset = list_Nil(); |
| |
| symbolScan = actSortSymbols; |
| unifierScan = myUnifiers; |
| |
| do { |
| while (!list_Empty(symbolScan) && !list_Empty(unifierScan)) { |
| LITERAL actLit = list_Car(unifierScan); |
| |
| if (symbol_Equal(clause_LiteralPredicate(list_Car(unifierScan)), |
| (SYMBOL)list_Car(symbolScan))) { |
| cont_StartBinding(); |
| if (unify_UnifyNoOC(cont_LeftContext(), searchTerm, cont_RightContext(), |
| term_FirstArgument(clause_LiteralAtom(actLit)))) { |
| /* Found corresponding literal for sort symbol */ |
| stack_Push(symbolScan); |
| stack_Push(list_Cdr(unifierScan)); |
| subset = list_Cons(actLit, subset); |
| /* Now search literals for the next sort symbol */ |
| symbolScan = list_Cdr(symbolScan); |
| |
| if (!list_Empty(symbolScan)) |
| /* Start search for literal at the beginning of unifier list */ |
| unifierScan = myUnifiers; |
| else |
| unifierScan = list_Cdr(unifierScan); |
| } else { |
| cont_BackTrack(); |
| unifierScan = list_Cdr(unifierScan); |
| } |
| } else |
| unifierScan = list_Cdr(unifierScan); |
| } |
| |
| if (list_Empty(symbolScan)) { |
| /*putchar('\n'); |
| clause_LiteralListPrint(subset);*/ |
| /* Found subset */ |
| result = list_Nconc(inf_ApplyWeakening(Clause, TLits, subset, |
| sort_PairCondition(actSoju), |
| Flags, Precedence), |
| result); |
| } |
| |
| while (!stack_Empty(stack) && list_Empty(stack_Top())) { |
| /* No more literals */ |
| stack_NPop(2); |
| cont_BackTrack(); |
| subset = list_Pop(subset); |
| } |
| |
| if (!stack_Empty(stack)) { |
| /* Implies that stack_Top is a non-empty list */ |
| unifierScan = stack_PopResult(); |
| symbolScan = stack_PopResult(); |
| cont_BackTrack(); |
| subset = list_Pop(subset); |
| } |
| } while (!stack_Empty(stack) || !list_Empty(unifierScan)); |
| |
| list_Delete(actSortSymbols); |
| } |
| sort_PairDelete(actSoju); |
| } /* For all SOJUs */ |
| |
| inf_DeleteUnifierClauses(myUnifiers); |
| list_Delete(myUnifiers); |
| |
| return result; |
| } |
| |
| LIST inf_ForwardWeakening(CLAUSE GivenClause, st_INDEX Index, |
| SORTTHEORY SortTheory, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, an index of clauses, a sort theory, a flag store |
| and a precedence. |
| The sort constraint of the clause must contain a non-variable term |
| (this implies the sort constraint is unsolved). |
| RETURNS: A list of clauses derived from the GivenClause by |
| the Weakening rule. |
| MEMORY: Memory is allocated for the returned list and the clauses. |
| ***************************************************************/ |
| { |
| LIST result; |
| int i, lc; |
| BOOL hit; |
| |
| #ifdef CHECK |
| if (!clause_HasTermSortConstraintLits(GivenClause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_ForwardWeakening: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| result = list_Nil(); |
| lc = clause_LastConstraintLitIndex(GivenClause); |
| hit = FALSE; |
| |
| for (i = clause_FirstLitIndex(); i <= lc && !hit; i++) { |
| |
| if (!term_IsVariable(term_FirstArgument(clause_GetLiteralAtom(GivenClause, i)))) { |
| /* Condition implies that constraint is unsolved */ |
| LITERAL tLit; |
| LIST unifiers; |
| int j; |
| |
| tLit = clause_GetLiteral(GivenClause, i); |
| hit = TRUE; /* Try only the first appropriate constraint literal */ |
| unifiers = inf_GetForwardPartnerLits(tLit, Index); |
| |
| if (!list_Empty(unifiers)) { |
| TERM tAtom; |
| LIST tLits, sojuList; |
| SORT tSort, unifierSort; |
| |
| tAtom = clause_GetLiteralAtom(GivenClause, i); |
| |
| /* Search the other T_k(t) in GivenClause */ |
| tLits = list_Nil(); |
| tSort = sort_TopSort(); |
| for (j = lc; j > i; j--) { |
| TERM actAtom; |
| actAtom = clause_GetLiteralAtom(GivenClause, j); |
| if (term_FirstArgument(actAtom) == term_FirstArgument(tAtom)) { |
| tLits = list_Cons((POINTER)j, tLits); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(actAtom)), |
| tSort); |
| } |
| } |
| tLits = list_Cons((POINTER)i, tLits); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(tAtom)), |
| tSort); |
| list_PointerDeleteDuplicates(tSort); |
| /* Necessary for Christoph's function */ |
| |
| unifierSort = inf_GetSortFromLits(unifiers, SortTheory); |
| sojuList = sort_TheoryComputeAllSubsortHits(SortTheory, unifierSort, tSort); |
| sort_Delete(unifierSort); |
| sort_Delete(tSort); |
| |
| result = |
| list_Nconc(inf_InternWeakening(GivenClause, tLits, unifiers, NULL, |
| sojuList, Flags, Precedence), |
| result); |
| |
| list_Delete(tLits); |
| list_Delete(unifiers); |
| } |
| } |
| } |
| return result; |
| } |
| |
| LIST inf_BackwardWeakening(CLAUSE GivenClause, st_INDEX Index, |
| SORTTHEORY SortTheory, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with solved sort constraint, an index of clauses, |
| a sort theory, a flag store and a precedence. |
| RETURNS: A list of clauses inferred from the GivenClause by |
| the Weakening rule. |
| MEMORY: Memory is allocated for the list and the clauses. |
| ***************************************************************/ |
| { |
| LIST result; |
| int i, ls; |
| |
| #ifdef CHECK |
| if (!clause_HasSolvedConstraint(GivenClause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BackwardWeakening: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| result = list_Nil(); |
| ls = clause_LastSuccedentLitIndex(GivenClause); |
| |
| for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= ls; i++) { |
| LITERAL sLit; |
| TERM sAtom; |
| |
| sLit = clause_GetLiteral(GivenClause, i); |
| sAtom = clause_LiteralAtom(sLit); |
| if (clause_LiteralGetFlag(sLit, STRICTMAXIMAL) && |
| clause_LiteralIsSort(sLit) && |
| (!term_IsVariable(term_FirstArgument(sAtom)) || |
| clause_HasEmptyConstraint(GivenClause))) { |
| LIST unifiers, partners; |
| SORT unifierSort; |
| |
| unifiers = partners = list_Nil(); |
| inf_GetBackwardPartnerLits(sLit,Index,&partners,&unifiers,FALSE,Flags, |
| Precedence); |
| unifiers = list_Cons(sLit, unifiers); |
| /* <partners> holds monadic constraint literals */ |
| /* <unifiers> holds monadic, maximal succedent literals */ |
| unifierSort = inf_GetSortFromLits(unifiers, SortTheory); |
| |
| for ( ; !list_Empty(partners); partners = list_Pop(partners)) { |
| LITERAL tLit; |
| CLAUSE tClause; |
| TERM tAtom; |
| int ti; |
| int lc; |
| int j; |
| LIST tLits, sojuList; |
| SORT tSort; |
| |
| tLit = list_Car(partners); |
| tClause = clause_LiteralOwningClause(tLit); |
| tAtom = clause_LiteralAtom(tLit); |
| ti = clause_LiteralGetIndex(tLit); |
| lc = clause_LastConstraintLitIndex(tClause); |
| |
| /* Search the other T_k(t) in GivenClause */ |
| tLits = list_Nil(); |
| tSort = sort_TopSort(); |
| for (j = lc; j >= clause_FirstLitIndex(); j--) { |
| TERM actAtom; |
| |
| actAtom = clause_GetLiteralAtom(tClause, j); |
| if (j != ti && |
| term_FirstArgument(actAtom) == term_FirstArgument(tAtom)) { |
| tLits = list_Cons((POINTER)j, tLits); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(actAtom)), |
| tSort); |
| } |
| } |
| tLits = list_Cons((POINTER)ti, tLits); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(tAtom)), |
| tSort); |
| list_PointerDeleteDuplicates(tSort); |
| |
| sojuList = sort_TheoryComputeAllSubsortHits(SortTheory, unifierSort, tSort); |
| sort_Delete(tSort); |
| |
| cont_StartBinding(); |
| unify_UnifyNoOC(cont_LeftContext(), tAtom, |
| cont_RightContext(), sAtom); |
| |
| result = |
| list_Nconc(inf_InternWeakening(tClause, tLits, unifiers, sLit, |
| sojuList, Flags, Precedence), |
| result); |
| |
| cont_BackTrack(); |
| |
| list_Delete(tLits); |
| } |
| sort_Delete(unifierSort); |
| list_Delete(unifiers); |
| } |
| } |
| |
| return result; |
| } |
| |
| LIST inf_ForwardEmptySortPlusPlus(CLAUSE GivenClause, st_INDEX Index, |
| SORTTHEORY SortTheory, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, an 'Index' of clauses, a sort theory, a flag store |
| and a precedence. |
| The sort constraint of the clause must not contain a |
| non-variable term, but the sort constraint has to be unsolved. |
| RETURNS: A list of clauses derived from the GivenClause by |
| the Empty Sort rule. |
| MEMORY: Memory is allocated for the returned list and the clauses. |
| ***************************************************************/ |
| { |
| LIST result; |
| int i, lc; |
| BOOL hit; |
| |
| #ifdef CHECK |
| if (clause_HasTermSortConstraintLits(GivenClause) || |
| clause_HasSolvedConstraint(GivenClause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_ForwardEmptySortPlusPlus: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| result = list_Nil(); |
| lc = clause_LastConstraintLitIndex(GivenClause); |
| hit = FALSE; |
| |
| for (i = clause_FirstLitIndex(); i <= lc && !hit; i++) { |
| |
| if (term_IsVariable(term_FirstArgument(clause_GetLiteralAtom(GivenClause,i)))) { |
| LITERAL tLit; |
| TERM var; |
| int j, ls; |
| BOOL varOccursNoMore; |
| |
| tLit = clause_GetLiteral(GivenClause, i); |
| var = term_FirstArgument(clause_LiteralAtom(tLit)); |
| ls = clause_LastSuccedentLitIndex(GivenClause); |
| varOccursNoMore = TRUE; |
| /* Check if the variable occurs in antecedent or succedent literals */ |
| for (j = clause_FirstAntecedentLitIndex(GivenClause); |
| (j <= ls) && varOccursNoMore; j++) { |
| if (term_ContainsSymbol(clause_GetLiteralAtom(GivenClause,j), |
| term_TopSymbol(var))) |
| varOccursNoMore = FALSE; |
| } |
| |
| if (varOccursNoMore) { |
| /* Condition implies that constraint is unsolved */ |
| LIST unifiers; |
| |
| unifiers = inf_GetForwardPartnerLits(tLit, Index); |
| hit = TRUE; /* We found the first appropriate constraint literal */ |
| |
| if (!list_Empty(unifiers)) { |
| TERM tAtom = clause_LiteralAtom(tLit); |
| LIST tLits, sojuList; |
| SORT tSort, unifierSort; |
| |
| /* Search the other T_k(t) in GivenClause */ |
| tLits = list_Nil(); |
| tSort = sort_TopSort(); |
| for (j = lc; j > i; j--) { |
| TERM actAtom; |
| |
| actAtom = clause_GetLiteralAtom(GivenClause, j); |
| if (term_FirstArgument(actAtom) == var) { /* tClause is shared */ |
| tLits = list_Cons((POINTER)j, tLits); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, |
| term_TopSymbol(actAtom)), |
| tSort); |
| } |
| } |
| tLits = list_Cons((POINTER)i, tLits); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, |
| term_TopSymbol(tAtom)), |
| tSort); |
| list_PointerDeleteDuplicates(tSort); |
| |
| unifierSort = inf_GetSortFromLits(unifiers, SortTheory); |
| sojuList = sort_TheoryComputeAllSubsortHits(SortTheory, unifierSort, tSort); |
| |
| sort_Delete(unifierSort); |
| sort_Delete(tSort); |
| |
| result = |
| list_Nconc(inf_InternWeakening(GivenClause, tLits, unifiers, NULL, |
| sojuList, Flags, Precedence), |
| result); |
| |
| list_Delete(tLits); |
| list_Delete(unifiers); |
| } |
| } |
| } |
| } |
| return result; |
| } |
| |
| LIST inf_BackwardEmptySortPlusPlus(CLAUSE GivenClause, st_INDEX Index, |
| SORTTHEORY SortTheory, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with solved sort constraint, an index of clauses, |
| a sort theory, a flag store and a precedence. |
| RETURNS: A list of clauses inferred from the GivenClause by |
| the Empty Sort rule. |
| MEMORY: Memory is allocated for the list and the clauses. |
| ***************************************************************/ |
| { |
| LIST result; |
| int i, ls; |
| |
| #ifdef CHECK |
| if (!clause_HasSolvedConstraint(GivenClause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BackwardEmptySortPlusPlus: Illegal input.\n"); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| result = list_Nil(); |
| ls = clause_LastSuccedentLitIndex(GivenClause); |
| |
| for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= ls; i++) { |
| LITERAL sLit; |
| TERM sAtom; |
| |
| sLit = clause_GetLiteral(GivenClause, i); |
| sAtom = clause_LiteralAtom(sLit); |
| if (clause_LiteralGetFlag(sLit,STRICTMAXIMAL) && |
| clause_LiteralIsSort(sLit) && |
| (!term_IsVariable(term_FirstArgument(sAtom)) || |
| clause_HasEmptyConstraint(GivenClause))) { |
| LIST unifiers, partners; |
| SORT unifierSort; |
| |
| unifiers = partners = list_Nil(); |
| inf_GetBackwardPartnerLits(sLit, Index, &partners, &unifiers, TRUE, Flags, |
| Precedence); |
| unifiers = list_Cons(sLit, unifiers); |
| /* <partners> holds monadic constraint literals */ |
| /* <unifiers> holds monadic, maximal succedent literals */ |
| |
| unifierSort = inf_GetSortFromLits(unifiers, SortTheory); |
| |
| for ( ; !list_Empty(partners); partners = list_Pop(partners)) { |
| LITERAL tLit; |
| CLAUSE tClause; |
| TERM tAtom; |
| int ti; |
| int li; |
| TERM var; |
| BOOL varOccursNoMore; |
| int j; |
| |
| tLit = list_Car(partners); |
| tClause = clause_LiteralOwningClause(tLit); |
| tAtom = clause_LiteralAtom(tLit); |
| ti = clause_LiteralGetIndex(tLit); |
| li = clause_LastSuccedentLitIndex(tClause); |
| var = term_FirstArgument(tAtom); |
| varOccursNoMore = TRUE; |
| for (j = clause_FirstAntecedentLitIndex(tClause); |
| j <= li && varOccursNoMore; |
| j++) { |
| if (term_ContainsSymbol(clause_GetLiteralAtom(tClause,j), |
| term_TopSymbol(var))) |
| varOccursNoMore = FALSE; |
| } |
| |
| if (varOccursNoMore) { |
| /* Condition implies that constraint is unsolved */ |
| int lc; |
| LIST tLits, sojuList; |
| SORT tSort; |
| |
| lc = clause_LastConstraintLitIndex(tClause); |
| |
| /* Search the other T_k(t) in GivenClause */ |
| tLits = list_Nil(); |
| tSort = sort_TopSort(); |
| for (j = lc; j >= clause_FirstLitIndex(); j--) { |
| TERM actAtom; |
| |
| actAtom = clause_GetLiteralAtom(tClause, j); |
| if (j != ti && |
| term_TopSymbol(term_FirstArgument(actAtom)) == term_TopSymbol(var)) { |
| tLits = list_Cons((POINTER)j, tLits); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(actAtom)), |
| tSort); |
| } |
| } |
| tLits = list_Cons((POINTER)ti, tLits); |
| tSort = sort_Intersect(sort_TheorySortOfSymbol(SortTheory, term_TopSymbol(tAtom)), |
| tSort); |
| list_PointerDeleteDuplicates(tSort); |
| |
| sojuList = sort_TheoryComputeAllSubsortHits(SortTheory, unifierSort, tSort); |
| sort_Delete(tSort); |
| |
| cont_StartBinding(); |
| unify_UnifyNoOC(cont_LeftContext(), tAtom, |
| cont_RightContext(), sAtom); |
| |
| result = |
| list_Nconc(inf_InternWeakening(tClause, tLits, unifiers, sLit, |
| sojuList, Flags, Precedence), |
| result); |
| |
| cont_BackTrack(); |
| |
| list_Delete(tLits); |
| } |
| } |
| sort_Delete(unifierSort); |
| list_Delete(unifiers); |
| } |
| } |
| |
| return result; |
| } |
