blob: da6d959ed613115899430c4fe5095381277df482 [file] [log] [blame]
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * 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