| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * INFERENCE RULES * */ |
| /* * * */ |
| /* * $Module: INFRULES * */ |
| /* * * */ |
| /* * 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-inf.h" |
| |
| |
| /**************************************************************/ |
| /* Some auxiliary functions for testing postconditions */ |
| /**************************************************************/ |
| |
| static BOOL inf_LitMax(CLAUSE Clause, int i, int j, SUBST Subst, BOOL Strict, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, the index of a maximal literal, another |
| literal index, a substitution, a boolean flag, a |
| flag store and a precedence. |
| RETURNS: If <Strict>=FALSE the function returns TRUE iff the |
| literal at index <i> is still maximal in the |
| instantiated clause. |
| If <Strict>=TRUE the function returns TRUE iff the |
| literal is STRICTLY maximal in the instantiated |
| clause. The literal at index j is omitted at literal |
| comparison. |
| However, setting j to a negative number ensures that |
| all literals are compared with the literal at |
| index <i>. |
| CAUTION: DON'T call this function with a clause with selected |
| literals! |
| ***************************************************************/ |
| { |
| TERM Max, LitTerm; |
| LITERAL Lit; |
| ord_RESULT Compare; |
| int k, l; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsMaximal(clause_GetLiteral(Clause, i)) || |
| (Strict && |
| !clause_LiteralGetFlag(clause_GetLiteral(Clause, i), STRICTMAXIMAL))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_LitMax: Literal %d isn't %smaximal.", |
| i, Strict ? "strictly " : ""); |
| misc_FinishErrorReport(); |
| } |
| if (i < clause_FirstAntecedentLitIndex(Clause) || |
| i > clause_LastSuccedentLitIndex(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_LitMax: Literal index %d is out of range.", i); |
| misc_FinishErrorReport(); |
| } |
| /* If literal <i> is selected, there's no need to check for maximality, */ |
| /* if <i> isn't selected, but there're other literals selected, */ |
| /* inferences with literal <i> are forbidden. */ |
| if (clause_GetFlag(Clause, CLAUSESELECT)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_LitMax: There're selected literals.", i); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Lit = clause_GetLiteral(Clause, i); |
| /* Check necessary condition */ |
| if (!clause_LiteralIsMaximal(Lit) || |
| (Strict && !clause_LiteralGetFlag(Lit, STRICTMAXIMAL))) |
| return FALSE; |
| /* Only antecedent and succedent literals are compared, so if there's */ |
| /* only one such literal, it's maximal. */ |
| /* If the substitution is empty, the necessary condition tested above */ |
| /* is sufficient, too. */ |
| if ((clause_NumOfAnteLits(Clause) + clause_NumOfSuccLits(Clause) == 1) || |
| subst_Empty(Subst)) |
| return TRUE; |
| |
| l = clause_LastSuccedentLitIndex(Clause); |
| Max = subst_Apply(Subst,term_Copy(clause_GetLiteralTerm(Clause,i))); |
| |
| for (k = clause_FirstAntecedentLitIndex(Clause); k <= l; k++) |
| if (k != i && k != j && |
| clause_LiteralIsMaximal(clause_GetLiteral(Clause, k))) { |
| /* Only compare with maximal literals, since for every non-maximal */ |
| /* literal, there's at least one maximal literal, that is bigger. */ |
| LitTerm = subst_Apply(Subst,term_Copy(clause_GetLiteralTerm(Clause,k))); |
| Compare = ord_LiteralCompare(Max, |
| clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i)), |
| LitTerm, |
| clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,k)), |
| TRUE, Flags, Precedence); |
| if (Compare == ord_SmallerThan() || (Strict && Compare == ord_Equal())) { |
| term_Delete(Max); |
| term_Delete(LitTerm); |
| return FALSE; |
| } |
| term_Delete(LitTerm); |
| } |
| term_Delete(Max); |
| |
| return TRUE; |
| } |
| |
| |
| static BOOL inf_LiteralsMax(CLAUSE Clause, int i, SUBST Subst, |
| CLAUSE PartnerClause, int j, SUBST PartnerSubst, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: The parents of a resolution inference, the respective |
| literal indices and substitutions, a flag store and |
| a precedence. |
| RETURNS: TRUE iff the positive/negative literals are still |
| strictly maximal/maximal in the instantiated clause. |
| If a negative literal is selected, no comparison |
| is made. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if ((clause_GetFlag(Clause, CLAUSESELECT) && |
| !clause_LiteralGetFlag(clause_GetLiteral(Clause,i),LITSELECT)) || |
| (clause_GetFlag(PartnerClause, CLAUSESELECT) && |
| !clause_LiteralGetFlag(clause_GetLiteral(PartnerClause,j),LITSELECT))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_LiteralsMax: Another literal is selected."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (!clause_GetFlag(Clause, CLAUSESELECT) && |
| !inf_LitMax(Clause,i,-1,Subst, |
| i>clause_LastAntecedentLitIndex(Clause),Flags, Precedence)) |
| return FALSE; |
| if (!clause_GetFlag(PartnerClause, CLAUSESELECT) && |
| !inf_LitMax(PartnerClause,j,-1,PartnerSubst, |
| j>clause_LastAntecedentLitIndex(PartnerClause), Flags, Precedence)) |
| return FALSE; |
| |
| return TRUE; |
| } |
| |
| |
| static BOOL inf_LitMaxWith2Subst(CLAUSE Clause, int i, int j, SUBST Subst2, |
| SUBST Subst1, BOOL Strict, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, the index of a maximal literal, another |
| literal index, two substitutions, a boolean flag, |
| a flag store and a precedence. |
| RETURNS: In contrast to the function inf_LitMax this function |
| compares the literals with respect to the composition |
| of the two substitutions Subst2 ° Subst1. |
| If <Strict>=FALSE the function returns TRUE iff the |
| literal at index <i> is still maximal in the |
| instantiated clause. |
| If <Strict>=TRUE the function returns TRUE iff the |
| literal is STRICTLY maximal in the instantiated |
| clause. |
| The literal at index j is omitted at literal |
| comparison. |
| However, setting j to a negative number ensures that |
| all literals are compared with the literal at |
| index <i>. |
| CAUTION: DON'T call this function with a clause with selected |
| literals! |
| ***************************************************************/ |
| { |
| TERM Max, LitTerm; |
| LITERAL Lit; |
| ord_RESULT Compare; |
| int k, l; |
| |
| #ifdef CHECK |
| if (!clause_LiteralIsMaximal(clause_GetLiteral(Clause, i)) || |
| (Strict && |
| !clause_LiteralGetFlag(clause_GetLiteral(Clause, i), STRICTMAXIMAL))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_LitMaxWith2Subst: Literal %d isn't %smaximal.", |
| i, Strict ? "strictly " : ""); |
| misc_FinishErrorReport(); |
| } |
| if (i < clause_FirstAntecedentLitIndex(Clause) || |
| i > clause_LastSuccedentLitIndex(Clause)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_LitMaxWith2Subst: Literal index %d is out of range.", i); |
| misc_FinishErrorReport(); |
| } |
| /* If literal <i> is selected, there's no need to check for maximality, */ |
| /* if <i> isn't selected, but there're other literals selected, */ |
| /* inferences with literal <i> are forbidden. */ |
| if (clause_GetFlag(Clause, CLAUSESELECT)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_LitMaxWith2Subst: There're selected literals.", i); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Lit = clause_GetLiteral(Clause, i); |
| /* Check necessary condition */ |
| if (!clause_LiteralIsMaximal(Lit) || |
| (Strict && !clause_LiteralGetFlag(Lit, STRICTMAXIMAL))) |
| return FALSE; |
| /* Only antecedent and succedent literals are compared, so if there's */ |
| /* only one such literal, it's maximal. */ |
| /* If both substitutions are empty, the necessary condition tested above */ |
| /* is sufficient, too. */ |
| if ((clause_NumOfAnteLits(Clause) + clause_NumOfSuccLits(Clause) == 1) || |
| (subst_Empty(Subst1) && subst_Empty(Subst2))) |
| return TRUE; |
| |
| l = clause_LastSuccedentLitIndex(Clause); |
| Max = subst_Apply(Subst1, term_Copy(clause_GetLiteralTerm(Clause,i))); |
| Max = subst_Apply(Subst2, Max); |
| |
| for (k = clause_FirstAntecedentLitIndex(Clause); k <= l; k++) |
| if (k != i && k != j && |
| clause_LiteralIsMaximal(clause_GetLiteral(Clause, k))) { |
| /* Only compare with maximal literals, since for every non-maximal */ |
| /* literal, there's at least one maximal literal, that is bigger. */ |
| LitTerm = subst_Apply(Subst1,term_Copy(clause_GetLiteralTerm(Clause,k))); |
| LitTerm = subst_Apply(Subst2, LitTerm); |
| Compare = ord_LiteralCompare(Max, |
| clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i)), |
| LitTerm, |
| clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,k)), |
| TRUE, Flags, Precedence); |
| if (Compare == ord_SmallerThan() || (Strict && Compare == ord_Equal())) { |
| term_Delete(Max); |
| term_Delete(LitTerm); |
| return FALSE; |
| } |
| term_Delete(LitTerm); |
| } |
| term_Delete(Max); |
| |
| return TRUE; |
| } |
| |
| |
| static BOOL inf_LiteralsMaxWith2Subst(CLAUSE Clause, int i, CLAUSE PartnerClause, |
| int j, SUBST Subst2, SUBST Subst1, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: The parents of a resolution inference, the |
| respective literal indices and substitutions, a |
| flag store and a precedence. |
| RETURNS: In contrast to the function inf_LiteralsMax |
| the composition Subst2 ° Subst1 is applied to both |
| clauses. |
| The function returns TRUE iff the positive/negative |
| literals are still strictly maximal/maximal in the |
| instantiated clause. |
| If a negative literal is selected, no comparison |
| is made. |
| ***************************************************************/ |
| { |
| #ifdef CHECK |
| if ((clause_GetFlag(Clause, CLAUSESELECT) && |
| !clause_LiteralGetFlag(clause_GetLiteral(Clause,i),LITSELECT)) || |
| (clause_GetFlag(PartnerClause, CLAUSESELECT) && |
| !clause_LiteralGetFlag(clause_GetLiteral(PartnerClause,j),LITSELECT))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_LiteralsMaxWith2Subst: Another literal is selected."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (!clause_GetFlag(Clause, CLAUSESELECT) && |
| !inf_LitMaxWith2Subst(Clause, i, -1, Subst2, Subst1, |
| i>clause_LastAntecedentLitIndex(Clause), Flags, Precedence)) |
| return FALSE; |
| if (!clause_GetFlag(PartnerClause, CLAUSESELECT) && |
| !inf_LitMaxWith2Subst(PartnerClause, j, -1, Subst2, Subst1, |
| j>clause_LastAntecedentLitIndex(PartnerClause), Flags, Precedence)) |
| return FALSE; |
| |
| return TRUE; |
| } |
| |
| |
| /**************************************************************/ |
| /* Inference rules */ |
| /**************************************************************/ |
| |
| LIST inf_EqualityResolution(CLAUSE GivenClause, BOOL Ordered, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause and a flag determining whether ordering |
| constraints apply. |
| For <Ordered>=TRUE the function makes Equality Resolution |
| inferences, for <Ordered>=FALSE Reflexivity Resolution |
| inferences are made. |
| A flag store. |
| A precedence. |
| RETURNS: A list of clauses inferred from the GivenClause by |
| Equality/Reflexivity Resolution. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result; |
| LITERAL ActLit; |
| int i, last; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_EqualityResolution: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (clause_HasEmptyAntecedent(GivenClause) || |
| !clause_HasSolvedConstraint(GivenClause)) { |
| return list_Nil(); |
| } |
| |
| Result = list_Nil(); |
| last = clause_LastAntecedentLitIndex(GivenClause); |
| |
| for (i = clause_FirstAntecedentLitIndex(GivenClause); i <= last; i++) { |
| ActLit = clause_GetLiteral(GivenClause, i); |
| |
| if (clause_LiteralIsEquality(ActLit) && |
| (clause_LiteralGetFlag(ActLit,LITSELECT) || |
| (!clause_GetFlag(GivenClause,CLAUSESELECT) && |
| (!Ordered || clause_LiteralIsMaximal(ActLit))))) { |
| TERM Atom; |
| |
| Atom = clause_GetLiteralAtom(GivenClause, i); |
| |
| cont_Check(); |
| if (unify_UnifyCom(cont_LeftContext(), |
| term_FirstArgument(Atom), |
| term_SecondArgument(Atom))) { |
| SUBST mgu; |
| CLAUSE NewClause; |
| int j, k, bound; |
| |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| /* Check postcondition */ |
| if (clause_LiteralGetFlag(ActLit,LITSELECT) || |
| !Ordered || inf_LitMax(GivenClause, i, -1, mgu, |
| FALSE, Flags, Precedence)) { |
| |
| NewClause = clause_CreateBody(clause_Length(GivenClause) - 1); |
| clause_SetNumOfConsLits(NewClause, clause_NumOfConsLits(GivenClause)); |
| clause_SetNumOfAnteLits(NewClause, |
| (clause_NumOfAnteLits(GivenClause) - 1)); |
| clause_SetNumOfSuccLits(NewClause, clause_NumOfSuccLits(GivenClause)); |
| |
| bound = clause_LastLitIndex(GivenClause); |
| /* j iterates over the given clause, k iterates over the new one */ |
| for (j = k = clause_FirstLitIndex(); j <= bound; j++) { |
| if (j != i) { |
| clause_SetLiteral(NewClause, k, |
| clause_LiteralCreate(subst_Apply(mgu, |
| term_Copy(clause_GetLiteralTerm(GivenClause,j))),NewClause)); |
| k++; |
| } |
| } |
| clause_SetDataFromFather(NewClause, GivenClause, i, Flags, Precedence); |
| clause_SetFromEqualityResolution(NewClause); |
| |
| Result = list_Cons(NewClause, Result); |
| } |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| } /* end of if 'ActLit is maximal'. */ |
| } /*end of for 'all literals'. */ |
| return(Result); |
| } |
| |
| static CLAUSE inf_ApplyEqualityFactoring(CLAUSE Clause, TERM Left, TERM Right, |
| int i, int j, SUBST Subst, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, two terms, two indices in the clause, |
| a substitution, a flag store and a precedence. |
| RETURNS: A new clause, where <Left>=<Right> is added as antecedent atom, |
| the <i>th literal is deleted, the <j>th kept and |
| <Subst> is applied to a copy of <clause>. |
| ***************************************************************/ |
| { |
| CLAUSE NewClause; |
| TERM Atom; |
| int k,c,a,s; |
| |
| NewClause = clause_CreateBody(clause_Length(Clause)); |
| |
| c = clause_LastConstraintLitIndex(Clause); |
| clause_SetNumOfConsLits(NewClause, clause_NumOfConsLits(Clause)); |
| a = clause_LastAntecedentLitIndex(Clause); |
| clause_SetNumOfAnteLits(NewClause, clause_NumOfAnteLits(Clause) + 1); |
| s = clause_LastSuccedentLitIndex(Clause); |
| clause_SetNumOfSuccLits(NewClause, clause_NumOfSuccLits(Clause) - 1); |
| |
| for (k = clause_FirstLitIndex(); k <= c; k++) { |
| clause_SetLiteral(NewClause, k, |
| clause_LiteralCreate(subst_Apply(Subst, |
| term_Copy(clause_GetLiteralTerm(Clause, k))),NewClause)); |
| } |
| |
| for ( ; k <= a; k++) { |
| clause_SetLiteral(NewClause, k, |
| clause_LiteralCreate(subst_Apply(Subst, |
| term_Copy(clause_GetLiteralTerm(Clause, k))),NewClause)); |
| } |
| |
| Atom = term_Create(fol_Equality(), |
| list_Cons(term_Copy(Left),list_List(term_Copy(Right)))); |
| |
| clause_SetLiteral(NewClause, k, clause_LiteralCreate( |
| term_Create(fol_Not(), list_List(subst_Apply(Subst,Atom))), NewClause)); |
| |
| a = 1; /* Shift */ |
| |
| for ( ; k <= s; k++) { |
| if (k == i) |
| a = 0; |
| else { |
| clause_SetLiteral(NewClause, (k + a), |
| clause_LiteralCreate(subst_Apply(Subst, |
| term_Copy(clause_GetLiteralTerm(Clause, k))),NewClause)); |
| } |
| } |
| |
| clause_AddParentClause(NewClause, clause_Number(Clause)); |
| clause_AddParentLiteral(NewClause, j); |
| clause_SetDataFromFather(NewClause, Clause, i, Flags, Precedence); |
| |
| clause_SetFromEqualityFactoring(NewClause); |
| |
| return NewClause; |
| } |
| |
| |
| static BOOL inf_EqualityFactoringApplicable(CLAUSE Clause, int i, TERM Left, |
| TERM Right, SUBST Subst, |
| FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause <Clause>, the index <i> of a maximal |
| equality literal in <Clause> <j>, <Left> and |
| <Right> are the left and right side of the literal, |
| where <Right> is not greater than <Left> wrt the |
| ordering, a unifier <Subst>, a flag store and a |
| precedence. |
| RETURNS: TRUE iff the literal at index <i> is strictly |
| maximal in the instantiated clause and <Right> is |
| not greater than or equal to <Left> after |
| application of the substitution. |
| Otherwise, the function returns FALSE. |
| ***************************************************************/ |
| { |
| ord_RESULT Help; |
| |
| /* Literal oriented? */ |
| if (!clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause, i))) { |
| TERM NLeft, NRight; |
| NLeft = subst_Apply(Subst, term_Copy(Left)); |
| NRight = subst_Apply(Subst, term_Copy(Right)); |
| if ((Help = ord_Compare(NLeft,NRight,Flags, Precedence)) == ord_SmallerThan() || |
| Help == ord_Equal()) { |
| term_Delete(NLeft); |
| term_Delete(NRight); |
| return FALSE; |
| } |
| term_Delete(NLeft); |
| term_Delete(NRight); |
| } |
| /* Literal maximal? */ |
| return inf_LitMax(Clause, i, -1, Subst, FALSE, Flags, Precedence); |
| } |
| |
| |
| LIST inf_EqualityFactoring(CLAUSE GivenClause, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a flag store and a precedence. |
| RETURNS: A list of clauses derivable from 'GivenClause' by EF. |
| ***************************************************************/ |
| { |
| LIST Result; |
| LITERAL ActLit; |
| int i, j, last; |
| SUBST mgu; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_EqualityFactoring: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (clause_HasEmptySuccedent(GivenClause) || |
| clause_GetFlag(GivenClause, CLAUSESELECT) || |
| !clause_HasSolvedConstraint(GivenClause)) { |
| return list_Nil(); |
| } |
| |
| Result = list_Nil(); |
| |
| last = clause_LastSuccedentLitIndex(GivenClause); |
| |
| for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= last; i++) { |
| |
| ActLit = clause_GetLiteral(GivenClause, i); |
| |
| if (clause_LiteralIsMaximal(ActLit) && |
| clause_LiteralIsEquality(ActLit)) { |
| TERM Atom, Left, Right; |
| LITERAL PartnerLit; |
| |
| Atom = clause_LiteralAtom(ActLit); |
| Left = term_FirstArgument(Atom); |
| Right = term_SecondArgument(Atom); |
| |
| for (j = clause_FirstSuccedentLitIndex(GivenClause); j <= last; j++) { |
| PartnerLit = clause_GetLiteral(GivenClause, j); |
| if (i != j && clause_LiteralIsEquality(PartnerLit)) { |
| /* i==j can be excluded since this inference would either generate */ |
| /* a copy of the given clause (if one side of the equality is */ |
| /* unified with itself), or generate a tautology (if different */ |
| /* sides of the equality are unified). */ |
| TERM PartnerAtom, PartnerLeft, PartnerRight; |
| |
| PartnerAtom = clause_LiteralAtom(PartnerLit); |
| PartnerLeft = term_FirstArgument(PartnerAtom); |
| PartnerRight = term_SecondArgument(PartnerAtom); |
| |
| /* try <Left> and <PartnerLeft> */ |
| cont_Check(); |
| if (unify_UnifyCom(cont_LeftContext(), Left, PartnerLeft)) { |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| if (inf_EqualityFactoringApplicable(GivenClause, i, Left, Right, |
| mgu, Flags, Precedence)) |
| Result = list_Cons(inf_ApplyEqualityFactoring(GivenClause,Right, |
| PartnerRight,i,j, |
| mgu,Flags, |
| Precedence), |
| Result); |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| |
| /* try <Left> and <PartnerRight> */ |
| cont_Check(); |
| if (unify_UnifyCom(cont_LeftContext(), Left, PartnerRight)) { |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| |
| if (inf_EqualityFactoringApplicable(GivenClause, i, Left, Right, |
| mgu, Flags, Precedence)) |
| Result = list_Cons(inf_ApplyEqualityFactoring(GivenClause,Right, |
| PartnerLeft,i,j, |
| mgu,Flags, |
| Precedence), |
| Result); |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| |
| if (!clause_LiteralIsOrientedEquality(ActLit)) { |
| /* try <Right> and <PartnerLeft> */ |
| cont_Check(); |
| if (unify_UnifyCom(cont_LeftContext(), Right, PartnerLeft)) { |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| |
| if (inf_EqualityFactoringApplicable(GivenClause, i, Right, Left, |
| mgu, Flags, Precedence)) |
| Result = list_Cons(inf_ApplyEqualityFactoring(GivenClause,Left, |
| PartnerRight,i,j, |
| mgu,Flags, |
| Precedence), |
| Result); |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| |
| /* try <Right> and <PartnerRight> */ |
| cont_Check(); |
| if (unify_UnifyCom(cont_LeftContext(), Right, PartnerRight)) { |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| |
| if (inf_EqualityFactoringApplicable(GivenClause, i, Right, Left, |
| mgu, Flags, Precedence)) |
| Result = list_Cons(inf_ApplyEqualityFactoring(GivenClause,Left, |
| PartnerLeft,i,j, |
| mgu,Flags, |
| Precedence), |
| Result); |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| } |
| } |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| /* START of block with new term replacement */ |
| |
| static BOOL inf_NAllTermsRplac(TERM Term, TERM TestTerm, TERM RplacTerm, |
| SUBST Subst) |
| /************************************************************** |
| INPUT: Three terms, a substitution and an integer. |
| All occurrences of <TestTerm> in <Term> are replaced |
| by <RplacTerm>. The substitution <Subst> is applied to <Term>. |
| RETURNS: TRUE, if TestTerm was replaced by RplacTerm, |
| FALSE otherwise. |
| EFFECT: <Term> is destructively changed! |
| ***************************************************************/ |
| { |
| LIST ArgListNode; |
| BOOL Replaced; |
| int Bottom; |
| |
| Replaced = FALSE; |
| |
| /* check if whole term must be replaced */ |
| if (term_Equal(Term, TestTerm)) { |
| term_RplacTop(Term,term_TopSymbol(RplacTerm)); |
| ArgListNode = term_ArgumentList(Term); |
| term_RplacArgumentList(Term, term_CopyTermList(term_ArgumentList(RplacTerm))); |
| term_DeleteTermList(ArgListNode); |
| return TRUE; |
| } |
| |
| if (term_IsVariable(Term)) |
| subst_Apply(Subst, Term); |
| |
| /* if not, scan whole term. */ |
| if (!list_Empty(term_ArgumentList(Term))) { |
| |
| Bottom = stack_Bottom(); |
| stack_Push(term_ArgumentList(Term)); |
| |
| while (!stack_Empty(Bottom)) { |
| ArgListNode = stack_Top(); |
| Term = (TERM)list_Car(ArgListNode); |
| stack_RplacTop(list_Cdr(ArgListNode)); |
| |
| if (term_Equal(Term, TestTerm)) { |
| Replaced = TRUE; |
| list_Rplaca(ArgListNode, term_Copy(RplacTerm)); |
| term_Delete(Term); |
| } |
| else { |
| if (term_IsComplex(Term)) |
| stack_Push(term_ArgumentList(Term)); |
| else if (term_IsVariable(Term)) |
| subst_Apply(Subst,Term); |
| } |
| |
| /* remove empty lists (corresponding to scanned terms) */ |
| while (!stack_Empty(Bottom) && list_Empty(stack_Top())) |
| stack_Pop(); |
| } |
| } |
| return Replaced; |
| } |
| |
| |
| static TERM inf_AllTermsRplac(TERM Term, TERM TestTerm, TERM RplacTerm, |
| SUBST Subst) |
| /************************************************************** |
| INPUT: Three terms, a substitution. |
| All occurrences of <TestTerm> in A COPY of <Term> are replaced |
| by <RplacTerm>. The substitution <Subst> is applied to |
| the copy of <Term>. If no occurrence is found, |
| NULL is returned. |
| This function is not destructive |
| like NAllTermRplac. |
| RETURNS: TRUE, if TestTerm was replaced by RplacTerm, |
| FALSE otherwise. |
| ***************************************************************/ |
| { |
| TERM ActTerm = term_Copy(Term); |
| |
| if (!inf_NAllTermsRplac(ActTerm,TestTerm, RplacTerm, Subst )) { |
| term_Delete(ActTerm); |
| ActTerm = NULL; |
| } |
| |
| return(ActTerm); |
| } |
| |
| static TERM inf_AllTermsSideRplacs(TERM Term, TERM TestTerm, TERM RplacTerm, |
| SUBST Subst, BOOL Right) |
| /************************************************************** |
| INPUT: Three terms, a substitution and a boolean flag. |
| <Term> is typically an equality term. |
| RETURNS: If <TestTerm> occurs in the right (Right=TRUE) or |
| left side (Right=FALSE) of <Term>: |
| |
| A copy of the term where all occurrences of <TestTerm> |
| in the ENTIRE <Term> are replaced by <RplacTerm> and |
| the substitution <Subst> is applied to all other subterms. |
| |
| If <TestTerm> does not occur in the right/left side of |
| <Term>, NULL is returned. |
| |
| In non-equality terms, The 'sides' correspond to the |
| first and second argument of the term. |
| ***************************************************************/ |
| { |
| TERM ActTerm = term_Copy(Term); |
| TERM ReplSide, OtherSide; /* ReplSide is the side in which terms are |
| replaced */ |
| |
| if (Right) { |
| ReplSide = term_SecondArgument(ActTerm); |
| OtherSide = term_FirstArgument(ActTerm); |
| } |
| else { |
| ReplSide = term_FirstArgument(ActTerm); |
| OtherSide = term_SecondArgument(ActTerm); |
| } |
| |
| if (inf_NAllTermsRplac(ReplSide, TestTerm, RplacTerm, Subst)) |
| /* If <TestTerm> occurs in <ReplSide> also replace it in <OtherSide>. */ |
| inf_NAllTermsRplac(OtherSide, TestTerm, RplacTerm, Subst); |
| else { |
| term_Delete(ActTerm); |
| ActTerm = NULL; |
| } |
| |
| return ActTerm; |
| } |
| |
| |
| static TERM inf_AllTermsRightRplac(TERM Term, TERM TestTerm, TERM RplacTerm, |
| SUBST Subst) |
| /************************************************************** |
| INPUT: Three terms, a substitution. |
| <Term> is typically an equality term. |
| RETURNS: See inf_AllTermSideRplac with argument |
| 'Right' set to TRUE |
| **************************************************************/ |
| { |
| return(inf_AllTermsSideRplacs(Term, TestTerm, RplacTerm, Subst, TRUE)); |
| } |
| |
| |
| static TERM inf_AllTermsLeftRplac(TERM Term, TERM TestTerm, TERM RplacTerm, |
| SUBST Subst) |
| /************************************************************** |
| INPUT: Three terms, a substitution. |
| <Term> is typically an equality term. |
| RETURNS: See inf_AllTermSideRplac with argument |
| 'Right' set to FALSE. |
| ***************************************************************/ |
| { |
| return(inf_AllTermsSideRplacs(Term, TestTerm, RplacTerm, Subst, FALSE)); |
| } |
| |
| |
| /* END of block with new term replacement */ |
| |
| |
| static CLAUSE inf_ApplyGenSuperposition(CLAUSE Clause, int ci, SUBST Subst, |
| CLAUSE PartnerClause, int pci, |
| SUBST PartnerSubst, TERM SupAtom, |
| BOOL Right, BOOL OrdPara, BOOL MaxPara, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: Two clauses where a generalized superposition inference can be |
| applied using the positive equality literal <i> from <Clause> with |
| subst <Subst> using the literal <j> from <PartnerClause> with subst |
| <PartnerSubst> where SupAtom is a derivable atom. Returns |
| NULL if SupAtom is NULL. |
| |
| Right is TRUE if the inference is a superposition right inference |
| Right is FALSE if the inference is a superposition left inference, |
| |
| where the inference is selected by MaxPara and OrdPara: |
| (see also inf_GenSuperpositionLeft) |
| |
| OrdPara=TRUE, MaxPara=TRUE |
| -> Superposition (Left or Right) |
| |
| OrdPara=TRUE, MaxPara=FALSE |
| -> ordered Paramodulation |
| |
| OrdPara=FALSE, MaxPara=FALSE |
| -> simple Paramodulation |
| |
| OrdPara=FALSE, MaxPara=TRUE |
| -> not defined |
| |
| A flag store. |
| A precedence. |
| RETURNS: The new clause. |
| MEMORY: Memory for the new clause is allocated. |
| ***************************************************************/ |
| { |
| CLAUSE NewClause; |
| int j,lc,la,ls,pls,pla,plc,help; |
| |
| #ifdef CHECK |
| if (!OrdPara && MaxPara) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_ApplyGenSuperposition : Illegal inference"); |
| misc_ErrorReport("\n rule selection, OrdPara=FALSE and MaxPara=TRUE."); |
| misc_FinishErrorReport(); |
| } |
| if (SupAtom == NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_ApplyGenSuperposition: Atom is NULL."); |
| misc_FinishErrorReport(); |
| return clause_Null(); |
| } |
| #endif |
| |
| pls = clause_LastSuccedentLitIndex(PartnerClause); |
| pla = clause_LastAntecedentLitIndex(PartnerClause); |
| plc = clause_LastConstraintLitIndex(PartnerClause); |
| |
| ls = clause_LastSuccedentLitIndex(Clause); |
| la = clause_LastAntecedentLitIndex(Clause); |
| lc = clause_LastConstraintLitIndex(Clause); |
| |
| |
| NewClause = clause_CreateBody(clause_Length(Clause) - 1 + |
| clause_Length(PartnerClause)); |
| |
| clause_SetNumOfConsLits(NewClause, (clause_NumOfConsLits(Clause) + |
| clause_NumOfConsLits(PartnerClause))); |
| clause_SetNumOfAnteLits(NewClause, (clause_NumOfAnteLits(Clause) + |
| clause_NumOfAnteLits(PartnerClause))); |
| clause_SetNumOfSuccLits(NewClause, ((clause_NumOfSuccLits(Clause) -1)+ |
| clause_NumOfSuccLits(PartnerClause))); |
| |
| /* First set the literals from the Clause : */ |
| |
| for (j = clause_FirstLitIndex(); j <= lc; j++) { |
| clause_SetLiteral(NewClause, j, |
| clause_LiteralCreate(subst_Apply(Subst, term_Copy( |
| clause_GetLiteralTerm(Clause, j))),NewClause)); |
| } |
| |
| /* help = number of literals to leave empty */ |
| help = clause_NumOfConsLits(PartnerClause); |
| |
| for ( ; j <= la; j++) { |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(Subst, term_Copy( |
| clause_GetLiteralTerm(Clause, j))),NewClause)); |
| } |
| |
| /* help = number of literals to leave empty */ |
| help += clause_NumOfAnteLits(PartnerClause); |
| |
| for ( ; j <= ls; j++) { |
| if (j != ci) { |
| /* The literal used in the inference isn't copied */ |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(Subst, |
| term_Copy(clause_GetLiteralTerm(Clause, j))),NewClause)); |
| |
| } else { |
| /*the index has to be decreased to avoid an empty literal! */ |
| help--; |
| } |
| } |
| |
| /* Now we consider the PartnerClause : */ |
| |
| /* help = number of already set constraint (Clause) literals */ |
| help = clause_NumOfConsLits(Clause); |
| |
| for (j = clause_FirstLitIndex(); j <= plc; j++) { |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(PartnerSubst, |
| term_Copy(clause_GetLiteralTerm(PartnerClause, j))),NewClause)); |
| } |
| |
| /* help = number of already set constraint and antecedent Given-literals */ |
| help += clause_NumOfAnteLits(Clause); |
| |
| for ( ; j <= pla; j++) { |
| if (j != pci) { |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(PartnerSubst, |
| term_Copy(clause_GetLiteralTerm(PartnerClause, j))),NewClause)); |
| } else { |
| /* The PartnerLit is modified appropriately! */ |
| clause_SetLiteral(NewClause, (j + help), clause_LiteralCreate( |
| term_Create(fol_Not(),list_List(SupAtom)), NewClause)); |
| } |
| } |
| |
| |
| /* help = number of already set Given-literals */ |
| help = clause_Length(Clause) - 1; |
| |
| for ( ; j <= pls; j++) { |
| if (j != pci) { |
| /* The PartnerLit isn't copied! */ |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(PartnerSubst, |
| term_Copy(clause_GetLiteralTerm(PartnerClause, j))),NewClause)); |
| |
| } else { |
| /* The PartnerLit is modified appropriately! */ |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(SupAtom, NewClause)); |
| } |
| } |
| |
| /* |
| * Set inference type. Note that, in the case of (ordered) paramodulation, |
| * we do not distinguish which side was paramodulated into, as compared |
| * to the case of superposition. |
| */ |
| |
| if (OrdPara && MaxPara) { |
| if (Right) |
| clause_SetFromSuperpositionRight(NewClause); |
| else |
| clause_SetFromSuperpositionLeft(NewClause); |
| } |
| else if (OrdPara && !MaxPara) |
| clause_SetFromOrderedParamodulation(NewClause); |
| else |
| clause_SetFromParamodulation(NewClause); |
| |
| clause_SetDataFromParents(NewClause, PartnerClause, pci, Clause, ci, Flags, |
| Precedence); |
| |
| return NewClause; |
| } |
| |
| |
| /* START of block with new superposition right rule */ |
| |
| static LIST inf_GenLitSPRight(CLAUSE Clause, TERM Left, TERM Right, int i, |
| SHARED_INDEX ShIndex, BOOL OrdPara, BOOL MaxPara, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause (unshared) with a positive equality literal |
| at position <i> where <Left> and <Right> are the arguments |
| of just that literal and <Right> is not greater wrt. the |
| ordering than <Left>, |
| two boolean flags for controlling inference |
| preconditions (see inf_GenSuperpositionRight), |
| a flag store and a precedence. |
| RETURNS: A list of clauses derivable with the literals owning |
| clause by general superposition right wrt. the Index. |
| (see inf_GenSuperpositionRight for selection of inference |
| rule by OrdPara/MaxPara) |
| MEMORY: The list of clauses is extended, where memory for the |
| list and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, Terms; |
| |
| Result = list_Nil(); |
| Terms = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), Left); |
| |
| for ( ; !list_Empty(Terms); Terms = list_Pop(Terms)) { |
| LIST Lits; |
| TERM Term; |
| |
| Term = (TERM)list_First(Terms); |
| |
| if (!term_IsVariable(Term) && !symbol_IsPredicate(term_TopSymbol(Term))) { |
| |
| Lits = sharing_GetDataList(Term, ShIndex); |
| |
| for ( ; !list_Empty(Lits); Lits = list_Pop(Lits)) { |
| LITERAL PartnerLit; |
| TERM PartnerAtom; |
| CLAUSE PartnerClause; |
| int pli; |
| |
| PartnerLit = (LITERAL)list_Car(Lits); |
| PartnerAtom = clause_LiteralAtom(PartnerLit); |
| pli = clause_LiteralGetIndex(PartnerLit); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| |
| if (!clause_GetFlag(PartnerClause,CLAUSESELECT) && |
| (!MaxPara || clause_LiteralGetFlag(PartnerLit,STRICTMAXIMAL)) && |
| !clause_GetFlag(PartnerClause,NOPARAINTO) && |
| clause_LiteralIsPositive(PartnerLit) && |
| clause_HasSolvedConstraint(PartnerClause)) { |
| |
| SUBST Subst, PartnerSubst; |
| TERM NewLeft,NewRight; |
| SYMBOL PartnerMaxVar; |
| TERM SupAtom; |
| |
| SupAtom = (TERM)NULL; |
| |
| PartnerMaxVar = clause_MaxVar(PartnerClause); |
| NewLeft = Left; |
| clause_RenameVarsBiggerThan(Clause, PartnerMaxVar); |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), Left, cont_RightContext(), Term); |
| subst_ExtractUnifier(cont_LeftContext(), &Subst, cont_RightContext(), &PartnerSubst); |
| cont_Reset(); |
| if (!MaxPara || |
| inf_LiteralsMax(Clause, i, Subst, PartnerClause, pli, |
| PartnerSubst, Flags, Precedence)) { |
| NewRight = subst_Apply(Subst, term_Copy(Right)); |
| if (OrdPara && |
| !clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i))) |
| NewLeft = subst_Apply(Subst, term_Copy(Left)); |
| if (!OrdPara || |
| NewLeft == Left || /* TRUE, if oriented */ |
| ord_Compare(NewLeft,NewRight, Flags, Precedence) != ord_SmallerThan()) { |
| if (!MaxPara || clause_LiteralIsPredicate(PartnerLit)) { |
| SupAtom = inf_AllTermsRplac(PartnerAtom, Term, |
| NewRight, PartnerSubst); |
| } else { |
| /* Superposition and <PartnerLit> is equality */ |
| if (clause_LiteralIsOrientedEquality(PartnerLit)) |
| SupAtom = inf_AllTermsLeftRplac(PartnerAtom, Term, |
| NewRight, PartnerSubst); |
| else { |
| TERM NewPartnerLeft,NewPartnerRight; |
| NewPartnerLeft = |
| subst_Apply(PartnerSubst, |
| term_Copy(term_FirstArgument(PartnerAtom))); |
| NewPartnerRight = |
| subst_Apply(PartnerSubst, |
| term_Copy(term_SecondArgument(PartnerAtom))); |
| switch (ord_Compare(NewPartnerLeft,NewPartnerRight, |
| Flags, Precedence)) { |
| case ord_SMALLER_THAN: |
| SupAtom = inf_AllTermsRightRplac(PartnerAtom,Term, |
| NewRight,PartnerSubst); |
| break; |
| case ord_GREATER_THAN: |
| SupAtom = inf_AllTermsLeftRplac(PartnerAtom,Term, |
| NewRight,PartnerSubst); |
| break; |
| default: |
| SupAtom = inf_AllTermsRplac(PartnerAtom,Term, |
| NewRight,PartnerSubst); |
| } |
| term_Delete(NewPartnerLeft); |
| term_Delete(NewPartnerRight); |
| } |
| } |
| |
| if (SupAtom != NULL) |
| Result = |
| list_Cons(inf_ApplyGenSuperposition(Clause, i, Subst, |
| PartnerClause, pli, |
| PartnerSubst, SupAtom, |
| TRUE, OrdPara, MaxPara, |
| Flags, Precedence), |
| Result); |
| } |
| if (NewLeft != Left) |
| term_Delete(NewLeft); |
| term_Delete(NewRight); |
| } |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| static LIST inf_GenSPRightEqToGiven(CLAUSE Clause, int i, BOOL Left, |
| SHARED_INDEX ShIndex, BOOL OrdPara, |
| BOOL MaxPara, BOOL Unit, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An unshared clause, the index of a succedent literal |
| that is an equality literal and a boolean value which |
| argument to use: |
| If Left==TRUE then the left argument is used |
| otherwise the right argument. |
| Three boolean flags for controlling inference |
| preconditions (see inf_GenSuperpositionRight). |
| A flag store. |
| A precedence. |
| RETURNS: A list of clauses derivable from general superposition right on the |
| GivenCopy wrt. the Index. |
| (see inf_GenSuperpositionRight for selection of inference |
| rule by OrdPara/MaxPara) |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, TermList, Parents; |
| int Bottom; |
| LITERAL Lit; |
| TERM Atom, Term, PartnerTerm, PartnerEq; |
| |
| Result = list_Nil(); |
| Lit = clause_GetLiteral(Clause,i); |
| Atom = clause_LiteralAtom(Lit); |
| |
| #ifdef CHECK |
| if (!fol_IsEquality(Atom) || |
| (MaxPara && clause_LiteralIsOrientedEquality(Lit) && !Left) || |
| (MaxPara && !clause_LiteralGetFlag(Lit, STRICTMAXIMAL))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPRightEqToGiven: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Bottom = stack_Bottom(); |
| if (Left) /* Top Level considered in inf_LitSPRight */ |
| sharing_PushListOnStack(term_ArgumentList(term_FirstArgument(Atom))); |
| else |
| sharing_PushListOnStack(term_ArgumentList(term_SecondArgument(Atom))); |
| |
| while (!stack_Empty(Bottom)) { |
| Term = (TERM)stack_PopResult(); |
| if (!term_IsVariable(Term)) { |
| /* Superposition into variables is not necessary */ |
| TermList = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), Term); |
| for ( ; !list_Empty(TermList); TermList = list_Pop(TermList)) { |
| PartnerTerm = (TERM)list_Car(TermList); |
| for (Parents = term_SupertermList(PartnerTerm); |
| !list_Empty(Parents); Parents = list_Cdr(Parents)) { |
| PartnerEq = (TERM)list_Car(Parents); |
| if (fol_IsEquality(PartnerEq)) { |
| CLAUSE PartnerClause; |
| LITERAL PartnerLit; |
| LIST Scl; |
| int j; |
| for (Scl = sharing_NAtomDataList(PartnerEq); |
| !list_Empty(Scl); Scl = list_Cdr(Scl)) { |
| PartnerLit = (LITERAL)list_Car(Scl); |
| j = clause_LiteralGetIndex(PartnerLit); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| if (!clause_GetFlag(PartnerClause,CLAUSESELECT) && |
| (!MaxPara || |
| clause_LiteralGetFlag(PartnerLit,STRICTMAXIMAL)) && |
| (!OrdPara || PartnerTerm==term_FirstArgument(PartnerEq) || |
| !clause_LiteralIsOrientedEquality(PartnerLit)) && |
| clause_LiteralIsPositive(PartnerLit) && |
| clause_Number(PartnerClause) != clause_Number(Clause) && |
| (!Unit || clause_Length(PartnerClause) == 1) && |
| clause_HasSolvedConstraint(PartnerClause)) { |
| /* We exclude the same clause since that inference will be */ |
| /* made by the "forward" function inf_GenLitSPRight. */ |
| SYMBOL MaxVar; |
| SUBST Subst, PartnerSubst; |
| |
| MaxVar = clause_MaxVar(PartnerClause); |
| clause_RenameVarsBiggerThan(Clause, MaxVar); |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), Term, cont_RightContext(), |
| PartnerTerm); |
| subst_ExtractUnifier(cont_LeftContext(), &Subst, |
| cont_RightContext(), &PartnerSubst); |
| cont_Reset(); |
| if (!MaxPara || |
| inf_LiteralsMax(Clause, i, Subst, PartnerClause, j, |
| PartnerSubst, Flags, Precedence)) { |
| TERM PartnerLeft,PartnerRight; |
| BOOL Check, PartnerCheck; |
| PartnerLeft = PartnerRight = NULL; |
| PartnerCheck = Check = TRUE; |
| if (OrdPara && |
| !clause_LiteralIsOrientedEquality(PartnerLit)) { |
| /* Check post condition for partner literal */ |
| if (PartnerTerm == term_FirstArgument(PartnerEq)) |
| PartnerRight = term_SecondArgument(PartnerEq); |
| else |
| PartnerRight = term_FirstArgument(PartnerEq); |
| PartnerLeft = subst_Apply(PartnerSubst, |
| term_Copy(PartnerTerm)); |
| PartnerRight = subst_Apply(PartnerSubst, |
| term_Copy(PartnerRight)); |
| PartnerCheck = (ord_Compare(PartnerLeft, PartnerRight, |
| Flags, Precedence) |
| != ord_SmallerThan()); |
| } |
| if (PartnerCheck && |
| MaxPara && !clause_LiteralIsOrientedEquality(Lit)) { |
| /* Check post condition for literal in given clause */ |
| TERM NewLeft, NewRight; |
| if (Left) { |
| NewLeft = term_FirstArgument(Atom); |
| NewRight = term_SecondArgument(Atom); |
| } else { |
| NewLeft = term_SecondArgument(Atom); |
| NewRight = term_FirstArgument(Atom); |
| } |
| NewLeft = subst_Apply(Subst, term_Copy(NewLeft)); |
| NewRight = subst_Apply(Subst, term_Copy(NewRight)); |
| Check = (ord_Compare(NewLeft, NewRight, Flags, Precedence) |
| != ord_SmallerThan()); |
| term_Delete(NewLeft); |
| term_Delete(NewRight); |
| } |
| if (Check && PartnerCheck) { |
| /* Make inference only if both tests were successful */ |
| TERM SupAtom; |
| SupAtom = NULL; |
| if (PartnerRight == NULL) { |
| if (PartnerTerm==term_FirstArgument(PartnerEq)) |
| PartnerRight = term_SecondArgument(PartnerEq); |
| else |
| PartnerRight = term_FirstArgument(PartnerEq); |
| PartnerRight = subst_Apply(PartnerSubst, |
| term_Copy(PartnerRight)); |
| } |
| if (Left) |
| SupAtom = inf_AllTermsLeftRplac(Atom, Term, |
| PartnerRight, Subst); |
| else |
| SupAtom = inf_AllTermsRightRplac(Atom, Term, |
| PartnerRight, Subst); |
| #ifdef CHECK |
| if (SupAtom == NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPRightEqToGiven:"); |
| misc_ErrorReport(" replacement wasn't possible."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| Result = |
| list_Cons(inf_ApplyGenSuperposition(PartnerClause, j, |
| PartnerSubst, Clause, |
| i, Subst, SupAtom, |
| TRUE,OrdPara,MaxPara, |
| Flags, Precedence), |
| Result); |
| } |
| if (PartnerLeft != term_Null()) |
| term_Delete(PartnerLeft); |
| if (PartnerRight != term_Null()) |
| term_Delete(PartnerRight); |
| } |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } |
| } |
| } |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| static LIST inf_GenSPRightLitToGiven(CLAUSE Clause, int i, TERM Atom, |
| SHARED_INDEX ShIndex, BOOL OrdPara, |
| BOOL MaxPara, BOOL Unit, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An unshared clause, the index of a succedent literal |
| that is not an equality literal and its atom, |
| three boolean flags for controlling inference |
| preconditions (see inf_GenSuperpositionRight), |
| a flag store and a precedence. |
| RETURNS: A list of clauses derivable from general superposition right on the |
| GivenCopy wrt. the Index. |
| (see inf_GenSuperpositionRight for selection of inference |
| rule by OrdPara/MaxPara) |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, TermList, ParentList; |
| int Bottom; |
| TERM Term, PartnerTerm, PartnerEq; |
| |
| Result = list_Nil(); |
| |
| Bottom = stack_Bottom(); |
| sharing_PushListOnStack(term_ArgumentList(Atom)); |
| |
| while (!stack_Empty(Bottom)) { |
| Term = (TERM)stack_PopResult(); |
| if (!term_IsVariable(Term)) { |
| /* Superposition into variables is not necessary */ |
| TermList = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), Term); |
| for ( ; !list_Empty(TermList); TermList=list_Pop(TermList)) { |
| PartnerTerm = (TERM)list_Car(TermList); |
| for (ParentList = term_SupertermList(PartnerTerm); |
| !list_Empty(ParentList); ParentList = list_Cdr(ParentList)) { |
| PartnerEq = (TERM)list_Car(ParentList); |
| if (fol_IsEquality(PartnerEq)) { |
| CLAUSE PartnerClause; |
| LITERAL PartnerLit; |
| LIST Scl; |
| int j; |
| for (Scl = sharing_NAtomDataList(PartnerEq); |
| !list_Empty(Scl); Scl = list_Cdr(Scl)) { |
| PartnerLit = (LITERAL)list_Car(Scl); |
| j = clause_LiteralGetIndex(PartnerLit); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| if (!clause_GetFlag(PartnerClause,CLAUSESELECT) && |
| (!MaxPara || |
| clause_LiteralGetFlag(PartnerLit,STRICTMAXIMAL)) && |
| (!OrdPara || PartnerTerm==term_FirstArgument(PartnerEq) || |
| !clause_LiteralIsOrientedEquality(PartnerLit)) && |
| clause_LiteralIsPositive(PartnerLit) && |
| clause_Number(PartnerClause) != clause_Number(Clause) && |
| (!Unit || clause_Length(PartnerClause) == 1) && |
| clause_HasSolvedConstraint(PartnerClause)) { |
| /* We exclude the same clause since that inference will be */ |
| /* made by the "forward" function inf_GenLitSPRight. */ |
| SYMBOL MaxVar; |
| TERM PartnerLeft,PartnerRight; |
| SUBST Subst, PartnerSubst; |
| TERM SupAtom; |
| |
| SupAtom = (TERM)NULL; |
| MaxVar = clause_MaxVar(PartnerClause); |
| clause_RenameVarsBiggerThan(Clause,MaxVar); |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), Term, |
| cont_RightContext(),PartnerTerm); |
| subst_ExtractUnifier(cont_LeftContext(), &Subst, |
| cont_RightContext(),&PartnerSubst); |
| cont_Reset(); |
| |
| if (!MaxPara || |
| inf_LiteralsMax(Clause, i, Subst, PartnerClause, j, |
| PartnerSubst, Flags, Precedence)) { |
| PartnerLeft = subst_Apply(PartnerSubst, |
| term_Copy(PartnerTerm)); |
| if (PartnerTerm == term_FirstArgument(PartnerEq)) |
| PartnerRight = |
| subst_Apply(PartnerSubst, |
| term_Copy(term_SecondArgument(PartnerEq))); |
| else |
| PartnerRight = |
| subst_Apply(PartnerSubst, |
| term_Copy(term_FirstArgument(PartnerEq))); |
| |
| if (!OrdPara || |
| clause_LiteralIsOrientedEquality(PartnerLit) || |
| ord_Compare(PartnerLeft,PartnerRight, Flags, Precedence) |
| != ord_SmallerThan()) { |
| SupAtom = inf_AllTermsRplac(Atom,Term,PartnerRight,Subst); |
| #ifdef CHECK |
| if (SupAtom == NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPRightLitToGiven:"); |
| misc_ErrorReport(" replacement wasn't possible."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| Result = |
| list_Cons(inf_ApplyGenSuperposition(PartnerClause, j, |
| PartnerSubst, Clause, |
| i, Subst, SupAtom, |
| TRUE,OrdPara,MaxPara, |
| Flags, Precedence), |
| Result); |
| |
| } |
| term_Delete(PartnerLeft); |
| term_Delete(PartnerRight); |
| } |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } |
| } |
| } |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| static LIST inf_GenSPRightToGiven(CLAUSE Clause, int i, SHARED_INDEX ShIndex, |
| BOOL OrdPara, BOOL MaxPara, BOOL Unit, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An unshared clause, the index of a succedent literal |
| and an index of shared clauses, |
| three boolean flags for controlling inference |
| preconditions (see inf_GenSuperpositionRight), |
| a flag store and a precedence. |
| RETURNS: A list of clauses derivable from superposition right on the |
| GivenCopy wrt. the Index. |
| (see inf_GenSuperpositionRight for selection of inference |
| rule by OrdPara/MaxPara) |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| TERM Atom; |
| LIST Result; |
| |
| #ifdef CHECK |
| if (clause_GetFlag(Clause, NOPARAINTO) || |
| clause_GetFlag(Clause, CLAUSESELECT) || |
| (MaxPara && |
| !clause_LiteralGetFlag(clause_GetLiteral(Clause,i), STRICTMAXIMAL))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPRightToGiven: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i)); |
| |
| if (fol_IsEquality(Atom)) { |
| Result = list_Nconc(inf_GenSPRightEqToGiven(Clause,i,TRUE,ShIndex,OrdPara, |
| MaxPara,Unit,Flags, Precedence), |
| Result); |
| |
| if (!MaxPara || |
| !clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i))) |
| /* For SPm and OPm always try other direction, for SpR try it */ |
| /* only if the literal is not oriented. */ |
| Result = list_Nconc(inf_GenSPRightEqToGiven(Clause, i, FALSE, ShIndex, |
| OrdPara,MaxPara,Unit, |
| Flags, Precedence), |
| Result); |
| } else |
| Result = list_Nconc(inf_GenSPRightLitToGiven(Clause,i,Atom,ShIndex, |
| OrdPara,MaxPara,Unit, |
| Flags, Precedence), |
| Result); |
| |
| return Result; |
| } |
| |
| |
| LIST inf_GenSuperpositionRight(CLAUSE GivenClause, SHARED_INDEX ShIndex, |
| BOOL OrdPara, BOOL MaxPara, BOOL Unit, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause and an Index, usually the WorkedOffIndex, |
| three boolean flags for controlling inference |
| preconditions, a flag store and a precedence. |
| RETURNS: A list of clauses derivable from the given clause by |
| superposition right wrt. the Index. |
| |
| OrdPara=TRUE, MaxPara=TRUE |
| -> Superposition Right |
| |
| OrdPara=TRUE, MaxPara=FALSE |
| -> ordered Paramodulation |
| |
| OrdPara=FALSE, MaxPara=FALSE |
| -> simple Paramodulation |
| |
| OrdPara=FALSE, MaxPara=TRUE |
| -> not defined |
| |
| If <Unit>==TRUE the clause with the maximal equality |
| additionally must be a unit clause. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result; |
| TERM Atom; |
| CLAUSE Copy; |
| int i, n; |
| LITERAL ActLit; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSuperpositionRight: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| if (!OrdPara && MaxPara) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSuperpositionRight: Illegal inference"); |
| misc_ErrorReport("\n rule selection, OrdPara=FALSE & MaxPara=TRUE."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (clause_GetFlag(GivenClause,CLAUSESELECT) || |
| clause_HasEmptySuccedent(GivenClause) || |
| !clause_HasSolvedConstraint(GivenClause)) |
| return list_Nil(); |
| |
| Result = list_Nil(); |
| |
| Copy = clause_Copy(GivenClause); |
| n = clause_LastSuccedentLitIndex(Copy); |
| |
| for (i = clause_FirstSuccedentLitIndex(Copy); i <= n; i++) { |
| |
| ActLit = clause_GetLiteral(Copy, i); |
| Atom = clause_LiteralSignedAtom(ActLit); |
| |
| if (!MaxPara || |
| clause_LiteralGetFlag(ActLit,STRICTMAXIMAL)) { |
| if (fol_IsEquality(Atom) && |
| (!Unit || clause_Length(GivenClause) == 1)) { |
| |
| Result = list_Nconc(inf_GenLitSPRight(Copy, term_FirstArgument(Atom), |
| term_SecondArgument(Atom), i, |
| ShIndex,OrdPara,MaxPara,Flags, |
| Precedence), |
| Result); |
| |
| if (!OrdPara || |
| !clause_LiteralIsOrientedEquality(ActLit)) |
| Result = list_Nconc(inf_GenLitSPRight(Copy, |
| term_SecondArgument(Atom), |
| term_FirstArgument(Atom), i, |
| ShIndex,OrdPara,MaxPara,Flags, |
| Precedence), |
| Result); |
| } |
| if (!clause_GetFlag(Copy, NOPARAINTO)) |
| Result = list_Nconc(inf_GenSPRightToGiven(Copy, i, ShIndex, OrdPara, |
| MaxPara,Unit,Flags,Precedence), |
| Result); |
| } |
| } |
| clause_Delete(Copy); |
| |
| return Result; |
| } |
| |
| |
| |
| /* END of block with new superposition right rule */ |
| |
| |
| static LIST inf_ApplyMParamod(CLAUSE C1, CLAUSE C2, int i, int j, int k, |
| TERM u_tau, TERM v, TERM s2, TERM t, |
| TERM v2_sigma, SUBST tau, SUBST rho, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: Two clauses, <i> is a literal index in <C1>, <j> and <k> |
| are literal indices in <C2>, <u_tau> with <rho> applied |
| is used as left side of the two new literals, <v> with |
| subterm <s2> replaced by <t> is used as right side of |
| the first new literal, <v2_sigma> as right side of the |
| second new literal, two substitutions and a flag store. |
| The substitution <rho> is applied after <tau>. |
| A flag store. |
| A precedence. |
| RETURNS: A list containing one clause derived from the given |
| clauses and literals by merging paramodulation. |
| MEMORY: Memory for the list and the clause is allocated. |
| ***************************************************************/ |
| { |
| CLAUSE newClause; |
| TERM u_sigma; |
| int m, lc, la, ls, pls, pla, plc, help; |
| |
| pls = clause_LastSuccedentLitIndex(C2); |
| pla = clause_LastAntecedentLitIndex(C2); |
| plc = clause_LastConstraintLitIndex(C2); |
| |
| ls = clause_LastSuccedentLitIndex(C1); |
| la = clause_LastAntecedentLitIndex(C1); |
| lc = clause_LastConstraintLitIndex(C1); |
| |
| newClause = clause_CreateBody(clause_Length(C1) + clause_Length(C2) - 1); |
| |
| clause_SetNumOfConsLits(newClause, (clause_NumOfConsLits(C1) + |
| clause_NumOfConsLits(C2))); |
| clause_SetNumOfAnteLits(newClause, (clause_NumOfAnteLits(C1) + |
| clause_NumOfAnteLits(C2))); |
| clause_SetNumOfSuccLits(newClause, (clause_NumOfSuccLits(C1) - 1 + |
| clause_NumOfSuccLits(C2))); |
| |
| for (m = clause_FirstLitIndex(); m <= lc; m++) |
| clause_SetLiteral(newClause, m, |
| clause_LiteralCreate(subst_Apply(rho, subst_Apply(tau, |
| term_Copy(clause_GetLiteralTerm(C1, m)))), newClause)); |
| |
| /* help = number of literals to leave empty */ |
| help = clause_NumOfConsLits(C2); |
| |
| for ( ; m <= la; m++) |
| clause_SetLiteral(newClause, (m + help), |
| clause_LiteralCreate(subst_Apply(rho, subst_Apply(tau, |
| term_Copy(clause_GetLiteralTerm(C1, m)))), newClause)); |
| |
| /* help = number of literals to leave empty */ |
| help += clause_NumOfAnteLits(C2); |
| |
| for ( ; m <= ls; m++) { |
| if (m != i) |
| /* The literal used in the inference isn't copied */ |
| clause_SetLiteral(newClause, (m + help), |
| clause_LiteralCreate(subst_Apply(rho, subst_Apply(tau, |
| term_Copy(clause_GetLiteralTerm(C1, m)))),newClause)); |
| else |
| /* the index has to be decreased to avoid an empty literal! */ |
| help--; |
| } |
| |
| /* Now we consider the PartnerClause : */ |
| |
| /* help = number of already set constraint (Clause) literals */ |
| help = clause_NumOfConsLits(C1); |
| |
| for (m = clause_FirstLitIndex(); m <= plc; m++) |
| clause_SetLiteral(newClause, (m + help), |
| clause_LiteralCreate(subst_Apply(rho, subst_Apply(tau, |
| term_Copy(clause_GetLiteralTerm(C2, m)))),newClause)); |
| |
| /* help = number of already set constraint and antecedent Given-literals */ |
| help += clause_NumOfAnteLits(C1); |
| |
| for ( ; m <= pla; m++) |
| clause_SetLiteral(newClause, (m + help), |
| clause_LiteralCreate(subst_Apply(rho, subst_Apply(tau, |
| term_Copy(clause_GetLiteralTerm(C2, m)))),newClause)); |
| |
| /* help = number of already set literals */ |
| help += clause_NumOfSuccLits(C1) - 1; |
| /*help = clause_Length(Clause) - 1;*/ |
| |
| u_sigma = subst_Apply(rho, term_Copy(u_tau)); |
| |
| for ( ; m <= pls; m++) { |
| TERM newAtom; |
| |
| if (m == j) { |
| /* The first partner literal is modified appropriately! */ |
| TERM right; |
| if (v == s2) |
| /* Necessary because term_ReplaceSubtermBy doesn't treat top level */ |
| right = term_Copy(t); |
| else { |
| right = term_Copy(v); |
| term_ReplaceSubtermBy(right, s2, t); |
| } |
| newAtom = term_Create(fol_Equality(), list_Cons(term_Copy(u_sigma), |
| list_List(subst_Apply(rho, subst_Apply(tau, right))))); |
| } else if (m == k) { |
| /* The second partner lit is modified appropriately! */ |
| newAtom = term_Create(fol_Equality(), list_Cons(term_Copy(u_sigma), |
| list_List(term_Copy(v2_sigma)))); |
| } else { |
| /* Apply substitutions to all other literals */ |
| newAtom = subst_Apply(rho, subst_Apply(tau, |
| term_Copy(clause_GetLiteralTerm(C2, m)))); |
| } |
| |
| clause_SetLiteral(newClause, (m + help), |
| clause_LiteralCreate(newAtom, newClause)); |
| } |
| |
| term_Delete(u_sigma); |
| |
| clause_SetFromMergingParamodulation(newClause); |
| |
| clause_AddParentClause(newClause, clause_Number(C2)); |
| clause_AddParentLiteral(newClause, k); |
| clause_SetDataFromParents(newClause, C2, j, C1, k, Flags, Precedence); |
| |
| return list_List(newClause); |
| } |
| |
| |
| static LIST inf_Lit2MParamod(CLAUSE C1, CLAUSE C2, int i, int j, TERM s, TERM t, |
| TERM s2, TERM v, TERM u_tau, SUBST tau, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: Two clauses, the index <i> of a strict maximal literal |
| in <C1>, the index <j> of a strict maximal index in <C2>, |
| <s> and <t> are from literal <i>, <s2> is a subterm |
| of <v>, <v> is from literal <j>, <u_tau> is <u> with |
| substitution <tau> applied, a flag store, and a precedence. |
| <u_tau> must be greater than <v>tau wrt. the ordering. |
| RETURNS: A list of clauses derivable from the given data |
| by merging paramodulation. |
| This function searches <C2> for a second positive literal |
| u'=v', where u' is unifiable with <u_tau>. |
| MEMORY: Memory is allocated for the list and the clauses. |
| ***************************************************************/ |
| { |
| LIST result; |
| int k, last; |
| |
| result = list_Nil(); |
| |
| /* Now find the 3rd literal u' = v' in C2 */ |
| last = clause_LastSuccedentLitIndex(C2); /* Last index */ |
| for (k = clause_FirstSuccedentLitIndex(C2); k <= last; k++) { |
| LITERAL partnerLit2 = clause_GetLiteral(C2, k); |
| TERM partnerAtom2 = clause_LiteralSignedAtom(partnerLit2); |
| |
| if (k != j && fol_IsEquality(partnerAtom2)) { |
| /* partnerLit2: u' = v' or v' = u' */ |
| SUBST rho; |
| TERM pLeft2, pRight2, s_sigma, t_sigma, v2_sigma; |
| ord_RESULT ordResult; |
| BOOL checkPassed; |
| |
| pLeft2 = subst_Apply(tau, term_Copy(term_FirstArgument(partnerAtom2))); |
| pRight2 = subst_Apply(tau, term_Copy(term_SecondArgument(partnerAtom2))); |
| |
| /* First try unification with left side */ |
| cont_Check(); |
| |
| if (unify_UnifyCom(cont_LeftContext(), u_tau, pLeft2)) { |
| subst_ExtractUnifierCom(cont_LeftContext(), &rho); |
| |
| s_sigma = t_sigma = (TERM) NULL; |
| checkPassed = TRUE; |
| |
| if (!clause_LiteralIsOrientedEquality(clause_GetLiteral(C1,i))) { |
| s_sigma = subst_Apply(rho, subst_Apply(tau, term_Copy(s))); |
| t_sigma = subst_Apply(rho, subst_Apply(tau, term_Copy(t))); |
| ordResult = ord_Compare(s_sigma, t_sigma, Flags, Precedence); |
| if (ordResult == ord_SmallerThan() || ordResult == ord_Equal()) |
| checkPassed = FALSE; |
| } |
| |
| if (checkPassed && inf_LiteralsMaxWith2Subst(C1,i,C2,j,rho,tau, |
| Flags, Precedence)) { |
| v2_sigma = subst_Apply(rho, term_Copy(pRight2)); |
| result = list_Nconc(inf_ApplyMParamod(C1,C2,i,j,k,u_tau,v,s2, |
| t,v2_sigma,tau,rho, |
| Flags, Precedence), |
| result); |
| term_Delete(v2_sigma); |
| } |
| /* Now cleanup */ |
| if (s_sigma != NULL) { /* Also t_sigma != NULL */ |
| term_Delete(s_sigma); |
| term_Delete(t_sigma); |
| } |
| subst_Delete(rho); |
| } |
| |
| cont_Reset(); |
| |
| /* Now try unification with right side */ |
| if (unify_UnifyCom(cont_LeftContext(), u_tau, pRight2)) { |
| subst_ExtractUnifierCom(cont_LeftContext(), &rho); |
| |
| s_sigma = t_sigma = (TERM) NULL; |
| checkPassed = TRUE; |
| |
| if (!clause_LiteralIsOrientedEquality(clause_GetLiteral(C1,i))) { |
| s_sigma = subst_Apply(rho, subst_Apply(tau, term_Copy(s))); |
| t_sigma = subst_Apply(rho, subst_Apply(tau, term_Copy(t))); |
| ordResult = ord_Compare(s_sigma, t_sigma, Flags, Precedence); |
| if (ordResult == ord_SmallerThan() || ordResult == ord_Equal()) |
| checkPassed = FALSE; |
| } |
| |
| if (checkPassed && inf_LiteralsMaxWith2Subst(C1,i,C2,j,rho,tau, |
| Flags, Precedence)) { |
| v2_sigma = subst_Apply(rho, term_Copy(pLeft2)); |
| result = list_Nconc(inf_ApplyMParamod(C1,C2,i,j,k,u_tau,v,s2, |
| t,v2_sigma,tau,rho, |
| Flags, Precedence), |
| result); |
| term_Delete(v2_sigma); |
| } |
| /* Now cleanup */ |
| if (s_sigma != NULL) { /* Also t_sigma != NULL */ |
| term_Delete(s_sigma); |
| term_Delete(t_sigma); |
| } |
| subst_Delete(rho); |
| } |
| |
| cont_Reset(); |
| |
| term_Delete(pLeft2); |
| term_Delete(pRight2); |
| } /* k != j */ |
| } /* for k */ |
| |
| return result; |
| } |
| |
| |
| static LIST inf_LitMParamod(CLAUSE Clause, int i, BOOL Turn, |
| SHARED_INDEX ShIndex, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with a strict maximal equality literal at |
| position <i>, a boolean value, a shared index, a |
| flag store and a precedence. |
| If <Turn> is TRUE, the left and right term of the |
| equality are exchanged. |
| RETURNS: A list of clauses derivable from the given clause |
| by merging paramodulation. |
| This function searches a second clause with at least |
| two positive equalities, where the first equation |
| has a subterm s', that is unifiable with the left |
| (or right) side of the given equation. |
| ***************************************************************/ |
| { |
| LIST result, unifiers, literals; |
| LITERAL actLit; |
| TERM s, t, help; |
| |
| actLit = clause_GetLiteral(Clause, i); |
| s = term_FirstArgument(clause_LiteralSignedAtom(actLit)); |
| t = term_SecondArgument(clause_LiteralSignedAtom(actLit)); |
| if (Turn) { |
| /* Exchange s and t */ |
| help = s; |
| s = t; |
| t = help; |
| } |
| result = list_Nil(); |
| |
| unifiers = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), s); |
| |
| for ( ; !list_Empty(unifiers); unifiers = list_Pop(unifiers)) { |
| TERM s2 = (TERM) list_Car(unifiers); /* Unifiable with s */ |
| |
| if (!term_IsVariable(s2) && !term_IsAtom(s2)) { |
| for (literals = sharing_GetDataList(s2, ShIndex); |
| !list_Empty(literals); |
| literals = list_Pop(literals)) { |
| LITERAL partnerLit = (LITERAL) list_Car(literals); /* u = v[s'] */ |
| CLAUSE partnerClause = clause_LiteralOwningClause(partnerLit); |
| TERM partnerAtom = clause_LiteralAtom(partnerLit); |
| int pli = clause_LiteralGetIndex(partnerLit); |
| |
| if (!clause_GetFlag(partnerClause, CLAUSESELECT) && |
| clause_LiteralGetFlag(partnerLit, STRICTMAXIMAL) && |
| clause_LiteralIsPositive(partnerLit) && /* succedent literal */ |
| clause_LiteralIsEquality(partnerLit) && |
| clause_NumOfSuccLits(partnerClause) > 1 && /* > 1 pos. literals */ |
| clause_HasSolvedConstraint(partnerClause)) { |
| TERM partnerLeft = term_FirstArgument(partnerAtom); |
| TERM partnerRight = term_SecondArgument(partnerAtom); |
| BOOL inPartnerRight = term_HasPointerSubterm(partnerRight, s2); |
| |
| if (!clause_LiteralIsOrientedEquality(partnerLit) || inPartnerRight){ |
| /* Don't do this if u=v is oriented and s2 is not a subterm of v */ |
| TERM newPLeft, newPRight; |
| SUBST tau; |
| SYMBOL partnerMaxVar; |
| ord_RESULT ordResult; |
| |
| partnerMaxVar = clause_MaxVar(partnerClause); |
| clause_RenameVarsBiggerThan(Clause, partnerMaxVar); |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), s, cont_RightContext(), s2); |
| subst_ExtractUnifierCom(cont_LeftContext(), &tau); |
| cont_Reset(); |
| |
| newPLeft = subst_Apply(tau, term_Copy(partnerLeft)); |
| newPRight = subst_Apply(tau, term_Copy(partnerRight)); |
| if (clause_LiteralIsOrientedEquality(partnerLit)) |
| ordResult = ord_GreaterThan(); |
| else |
| ordResult = ord_Compare(newPLeft, newPRight, Flags, Precedence); |
| |
| if (inPartnerRight && ord_IsGreaterThan(ordResult)) { |
| /* Take a look at right side */ |
| result = list_Nconc(inf_Lit2MParamod(Clause,partnerClause,i,pli, |
| s, t,s2,partnerRight,newPLeft, |
| tau, Flags, Precedence), |
| result); |
| } |
| if (ord_IsSmallerThan(ordResult) && |
| (!inPartnerRight || term_HasPointerSubterm(partnerLeft, s2))) { |
| /* If s2 is not in partnerRight, it MUST be in partnerLeft, |
| else really do the test */ |
| /* Take a look at left side */ |
| result = list_Nconc(inf_Lit2MParamod(Clause,partnerClause,i,pli, |
| s,t,s2,partnerLeft,newPRight, |
| tau,Flags, Precedence), |
| result); |
| } |
| |
| term_Delete(newPLeft); |
| term_Delete(newPRight); |
| subst_Delete(tau); |
| } |
| } |
| } /* for all Literals containing s2 */ |
| } /* if s2 isn't a variable */ |
| } /* for all unifiers s2 */ |
| |
| return result; |
| } |
| |
| |
| static LIST inf_MParamodLitToGiven(CLAUSE Clause, int j, BOOL Turn, |
| SHARED_INDEX ShIndex, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with a strict maximal equality literal at |
| position <j>, a boolean value, a shared index a |
| flag store and a precedence. |
| If <Turn> is TRUE, the left and right term of the |
| equality are exchanged. |
| RETURNS: A list of clauses derivable from the given clause |
| by merging paramodulation with this literal as second |
| literal of the rule. |
| ***************************************************************/ |
| { |
| LIST result, unifiers, superterms, literals; |
| LITERAL actLit; |
| TERM u, v; |
| int bottom; |
| |
| if (clause_NumOfSuccLits(Clause) < 2) |
| return list_Nil(); /* There must be at least two positive literals */ |
| |
| actLit = clause_GetLiteral(Clause, j); |
| u = term_FirstArgument(clause_LiteralSignedAtom(actLit)); |
| v = term_SecondArgument(clause_LiteralSignedAtom(actLit)); |
| if (Turn) { |
| /* Exchange s and t */ |
| TERM help = u; |
| u = v; |
| v = help; |
| } |
| result = list_Nil(); |
| bottom = stack_Bottom(); |
| |
| sharing_PushReverseOnStack(v); /* Without variables! */ |
| |
| while (!stack_Empty(bottom)) { |
| TERM s2 = (TERM) stack_PopResult(); |
| |
| for (unifiers = st_GetUnifier(cont_LeftContext(),sharing_Index(ShIndex), |
| cont_RightContext(), s2); |
| !list_Empty(unifiers); |
| unifiers = list_Pop(unifiers)) { |
| TERM s = (TERM) list_Car(unifiers); |
| |
| for (superterms = term_SupertermList(s); |
| !list_Empty(superterms); |
| superterms = list_Cdr(superterms)) { |
| TERM partnerAtom = (TERM) list_Car(superterms); |
| |
| if (fol_IsEquality(partnerAtom)) { |
| for (literals = sharing_NAtomDataList(partnerAtom); |
| !list_Empty(literals); |
| literals = list_Cdr(literals)) { |
| LITERAL partnerLit = (LITERAL) list_Car(literals); |
| CLAUSE partnerClause = clause_LiteralOwningClause(partnerLit); |
| int i = clause_LiteralGetIndex(partnerLit); |
| |
| if (!clause_GetFlag(partnerClause,CLAUSESELECT) && |
| clause_LiteralGetFlag(partnerLit,STRICTMAXIMAL) && |
| clause_LiteralIsPositive(partnerLit) && |
| (s == term_FirstArgument(partnerAtom) || |
| !clause_LiteralIsOrientedEquality(partnerLit)) && |
| clause_HasSolvedConstraint(partnerClause) && |
| clause_Number(partnerClause) != clause_Number(Clause)) { |
| /* We don't allow self inferences (both clauses having the */ |
| /* same number) here, because they're already made in function */ |
| /* inf_LitMParamod. */ |
| SYMBOL partnerMaxVar; |
| SUBST tau; |
| TERM u_tau, v_tau; |
| BOOL checkPassed; |
| |
| partnerMaxVar = clause_MaxVar(partnerClause); |
| clause_RenameVarsBiggerThan(Clause, partnerMaxVar); |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), s, cont_RightContext(), s2); |
| subst_ExtractUnifierCom(cont_LeftContext(), &tau); |
| cont_Reset(); |
| |
| u_tau = v_tau = (TERM) NULL; |
| checkPassed = TRUE; |
| |
| /* u_tau must be greater than v_tau */ |
| if (!clause_LiteralIsOrientedEquality(actLit)) { |
| u_tau = subst_Apply(tau, term_Copy(u)); |
| v_tau = subst_Apply(tau, term_Copy(v)); |
| if (ord_Compare(u_tau, v_tau, Flags, Precedence) != ord_GreaterThan()) |
| checkPassed = FALSE; |
| } |
| |
| if (checkPassed) { |
| /* u_tau > v_tau */ |
| TERM t; |
| |
| if (s == term_FirstArgument(partnerAtom)) |
| t = term_SecondArgument(partnerAtom); |
| else |
| t = term_FirstArgument(partnerAtom); |
| if (u_tau == (TERM)NULL) { |
| u_tau = subst_Apply(tau, term_Copy(u)); |
| v_tau = subst_Apply(tau, term_Copy(v)); |
| } |
| |
| result = list_Nconc(inf_Lit2MParamod(partnerClause,Clause,i,j, |
| s,t,s2,v,u_tau, tau,Flags, |
| Precedence), |
| result); |
| } |
| |
| /* Now cleanup */ |
| if (u_tau != (TERM)NULL) { |
| term_Delete(u_tau); |
| term_Delete(v_tau); |
| } |
| subst_Delete(tau); |
| clause_Normalize(Clause); |
| } |
| } |
| } /* partnerAtom is equality */ |
| } |
| } |
| } |
| |
| return result; |
| } |
| |
| |
| LIST inf_MergingParamodulation(CLAUSE GivenClause, SHARED_INDEX ShIndex, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, a shared index, a flag store and a |
| precedence. |
| RETURNS: A list of clauses derivable from the given clause |
| by merging paramodulation. |
| MEMORY: Memory is allocated for the list and the clauses. |
| ***************************************************************/ |
| { |
| LIST result; |
| CLAUSE copy; |
| int last, i; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_MergingParamodulation: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (clause_GetFlag(GivenClause, CLAUSESELECT) || |
| clause_HasEmptySuccedent(GivenClause) || |
| !clause_HasSolvedConstraint(GivenClause)) |
| return list_Nil(); |
| |
| result = list_Nil(); |
| copy = clause_Copy(GivenClause); |
| last = clause_LastSuccedentLitIndex(copy); |
| |
| for (i = clause_FirstSuccedentLitIndex(copy); i <= last; i++) { |
| LITERAL actLit = clause_GetLiteral(copy, i); |
| TERM atom = clause_LiteralSignedAtom(actLit); |
| |
| if (clause_LiteralGetFlag(actLit, STRICTMAXIMAL) && |
| fol_IsEquality(atom)) { |
| |
| result = list_Nconc(inf_LitMParamod(copy,i,FALSE,ShIndex, |
| Flags, Precedence), |
| result); |
| /* Assume GivenClause is the second clause of the rule */ |
| result = list_Nconc(inf_MParamodLitToGiven(copy,i,FALSE,ShIndex, |
| Flags, Precedence), |
| result); |
| |
| if (!clause_LiteralIsOrientedEquality(actLit)) { |
| /* First check rule with left and right side exchanged */ |
| result = list_Nconc(inf_LitMParamod(copy, i, TRUE, ShIndex, |
| Flags, Precedence), |
| result); |
| /* Now assume GivenClause is the second clause of the rule */ |
| /* Check with sides exchanged */ |
| result = list_Nconc(inf_MParamodLitToGiven(copy,i,TRUE,ShIndex, |
| Flags, Precedence), |
| result); |
| } |
| } |
| } /* for */ |
| clause_Delete(copy); |
| |
| return result; |
| } |
| |
| |
| static CLAUSE inf_ApplyGenRes(LITERAL PosLit, LITERAL NegLit, SUBST SubstTermS, |
| SUBST SubstPartnerTermS, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause to use for Resolution, the index of a |
| positive non-equality literal, a unifiable literal, |
| the substitutions for the terms to unify, a flag |
| store and a precedence. |
| RETURNS: A clause derivable from the literals owning |
| clause by Resolution wrt. the Index. |
| MEMORY: Memory for the new clause is allocated. |
| ***************************************************************/ |
| { |
| CLAUSE NewClause, GivenClause, PartnerClause; |
| int i,j,lc,la,ls,pi,pls,pla,plc,help,ConNeg,AntNeg; /* p=Partner,l=last */ |
| |
| PartnerClause = clause_LiteralOwningClause(NegLit); |
| GivenClause = clause_LiteralOwningClause(PosLit); |
| |
| pls = clause_LastSuccedentLitIndex(PartnerClause); |
| pla = clause_LastAntecedentLitIndex(PartnerClause); |
| plc = clause_LastConstraintLitIndex(PartnerClause); |
| |
| pi = clause_LiteralGetIndex(NegLit); |
| |
| ls = clause_LastSuccedentLitIndex(GivenClause); |
| la = clause_LastAntecedentLitIndex(GivenClause); |
| lc = clause_LastConstraintLitIndex(GivenClause); |
| |
| i = clause_LiteralGetIndex(PosLit); |
| |
| if (pi <= plc) { |
| ConNeg = 1; |
| AntNeg = 0; |
| } |
| else { |
| ConNeg = 0; |
| AntNeg = 1; |
| } |
| |
| NewClause = clause_CreateBody((clause_Length(GivenClause) -1) + |
| clause_Length(PartnerClause) -1); |
| |
| clause_SetNumOfConsLits(NewClause, |
| (clause_NumOfConsLits(GivenClause) + |
| (clause_NumOfConsLits(PartnerClause)-ConNeg))); |
| |
| clause_SetNumOfAnteLits(NewClause, |
| (clause_NumOfAnteLits(GivenClause) + |
| (clause_NumOfAnteLits(PartnerClause)-AntNeg))); |
| |
| clause_SetNumOfSuccLits(NewClause, |
| ((clause_NumOfSuccLits(GivenClause) -1)+ |
| clause_NumOfSuccLits(PartnerClause))); |
| |
| |
| /* First set the literals from the GivenClause : */ |
| for (j = clause_FirstLitIndex(); j <= lc; j++) { |
| clause_SetLiteral(NewClause, j, |
| clause_LiteralCreate(subst_Apply(SubstTermS, |
| term_Copy(clause_GetLiteralTerm(GivenClause, j))),NewClause)); |
| } |
| |
| /* help = number of literals to leave empty */ |
| help = clause_NumOfConsLits(PartnerClause)-ConNeg; |
| |
| for ( ; j <= la; j++) { |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(SubstTermS, |
| term_Copy(clause_GetLiteralTerm(GivenClause, j))),NewClause)); |
| } |
| |
| /* help = number of literals to leave empty */ |
| help += clause_NumOfAnteLits(PartnerClause)-AntNeg; |
| |
| |
| |
| for ( ; j <= ls; j++) { |
| if (j != i) { |
| /* The ActLit isn't copied! */ |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(SubstTermS, |
| term_Copy(clause_GetLiteralTerm(GivenClause, j))),NewClause)); |
| |
| } else { |
| /*the index has to be decreased to avoid an empty literal! */ |
| help--; |
| } |
| } |
| |
| /* Now we consider the PartnerClause : */ |
| |
| /* help = number of already set constraint (GivenClause-) literals */ |
| help = clause_NumOfConsLits(GivenClause); |
| |
| for (j = clause_FirstLitIndex(); j <= plc; j++) { |
| if (j != pi) { |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(SubstPartnerTermS, |
| term_Copy(clause_GetLiteralTerm(PartnerClause, j))),NewClause)); |
| } else { |
| help--; |
| } |
| } |
| |
| /* help = number of already set constraint and antecedent Given-literals */ |
| help += clause_NumOfAnteLits(GivenClause); |
| |
| for ( ; j <= pla; j++) { |
| |
| if (j != pi) { |
| /* The NegLit isn't copied! */ |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(SubstPartnerTermS, |
| term_Copy(clause_GetLiteralTerm(PartnerClause, j))),NewClause)); |
| |
| } else { |
| /* The index has to be shifted as above. */ |
| help--; |
| } |
| } |
| |
| /* help = number of already set (GivenClause-) literals */ |
| help += clause_NumOfSuccLits(GivenClause) - 1; |
| |
| for ( ; j <= pls; j++) { |
| clause_SetLiteral(NewClause, (j + help), |
| clause_LiteralCreate(subst_Apply(SubstPartnerTermS, |
| term_Copy(clause_GetLiteralTerm(PartnerClause, j))),NewClause)); |
| } /* end of NewClause creation (last for loop). */ |
| |
| |
| clause_SetDataFromParents(NewClause,PartnerClause,pi,GivenClause,i, |
| Flags, Precedence); |
| clause_SetFromGeneralResolution(NewClause); |
| |
| return(NewClause); |
| } |
| |
| |
| LIST inf_GeneralResolution(CLAUSE GivenClause, SHARED_INDEX ShIndex, |
| BOOL Ordered, BOOL Equations, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause and an Index, usually the WorkedOffIndex, |
| two boolean flags, a flag store and a precedence. |
| RETURNS: A list of clauses derivable from the GivenClause by |
| GeneralResolution wrt. the Index. |
| If <Ordered>=TRUE, this function generates ordered |
| resolution inferences (the literals must be selected or |
| (strict) maximal), otherwise it generates standard |
| resolution inferences. |
| If <Equations>=TRUE, equations are allowed for inferences, |
| else no inferences with equations are generated. The |
| default is <Equations>=FALSE.. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| CLAUSE GivenCopy; |
| LIST Result; |
| LITERAL ActLit; |
| TERM Atom; |
| int i,n; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GeneralResolution: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (!clause_HasSolvedConstraint(GivenClause)) |
| return list_Nil(); |
| |
| Result = list_Nil(); |
| GivenCopy = clause_Copy(GivenClause); |
| |
| if (clause_GetFlag(GivenCopy,CLAUSESELECT)) |
| n = clause_LastAntecedentLitIndex(GivenCopy); |
| else |
| n = clause_LastSuccedentLitIndex(GivenCopy); |
| |
| for (i = clause_FirstAntecedentLitIndex(GivenCopy); i <= n; i++) { |
| |
| ActLit = clause_GetLiteral(GivenCopy, i); |
| Atom = clause_LiteralAtom(ActLit); |
| |
| if ((Equations || !fol_IsEquality(Atom)) && |
| (clause_LiteralGetFlag(ActLit,LITSELECT) || |
| (!clause_GetFlag(GivenCopy,CLAUSESELECT) && |
| (!Ordered || clause_LiteralIsMaximal(ActLit)))) && |
| (!Ordered || clause_LiteralIsFromAntecedent(ActLit) || |
| clause_LiteralGetFlag(ActLit,STRICTMAXIMAL))) { |
| /* Positive literals must be strict maximal for ORe, */ |
| /* negative literals must be either selected or maximal. */ |
| LIST TermList; |
| BOOL Swapped; |
| |
| Swapped = FALSE; |
| |
| /* The 'endless' loop may run twice for equations, once for other atoms */ |
| while (TRUE) { |
| TermList = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), Atom); |
| |
| for ( ; !list_Empty(TermList); TermList = list_Pop(TermList)) { |
| LIST LitList; |
| TERM PartnerAtom; |
| |
| PartnerAtom = list_First(TermList); |
| |
| if (!term_IsVariable(PartnerAtom)) { |
| LITERAL PartnerLit; |
| int j; |
| CLAUSE PartnerClause; |
| |
| for (LitList = sharing_NAtomDataList(PartnerAtom); |
| !list_Empty(LitList); LitList = list_Cdr(LitList)) { |
| PartnerLit = list_Car(LitList); |
| j = clause_LiteralGetIndex(PartnerLit); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| |
| if (clause_LiteralsAreComplementary(PartnerLit,ActLit) && |
| clause_HasSolvedConstraint(PartnerClause) && |
| /* Negative literals must be from the antecedent */ |
| (clause_LiteralIsPositive(PartnerLit) || |
| clause_LiteralIsFromAntecedent(PartnerLit)) && |
| /* Check whether literal is selected or maximal */ |
| (clause_LiteralGetFlag(PartnerLit,LITSELECT) || |
| (!clause_GetFlag(PartnerClause,CLAUSESELECT) && |
| (!Ordered || clause_LiteralIsMaximal(PartnerLit)))) && |
| /* Positive literals must be strict maximal for ORe */ |
| (!Ordered || clause_LiteralIsNegative(PartnerLit) || |
| clause_LiteralGetFlag(PartnerLit,STRICTMAXIMAL)) && |
| /* Avoid duplicate self-inferences */ |
| (clause_LiteralIsPositive(PartnerLit) || |
| clause_Number(GivenClause) != clause_Number(PartnerClause))) { |
| SUBST Subst, PartnerSubst; |
| SYMBOL MaxVar; |
| |
| MaxVar = clause_MaxVar(PartnerClause); |
| clause_RenameVarsBiggerThan(GivenCopy, MaxVar); |
| |
| cont_Check(); |
| if (!unify_UnifyNoOC(cont_LeftContext(), Atom, cont_RightContext(), |
| PartnerAtom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GeneralResolution: Unification failed."); |
| misc_FinishErrorReport(); |
| } |
| subst_ExtractUnifier(cont_LeftContext(), &Subst, |
| cont_RightContext(), &PartnerSubst); |
| cont_Reset(); |
| |
| if (!Ordered || |
| inf_LiteralsMax(GivenCopy, i, Subst, PartnerClause, j, |
| PartnerSubst, Flags, Precedence)) { |
| if (clause_LiteralIsNegative(PartnerLit)) |
| Result = list_Cons(inf_ApplyGenRes(ActLit,PartnerLit,Subst, |
| PartnerSubst, |
| Flags, Precedence), |
| Result); |
| else |
| Result = list_Cons(inf_ApplyGenRes(PartnerLit, ActLit, |
| PartnerSubst,Subst, |
| Flags, Precedence), |
| Result); |
| } |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } /* end of for (LitList = sharing_NAtomDataList ...). */ |
| } /* end of if (!term_IsVariable(PartnerAtom)). */ |
| } /* end of for (TermList = st_GetUnifier...). */ |
| if (!Swapped && fol_IsEquality(Atom)) { |
| term_EqualitySwap(Atom); /* Atom is from copied clause */ |
| Swapped = TRUE; |
| } else |
| break; |
| } /* end of 'endless' loop */ |
| } /* end of if (clause_LiteralIsMaximal(ActLit)). */ |
| } /* end of for 'all antecedent and succedent literals'. */ |
| |
| clause_Delete(GivenCopy); |
| |
| return Result; |
| } |
| |
| |
| LIST inf_UnitResolution(CLAUSE GivenClause, SHARED_INDEX ShIndex, |
| BOOL Equations, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause and an Index, usually the WorkedOffIndex, |
| a boolean flag, a flag store and a precedence. |
| RETURNS: A list of clauses derivable from the Givenclause by |
| Unit Resolution wrt. the Index. |
| This function does the same inferences as standard resolution, |
| except that at least one of the clauses must be a unit clause. |
| The involved literals don't have to be maximal. |
| If <Equations>=TRUE, equations are allowed for inferences, |
| else no inferences with equations are made. The |
| default is <Equations>=FALSE.. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| CLAUSE GivenCopy; |
| LIST Result; |
| LITERAL ActLit; |
| TERM Atom; |
| BOOL GivenIsUnit; |
| int i,n; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_UnitResolution: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (!clause_HasSolvedConstraint(GivenClause)) |
| return list_Nil(); |
| |
| Result = list_Nil(); |
| |
| GivenCopy = clause_Copy(GivenClause); |
| GivenIsUnit = (clause_Length(GivenCopy) == 1); |
| |
| if (clause_GetFlag(GivenCopy,CLAUSESELECT)) |
| n = clause_LastAntecedentLitIndex(GivenCopy); |
| else |
| n = clause_LastSuccedentLitIndex(GivenCopy); |
| |
| for (i=clause_FirstAntecedentLitIndex(GivenCopy); i <= n; i++) { |
| |
| ActLit = clause_GetLiteral(GivenCopy, i); |
| Atom = clause_LiteralAtom(ActLit); |
| |
| if ((Equations || !fol_IsEquality(Atom)) && |
| (clause_LiteralGetFlag(ActLit,LITSELECT) || |
| !clause_GetFlag(GivenCopy,CLAUSESELECT))) { |
| LIST TermList; |
| BOOL Swapped; |
| |
| Swapped = FALSE; |
| |
| /* The 'endless' loop runs twice for equations, once for other atoms */ |
| while (TRUE) { |
| TermList = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), Atom); |
| |
| for ( ; !list_Empty(TermList); TermList = list_Pop(TermList)) { |
| LIST LitList; |
| TERM PartnerAtom; |
| |
| PartnerAtom = list_First(TermList); |
| |
| if (!term_IsVariable(PartnerAtom)) { |
| LITERAL PartnerLit; |
| CLAUSE PartnerClause; |
| |
| for (LitList = sharing_NAtomDataList(PartnerAtom); |
| !list_Empty(LitList); LitList = list_Cdr(LitList)) { |
| PartnerLit = list_Car(LitList); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| |
| if ((GivenIsUnit || clause_Length(PartnerClause) == 1) && |
| clause_LiteralsAreComplementary(PartnerLit,ActLit) && |
| clause_HasSolvedConstraint(PartnerClause) && |
| /* Negative literals must be from the antecedent */ |
| (clause_LiteralIsPositive(PartnerLit) || |
| clause_LiteralIsFromAntecedent(PartnerLit)) && |
| /* Either the literal is selected or no literal is selected */ |
| (clause_LiteralGetFlag(PartnerLit,LITSELECT) || |
| !clause_GetFlag(PartnerClause,CLAUSESELECT))) { |
| /* Self-inferences aren't possible, since then the clause must */ |
| /* be a unit and a single literal can't be both positive and */ |
| /* negative. */ |
| SUBST Subst, PartnerSubst; |
| SYMBOL MaxVar; |
| |
| MaxVar = clause_MaxVar(PartnerClause); |
| clause_RenameVarsBiggerThan(GivenCopy, MaxVar); |
| |
| cont_Check(); |
| if (!unify_UnifyNoOC(cont_LeftContext(), Atom, |
| cont_RightContext(), PartnerAtom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_UnitResolution: Unification failed."); |
| misc_FinishErrorReport(); |
| } |
| subst_ExtractUnifier(cont_LeftContext(), &Subst, |
| cont_RightContext(), &PartnerSubst); |
| cont_Reset(); |
| |
| if (clause_LiteralIsNegative(PartnerLit)) |
| Result = list_Cons(inf_ApplyGenRes(ActLit, PartnerLit, Subst, |
| PartnerSubst, |
| Flags, Precedence), |
| Result); |
| else |
| Result = list_Cons(inf_ApplyGenRes(PartnerLit, ActLit, |
| PartnerSubst,Subst, |
| Flags, Precedence), |
| Result); |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } /* end of for (LitList = sharing_NAtomDataList ...). */ |
| } /* end of if (!term_IsVariable(PartnerAtom)). */ |
| } /* end of for (TermList = st_GetUnifier...). */ |
| if (!Swapped && fol_IsEquality(Atom)) { |
| term_EqualitySwap(Atom); /* Atom is from copied clause */ |
| Swapped = TRUE; |
| } else |
| break; |
| } /* end of 'endless' loop */ |
| } /* end of if (clause_LiteralIsMaximal(ActLit)). */ |
| } /* end of for 'all antecedent and succedent literals'. */ |
| |
| clause_Delete(GivenCopy); |
| |
| return Result; |
| } |
| |
| LIST inf_BoundedDepthUnitResolution(CLAUSE GivenClause, SHARED_INDEX ShIndex, |
| BOOL ConClause, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause and an Index, usually the WorkedOffIndex, |
| a flag indicating whether the partner clause must be |
| a conjecture clause, a flag store and a precedence. |
| RETURNS: A list of clauses derivable from the Givenclause by |
| bounded depth unit resolution wrt. the Index. |
| This acts similar to inf_UnitResolution, except that |
| it limits the depth of resolvents to the maximum |
| depth of its parent clauses. |
| MEMORY: A list of clauses is produced, where memory for the |
| list and the clauses is allocated. |
| ***************************************************************/ |
| /* GivenClause is always a CONCLAUSE */ |
| { |
| CLAUSE GivenCopy; |
| LIST Result; |
| LITERAL ActLit; |
| TERM Atom; |
| int i,n,depth; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BoundedDepthUnitResolution: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| cont_Check(); |
| #endif |
| |
| Result = list_Nil(); |
| GivenCopy = clause_Copy(GivenClause); |
| n = clause_LastLitIndex(GivenCopy); |
| depth = clause_ComputeTermDepth(GivenCopy); |
| |
| for (i = clause_FirstLitIndex(); i <= n; i++) { |
| LIST TermList; |
| BOOL Swapped; |
| |
| ActLit = clause_GetLiteral(GivenCopy, i); |
| Atom = clause_LiteralAtom(ActLit); |
| Swapped = FALSE; |
| |
| /* The 'endless' loop runs twice for equations, once for other atoms */ |
| while (TRUE) { |
| TermList = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), Atom); |
| |
| for ( ; !list_Empty(TermList); TermList = list_Pop(TermList)) { |
| LIST LitList; |
| TERM PartnerAtom; |
| |
| PartnerAtom = list_First(TermList); |
| |
| if (!term_IsVariable(PartnerAtom)) { |
| LITERAL PartnerLit; |
| CLAUSE PartnerClause; |
| |
| for (LitList = sharing_NAtomDataList(PartnerAtom); |
| !list_Empty(LitList); LitList = list_Cdr(LitList)) { |
| PartnerLit = list_Car(LitList); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| |
| if (clause_LiteralsAreComplementary(PartnerLit,ActLit) && |
| (clause_Length(GivenCopy)==1 || clause_Length(PartnerClause)==1) && |
| (clause_GetFlag(GivenCopy,CONCLAUSE) || |
| clause_GetFlag(PartnerClause,CONCLAUSE)) && |
| (!ConClause || clause_GetFlag(PartnerClause,CONCLAUSE))) { |
| SUBST Subst, PartnerSubst; |
| SYMBOL MaxVar; |
| int maxdepth; |
| CLAUSE Resolvent; |
| |
| maxdepth = misc_Max(depth, clause_ComputeTermDepth(PartnerClause)); |
| MaxVar = clause_MaxVar(PartnerClause); |
| clause_RenameVarsBiggerThan(GivenCopy, MaxVar); |
| |
| cont_Check(); |
| if (!unify_UnifyNoOC(cont_LeftContext(), Atom, |
| cont_RightContext(), PartnerAtom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BoundedDepthUnitResolution: Unification failed."); |
| misc_FinishErrorReport(); |
| } |
| subst_ExtractUnifier(cont_LeftContext(), &Subst, |
| cont_RightContext(), &PartnerSubst); |
| cont_Reset(); |
| |
| if (clause_LiteralIsNegative(PartnerLit)) |
| Resolvent = inf_ApplyGenRes(ActLit, PartnerLit, Subst, |
| PartnerSubst, Flags, Precedence); |
| else |
| Resolvent = inf_ApplyGenRes(PartnerLit, ActLit, PartnerSubst, |
| Subst, Flags, Precedence); |
| |
| if (clause_ComputeTermDepth(Resolvent) > maxdepth) |
| clause_Delete(Resolvent); |
| else { |
| Result = list_Cons(Resolvent,Result); |
| } |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } |
| } |
| } |
| if (!Swapped && fol_IsEquality(Atom)) { |
| term_EqualitySwap(Atom); /* Given Clause is a copy */ |
| Swapped = TRUE; |
| } else |
| break; |
| } /* end of 'endless' loop */ |
| } |
| |
| clause_Delete(GivenCopy); |
| |
| return(Result); |
| } |
| |
| static CLAUSE inf_ApplyGeneralFactoring(CLAUSE Clause, NAT i, NAT j, |
| SUBST Subst, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause an index in the clause, a substitution a |
| flag store and a precedence. |
| RETURNS: A new clause obtained from <Clause> by applying <Subst> |
| and deleting literal <j> keeping literal <i> |
| ***************************************************************/ |
| { |
| CLAUSE NewClause; |
| |
| NewClause = clause_Copy(Clause); |
| clause_ClearFlags(NewClause); |
| clause_SubstApply(Subst, NewClause); |
| |
| clause_DeleteLiteral(NewClause, i, Flags, Precedence); |
| |
| list_Delete(clause_ParentClauses(NewClause)); |
| list_Delete(clause_ParentLiterals(NewClause)); |
| clause_SetParentLiterals(NewClause,list_Nil()); |
| clause_SetParentClauses(NewClause,list_Nil()); |
| |
| clause_SetDataFromFather(NewClause, Clause, j, Flags, Precedence); |
| clause_SetFromGeneralFactoring(NewClause); |
| |
| clause_AddParentClause(NewClause, clause_Number(Clause)); |
| clause_AddParentLiteral(NewClause, i); |
| |
| clause_NewNumber(NewClause); |
| |
| return NewClause; |
| } |
| |
| |
| LIST inf_GeneralFactoring(CLAUSE GivenClause, BOOL Ordered, BOOL Left, |
| BOOL Equations, FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, three boolean flags, a flag store and a |
| precedence. |
| If <Ordered>=TRUE, this function generates ordered |
| factoring inferences, otherwise standard factoring |
| inferences. |
| If <Left> is FALSE, this function only makes factoring |
| right inferences, otherwise it also makes factoring left |
| inferences. |
| If <Equations>=TRUE, equations are allowed for inferences, |
| else no inferences with equations are generated. The |
| default is <Equations>=TRUE. |
| RETURNS: A list of clauses derivable from <GivenClause> by GF. |
| ***************************************************************/ |
| { |
| LIST Result; |
| LITERAL ActLit; |
| int i,j,last; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GeneralFactoring: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (!clause_HasSolvedConstraint(GivenClause)) |
| return list_Nil(); |
| |
| Result = list_Nil(); |
| |
| /* Always try Factoring Right inferences */ |
| last = clause_LastSuccedentLitIndex(GivenClause); |
| if (!clause_GetFlag(GivenClause,CLAUSESELECT)) { |
| for (i = clause_FirstSuccedentLitIndex(GivenClause); i <= last; i++) { |
| ActLit = clause_GetLiteral(GivenClause, i); |
| if ((!Ordered || clause_LiteralIsMaximal(ActLit)) && |
| (Equations || !clause_LiteralIsEquality(ActLit))) { |
| TERM Atom, PartnerAtom; |
| LITERAL PartnerLit; |
| Atom = clause_LiteralAtom(ActLit); |
| for (j = clause_FirstSuccedentLitIndex(GivenClause); j <= last; j++) { |
| if (i != j) { |
| PartnerLit = clause_GetLiteral(GivenClause, j); |
| PartnerAtom = clause_LiteralAtom(PartnerLit); |
| if ((j>i ||(Ordered && !clause_LiteralIsMaximal(PartnerLit))) && |
| term_EqualTopSymbols(Atom, PartnerAtom)) { |
| /* This condition avoids duplicate inferences */ |
| cont_Check(); |
| if (unify_UnifyCom(cont_LeftContext(), Atom, PartnerAtom)) { |
| SUBST mgu; |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| if (!Ordered || inf_LitMax(GivenClause,i,j,mgu,FALSE, |
| Flags, Precedence)) |
| Result = list_Cons(inf_ApplyGeneralFactoring(GivenClause,i,j, |
| mgu,Flags, |
| Precedence), |
| Result); |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| if (fol_IsEquality(Atom) && /* PartnerAtom is equality, too */ |
| unify_UnifyCom(cont_LeftContext(), |
| term_SecondArgument(Atom), |
| term_FirstArgument(PartnerAtom)) && |
| unify_UnifyCom(cont_LeftContext(), |
| term_FirstArgument(Atom), |
| term_SecondArgument(PartnerAtom))) { |
| SUBST mgu; |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| if (!Ordered || inf_LitMax(GivenClause,i,j,mgu,FALSE, |
| Flags, Precedence)) |
| Result = list_Cons(inf_ApplyGeneralFactoring(GivenClause,i,j, |
| mgu,Flags, |
| Precedence), |
| Result); |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| } |
| } |
| } |
| } |
| } |
| } |
| /* Try Factoring Left inferences only if <Left>==TRUE */ |
| if (Left) { |
| last = clause_LastAntecedentLitIndex(GivenClause); |
| for (i = clause_FirstAntecedentLitIndex(GivenClause); i <= last; i++) { |
| ActLit = clause_GetLiteral(GivenClause, i); |
| if ((Equations || !clause_LiteralIsEquality(ActLit)) && |
| (clause_LiteralGetFlag(ActLit,LITSELECT) || |
| (!clause_GetFlag(GivenClause,CLAUSESELECT) && |
| (!Ordered || clause_LiteralIsMaximal(ActLit))))) { |
| TERM Atom, PartnerAtom; |
| LITERAL PartnerLit; |
| Atom = clause_LiteralAtom(ActLit); |
| for (j = clause_FirstAntecedentLitIndex(GivenClause);j <= last; j++) { |
| if (i != j) { |
| PartnerLit = clause_GetLiteral(GivenClause, j); |
| PartnerAtom = clause_LiteralAtom(PartnerLit); |
| /* In order to avoid duplicate inferences, we do the following */ |
| /* somewhat "tricky" test. What we want is something like */ |
| /* "if (j>i || j wasn't considered within the outer loop) {...} */ |
| /* This lengthy condition can be transformed into the following */ |
| /* condition, because only one negative literal is selected. */ |
| /* This implies that the literal at index j can't be selected. */ |
| if ((j>i || clause_LiteralGetFlag(ActLit,LITSELECT) || |
| (Ordered && !clause_LiteralIsMaximal(PartnerLit))) && |
| term_EqualTopSymbols(Atom, PartnerAtom)) { |
| PartnerAtom = clause_LiteralAtom(PartnerLit); |
| cont_Check(); |
| if (unify_UnifyCom(cont_LeftContext(), Atom, PartnerAtom)) { |
| SUBST mgu; |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| if (!Ordered || clause_LiteralGetFlag(ActLit,LITSELECT) || |
| inf_LitMax(GivenClause,i,j,mgu,FALSE,Flags, Precedence)) |
| Result = list_Cons(inf_ApplyGeneralFactoring(GivenClause,i,j, |
| mgu,Flags, |
| Precedence), |
| Result); |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| if (fol_IsEquality(Atom) && /* PartnerAtom is equality, too */ |
| unify_UnifyCom(cont_LeftContext(), |
| term_SecondArgument(Atom), |
| term_FirstArgument(PartnerAtom)) && |
| unify_UnifyCom(cont_LeftContext(), |
| term_FirstArgument(Atom), |
| term_SecondArgument(PartnerAtom))) { |
| SUBST mgu; |
| subst_ExtractUnifierCom(cont_LeftContext(), &mgu); |
| if (!Ordered || clause_LiteralGetFlag(ActLit,LITSELECT) || |
| inf_LitMax(GivenClause,i,j,mgu,FALSE,Flags, Precedence)) |
| Result = list_Cons(inf_ApplyGeneralFactoring(GivenClause,i,j, |
| mgu,Flags, |
| Precedence), |
| Result); |
| subst_Delete(mgu); |
| } |
| cont_Reset(); |
| } |
| } |
| } |
| } |
| } |
| } |
| cont_Check(); |
| |
| return Result; |
| } |
| |
| |
| /***************************************************************/ |
| /* START of code for new Superposition Left rule */ |
| /***************************************************************/ |
| |
| |
| static LIST inf_GenLitSPLeft(CLAUSE Clause, TERM Left, TERM Right, int i, |
| SHARED_INDEX ShIndex,BOOL OrdPara, BOOL MaxPara, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause (unshared) with a positive equality literal |
| at position <i> where <Left> and <Right> are the |
| arguments of just that literal, two boolean flags, |
| a flag store and a precedence. |
| For Ordered Paramodulation and Superposition <Right> |
| mustn't be greater wrt. the ordering than <Left>. |
| For Superposition the literal must be strictly maximal. |
| RETURNS: A list of clauses derivable with the literals owning |
| clause by Superposition Left wrt. the Index. |
| MEMORY: The list of clauses is extended, where memory for the |
| list and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, Terms; |
| |
| #ifdef CHECK |
| if (clause_GetFlag(Clause, CLAUSESELECT) || |
| (OrdPara && |
| clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i)) && |
| Left == term_SecondArgument(clause_GetLiteralAtom(Clause,i))) || |
| (MaxPara && |
| !clause_LiteralGetFlag(clause_GetLiteral(Clause,i), STRICTMAXIMAL))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenLitSPLeft: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| Terms = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), Left); |
| |
| for ( ; !list_Empty(Terms); Terms = list_Pop(Terms)) { |
| LIST Lits; |
| TERM Term; |
| |
| Term = (TERM)list_First(Terms); |
| |
| if (!term_IsVariable(Term) && !symbol_IsPredicate(term_TopSymbol(Term))) { |
| |
| Lits = sharing_GetDataList(Term, ShIndex); |
| |
| for ( ; !list_Empty(Lits); Lits = list_Pop(Lits)){ |
| |
| LITERAL PartnerLit; |
| TERM PartnerAtom; |
| CLAUSE PartnerClause; |
| int pli; |
| |
| PartnerLit = (LITERAL)list_Car(Lits); /* Antecedent Literal ! */ |
| PartnerAtom = clause_LiteralAtom(PartnerLit); |
| pli = clause_LiteralGetIndex(PartnerLit); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| |
| if ((clause_LiteralGetFlag(PartnerLit,LITSELECT) || |
| (!clause_GetFlag(PartnerClause,CLAUSESELECT) && |
| (!MaxPara || clause_LiteralIsMaximal(PartnerLit)))) && |
| clause_LiteralIsNegative(PartnerLit) && |
| !clause_GetFlag(PartnerClause,NOPARAINTO) && |
| clause_HasSolvedConstraint(PartnerClause)) { |
| /* If <PartnerClause> has a solved constraint and <PartnerLit> */ |
| /* is negative then <PartnerLit> is from the antecedent. */ |
| |
| SUBST Subst, PartnerSubst; |
| TERM NewLeft,NewRight; |
| SYMBOL PartnerMaxVar; |
| TERM SupAtom; |
| |
| SupAtom = (TERM)NULL; |
| PartnerMaxVar = clause_MaxVar(PartnerClause); |
| NewLeft = Left; |
| clause_RenameVarsBiggerThan(Clause, PartnerMaxVar); |
| |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), Left, cont_RightContext(), Term); |
| subst_ExtractUnifier(cont_LeftContext(), &Subst, |
| cont_RightContext(), &PartnerSubst); |
| cont_Reset(); |
| |
| if (!MaxPara || |
| inf_LiteralsMax(Clause, i, Subst, PartnerClause, pli, |
| PartnerSubst, Flags, Precedence)) { |
| NewRight = subst_Apply(Subst, term_Copy(Right)); |
| if (OrdPara && |
| !clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i))) |
| NewLeft = subst_Apply(Subst, term_Copy(Left)); |
| if (!OrdPara || |
| NewLeft == Left || |
| ord_Compare(NewLeft,NewRight,Flags, Precedence) != ord_SmallerThan()) { |
| if (!MaxPara || clause_LiteralIsPredicate(PartnerLit)) { |
| SupAtom = inf_AllTermsRplac(PartnerAtom,Term,NewRight, |
| PartnerSubst); |
| } else { |
| /* Superposition and <PartnerLit> is equality */ |
| if (clause_LiteralIsOrientedEquality(PartnerLit)) |
| SupAtom = inf_AllTermsLeftRplac(PartnerAtom,Term,NewRight, |
| PartnerSubst); |
| else { |
| TERM NewPartnerLeft,NewPartnerRight; |
| NewPartnerLeft = subst_Apply(PartnerSubst, |
| term_Copy(term_FirstArgument(PartnerAtom))); |
| NewPartnerRight = subst_Apply(PartnerSubst, |
| term_Copy(term_SecondArgument(PartnerAtom))); |
| switch (ord_Compare(NewPartnerLeft,NewPartnerRight, |
| Flags, Precedence)) { |
| case ord_SMALLER_THAN: |
| SupAtom = inf_AllTermsRightRplac(PartnerAtom,Term, |
| NewRight,PartnerSubst); |
| break; |
| case ord_GREATER_THAN: |
| SupAtom = inf_AllTermsLeftRplac(PartnerAtom,Term, |
| NewRight,PartnerSubst); |
| break; |
| default: |
| SupAtom = inf_AllTermsRplac(PartnerAtom,Term, |
| NewRight,PartnerSubst); |
| } |
| term_Delete(NewPartnerLeft); |
| term_Delete(NewPartnerRight); |
| } |
| } |
| |
| if (SupAtom != NULL) |
| Result = list_Cons(inf_ApplyGenSuperposition(Clause, i, Subst, |
| PartnerClause, pli, |
| PartnerSubst, |
| SupAtom, FALSE, |
| OrdPara, MaxPara, |
| Flags, Precedence), |
| Result); |
| } |
| if (NewLeft != Left) |
| term_Delete(NewLeft); |
| term_Delete(NewRight); |
| } |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| static LIST inf_GenSPLeftEqToGiven(CLAUSE Clause, int i, BOOL Left, |
| SHARED_INDEX ShIndex, BOOL OrdPara, |
| BOOL MaxPara, BOOL Unit, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An unshared clause, the index of an antecedent |
| literal that is an equality literal, a boolean |
| value, a shared index, three boolean flags |
| controlling inference preconditions, a flag store |
| and a precedence. |
| If Left==TRUE then the left argument of the literal is used |
| otherwise the right argument. |
| OrdPara and MaxPara control inference conditions. |
| If <Unit>==TRUE the clause with the maximal, positive |
| equality must be a unit clause. |
| RETURNS: A list of clauses derivable from generalized |
| superposition Left on the |
| GivenCopy wrt. the Index. See GenSuperpositionLeft |
| for effects of OrdPara and MaxPara |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, TermList, ParentList; |
| int Bottom; |
| LITERAL Lit; |
| TERM Atom, Term, PartnerTerm, PartnerEq; |
| |
| Result = list_Nil(); |
| Lit = clause_GetLiteral(Clause,i); /* Is an antecedent Literal ! */ |
| Atom = clause_LiteralAtom(Lit); |
| |
| #ifdef CHECK |
| if (clause_GetFlag(Clause, NOPARAINTO) || |
| !clause_LiteralIsEquality(Lit) || |
| !clause_LiteralIsFromAntecedent(Lit) || |
| (MaxPara && clause_LiteralIsOrientedEquality(Lit) && !Left) || |
| (!clause_LiteralGetFlag(clause_GetLiteral(Clause,i),LITSELECT) && |
| (clause_GetFlag(Clause, CLAUSESELECT) || |
| (MaxPara && !clause_LiteralIsMaximal(clause_GetLiteral(Clause,i)))))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPLeftEqToGiven: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Bottom = stack_Bottom(); |
| if (Left) |
| sharing_PushOnStack(term_FirstArgument(Atom)); |
| else |
| sharing_PushOnStack(term_SecondArgument(Atom)); |
| |
| while (!stack_Empty(Bottom)) { |
| Term = (TERM)stack_PopResult(); |
| if (!term_IsVariable(Term)) { |
| /* Superposition into variables is not necessary */ |
| TermList = st_GetUnifier(cont_LeftContext(), sharing_Index(ShIndex), |
| cont_RightContext(), Term); |
| for ( ;!list_Empty(TermList); TermList = list_Pop(TermList)) { |
| PartnerTerm = (TERM)list_Car(TermList); |
| for (ParentList = term_SupertermList(PartnerTerm); |
| !list_Empty(ParentList); ParentList = list_Cdr(ParentList)) { |
| PartnerEq = (TERM)list_Car(ParentList); |
| if (fol_IsEquality(PartnerEq)) { |
| CLAUSE PartnerClause; |
| LITERAL PartnerLit; |
| LIST Scl; |
| int j; |
| for (Scl = sharing_NAtomDataList(PartnerEq); |
| !list_Empty(Scl); Scl = list_Cdr(Scl)) { |
| PartnerLit = (LITERAL)list_Car(Scl); |
| j = clause_LiteralGetIndex(PartnerLit); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| |
| if (!clause_GetFlag(PartnerClause,CLAUSESELECT) && |
| (!MaxPara || |
| clause_LiteralGetFlag(PartnerLit,STRICTMAXIMAL)) && |
| (!OrdPara || |
| PartnerTerm == term_FirstArgument(PartnerEq) || |
| !clause_LiteralIsOrientedEquality(PartnerLit)) && |
| clause_LiteralIsPositive(PartnerLit) && |
| clause_Number(PartnerClause) != clause_Number(Clause) && |
| (!Unit || clause_Length(PartnerClause) == 1) && |
| clause_HasSolvedConstraint(PartnerClause)) { |
| SYMBOL MaxVar; |
| SUBST Subst, PartnerSubst; |
| |
| MaxVar = clause_MaxVar(PartnerClause); |
| clause_RenameVarsBiggerThan(Clause,MaxVar); |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(), Term, |
| cont_RightContext(),PartnerTerm); |
| subst_ExtractUnifier(cont_LeftContext(), &Subst, |
| cont_RightContext(),&PartnerSubst); |
| cont_Reset(); |
| if (!MaxPara || |
| inf_LiteralsMax(Clause, i, Subst, PartnerClause, j, |
| PartnerSubst, Flags, Precedence)) { |
| TERM PartnerLeft,PartnerRight; |
| BOOL Check, PartnerCheck; |
| PartnerLeft = PartnerRight = NULL; |
| PartnerCheck = Check = TRUE; |
| if (OrdPara && |
| !clause_LiteralIsOrientedEquality(PartnerLit)) { |
| /* Check post condition for partner literal */ |
| if (PartnerTerm == term_FirstArgument(PartnerEq)) |
| PartnerRight = term_SecondArgument(PartnerEq); |
| else |
| PartnerRight = term_FirstArgument(PartnerEq); |
| PartnerLeft = subst_Apply(PartnerSubst, |
| term_Copy(PartnerTerm)); |
| PartnerRight = subst_Apply(PartnerSubst, |
| term_Copy(PartnerRight)); |
| PartnerCheck = (ord_Compare(PartnerLeft,PartnerRight, |
| Flags, Precedence) |
| != ord_SmallerThan()); |
| } |
| if (PartnerCheck && |
| MaxPara && !clause_LiteralIsOrientedEquality(Lit)) { |
| /* Check post condition for literal in given clause */ |
| TERM NewLeft, NewRight; |
| if (Left) { |
| NewLeft = term_FirstArgument(Atom); |
| NewRight = term_SecondArgument(Atom); |
| } else { |
| NewLeft = term_SecondArgument(Atom); |
| NewRight = term_FirstArgument(Atom); |
| } |
| NewLeft = subst_Apply(Subst, term_Copy(NewLeft)); |
| NewRight = subst_Apply(Subst, term_Copy(NewRight)); |
| Check = (ord_Compare(NewLeft, NewRight, Flags, Precedence) |
| != ord_SmallerThan()); |
| term_Delete(NewLeft); |
| term_Delete(NewRight); |
| } |
| if (Check && PartnerCheck) { |
| /* Make inference only if both tests were successful */ |
| TERM SupAtom; |
| SupAtom = NULL; |
| if (PartnerRight == NULL) { |
| if (PartnerTerm==term_FirstArgument(PartnerEq)) |
| PartnerRight = term_SecondArgument(PartnerEq); |
| else |
| PartnerRight = term_FirstArgument(PartnerEq); |
| PartnerRight = subst_Apply(PartnerSubst, |
| term_Copy(PartnerRight)); |
| } |
| if (Left) |
| SupAtom = inf_AllTermsLeftRplac(Atom, Term, |
| PartnerRight, Subst); |
| else |
| SupAtom = inf_AllTermsRightRplac(Atom, Term, |
| PartnerRight, Subst); |
| #ifdef CHECK |
| if (SupAtom == NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPLeftEqToGiven:"); |
| misc_ErrorReport(" replacement wasn't possible."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| Result = |
| list_Cons(inf_ApplyGenSuperposition(PartnerClause, j, |
| PartnerSubst,Clause, |
| i,Subst,SupAtom, |
| FALSE,OrdPara, |
| MaxPara,Flags, |
| Precedence), |
| Result); |
| } |
| if (PartnerLeft != term_Null()) |
| term_Delete(PartnerLeft); |
| if (PartnerRight != term_Null()) |
| term_Delete(PartnerRight); |
| } |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } |
| } |
| } |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| static LIST inf_GenSPLeftLitToGiven(CLAUSE Clause, int i, TERM Atom, |
| SHARED_INDEX ShIndex, BOOL OrdPara, |
| BOOL MaxPara, BOOL Unit, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An unshared clause, the index of an antecedent |
| literal that is not an equality literal and its |
| atom, a shared index, three boolean flags |
| controlling inference preconditions (see also |
| inf_GenSuperpositionLeft), a flag store and a |
| precedence. |
| RETURNS: A list of clauses derivable from superposition left on the |
| GivenCopy wrt. the Index. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, TermList, ParentList; |
| int Bottom; |
| LITERAL Lit; |
| TERM Term, PartnerTerm, PartnerEq; |
| |
| Result = list_Nil(); |
| Lit = clause_GetLiteral(Clause,i); |
| |
| #ifdef CHECK |
| if (clause_LiteralIsEquality(Lit) || !clause_LiteralIsFromAntecedent(Lit)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPLeftLitToGiven: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Bottom = stack_Bottom(); |
| sharing_PushListOnStack(term_ArgumentList(Atom)); |
| |
| while (!stack_Empty(Bottom)) { |
| Term = (TERM)stack_PopResult(); |
| if (!term_IsVariable(Term)) { |
| /* Superposition into variables is not necessary */ |
| TermList = st_GetUnifier(cont_LeftContext(), |
| sharing_Index(ShIndex), |
| cont_RightContext(), |
| Term); |
| for ( ; !list_Empty(TermList); TermList=list_Pop(TermList)) { |
| PartnerTerm = (TERM)list_Car(TermList); |
| for (ParentList = term_SupertermList(PartnerTerm); |
| !list_Empty(ParentList); ParentList = list_Cdr(ParentList)) { |
| PartnerEq = (TERM)list_Car(ParentList); |
| if (fol_IsEquality(PartnerEq)) { |
| CLAUSE PartnerClause; |
| LITERAL PartnerLit; |
| TERM PartnerAtom; |
| LIST Scl; |
| int j; |
| for (Scl = sharing_NAtomDataList(PartnerEq); |
| !list_Empty(Scl); Scl = list_Cdr(Scl)) { |
| PartnerLit = (LITERAL)list_Car(Scl); |
| j = clause_LiteralGetIndex(PartnerLit); |
| PartnerClause = clause_LiteralOwningClause(PartnerLit); |
| PartnerAtom = clause_LiteralAtom(PartnerLit); |
| if (!clause_GetFlag(PartnerClause,CLAUSESELECT) && |
| (!MaxPara || |
| clause_LiteralGetFlag(PartnerLit,STRICTMAXIMAL)) && |
| (!OrdPara || |
| PartnerTerm == term_FirstArgument(PartnerAtom) || |
| !clause_LiteralIsOrientedEquality(PartnerLit)) && |
| clause_LiteralIsPositive(PartnerLit) && |
| clause_Number(PartnerClause) != clause_Number(Clause) && |
| (!Unit || clause_Length(PartnerClause) == 1) && |
| clause_HasSolvedConstraint(PartnerClause)) { |
| SYMBOL MaxVar; |
| TERM PartnerLeft,PartnerRight; |
| SUBST Subst, PartnerSubst; |
| TERM SupAtom; |
| |
| SupAtom = (TERM)NULL; |
| MaxVar = clause_MaxVar(PartnerClause); |
| clause_RenameVarsBiggerThan(Clause,MaxVar); |
| cont_Check(); |
| unify_UnifyNoOC(cont_LeftContext(),Term,cont_RightContext(),PartnerTerm); |
| subst_ExtractUnifier(cont_LeftContext(),&Subst,cont_RightContext(),&PartnerSubst); |
| cont_Reset(); |
| if (!MaxPara || |
| inf_LiteralsMax(Clause, i, Subst, PartnerClause, j, |
| PartnerSubst, Flags, Precedence)) { |
| PartnerLeft = subst_Apply(PartnerSubst, |
| term_Copy(PartnerTerm)); |
| if (PartnerTerm == term_FirstArgument(PartnerAtom)) |
| PartnerRight = subst_Apply(PartnerSubst, |
| term_Copy(term_SecondArgument(PartnerAtom))); |
| else |
| PartnerRight = subst_Apply(PartnerSubst, |
| term_Copy(term_FirstArgument(PartnerAtom))); |
| |
| if (!OrdPara || |
| clause_LiteralIsOrientedEquality(PartnerLit) || |
| ord_Compare(PartnerLeft,PartnerRight,Flags, Precedence) |
| != ord_SmallerThan()) { |
| SupAtom = inf_AllTermsRplac(Atom,Term,PartnerRight,Subst); |
| #ifdef CHECK |
| if (SupAtom == NULL) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPRightLitToGiven:"); |
| misc_ErrorReport(" replacement wasn't possible."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| Result = |
| list_Cons(inf_ApplyGenSuperposition(PartnerClause, j, |
| PartnerSubst, Clause, |
| i, Subst, SupAtom, |
| FALSE, OrdPara, |
| MaxPara, Flags, |
| Precedence), |
| Result); |
| |
| } |
| term_Delete(PartnerLeft); |
| term_Delete(PartnerRight); |
| } |
| subst_Delete(Subst); |
| subst_Delete(PartnerSubst); |
| } |
| } |
| } |
| } |
| } |
| } |
| } |
| return Result; |
| } |
| |
| |
| static LIST inf_GenSPLeftToGiven(CLAUSE Clause, int i, SHARED_INDEX ShIndex, |
| BOOL OrdPara, BOOL MaxPara, BOOL Unit, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: An unshared clause, the index of an antecedent |
| literal, an index of shared clauses, three boolean |
| flags for controlling inference preconditions (see |
| inf_GenSuperpositionLeft), a flag store and a |
| precedence. |
| RETURNS: A list of clauses derivable from Superposition Left |
| on the GivenCopy wrt. the Index. |
| MEMORY: A list of clauses is produced, where memory for the |
| list and the clauses is allocated. |
| ***************************************************************/ |
| { |
| TERM Atom; |
| LIST Result; |
| |
| #ifdef CHECK |
| if (clause_GetFlag(Clause, NOPARAINTO) || |
| (!clause_LiteralGetFlag(clause_GetLiteral(Clause,i),LITSELECT) && |
| (clause_GetFlag(Clause, CLAUSESELECT) || |
| (MaxPara && !clause_LiteralIsMaximal(clause_GetLiteral(Clause,i)))))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSPLeftToGiven: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i)); |
| |
| if (fol_IsEquality(Atom)) { |
| Result = list_Nconc(inf_GenSPLeftEqToGiven(Clause,i, TRUE,ShIndex, OrdPara, |
| MaxPara, Unit, Flags,Precedence), |
| Result); |
| if (!MaxPara || |
| !clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i))) |
| /* For SPm and OPm always try other direction, for SpR try it */ |
| /* only if the literal is not oriented. */ |
| Result = list_Nconc(inf_GenSPLeftEqToGiven(Clause,i,FALSE,ShIndex,OrdPara, |
| MaxPara,Unit,Flags,Precedence), |
| Result); |
| } else |
| Result = list_Nconc(inf_GenSPLeftLitToGiven(Clause,i,Atom,ShIndex,OrdPara, |
| MaxPara,Unit,Flags,Precedence), |
| Result); |
| |
| return Result; |
| } |
| |
| |
| LIST inf_GenSuperpositionLeft(CLAUSE GivenClause, SHARED_INDEX ShIndex, |
| BOOL OrdPara, BOOL MaxPara, BOOL Unit, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause and an Index, usually the WorkedOffIndex, |
| two boolean flags for controlling inference |
| preconditions, a flag store and a precedence. |
| RETURNS: A list of clauses derivable from the Givenclause by |
| one of the following inference rules wrt. the Index: |
| |
| OrdPara=TRUE, MaxPara=TRUE |
| -> Superposition Left |
| |
| OrdPara=TRUE, MaxPara=FALSE |
| -> ordered Paramodulation |
| |
| OrdPara=FALSE, MaxPara=FALSE |
| -> simple Paramodulation |
| |
| OrdPara=FALSE, MaxPara=TRUE |
| -> not defined |
| |
| If <Unit>==TRUE the clause with the maximal equality |
| additionally must be a unit clause. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result; |
| TERM Atom; |
| CLAUSE Copy; |
| int i, n; |
| LITERAL ActLit; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSuperpositionLeft: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| if (!OrdPara && MaxPara) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GenSuperpositionLeft: Illegal inference rule selection,"); |
| misc_ErrorReport("\n OrdPara=FALSE & MaxPara=TRUE."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| |
| if (!clause_HasSolvedConstraint(GivenClause)) |
| return Result; |
| |
| Copy = clause_Copy(GivenClause); |
| n = clause_LastSuccedentLitIndex(Copy); |
| |
| if (!clause_GetFlag(Copy, CLAUSESELECT) && |
| (!Unit || clause_Length(Copy) == 1)) { |
| for (i = clause_FirstSuccedentLitIndex(Copy); i <= n; i++) { |
| ActLit = clause_GetLiteral(Copy, i); |
| Atom = clause_LiteralSignedAtom(ActLit); |
| |
| if (fol_IsEquality(Atom) && |
| (!MaxPara || |
| clause_LiteralGetFlag(ActLit,STRICTMAXIMAL))) { |
| |
| Result = |
| list_Nconc(inf_GenLitSPLeft(Copy, term_FirstArgument(Atom), |
| term_SecondArgument(Atom), i, ShIndex, |
| OrdPara, MaxPara, Flags, Precedence), |
| Result); |
| if (!OrdPara || !clause_LiteralIsOrientedEquality(ActLit)) |
| /* For SPm always try the other direction, for OPm and SpL */ |
| /* only try it if the literal is not oriented. */ |
| Result = |
| list_Nconc(inf_GenLitSPLeft(Copy, term_SecondArgument(Atom), |
| term_FirstArgument(Atom), i, ShIndex, |
| OrdPara, MaxPara, Flags, Precedence), |
| Result); |
| } |
| } |
| } |
| |
| n = clause_LastAntecedentLitIndex(Copy); |
| if (!clause_GetFlag(Copy,NOPARAINTO)) { |
| for (i = clause_FirstAntecedentLitIndex(Copy); i <= n; i++) { |
| ActLit = clause_GetLiteral(Copy, i); |
| |
| if (clause_LiteralGetFlag(ActLit, LITSELECT) || |
| (!clause_GetFlag(Copy, CLAUSESELECT) && |
| (!MaxPara || clause_LiteralIsMaximal(ActLit)))) |
| Result = list_Nconc(inf_GenSPLeftToGiven(Copy, i, ShIndex, OrdPara, |
| MaxPara,Unit,Flags,Precedence), |
| Result); |
| } |
| } |
| clause_Delete(Copy); |
| |
| return(Result); |
| } |
| |
| |
| |
| LIST inf_ApplyDefinition(PROOFSEARCH Search, CLAUSE Clause, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A proof search object, a clause, a flag store and a |
| precedence. |
| RETURNS: A list of clauses derivable from the given clause by |
| applying the (potential) definitions in <Search>. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, Defs; |
| DEF Def; |
| |
| Result = list_Nil(); |
| for (Defs=prfs_Definitions(Search); !list_Empty(Defs); Defs=list_Cdr(Defs)) { |
| Def = (DEF)list_Car(Defs); |
| Result = list_Nconc(def_ApplyDefToClauseOnce(Def, Clause, Flags, Precedence), |
| Result); |
| } |
| return Result; |
| } |
| |
| |
| /************************************************************** |
| block with hyperresolution code starts here |
| ***************************************************************/ |
| |
| typedef struct { |
| LITERAL NucleusLit; |
| LITERAL ElectronLit; |
| SUBST ElectronSubst; |
| } INF_MAPNODE, *INF_MAPITEM; |
| |
| |
| static void inf_CopyHyperElectron(CLAUSE Clause, SUBST Subst2, SUBST Subst1, |
| int PLitInd, LIST* Constraint, |
| LIST* Succedent) |
| /************************************************************** |
| INPUT: An electron clause, a substitution, an index of a |
| succedent literal in this clause (the matched one), |
| and two lists by reference. |
| RETURNS: Nothing. |
| EFFECTS: The constraint and succedent literals are copied into |
| the corresponding lists except for the literal with |
| the given index. The composition <Subst2> ° <Subst1> |
| is applied to all copied literals. |
| The antecedent of the electron clause is empty, so |
| there's no need for a third list by reference. |
| ***************************************************************/ |
| { |
| TERM Atom; |
| int n, lc, j; |
| |
| #ifdef CHECK |
| if (clause_NumOfAnteLits(Clause) != 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_CopyHyperElectron: Electron contains antecedent literals."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| n = clause_LastSuccedentLitIndex(Clause); |
| lc = clause_LastConstraintLitIndex(Clause); |
| |
| for (j = clause_FirstConstraintLitIndex(Clause); j <= n; j++) { |
| if (j != PLitInd) { |
| Atom = subst_Apply(Subst1, term_Copy(clause_GetLiteralAtom(Clause, j))); |
| Atom = subst_Apply(Subst2, Atom); |
| if (j <= lc) |
| *Constraint = list_Cons(Atom, *Constraint); |
| else /* Literal must be from succedent */ |
| *Succedent = list_Cons(Atom, *Succedent); |
| } |
| } |
| } |
| |
| |
| static CLAUSE inf_BuildHyperResolvent(CLAUSE Nucleus, SUBST Subst, |
| LIST FoundMap, BOOL StrictlyMaximal, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause <Nucleus> with solved sort constraint, |
| the substitution <Subst> for <Nucleus>, a mapping |
| <FoundMap> of literals of already found partner |
| clauses, a boolean flag indicating whether this is |
| a ordered or a standard hyper resolution inference |
| a flag store and a precedence. |
| RETURNS: The newly created hyper resolvent. |
| ***************************************************************/ |
| { |
| CLAUSE NewClause; |
| LIST Constraint, Succedent, Parents, ParentNum, ParentLits, Scan; |
| int i, bound, Depth; |
| LITERAL Lit; |
| SUBST ESubst; |
| INF_MAPITEM MapItem; |
| |
| Parents = list_List(Nucleus); /* parent clauses */ |
| ParentNum = list_Nil(); /* parent clause numbers */ |
| ParentLits = list_Nil(); /* literal indices */ |
| Constraint = Succedent = list_Nil(); /* literals of the new clause */ |
| |
| /* Get constraint literals from nucleus */ |
| bound = clause_LastConstraintLitIndex(Nucleus); |
| for (i = clause_FirstConstraintLitIndex(Nucleus); i <= bound; i++) |
| Constraint = |
| list_Cons(subst_Apply(Subst,term_Copy(clause_GetLiteralAtom(Nucleus,i))), |
| Constraint); |
| /* Get succedent literals from nucleus */ |
| bound = clause_LastSuccedentLitIndex(Nucleus); |
| for (i = clause_FirstSuccedentLitIndex(Nucleus); i <= bound; i++) |
| Succedent = |
| list_Cons(subst_Apply(Subst,term_Copy(clause_GetLiteralAtom(Nucleus,i))), |
| Succedent); |
| |
| /* Now get the remaining data for the resolvent */ |
| Depth = clause_Depth(Nucleus); |
| bound = clause_LastAntecedentLitIndex(Nucleus); |
| for (i = clause_FirstAntecedentLitIndex(Nucleus); i <= bound; i++) { |
| /* Search <FoundMap> for the nucleus literal with index <i> */ |
| Lit = clause_GetLiteral(Nucleus, i); |
| for (Scan = FoundMap, MapItem = NULL; !list_Empty(Scan); |
| Scan = list_Cdr(Scan)) { |
| MapItem = list_Car(Scan); |
| if (MapItem->NucleusLit == Lit) |
| break; |
| } |
| |
| if (MapItem == NULL || MapItem->NucleusLit != Lit) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BuildHyperResolvent: Map entry not found."); |
| misc_FinishErrorReport(); |
| } |
| |
| Lit = MapItem->ElectronLit; |
| NewClause = clause_LiteralOwningClause(Lit); |
| ESubst = MapItem->ElectronSubst; |
| |
| Depth = misc_Max(Depth, clause_Depth(NewClause)); |
| Parents = list_Cons(NewClause, Parents); |
| ParentNum = list_Cons((POINTER) clause_Number(Nucleus), ParentNum); |
| ParentLits = list_Cons((POINTER) i, ParentLits); |
| ParentNum = list_Cons((POINTER) clause_Number(NewClause), ParentNum); |
| ParentLits = list_Cons((POINTER) clause_LiteralGetIndex(Lit), ParentLits); |
| |
| /* Get the remaining constraint and succedent literals from electron */ |
| inf_CopyHyperElectron(NewClause,Subst,ESubst,clause_LiteralGetIndex(Lit), |
| &Constraint, &Succedent); |
| } |
| |
| /* create new clause and set clause data */ |
| NewClause = clause_Create(Constraint, list_Nil(), Succedent, Flags,Precedence); |
| |
| if (StrictlyMaximal) |
| clause_SetFromOrderedHyperResolution(NewClause); |
| else |
| clause_SetFromSimpleHyperResolution(NewClause); |
| |
| clause_SetDepth(NewClause, Depth + 1); |
| |
| clause_SetSplitDataFromList(NewClause, Parents); |
| |
| clause_SetParentClauses(NewClause, list_NReverse(ParentNum)); |
| clause_SetParentLiterals(NewClause, list_NReverse(ParentLits)); |
| |
| /* clean up */ |
| list_Delete(Parents); |
| list_Delete(Constraint); |
| list_Delete(Succedent); |
| |
| return NewClause; |
| } |
| |
| |
| static LIST inf_GetHyperResolutionPartnerLits(TERM Atom, SHARED_INDEX Index, |
| BOOL StrictlyMaximal) |
| /************************************************************** |
| INPUT: An atom, a clause index, and a boolean flag. |
| RETURNS: A list of literals from purely positive clauses |
| from the index where either <StrictlyMaximal> is |
| false or the literals are strictly maximal in their |
| respective clauses. |
| ***************************************************************/ |
| { |
| LIST Result, TermList, LitScan; |
| LITERAL NextLit; |
| CLAUSE Clause; |
| |
| #ifdef CHECK |
| if (!term_IsAtom(Atom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_GetHyperResolutionPartnerLits: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Result = list_Nil(); |
| TermList = st_GetUnifier(cont_LeftContext(), sharing_Index(Index), |
| cont_RightContext(), Atom); |
| |
| for (; !list_Empty(TermList); TermList = list_Pop(TermList)) { |
| if (!term_IsVariable(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_LiteralIsFromSuccedent(NextLit) && |
| (!StrictlyMaximal || clause_LiteralGetFlag(NextLit, STRICTMAXIMAL)) && |
| clause_HasSolvedConstraint(Clause) && |
| clause_HasEmptyAntecedent(Clause)) |
| Result = list_Cons(NextLit, Result); |
| } |
| } |
| } |
| return Result; |
| } |
| |
| static LIST inf_HyperResolvents(CLAUSE Clause, SUBST Subst, LIST Restlits, |
| int GlobalMaxVar, LIST FoundMap, |
| BOOL StrictlyMaximal, SHARED_INDEX Index, |
| FLAGSTORE Flags, PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A nucleus <Clause> where the sort constraint is |
| solved, |
| a substitution, that has to be applied to the |
| nucleus, |
| a list <Restlits> of antecedent literals for which |
| a partner clause is searched, |
| a list <FoundMap> of map items (n,e,s), where |
| n is an antecedent literal from the nucleus, |
| e is a positive literal from an electron clause, |
| that is unifiable with n and s is a substitution |
| that has to be applied to the electron clause, |
| a flag store and |
| a precedence. |
| A main invariant of our algorithm is that all involved |
| clauses are pairwise variable disjoint. For that reason |
| we need, when building the resolvent, only apply the electron |
| specific substitution and the composed substitution <Subst> |
| to the electron clauses, and only <Subst> to the nucleus clause. |
| RETURNS: The list of hyper-resolvents. |
| ***************************************************************/ |
| { |
| LITERAL Lit, PLit; |
| |
| if (list_Empty(Restlits)) { |
| /* This case stops the recursion */ |
| LIST Scan; |
| INF_MAPITEM MapItem; |
| |
| /* A posteriori test for the electron literals */ |
| if (StrictlyMaximal) { /* only for ordered hyper resolution */ |
| for (Scan = FoundMap; !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| MapItem = list_Car(Scan); |
| Lit = MapItem->ElectronLit; |
| if (!inf_LitMaxWith2Subst(clause_LiteralOwningClause(Lit), |
| clause_LiteralGetIndex(Lit), -1, Subst, |
| MapItem->ElectronSubst,TRUE,Flags,Precedence)) |
| return list_Nil(); |
| } |
| } |
| /* Build the resolvent */ |
| return list_List(inf_BuildHyperResolvent(Clause, Subst, FoundMap, |
| StrictlyMaximal,Flags,Precedence)); |
| } |
| else { |
| CLAUSE PartnerCopy; |
| LIST Result, NextLits; |
| TERM AtomCopy; |
| SUBST NewSubst, RightSubst, HelpSubst; |
| SYMBOL NewMaxVar; |
| int PLitInd; |
| BOOL Swapped; |
| INF_MAPNODE MapNode; |
| |
| Result = list_Nil(); |
| 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))); |
| |
| Swapped = FALSE; |
| |
| /* The 'endless' loop may run twice for equations, once for other atoms */ |
| while (TRUE) { |
| NextLits = inf_GetHyperResolutionPartnerLits(AtomCopy,Index, |
| StrictlyMaximal); |
| |
| for ( ; !list_Empty(NextLits); NextLits = list_Pop(NextLits)) { |
| |
| PLit = list_Car(NextLits); |
| PLitInd = clause_LiteralGetIndex(PLit); |
| PartnerCopy = clause_Copy(clause_LiteralOwningClause(PLit)); |
| |
| clause_RenameVarsBiggerThan(PartnerCopy, GlobalMaxVar); |
| PLit = clause_GetLiteral(PartnerCopy, PLitInd); |
| |
| NewMaxVar = term_MaxVar(clause_LiteralAtom(PLit)); |
| NewMaxVar = symbol_GreaterVariable(GlobalMaxVar, NewMaxVar) ? |
| GlobalMaxVar : NewMaxVar; |
| |
| cont_Check(); |
| if (!unify_UnifyNoOC(cont_LeftContext(), AtomCopy, cont_RightContext(), |
| clause_LiteralAtom(PLit))) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_HyperResolvents: Unification failed."); |
| misc_FinishErrorReport(); |
| } |
| subst_ExtractUnifier(cont_LeftContext(), &NewSubst, |
| cont_RightContext(), &RightSubst); |
| cont_Reset(); |
| |
| HelpSubst = NewSubst; |
| NewSubst = subst_Compose(NewSubst, subst_Copy(Subst)); |
| subst_Delete(HelpSubst); |
| |
| MapNode.NucleusLit = Lit; |
| MapNode.ElectronLit = PLit; |
| MapNode.ElectronSubst = RightSubst; |
| FoundMap = list_Cons(&MapNode, FoundMap); |
| |
| Result = list_Nconc(inf_HyperResolvents(Clause, NewSubst, Restlits, |
| NewMaxVar, FoundMap, |
| StrictlyMaximal, Index, Flags, |
| Precedence), |
| Result); |
| |
| subst_Delete(NewSubst); |
| subst_Delete(RightSubst); |
| clause_Delete(PartnerCopy); |
| FoundMap = list_Pop(FoundMap); |
| } |
| if (!Swapped && fol_IsEquality(AtomCopy)) { |
| term_EqualitySwap(AtomCopy); |
| Swapped = TRUE; |
| } else |
| break; |
| } /* end of 'endless' loop */ |
| |
| list_Delete(Restlits); |
| term_Delete(AtomCopy); |
| |
| return Result; |
| } |
| } |
| |
| |
| static LIST inf_GetAntecedentLiterals(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause |
| RETURNS: The list of all antecedent literals of the clause. |
| ***************************************************************/ |
| { |
| int lc, i; |
| LIST Result; |
| |
| Result = list_Nil(); |
| lc = clause_LastAntecedentLitIndex(Clause); |
| for (i = clause_FirstAntecedentLitIndex(Clause); i <= lc ; i++) { |
| Result = list_Cons(clause_GetLiteral(Clause, i), Result); |
| } |
| return Result; |
| } |
| |
| |
| static LIST inf_ForwardHyperResolution(CLAUSE GivenClause, SHARED_INDEX Index, |
| BOOL StrictlyMaximal, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with an solved sort constraint, an 'Index' |
| of clauses, a boolean flag, a flag store and a |
| precedence. |
| RETURNS: A list of clauses inferred from <GivenClause> by |
| hyper resolution wrt. the index. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result, RestLits; |
| ; |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_ForwardHyperResolution: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (clause_HasEmptyAntecedent(GivenClause)) |
| return list_Nil(); |
| |
| Result = list_Nil(); |
| |
| /* Build up list of all antecedent literals. */ |
| RestLits = inf_GetAntecedentLiterals(GivenClause); |
| |
| Result = list_Nconc(inf_HyperResolvents(GivenClause, subst_Nil(), |
| RestLits,clause_MaxVar(GivenClause), |
| list_Nil(),StrictlyMaximal,Index, |
| Flags, Precedence), |
| Result); |
| list_Delete(RestLits); |
| |
| return Result; |
| } |
| |
| |
| static LIST inf_BackwardHyperResolution(CLAUSE Electron, SHARED_INDEX Index, |
| BOOL StrictlyMaximal, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause with an solved sort constraint, |
| an 'Index' of clauses, a boolean flag, a flag store, |
| and a precedence. |
| RETURNS: A list of clauses inferred by hyper resolution |
| wrt. the index with <Electron> as an electron. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| CLAUSE ElectronCopy; |
| LIST Result; |
| int i, ls; |
| |
| if (!clause_HasEmptyAntecedent(Electron) || |
| clause_HasEmptySuccedent(Electron)) |
| return list_Nil(); |
| |
| Result = list_Nil(); |
| |
| ElectronCopy = clause_Copy(Electron); |
| |
| /* Search succedent literal in <Electron> */ |
| ls = clause_LastSuccedentLitIndex(ElectronCopy); |
| for (i = clause_FirstSuccedentLitIndex(Electron); i <= ls; i++) { |
| LITERAL ElecLit; |
| TERM ElecAtom; |
| |
| ElecLit = clause_GetLiteral(ElectronCopy, i); |
| ElecAtom = clause_LiteralAtom(ElecLit); |
| |
| if (!StrictlyMaximal || clause_LiteralGetFlag(ElecLit, STRICTMAXIMAL)) { |
| LIST CandAtoms; |
| BOOL Swapped; |
| |
| Swapped = FALSE; |
| |
| /* The 'endless' loop may run twice for equations, once for other atoms */ |
| while (TRUE) { |
| /* Get unifiable antecedent literals in nucleus */ |
| CandAtoms = st_GetUnifier(cont_LeftContext(), sharing_Index(Index), |
| cont_RightContext(), ElecAtom); |
| |
| for ( ; !list_Empty(CandAtoms); CandAtoms = list_Pop(CandAtoms)) { |
| if (!term_IsVariable(list_Car(CandAtoms))) { |
| LIST CandLits; |
| |
| CandLits = sharing_NAtomDataList(list_Car(CandAtoms)); |
| |
| for (; !list_Empty(CandLits); CandLits = list_Cdr(CandLits)) { |
| LITERAL NucLit; |
| TERM NucAtom; |
| CLAUSE Nucleus; |
| |
| NucLit = list_Car(CandLits); |
| NucAtom = clause_LiteralAtom(NucLit); |
| Nucleus = clause_LiteralOwningClause(NucLit); |
| |
| if (clause_LiteralIsFromAntecedent(NucLit) && |
| clause_HasSolvedConstraint(Nucleus)) { |
| LIST FoundMap, RestLits; |
| SUBST LeftSubst, RightSubst; |
| SYMBOL GlobalMaxVar, MaxVar; |
| INF_MAPNODE MapNode; |
| |
| GlobalMaxVar = clause_MaxVar(Nucleus); |
| clause_RenameVarsBiggerThan(ElectronCopy, GlobalMaxVar); |
| MaxVar = clause_SearchMaxVar(ElectronCopy); |
| GlobalMaxVar = symbol_GreaterVariable(GlobalMaxVar, MaxVar) ? |
| GlobalMaxVar : MaxVar; |
| /* Now ElecLit is renamed, too */ |
| |
| RestLits = inf_GetAntecedentLiterals(Nucleus); |
| RestLits = list_PointerDeleteElement(RestLits, NucLit); |
| |
| /* Get unifier */ |
| cont_Check(); |
| if (!unify_UnifyNoOC(cont_LeftContext(), NucAtom, |
| cont_RightContext(), ElecAtom)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_BackwardHyperResolution: Unification failed."); |
| misc_FinishErrorReport(); |
| } |
| subst_ExtractUnifier(cont_LeftContext(), &LeftSubst, |
| cont_RightContext(), &RightSubst); |
| cont_Reset(); |
| |
| MapNode.NucleusLit = NucLit; |
| MapNode.ElectronLit = ElecLit; |
| MapNode.ElectronSubst = RightSubst; |
| FoundMap = list_List(&MapNode); |
| |
| Result = list_Nconc(inf_HyperResolvents(Nucleus, LeftSubst, |
| RestLits, GlobalMaxVar, |
| FoundMap,StrictlyMaximal, |
| Index, Flags,Precedence), |
| Result); |
| |
| /* clean up */ |
| subst_Delete(LeftSubst); |
| subst_Delete(RightSubst); |
| list_Delete(RestLits); |
| list_Free(FoundMap); |
| } /* if a nucleus has been found */ |
| } /* for all nucleus candidate literals */ |
| } /* if term is atom */ |
| } /* for all nucleus candidate atoms */ |
| if (!Swapped && fol_IsEquality(ElecAtom)) { |
| term_EqualitySwap(ElecAtom); /* Atom is from copied clause */ |
| Swapped = TRUE; |
| } else |
| break; |
| } /* end of 'endless' loop */ |
| } /* for all lits usable in electron for hyper resolution */ |
| } /* for all lits in succedent */ |
| clause_Delete(ElectronCopy); |
| |
| return Result; |
| } |
| |
| |
| LIST inf_GeneralHyperResolution(CLAUSE GivenClause, SHARED_INDEX Index, |
| BOOL Ordered, FLAGSTORE Flags, |
| PRECEDENCE Precedence) |
| /************************************************************** |
| INPUT: A clause, an 'Index' of clauses, a boolean flag, |
| a flag store and a precedence. |
| RETURNS: A list of clauses inferred by |
| (ordered) hyper resolution wrt. the index. |
| If <Ordered>=TRUE then ordered hyper resolution |
| inferences are made, else standard hyper resolution |
| inferences. |
| MEMORY: A list of clauses is produced, where memory for the list |
| and the clauses is allocated. |
| ***************************************************************/ |
| { |
| LIST Result; |
| |
| Result = list_Nil(); |
| if (clause_HasSolvedConstraint(GivenClause)) { |
| Result = inf_ForwardHyperResolution(GivenClause, Index, Ordered, |
| Flags, Precedence); |
| Result = list_Nconc(inf_BackwardHyperResolution(GivenClause, Index, Ordered, |
| Flags, Precedence), |
| Result); |
| } |
| return Result; |
| } |
| |
| |
| LIST inf_DerivableClauses(PROOFSEARCH Search, CLAUSE GivenClause) |
| /************************************************************** |
| INPUT: A clause and an Index, usually the WorkedOffIndex. |
| RETURNS: A list of clauses derivable from 'GivenClause' wrt index. |
| EFFECT: Allocates memory for the clauselistnodes and new clauses. |
| ***************************************************************/ |
| { |
| LIST ListOfDerivedClauses; |
| SHARED_INDEX ShIndex; |
| SORTTHEORY Dynamic; |
| FLAGSTORE Flags; |
| PRECEDENCE Precedence; |
| |
| Flags = prfs_Store(Search); |
| Precedence = prfs_Precedence(Search); |
| |
| #ifdef CHECK |
| if (!clause_IsClause(GivenClause, Flags, Precedence)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In inf_DerivableClauses: Illegal input."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| ListOfDerivedClauses = list_Nil(); |
| ShIndex = prfs_WorkedOffSharingIndex(Search); |
| Dynamic = prfs_DynamicSortTheory(Search); |
| |
| if (Dynamic && !clause_HasSolvedConstraint(GivenClause)) { |
| |
| if (clause_HasTermSortConstraintLits(GivenClause)) { |
| if (flag_GetFlagValue(Flags, flag_ISOR)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_ForwardSortResolution(GivenClause, |
| sort_TheoryIndex(Dynamic), |
| Dynamic, FALSE, Flags,Precedence), |
| ListOfDerivedClauses); |
| } |
| else |
| if (flag_GetFlagValue(Flags, flag_IEMS)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_ForwardEmptySort(GivenClause, |
| sort_TheoryIndex(Dynamic), Dynamic, |
| FALSE, Flags, Precedence), |
| ListOfDerivedClauses); |
| } else { /* Given with solved Constraint! */ |
| |
| if (Dynamic && flag_GetFlagValue(Flags, flag_IEMS)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_BackwardEmptySort(GivenClause, sharing_Index(ShIndex), |
| Dynamic, FALSE, Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| if (Dynamic && flag_GetFlagValue(Flags, flag_ISOR)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_BackwardSortResolution(GivenClause, |
| sharing_Index(ShIndex), Dynamic, |
| FALSE, Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IEQR)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_EqualityResolution(GivenClause, TRUE, Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IERR)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_EqualityResolution(GivenClause, FALSE, Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IMPM)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_MergingParamodulation(GivenClause, ShIndex, Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IEQF)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_EqualityFactoring(GivenClause,Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| switch (flag_GetFlagValue(Flags, flag_IOFC)) { |
| case flag_FACTORINGOFF: |
| break; /* Do nothing */ |
| case flag_FACTORINGONLYRIGHT: |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralFactoring(GivenClause, TRUE, FALSE,TRUE, Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| break; |
| case flag_FACTORINGRIGHTANDLEFT: |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralFactoring(GivenClause, TRUE, TRUE, TRUE, Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| break; |
| default: |
| misc_StartUserErrorReport(); |
| misc_UserErrorReport("\n Error: Flag \"IOFC\" has invalid value.\n"); |
| misc_FinishUserErrorReport(); |
| } |
| |
| if (flag_GetFlagValue(Flags, flag_ISFC)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralFactoring(GivenClause, FALSE, TRUE, TRUE, Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_ISPR)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_SuperpositionRight(GivenClause,ShIndex,Flags,Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_ISPM)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_Paramodulation(GivenClause, ShIndex, Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IOPM)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_OrderedParamodulation(GivenClause, ShIndex, Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_ISPL)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_SuperpositionLeft(GivenClause, ShIndex, Flags,Precedence), |
| ListOfDerivedClauses); |
| |
| switch (flag_GetFlagValue(Flags, flag_IORE)) { |
| case flag_ORDEREDRESOLUTIONOFF: |
| break; /* Do nothing */ |
| case flag_ORDEREDRESOLUTIONNOEQUATIONS: /* no equations */ |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralResolution(GivenClause,ShIndex,TRUE,FALSE,Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| break; |
| |
| case flag_ORDEREDRESOLUTIONWITHEQUATIONS: /* allow equations */ |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralResolution(GivenClause,ShIndex,TRUE,TRUE, Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| break; |
| default: |
| misc_StartUserErrorReport(); |
| misc_UserErrorReport("\n Error: Flag \"IORE\" has invalid value.\n"); |
| misc_FinishUserErrorReport(); |
| } |
| |
| |
| switch (flag_GetFlagValue(Flags, flag_ISRE)) { |
| case flag_STANDARDRESOLUTIONOFF: |
| break; /* Do nothing */ |
| case flag_STANDARDRESOLUTIONNOEQUATIONS: /* no equations */ |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralResolution(GivenClause,ShIndex,FALSE,FALSE,Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| break; |
| case flag_STANDARDRESOLUTIONWITHEQUATIONS: /* allow equations */ |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralResolution(GivenClause,ShIndex,FALSE,TRUE,Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| break; |
| default: |
| misc_StartUserErrorReport(); |
| misc_UserErrorReport("\n Error: Flag \"ISRE\" has invalid value.\n"); |
| misc_FinishUserErrorReport(); |
| } |
| |
| if (flag_GetFlagValue(Flags, flag_IUNR)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_UnitResolution(GivenClause, ShIndex, FALSE, |
| Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IBUR)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_BoundedDepthUnitResolution(GivenClause,ShIndex,FALSE, |
| Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_ISHY)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralHyperResolution(GivenClause,ShIndex,FALSE,Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IOHY)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_GeneralHyperResolution(GivenClause,ShIndex,TRUE,Flags, |
| Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IURR)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_URResolution(GivenClause, ShIndex, Flags, Precedence), |
| ListOfDerivedClauses); |
| |
| if (flag_GetFlagValue(Flags, flag_IDEF)) |
| ListOfDerivedClauses = |
| list_Nconc(inf_ApplyDefinition(Search, GivenClause, Flags, Precedence), |
| ListOfDerivedClauses); |
| } |
| |
| return ListOfDerivedClauses; |
| } |