Google Git
Sign in
llvm / llvm-test-suite / refs/heads/main / . / MultiSource / Applications / SPASS / rules-inf.c
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
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;
}