Google Git
Sign in
llvm / llvm-test-suite / refs/heads/ggreif/CallInst-operands / . / MultiSource / Applications / SPASS / rules-red.c
blob: c4bee6be2854e9f56684f47df017eba049f2a3e6 [file] [log] [blame]
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * REDUCTION RULES * */
/* * * */
/* * $Module: REDRULES * */
/* * * */
/* * 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$ */
#include "rules-red.h"
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * Globals * */
/* * * */
/* ********************************************************** */
/**************************************************************/
/* Needed for term stamping in red_RewriteRedUnitClause */
static NAT red_STAMPID;
const NAT red_USABLE = 1;
const NAT red_WORKEDOFF = 2;
const NAT red_ALL = 3;
/**************************************************************/
/* FUNTION PROTOTYPES */
/**************************************************************/
static BOOL red_SortSimplification(SORTTHEORY, CLAUSE, NAT, BOOL, FLAGSTORE,
PRECEDENCE, CLAUSE*);
static BOOL red_SelectedStaticReductions(PROOFSEARCH, CLAUSE*, CLAUSE*, LIST*,
NAT);
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * Functions * */
/* * * */
/* ********************************************************** */
/**************************************************************/
static void red_HandleRedundantIndexedClauses(PROOFSEARCH Search, LIST Blocked,
CLAUSE RedClause)
/*********************************************************
INPUT: A proof search object, a list <Blocked> of clauses from
the proof search object and a clause that causes the
already indexed clauses in <Blocked> to be redundant.
RETURNS: Nothing.
**********************************************************/
{
FLAGSTORE Flags;
CLAUSE Clause;
LIST Scan;
Flags = prfs_Store(Search);
for (Scan = Blocked; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
Clause = (CLAUSE)list_Car(Scan);
if (prfs_SplitLevelCondition(clause_SplitLevel(RedClause),clause_SplitLevel(Clause),
prfs_LastBacktrackLevel(Search)))
split_DeleteClauseAtLevel(Search, Clause, clause_SplitLevel(RedClause));
else {
if (clause_GetFlag(Clause, WORKEDOFF)) {
if (flag_GetFlagValue(Flags, flag_DOCPROOF))
prfs_MoveWorkedOffDocProof(Search, Clause);
else
prfs_DeleteWorkedOff(Search, Clause);
}
else
if (flag_GetFlagValue(Flags, flag_DOCPROOF))
prfs_MoveUsableDocProof(Search, Clause);
else
prfs_DeleteUsable(Search, Clause);
}
}
}
static void red_HandleRedundantDerivedClauses(PROOFSEARCH Search, LIST Blocked,
CLAUSE RedClause)
/*********************************************************
INPUT: A proof search object, a list <Blocked> of clauses from
the proof search object and a clause that causes the
derived clauses in <Blocked> to be redundant.
RETURNS: Nothing.
**********************************************************/
{
CLAUSE Clause;
LIST Scan;
for (Scan = Blocked; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
Clause = (CLAUSE)list_Car(Scan);
if (prfs_SplitLevelCondition(clause_SplitLevel(RedClause),clause_SplitLevel(Clause),
prfs_LastBacktrackLevel(Search))) {
split_KeepClauseAtLevel(Search, Clause, clause_SplitLevel(RedClause));
}
else {
if (flag_GetFlagValue(prfs_Store(Search), flag_DOCPROOF))
prfs_InsertDocProofClause(Search, Clause);
else
clause_Delete(Clause);
}
}
}
void red_Init(void)
/*********************************************************
INPUT: None.
RETURNS: Nothing.
EFFECT: Initializes the Reduction module, in particular
its stampid to stamp terms.
**********************************************************/
{
red_STAMPID = term_GetStampID();
}
static void red_DocumentObviousReductions(CLAUSE Clause, LIST Indexes)
/*********************************************************
INPUT: A clause and a list of literal indexes removed by
obvious reductions.
RETURNS: None
MEMORY: The <Indexes> list is consumed.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nil());
clause_SetParentLiterals(Clause, Indexes);
clause_AddParentClause(Clause,clause_Number(Clause)); /* Has to be done before increasing it! */
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromObviousReductions(Clause);
}
static BOOL red_ObviousReductions(CLAUSE Clause, BOOL Document,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed)
/**********************************************************
INPUT: A clause, a boolean flag for proof
documentation, a flag store and a precedence.
RETURNS: TRUE iff obvious reductions are possible.
If <Document> is false the clause is
destructively changed,
else a reduced copy of the clause is returned
in <*Changed>.
EFFECT: Multiple occurrences of the same literal as
well as trivial equations are removed.
********************************************************/
{
int i, j, end;
LIST Indexes;
TERM Atom, PartnerAtom;
#ifdef CHECK
clause_Check(Clause, Flags, Precedence);
#endif
Indexes = list_Nil();
end = clause_LastAntecedentLitIndex(Clause);
for (i = clause_FirstConstraintLitIndex(Clause); i <= end; i++) {
Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i));
if (fol_IsEquality(Atom) &&
!clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause, i)) &&
term_Equal(term_FirstArgument(Atom),term_SecondArgument(Atom))) {
Indexes = list_Cons((POINTER)i,Indexes);
}
else
for (j = i+1; j <= end; j++) {
PartnerAtom = clause_LiteralAtom(clause_GetLiteral(Clause,j));
if (term_Equal(PartnerAtom, Atom) ||
(fol_IsEquality(Atom) &&
fol_IsEquality(PartnerAtom) &&
term_Equal(term_FirstArgument(Atom),term_SecondArgument(PartnerAtom)) &&
term_Equal(term_FirstArgument(PartnerAtom),term_SecondArgument(Atom)))) {
Indexes = list_Cons((POINTER)i,Indexes);
j = end;
}
}
}
end = clause_LastSuccedentLitIndex(Clause);
for (i = clause_FirstSuccedentLitIndex(Clause); i <= end; i++) {
Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i));
for (j = i+1; j <= end; j++) {
PartnerAtom = clause_LiteralAtom(clause_GetLiteral(Clause,j));
if (term_Equal(PartnerAtom,Atom) ||
(fol_IsEquality(Atom) &&
fol_IsEquality(PartnerAtom) &&
term_Equal(term_FirstArgument(Atom),term_SecondArgument(PartnerAtom)) &&
term_Equal(term_FirstArgument(PartnerAtom),term_SecondArgument(Atom)))) {
Indexes = list_Cons((POINTER)i,Indexes);
j = end;
}
}
}
if (clause_Length(Clause) == 1 &&
clause_NumOfAnteLits(Clause) == 1 &&
!list_PointerMember(Indexes,(POINTER)clause_FirstAntecedentLitIndex(Clause)) &&
fol_IsEquality(clause_GetLiteralAtom(Clause,clause_FirstAntecedentLitIndex(Clause)))) {
cont_StartBinding();
if (unify_UnifyCom(cont_LeftContext(),
term_FirstArgument(clause_LiteralAtom(clause_GetLiteral(Clause,clause_FirstAntecedentLitIndex(Clause)))),
term_SecondArgument(clause_LiteralAtom(clause_GetLiteral(Clause,clause_FirstAntecedentLitIndex(Clause))))))
Indexes = list_Cons((POINTER)clause_FirstAntecedentLitIndex(Clause),Indexes);
cont_BackTrack();
}
if (!list_Empty(Indexes)) {
if (flag_GetFlagValue(Flags, flag_POBV)) {
fputs("\nObvious: ", stdout);
clause_Print(Clause);
fputs(" ==> ", stdout);
}
if (Document) {
CLAUSE Copy;
Copy = clause_Copy(Clause);
clause_DeleteLiterals(Copy,Indexes, Flags, Precedence);
red_DocumentObviousReductions(Copy,Indexes); /* Indexes is consumed */
if (flag_GetFlagValue(Flags, flag_POBV))
clause_Print(Copy);
*Changed = Copy;
}
else {
clause_DeleteLiterals(Clause,Indexes, Flags, Precedence);
list_Delete(Indexes);
if (flag_GetFlagValue(Flags, flag_POBV))
clause_Print(Clause);
}
return TRUE;
}
return FALSE;
}
static void red_DocumentCondensing(CLAUSE Clause, LIST Indexes)
/*********************************************************
INPUT: A clause and a list of literal indexes removed by condensing.
RETURNS: Nothing.
MEMORY: The <Indexes> list is consumed.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nil());
clause_SetParentLiterals(Clause, Indexes);
clause_AddParentClause(Clause,clause_Number(Clause)); /* Has to be done before increasing it! */
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromCondensing(Clause);
}
static BOOL red_Condensing(CLAUSE Clause, BOOL Document, FLAGSTORE Flags,
PRECEDENCE Precedence, CLAUSE *Changed)
/**********************************************************
INPUT: A non-empty unshared clause, a boolean flag
concerning proof documentation, a flag store and
a precedence.
RETURNS: TRUE iff condensing is applicable to <Clause>.
If <Document> is false the clause is
destructively changed else a condensed copy of
the clause is returned in <*Changed>.
***********************************************************/
{
LIST Indexes;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence) ||
(*Changed != (CLAUSE)NULL)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_Condensing : ");
misc_ErrorReport("Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
Indexes = cond_CondFast(Clause);
if (!list_Empty(Indexes)) {
if (flag_GetFlagValue(Flags, flag_PCON)) {
fputs("\nCondensing: ", stdout);
clause_Print(Clause);
fputs(" ==> ", stdout);
}
if (Document) {
CLAUSE Copy;
Copy = clause_Copy(Clause);
clause_DeleteLiterals(Copy, Indexes, Flags, Precedence);
red_DocumentCondensing(Copy, Indexes);
if (flag_GetFlagValue(Flags, flag_PCON))
clause_Print(Copy);
*Changed = Copy;
}
else {
clause_DeleteLiterals(Clause, Indexes, Flags, Precedence);
list_Delete(Indexes);
if (flag_GetFlagValue(Flags, flag_PCON))
clause_Print(Clause);
}
return TRUE;
}
return FALSE;
}
static void red_DocumentAssignmentEquationDeletion(CLAUSE Clause, LIST Indexes,
NAT NonTrivClauseNumber)
/*********************************************************
INPUT: A clause and a list of literal indexes pointing to
redundant equations and the clause number of a clause
implying a non-trivial domain.
RETURNS: Nothing.
MEMORY: The <Indexes> list is consumed.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nil());
clause_SetParentLiterals(Clause, Indexes);
clause_AddParentClause(Clause,clause_Number(Clause)); /* Has to be done before increasing it! */
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromAssignmentEquationDeletion(Clause);
if (NonTrivClauseNumber != 0) { /* Such a clause exists */
clause_AddParentClause(Clause, NonTrivClauseNumber);
clause_AddParentLiteral(Clause, 0); /* The non triv clause has exactly one negative literal */
}
}
static BOOL red_AssignmentEquationDeletion(CLAUSE Clause, FLAGSTORE Flags,
PRECEDENCE Precedence, CLAUSE *Changed,
NAT NonTrivClauseNumber,
BOOL NonTrivDomain)
/**********************************************************
INPUT: A non-empty unshared clause, a flag store, a
precedence, the clause number of a clause
implying a non-trivial domain and a boolean
flag indicating whether the current domain has
more than one element.
RETURNS: TRUE iff equations are removed.
If the <DocProof> flag is false the clause is
destructively changed else a copy of the clause
where redundant equations are removed is
returned in <*Changed>.
***********************************************************/
{
LIST Indexes; /* List of indexes of redundant equations*/
NAT i;
TERM LeftArg, RightArg;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence) ||
(*Changed != (CLAUSE)NULL) ||
(NonTrivDomain && NonTrivClauseNumber == 0) ||
(!NonTrivDomain && NonTrivClauseNumber > 0)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_AssignmentEquationDeletion: ");
misc_ErrorReport("Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
Indexes = list_Nil();
if (clause_ContainsNegativeEquations(Clause)) {
for (i = clause_FirstAntecedentLitIndex(Clause); i <= clause_LastAntecedentLitIndex(Clause); i++) {
if (clause_LiteralIsEquality(clause_GetLiteral(Clause,i))) {
LeftArg = term_FirstArgument(clause_GetLiteralAtom(Clause,i));
RightArg = term_SecondArgument(clause_GetLiteralAtom(Clause,i));
if ((term_IsVariable(LeftArg) &&
clause_NumberOfSymbolOccurrences(Clause, term_TopSymbol(LeftArg)) == 1) ||
(term_IsVariable(RightArg) &&
clause_NumberOfSymbolOccurrences(Clause, term_TopSymbol(RightArg)) == 1))
Indexes = list_Cons((POINTER)i, Indexes);
}
}
}
else
if (NonTrivDomain && clause_ContainsPositiveEquations(Clause)) {
for (i = clause_FirstSuccedentLitIndex(Clause); i <= clause_LastSuccedentLitIndex(Clause); i++) {
if (clause_LiteralIsEquality(clause_GetLiteral(Clause,i))) {
LeftArg = term_FirstArgument(clause_GetLiteralAtom(Clause,i));
RightArg = term_SecondArgument(clause_GetLiteralAtom(Clause,i));
if ((term_IsVariable(LeftArg) &&
clause_NumberOfSymbolOccurrences(Clause, term_TopSymbol(LeftArg)) == 1) ||
(term_IsVariable(RightArg) &&
clause_NumberOfSymbolOccurrences(Clause, term_TopSymbol(RightArg)) == 1))
Indexes = list_Cons((POINTER)i, Indexes);
}
}
}
if (!list_Empty(Indexes)) {
if (flag_GetFlagValue(Flags, flag_PAED)) {
fputs("\nAED: ", stdout);
clause_Print(Clause);
fputs(" ==> ", stdout);
}
if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
CLAUSE Copy;
Copy = clause_Copy(Clause);
clause_DeleteLiterals(Copy, Indexes, Flags, Precedence);
red_DocumentAssignmentEquationDeletion(Copy, Indexes, NonTrivClauseNumber);
if (flag_GetFlagValue(Flags, flag_PAED))
clause_Print(Copy);
*Changed = Copy;
}
else {
clause_DeleteLiterals(Clause, Indexes, Flags, Precedence);
list_Delete(Indexes);
if (flag_GetFlagValue(Flags, flag_PAED))
clause_Print(Clause);
}
return TRUE;
}
return FALSE;
}
static BOOL red_Tautology(CLAUSE Clause, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**********************************************************
INPUT: A non-empty clause, a flag store and a
precedence.
RETURNS: The boolean value TRUE if 'Clause' is a
tautology.
***********************************************************/
{
TERM Atom;
int i,j, la,n;
BOOL Result;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_Tautology :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
la = clause_LastAntecedentLitIndex(Clause);
n = clause_Length(Clause);
Result = FALSE;
for (j = clause_FirstSuccedentLitIndex(Clause); j < n && !Result; j++) {
Atom = clause_LiteralAtom(clause_GetLiteral(Clause, j));
if (fol_IsEquality(Atom) &&
!clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause, j)) &&
term_Equal(term_FirstArgument(Atom),term_SecondArgument(Atom)))
Result = TRUE;
for (i = clause_FirstLitIndex(); i <= la && !Result; i++)
if (term_Equal(Atom, clause_LiteralAtom(clause_GetLiteral(Clause, i))))
Result = TRUE;
}
if (!Result &&
flag_GetFlagValue(Flags, flag_RTAUT) == flag_RTAUTSEMANTIC &&
clause_NumOfAnteLits(Clause) != 0 &&
clause_NumOfSuccLits(Clause) != 0) {
Result = cc_Tautology(Clause);
}
if (Result && flag_GetFlagValue(Flags, flag_PTAUT)) {
fputs("\nTautology: ", stdout);
clause_Print(Clause);
}
return Result;
}
static LITERAL red_GetMRResLit(LITERAL ActLit, SHARED_INDEX ShIndex)
/**************************************************************
INPUT: A literal and an Index.
RETURNS: The most valid clause with a complementary literal,
(CLAUSE)NULL, if no such clause exists.
***************************************************************/
{
LITERAL NextLit;
int i;
CLAUSE ActClause;
TERM CandTerm;
LIST LitScan;
NextLit = (LITERAL)NULL;
ActClause = clause_LiteralOwningClause(ActLit);
i = clause_LiteralGetIndex(ActLit);
CandTerm = st_ExistGen(cont_LeftContext(),
sharing_Index(ShIndex),
clause_LiteralAtom(ActLit));
while (CandTerm) { /* First check units */
if (!term_IsVariable(CandTerm)) { /* Has to be an Atom! */
LitScan = sharing_NAtomDataList(CandTerm); /* CAUTION !!! the List is not a copy */
while (!list_Empty(LitScan)) {
NextLit = list_Car(LitScan);
if (clause_LiteralsAreComplementary(ActLit,NextLit))
if (clause_Length(clause_LiteralOwningClause(NextLit)) == 1 ||
subs_SubsumesBasic(clause_LiteralOwningClause(NextLit),ActClause,
clause_LiteralGetIndex(NextLit),i)) {
st_CancelExistRetrieval();
return NextLit;
}
LitScan = list_Cdr(LitScan);
}
}
CandTerm = st_NextCandidate();
}
return (LITERAL)NULL;
}
static void red_DocumentMatchingReplacementResolution(CLAUSE Clause, LIST LitInds,
LIST ClauseNums, LIST PLitInds)
/*********************************************************
INPUT: A clause, the involved literals indices in <Clause>,
the literal indices of the reduction literals
and the clauses number.
RETURNS: Nothing.
MEMORY: All input lists are consumed.
**********************************************************/
{
LIST Scan,Help;
Help = list_Nil();
for (Scan=LitInds; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
Help = list_Cons((POINTER)clause_Number(Clause), Help);
/* Has to be done before increasing the clause number! */
}
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nconc(Help,ClauseNums));
clause_SetParentLiterals(Clause, list_Nconc(LitInds,PLitInds));
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromMatchingReplacementResolution(Clause);
}
static BOOL red_MatchingReplacementResolution(CLAUSE Clause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed, int Level)
/**************************************************************
INPUT: A clause, an Index, a flag store, a precedence and a
split level indicating the need of a copy if
<Clause> is reduced by a clause of higher split
level than <Level>.
RETURNS: TRUE if reduction wrt the indexed clauses was
possible.
If the <DocProof> flag is true or the clauses used
for reductions have a higher split level then a
changed copy is returned in <*Changed>.
Otherwise <Clause> is destructively changed.
***************************************************************/
{
CLAUSE PClause,Copy;
LITERAL ActLit,PLit;
int i, j, length;
LIST ReducedBy,ReducedLits,PLits,Scan1,Scan2;
BOOL Document;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence) ||
(*Changed != (CLAUSE)NULL)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_MatchingReplacementResolution:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
Copy = Clause;
length = clause_Length(Clause);
ReducedBy = list_Nil();
ReducedLits = list_Nil();
PLits = list_Nil();
i = clause_FirstLitIndex();
j = 0;
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
while (i < length) {
ActLit = clause_GetLiteral(Copy, i);
if (!fol_IsEquality(clause_LiteralAtom(ActLit)) || /* Reduce with negative equations. */
clause_LiteralIsPositive(ActLit)) {
PLit = red_GetMRResLit(ActLit, ShIndex);
if (clause_LiteralExists(PLit)) {
if (list_Empty(PLits) && flag_GetFlagValue(Flags, flag_PMRR)) {
fputs("\nFMatchingReplacementResolution: ", stdout);
clause_Print(Copy);
}
PClause = clause_LiteralOwningClause(PLit);
ReducedBy = list_Cons((POINTER)clause_Number(PClause), ReducedBy);
PLits = list_Cons((POINTER)clause_LiteralGetIndex(PLit),PLits);
ReducedLits = list_Cons((POINTER)(i+j), ReducedLits);
if (Copy == Clause &&
(Document || prfs_SplitLevelCondition(clause_SplitLevel(PClause),clause_SplitLevel(Copy),Level)))
Copy = clause_Copy(Clause);
clause_UpdateSplitDataFromPartner(Copy, PClause);
clause_DeleteLiteral(Copy,i, Flags, Precedence);
length--;
j++;
}
else
i++;
}
else
i++;
}
if (!list_Empty(ReducedBy)) {
if (Document) {
ReducedBy = list_NReverse(ReducedBy);
ReducedLits = list_NReverse(ReducedLits);
PLits = list_NReverse(PLits);
red_DocumentMatchingReplacementResolution(Copy, ReducedLits, ReducedBy, PLits); /* Lists are consumed */
if (flag_GetFlagValue(Flags, flag_PMRR)) {
fputs(" ==> [ ", stdout);
for(Scan1=ReducedBy,Scan2=ReducedLits;!list_Empty(Scan1);
Scan1=list_Cdr(Scan1),Scan2=list_Cdr(Scan2))
printf("%d.%d ",(NAT)list_Car(Scan1),(NAT)list_Car(Scan2));
fputs("] ", stdout);
clause_Print(Copy);
}
}
else {
if (flag_GetFlagValue(Flags, flag_PMRR)) {
fputs(" ==> [ ", stdout);
for(Scan1=ReducedBy,Scan2=ReducedLits;!list_Empty(Scan1);
Scan1=list_Cdr(Scan1),Scan2=list_Cdr(Scan2))
printf("%d.%d ",(NAT)list_Car(Scan1),(NAT)list_Car(Scan2));
fputs("] ", stdout);
clause_Print(Copy);
}
list_Delete(ReducedBy);
list_Delete(ReducedLits);
list_Delete(PLits);
}
if (Copy != Clause)
*Changed = Copy;
return TRUE;
}
return FALSE;
}
static void red_DocumentUnitConflict(CLAUSE Clause, LIST LitInds,
LIST ClauseNums, LIST PLitInds)
/*********************************************************
INPUT: A clause, the involved literals indices and the clauses number.
RETURNS: Nothing.
MEMORY: All input lists are consumed.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, list_Nconc(list_List((POINTER)clause_Number(Clause)),ClauseNums));
clause_SetParentLiterals(Clause, list_Nconc(LitInds,PLitInds));
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromUnitConflict(Clause);
}
static BOOL red_UnitConflict(CLAUSE Clause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed, int Level)
/**************************************************************
INPUT: A clause, an Index, a flag store and a splitlevel
indicating the need of a copy if <Clause> is reduced
by a clause of higher split level than <Level>.
RETURNS: TRUE if a unit conflict with <Clause> and the
clauses in <ShIndex> happened.
If the <DocProof> flag is true or the clauses used for
reductions have a higher split level then a changed
copy is returned in <*Changed>.
Otherwise <Clause> is destructively changed.
***************************************************************/
{
CLAUSE PClause,Copy;
LITERAL ActLit,PLit;
LIST Scan;
TERM CandTerm;
BOOL Document;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence) || (*Changed != (CLAUSE)NULL)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ForwardUnitConflict :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
if (clause_Length(Clause) == 1) {
Copy = Clause;
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
ActLit = clause_GetLiteral(Copy, clause_FirstLitIndex());
PLit = (LITERAL)NULL;
CandTerm = st_ExistUnifier(cont_LeftContext(), sharing_Index(ShIndex), cont_RightContext(),
clause_LiteralAtom(ActLit));
while (PLit == (LITERAL)NULL && CandTerm) {
if (!term_IsVariable(CandTerm)) {
Scan = sharing_NAtomDataList(CandTerm); /* CAUTION !!! the List is not a copy */
while (!list_Empty(Scan)) {
PLit = list_Car(Scan);
if (clause_LiteralsAreComplementary(ActLit,PLit) &&
clause_Length(clause_LiteralOwningClause(PLit)) == 1) {
st_CancelExistRetrieval();
Scan = list_Nil();
}
else {
PLit = (LITERAL)NULL;
Scan = list_Cdr(Scan);
}
}
}
if (PLit == (LITERAL)NULL)
CandTerm = st_NextCandidate();
}
if (PLit == (LITERAL)NULL && fol_IsEquality(clause_LiteralAtom(ActLit))) {
TERM Atom;
Atom = term_Create(fol_Equality(),list_Reverse(term_ArgumentList(clause_LiteralAtom(ActLit))));
CandTerm = st_ExistUnifier(cont_LeftContext(), sharing_Index(ShIndex), cont_RightContext(), Atom);
while (PLit == (LITERAL)NULL && CandTerm) {
if (!term_IsVariable(CandTerm)) {
Scan = sharing_NAtomDataList(CandTerm); /* CAUTION !!! the List is not a copy */
while (!list_Empty(Scan)) {
PLit = list_Car(Scan);
if (clause_LiteralsAreComplementary(ActLit,PLit) &&
clause_Length(clause_LiteralOwningClause(PLit)) == 1) {
st_CancelExistRetrieval();
Scan = list_Nil();
}
else {
PLit = (LITERAL)NULL;
Scan = list_Cdr(Scan);
}
}
}
if (PLit == (LITERAL)NULL)
CandTerm = st_NextCandidate();
}
list_Delete(term_ArgumentList(Atom));
term_Free(Atom);
}
if (clause_LiteralExists(PLit)) {
if (flag_GetFlagValue(Flags, flag_PUNC)) {
fputs("\nUnitConflict: ", stdout);
clause_Print(Copy);
}
PClause = clause_LiteralOwningClause(PLit);
if (Copy == Clause &&
(Document || prfs_SplitLevelCondition(clause_SplitLevel(PClause),clause_SplitLevel(Copy),Level)))
Copy = clause_Copy(Clause);
clause_UpdateSplitDataFromPartner(Copy, PClause);
clause_DeleteLiteral(Copy,clause_FirstLitIndex(), Flags, Precedence);
if (Document)
red_DocumentUnitConflict(Copy, list_List((POINTER)clause_FirstLitIndex()),
list_List((POINTER)clause_Number(PClause)),
list_List((POINTER)clause_FirstLitIndex()));
if (flag_GetFlagValue(Flags, flag_PUNC)) {
printf(" ==> [ %d.%d ]", clause_Number(PClause), clause_FirstLitIndex());
clause_Print(Copy);
}
if (Copy != Clause)
*Changed = Copy;
return TRUE;
}
}
return FALSE;
}
static CLAUSE red_ForwardSubsumer(CLAUSE RedCl, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**********************************************************
INPUT: A pointer to a non-empty clause, an index of
clauses, a flag store and a precedence.
RETURNS: A clause that subsumes <RedCl>, or NULL if no such
clause exists.
***********************************************************/
{
TERM Atom,AtomGen;
CLAUSE CandCl;
LITERAL CandLit;
LIST LitScan;
int i, lc, fa, la, fs, ls;
#ifdef CHECK
if (!clause_IsClause(RedCl, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ForwardSubsumer:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedCl, Flags, Precedence);
#endif
lc = clause_LastConstraintLitIndex(RedCl);
fa = clause_FirstAntecedentLitIndex(RedCl);
la = clause_LastAntecedentLitIndex(RedCl);
fs = clause_FirstSuccedentLitIndex(RedCl);
ls = clause_LastSuccedentLitIndex(RedCl);
for (i = 0; i <= ls; i++) {
Atom = clause_GetLiteralAtom(RedCl, i);
AtomGen = st_ExistGen(cont_LeftContext(), sharing_Index(ShIndex), Atom);
while (AtomGen) {
if (!term_IsVariable(AtomGen)) {
for (LitScan = sharing_NAtomDataList(AtomGen);
!list_Empty(LitScan);
LitScan = list_Cdr(LitScan)) {
CandLit = list_Car(LitScan);
CandCl = clause_LiteralOwningClause(CandLit);
if (CandCl != RedCl &&
clause_GetLiteral(CandCl,clause_FirstLitIndex()) == CandLit &&
/* Literals must be from same part of the clause */
((i<=lc && clause_LiteralIsFromConstraint(CandLit)) ||
(i>=fa && i<=la && clause_LiteralIsFromAntecedent(CandLit)) ||
(i>=fs && clause_LiteralIsFromSuccedent(CandLit))) &&
subs_SubsumesBasic(CandCl, RedCl, clause_FirstLitIndex(), i)) {
st_CancelExistRetrieval();
return (CandCl);
}
}
}
AtomGen = st_NextCandidate();
}
if (fol_IsEquality(Atom) &&
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(RedCl,i))) {
Atom = term_Create(fol_Equality(),list_Reverse(term_ArgumentList(Atom)));
AtomGen = st_ExistGen(cont_LeftContext(), sharing_Index(ShIndex), Atom);
while (AtomGen) {
if (!term_IsVariable(AtomGen)) {
for (LitScan = sharing_NAtomDataList(AtomGen);
!list_Empty(LitScan);
LitScan = list_Cdr(LitScan)) {
CandLit = list_Car(LitScan);
CandCl = clause_LiteralOwningClause(CandLit);
if (CandCl != RedCl &&
clause_GetLiteral(CandCl,clause_FirstLitIndex()) == CandLit &&
/* Literals must be from same part of the clause */
((i<=lc && clause_LiteralIsFromConstraint(CandLit)) ||
(i>=fa && i<=la && clause_LiteralIsFromAntecedent(CandLit)) ||
(i>=fs && clause_LiteralIsFromSuccedent(CandLit))) &&
subs_SubsumesBasic(CandCl, RedCl, clause_FirstLitIndex(), i)) {
st_CancelExistRetrieval();
list_Delete(term_ArgumentList(Atom));
term_Free(Atom);
return (CandCl);
}
}
}
AtomGen = st_NextCandidate();
}
list_Delete(term_ArgumentList(Atom));
term_Free(Atom);
}
}
return((CLAUSE)NULL);
}
static CLAUSE red_ForwardSubsumption(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**********************************************************
INPUT: A clause, an index of clauses, a flag store and
a precedence.
RETURNS: The clause <RedClause> is subsumed by in <ShIndex>.
***********************************************************/
{
CLAUSE Subsumer;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ForwardSubsumption:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Subsumer = red_ForwardSubsumer(RedClause, ShIndex, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PSUB) && Subsumer) {
fputs("\nFSubsumption: ", stdout);
clause_Print(RedClause);
printf(" by %d %d ",clause_Number(Subsumer),clause_SplitLevel(Subsumer));
}
return Subsumer;
}
static void red_DocumentRewriting(CLAUSE Clause, int i, CLAUSE Rule, int ri)
/*********************************************************
INPUT: Two clauses and the literal indices involved in the rewrite step.
RETURNS: Nothing.
EFFECT: Documentation in <Clause> is set.
**********************************************************/
{
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause,
list_List((POINTER)clause_Number(Clause)));
/* Has to be done before increasing the number! */
clause_SetParentLiterals(Clause, list_List((POINTER)i));
clause_NewNumber(Clause);
clause_SetFromRewriting(Clause);
clause_AddParentClause(Clause,clause_Number(Rule));
clause_AddParentLiteral(Clause,ri);
}
static void red_DocumentFurtherRewriting(CLAUSE Clause, int i, CLAUSE Rule, int ri)
/*********************************************************
INPUT: Two clauses and the literal indices involved in the rewrite step.
RETURNS: Nothing.
EFFECT: Documentation in <Clause> is set.
**********************************************************/
{
clause_AddParentClause(Clause,
(int) list_Car(list_Cdr(clause_ParentClauses(Clause))));
clause_AddParentLiteral(Clause, i);
clause_AddParentClause(Clause, clause_Number(Rule));
clause_AddParentLiteral(Clause, ri);
}
static BOOL red_RewriteRedUnitClause(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed, int Level)
/**************************************************************
INPUT: A unit (!) clause, an Index, a flag store, a
precedence and a split level indicating the need of
a copy if <Clause> is reduced by a clause of higher
split level than <Level>.
RETURNS: TRUE iff rewriting was possible.
If the <DocProof> flag is true or the split level of
the rewrite rule is higher a copy of RedClause that
is rewritten wrt. the indexed clauses is returned in
<*Changed>.
Otherwise the clause is destructively rewritten.
***************************************************************/
{
TERM RedAtom, RedTermS;
int B_Stack;
BOOL Rewritten, Result, Oriented, Renamed, Document;
TERM TermS,PartnerEq;
LIST EqList,EqScan,LitScan;
CLAUSE Copy;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence) ||
*Changed != (CLAUSE)NULL ||
clause_Length(RedClause) != 1) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_RewriteRedUnitClause :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Result = FALSE;
Renamed = FALSE;
Copy = RedClause;
RedAtom = clause_GetLiteralAtom(Copy, clause_FirstLitIndex());
Rewritten = TRUE;
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
/* Don't apply this rule on constraint or propositional literals */
if (clause_FirstLitIndex() <= clause_LastConstraintLitIndex(RedClause) ||
list_Empty(term_ArgumentList(RedAtom)))
return Result;
if (term_StampOverflow(red_STAMPID))
term_ResetTermStamp(clause_LiteralSignedAtom(clause_GetLiteral(RedClause, clause_FirstLitIndex())));
term_StartStamp();
while (Rewritten) {
Rewritten = FALSE;
B_Stack = stack_Bottom();
sharing_PushListOnStackNoStamps(term_ArgumentList(RedAtom));
while (!stack_Empty(B_Stack)) {
RedTermS = (TERM)stack_PopResult();
TermS = st_ExistGen(cont_LeftContext(), sharing_Index(ShIndex), RedTermS);
while (TermS && !Rewritten) {
EqList = term_SupertermList(TermS);
for (EqScan = EqList; !list_Empty(EqScan) && !Rewritten;
EqScan = list_Cdr(EqScan)) {
PartnerEq = list_Car(EqScan);
if (fol_IsEquality(PartnerEq)) {
CLAUSE RewriteClause;
LITERAL RewriteLit;
TERM Right;
if (TermS == term_FirstArgument(PartnerEq))
Right = term_SecondArgument(PartnerEq);
else
Right = term_FirstArgument(PartnerEq);
for (LitScan = sharing_NAtomDataList(PartnerEq);
!list_Empty(LitScan) && !Rewritten;
LitScan = list_Cdr(LitScan)) {
RewriteLit = list_Car(LitScan);
RewriteClause = clause_LiteralOwningClause(RewriteLit);
if (clause_LiteralIsPositive(RewriteLit) &&
clause_Length(RewriteClause) == 1) {
Oriented = (clause_LiteralIsOrientedEquality(RewriteLit) &&
TermS == term_FirstArgument(PartnerEq));
if (!Oriented && !clause_LiteralIsOrientedEquality(RewriteLit)) {
Renamed = TRUE; /* If oriented, no renaming needed! */
term_StartMaxRenaming(clause_MaxVar(RewriteClause));
term_Rename(RedAtom); /* Renaming destructive, no extra match needed !! */
Oriented = ord_ContGreater(cont_LeftContext(), TermS,
cont_LeftContext(), Right,
Flags, Precedence);
/*if (Oriented) {
fputs("\n\n\tRedAtom: ",stdout);term_PrintPrefix(RedAtom);
fputs("\n\tSubTerm: ",stdout);term_PrintPrefix(RedTermS);
fputs("\n\tGenTerm: ",stdout);term_PrintPrefix(TermS);
fputs("\n\tGenRight: ",stdout);term_PrintPrefix(Right);
putchar('\n');cont_PrintCurrentTrail();putchar('\n');
}*/
}
if (Oriented) {
TERM TermT;
if (RedClause == Copy &&
(Document ||
prfs_SplitLevelCondition(clause_SplitLevel(RewriteClause),
clause_SplitLevel(RedClause),Level))) {
Copy = clause_Copy(RedClause);
RedAtom = clause_GetLiteralAtom(Copy, clause_FirstLitIndex());
}
if (!Result)
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("\nFRewriting: ", stdout);
clause_Print(Copy);
fputs(" ==>[ ", stdout);
}
if (Document) {
if (!Result)
red_DocumentRewriting(Copy, clause_FirstLitIndex(),
RewriteClause, clause_FirstLitIndex());
else
red_DocumentFurtherRewriting(Copy, clause_FirstLitIndex(),
RewriteClause, clause_FirstLitIndex());
}
Result = TRUE;
TermT = cont_ApplyBindingsModuloMatching(cont_LeftContext(), term_Copy(Right), TRUE);
if (cont_BindingsAreRenamingModuloMatching(cont_RightContext()))
term_SetTermSubtermStamp(TermT);
term_ReplaceSubtermBy(RedAtom, RedTermS, TermT);
Rewritten = TRUE;
clause_UpdateSplitDataFromPartner(Copy, RewriteClause);
term_Delete(TermT);
stack_SetBottom(B_Stack);
if (flag_GetFlagValue(Flags, flag_PREW))
printf("%d.%d ",clause_Number(RewriteClause), clause_FirstLitIndex());
clause_UpdateWeight(Copy, Flags);
}
}
}
}
}
if (!Rewritten)
TermS = st_NextCandidate();
}
st_CancelExistRetrieval();
if (!Rewritten)
term_SetTermStamp(RedTermS);
}
}
term_StopStamp();
if (Result) {
clause_OrientAndReInit(Copy, Flags, Precedence);
if (Copy != RedClause)
clause_OrientAndReInit(RedClause, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("] ", stdout);
clause_Print(Copy);
}
if (Copy != RedClause)
*Changed = Copy;
}
else
if (Renamed)
clause_OrientAndReInit(Copy, Flags, Precedence);
#ifdef CHECK
clause_Check(Copy, Flags, Precedence);
clause_Check(RedClause, Flags, Precedence);
#endif
return Result;
}
static BOOL red_RewriteRedClause(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
CLAUSE *Changed, int Level)
/**************************************************************
INPUT: A clause, an Index, a flag store, a precedence and
a split level indicating the need of a copy if
<Clause> is reduced by a clause of higher split
level than <Level>.
RETURNS: NULL, if no rewriting was possible.
If the <DocProof> flag is true or the split level of
the rewrite rule is higher a copy of RedClause
that is rewritten wrt. the indexed clauses.
Otherwise the clause is destructively rewritten and
returned.
***************************************************************/
{
TERM RedAtom, RedTermS;
int B_Stack;
int ci, length;
BOOL Rewritten, Result, Document;
TERM TermS,PartnerEq;
LIST EqScan,LitScan;
CLAUSE Copy;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_RewriteRedClause :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
length = clause_Length(RedClause);
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
if (length == 1)
return red_RewriteRedUnitClause(RedClause, ShIndex, Flags, Precedence,
Changed, Level);
Result = FALSE;
Copy = RedClause;
/* Don't apply this rule on constraint literals! */
for (ci = clause_FirstAntecedentLitIndex(RedClause); ci < length; ci++) {
Rewritten = TRUE;
if (!list_Empty(term_ArgumentList(clause_GetLiteralAtom(Copy, ci)))) {
while (Rewritten) {
Rewritten = FALSE;
RedAtom = clause_GetLiteralAtom(Copy, ci);
B_Stack = stack_Bottom();
/* push subterms on stack except variables */
sharing_PushListReverseOnStack(term_ArgumentList(RedAtom));
while (!stack_Empty(B_Stack)) {
RedTermS = (TERM)stack_PopResult();
TermS = st_ExistGen(cont_LeftContext(), sharing_Index(ShIndex), RedTermS);
while (TermS && !Rewritten) {
/* A variable can't be greater than any other term, */
/* so don't consider any variables here */
if (!term_IsVariable(TermS)) {
EqScan = term_SupertermList(TermS);
for ( ; !list_Empty(EqScan) && !Rewritten;
EqScan = list_Cdr(EqScan)) {
PartnerEq = list_Car(EqScan);
if (fol_IsEquality(PartnerEq) &&
(term_FirstArgument(PartnerEq) == TermS)) {
CLAUSE RewriteClause;
LITERAL RewriteLit;
int ri;
for (LitScan = sharing_NAtomDataList(PartnerEq);
!list_Empty(LitScan) && !Rewritten;
LitScan = list_Cdr(LitScan)) {
RewriteLit = list_Car(LitScan);
RewriteClause = clause_LiteralOwningClause(RewriteLit);
ri = clause_LiteralGetIndex(RewriteLit);
if (clause_LiteralIsPositive(RewriteLit) &&
clause_LiteralIsOrientedEquality(RewriteLit) &&
subs_SubsumesBasic(RewriteClause, Copy, ri, ci)) {
TERM TermT;
if (RedClause == Copy &&
(Document ||
prfs_SplitLevelCondition(clause_SplitLevel(RewriteClause),
clause_SplitLevel(RedClause),Level))) {
Copy = clause_Copy(RedClause);
RedAtom = clause_GetLiteralAtom(Copy, ci);
}
if (!Result) {
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("\nFRewriting: ", stdout);
clause_Print(Copy);
fputs(" ==>[ ", stdout);
}
}
if (Document) {
if (!Result)
red_DocumentRewriting(Copy, ci, RewriteClause, ri);
else
red_DocumentFurtherRewriting(Copy,ci,RewriteClause,ri);
}
Result = TRUE;
/* Since <TermS> is the bigger term of an oriented */
/* equation and all variables in <TermS> are bound, */
/* all variables in the smaller term are bound, too. */
/* So the strict version of cont_Apply... will work. */
TermT = cont_ApplyBindingsModuloMatching(cont_LeftContext(),
term_Copy(term_SecondArgument(PartnerEq)),
TRUE);
/* No variable renaming is necessary before creation */
/* of bindings and replacement of subterms because all */
/* variables of <TermT> are from <RedClause>/<Copy>. */
term_ReplaceSubtermBy(RedAtom, RedTermS, TermT);
Rewritten = TRUE;
clause_UpdateSplitDataFromPartner(Copy,RewriteClause);
term_Delete(TermT);
stack_SetBottom(B_Stack);
if (flag_GetFlagValue(Flags, flag_PREW))
printf("%d.%d ",clause_Number(RewriteClause), ri);
clause_UpdateWeight(Copy, Flags);
}
}
}
}
}
if (!Rewritten)
TermS = st_NextCandidate();
}
st_CancelExistRetrieval();
}
}
}
}
if (Result) {
clause_OrientAndReInit(Copy, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("] ", stdout);
clause_Print(Copy);
}
if (Copy != RedClause) {
clause_OrientAndReInit(RedClause, Flags, Precedence);
*Changed = Copy;
}
}
#ifdef CHECK
clause_Check(Copy, Flags, Precedence);
clause_Check(RedClause, Flags, Precedence);
#endif
return Result;
}
/**************************************************************/
/* FORWARD CONTEXTUAL REWRITING */
/**************************************************************/
static BOOL red_LeftTermOfEquationIsStrictlyMaximalTerm(CLAUSE Clause,
LITERAL Equation,
FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a literal of the clause, that is an
oriented equation, a flag store and a precedence.
RETURNS: TRUE, iff the bigger (i.e. left) term of the equation
is the strictly maximal term of the clause.
A term s is strictly maximal in a clause, iff for every atom
u=v (A=tt) of the clause s > u and s > v (s > A).
***************************************************************/
{
int i, except, last;
TERM LeftTerm, Atom;
LITERAL ActLit;
#ifdef CHECK
if (!clause_LiteralIsOrientedEquality(Equation)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_LeftTermOfEquationIsStrictlyMaximalTerm: ");
misc_ErrorReport("literal is not oriented");
misc_FinishErrorReport();
}
#endif
LeftTerm = term_FirstArgument(clause_LiteralSignedAtom(Equation));
except = clause_LiteralGetIndex(Equation);
/* Compare <LeftTerm> with all terms in the clause */
last = clause_LastLitIndex(Clause);
for (i = clause_FirstLitIndex() ; i <= last; i++) {
if (i != except) {
ActLit = clause_GetLiteral(Clause, i);
Atom = clause_LiteralAtom(ActLit);
if (fol_IsEquality(Atom)) {
/* Atom is an equation */
if (ord_Compare(LeftTerm, term_FirstArgument(Atom), Flags, Precedence)
!= ord_GREATER_THAN ||
(!clause_LiteralIsOrientedEquality(ActLit) &&
ord_Compare(LeftTerm, term_SecondArgument(Atom), Flags, Precedence)
!= ord_GREATER_THAN))
/* Compare only with left (i.e. greater) subterm if the atom is */
/* an oriented equation. */
return FALSE;
} else {
/* Atom is not an equation */
if (ord_Compare(LeftTerm, Atom, Flags, Precedence) != ord_GREATER_THAN)
return FALSE;
}
}
}
return TRUE;
}
static void red_CRwCalculateAdditionalParents(CLAUSE Reduced,
LIST RedundantClauses,
CLAUSE Subsumer,
int OriginalClauseNumber)
/**************************************************************
INPUT: A clause that was just reduced by forward reduction,
a list of intermediate clauses that were derived from
the original clause, a clause that subsumes <Reduced>
(NULL, if <Reduced> is not subsumed), and the clause
number of <Reduced> before it was reduced.
RETURNS: Nothing.
EFFECT: This function collects the information about parent
clauses and parent literals that is necessary for
proof documentation for Contextual Rewriting
and sets the parent information of <Reduced> accordingly.
The clause <Reduced> was derived in several steps
C1 -> C2 -> ... Cn -> <Reduced> from some clause C1.
<RedundantClauses> contains all those clauses C1, ..., Cn.
This function first collects the parent information from
the clauses C1, C2, ..., Cn, <Reduced>. All those clauses
were needed to derive <Reduced>, but for proof documentation
of the rewriting step we have to delete the numbers of
all clauses C1,...,Cn,Reduced.
As a simplification this function doesn't set the
correct parent literals. It simply assumes that every
reduction step was done by literal 0.
This isn't a problem since only the correct parent
clause numbers are really needed for proof documentation.
***************************************************************/
{
LIST Parents, Scan;
int ActNum;
/* First collect all parent clause numbers from the redundant clauses. */
/* Also add number of <Subsumer> if it exists. */
Parents = clause_ParentClauses(Reduced);
clause_SetParentClauses(Reduced, list_Nil());
for (Scan = RedundantClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
Parents = list_Append(clause_ParentClauses(list_Car(Scan)), Parents);
if (Subsumer != NULL)
Parents = list_Cons((POINTER)clause_Number(Subsumer), Parents);
/* Now delete <OriginalClauseNumber> and the numbers of all clauses */
/* that were derived from it. */
Parents = list_PointerDeleteElement(Parents, (POINTER) OriginalClauseNumber);
for (Scan = RedundantClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
ActNum = clause_Number(list_Car(Scan));
Parents = list_PointerDeleteElement(Parents, (POINTER) ActNum);
}
/* Finally set data of result clause <Reduced>. */
Parents = list_PointerDeleteDuplicates(Parents);
clause_SetParentClauses(Reduced, Parents);
/* Build list of literal numbers: in this simple version we just build */
/* a list with the same length as the parent clauses containing only the */
/* literal indices 0. */
Parents = list_Copy(Parents);
for (Scan = Parents; !list_Empty(Scan); Scan = list_Cdr(Scan))
list_Rplaca(Scan, (POINTER)0);
list_Delete(clause_ParentLiterals(Reduced));
clause_SetParentLiterals(Reduced, Parents);
}
static BOOL red_LiteralIsDefinition(LITERAL Literal)
/**************************************************************
INPUT: A literal.
RETURNS: TRUE, iff the literal is a definition, i.e. an equation x=t,
where x is a variable and x doesn't occur in t.
The function needs time O(1), it is independent of the size
of the literal.
CAUTION: The orientation of the literal must be correct.
***************************************************************/
{
TERM Atom;
Atom = clause_LiteralAtom(Literal);
if (fol_IsEquality(Atom) &&
!clause_LiteralIsOrientedEquality(Literal) &&
(term_IsVariable(term_FirstArgument(Atom)) ||
term_IsVariable(term_SecondArgument(Atom))) &&
!term_VariableEqual(term_FirstArgument(Atom),
term_SecondArgument(Atom)))
return TRUE;
else
return FALSE;
}
static BOOL red_PropagateDefinitions(CLAUSE Clause, TERM LeadingTerm,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a term, a flag store and a precedence.
RETURNS: TRUE, iff any definitions in <Clause> where propagated,
false otherwise.
Here, a definitions means a negative literal x=t, where
x is a variable and x doesn't occur in t.
Definitions are only propagated if all terms in the
resulting clause would be smaller than <LeadingTerm>.
The flag store and the precedence are only needed for
term comparisons with respect to the reduction ordering.
CAUTION: <Clause> is changed destructively!
***************************************************************/
{
LITERAL Lit;
TERM Term, Atom;
SYMBOL Var;
int i, last, j, lj;
BOOL success, applied;
LIST litsToRemove;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_PropagateDefinitions: clause is corrupted.");
misc_FinishErrorReport();
}
#endif
applied = FALSE;
litsToRemove = list_Nil(); /* collect indices of redundant literals */
last = clause_LastAntecedentLitIndex(Clause);
for (i = clause_FirstAntecedentLitIndex(Clause); i <= last; i++) {
Lit = clause_GetLiteral(Clause, i);
if (red_LiteralIsDefinition(Lit)) {
/* <Lit> is an equation x=t where the variable x doesn't occur in t. */
Term = term_FirstArgument(clause_LiteralAtom(Lit));
if (term_IsVariable(Term)) {
Var = term_TopSymbol(Term);
Term = term_SecondArgument(clause_LiteralAtom(Lit));
} else {
Var = term_TopSymbol(term_SecondArgument(clause_LiteralAtom(Lit)));
}
/* Establish variable binding x -> t in context */
#ifdef CHECK
cont_SaveState();
#endif
cont_StartBinding();
cont_CreateBinding(cont_LeftContext(), Var, cont_InstanceContext(), Term);
/* Check that for each literal u=v (A=tt) the conditions */
/* u{x->t} < LeadingTerm and v{x->t} < LeadingTerm (A < LeadingTerm) */
/* hold. */
success = TRUE;
Lit = NULL;
lj = clause_LastLitIndex(Clause);
for (j = clause_FirstLitIndex(); j <= lj && success; j++) {
if (j != i) {
success = FALSE;
Lit = clause_GetLiteral(Clause, j);
Atom = clause_LiteralAtom(Lit);
if (fol_IsEquality(Atom)) {
/* Atom is an equation */
if (ord_ContGreater(cont_InstanceContext(), LeadingTerm,
cont_LeftContext(), term_FirstArgument(Atom),
Flags, Precedence) &&
(clause_LiteralIsOrientedEquality(Lit) ||
ord_ContGreater(cont_InstanceContext(), LeadingTerm,
cont_LeftContext(), term_SecondArgument(Atom),
Flags, Precedence)))
/* Compare only with left (i.e. greater) subterm if the atom is */
/* an oriented equation. */
success = TRUE;
} else {
/* Atom is not an equation */
if (ord_ContGreater(cont_InstanceContext(), LeadingTerm,
cont_LeftContext(), Atom, Flags, Precedence))
success = TRUE;
}
}
}
cont_BackTrack();
#ifdef CHECK
cont_CheckState();
#endif
if (success) {
/* Replace variable <Var> in <Clause> by <Term> */
clause_ReplaceVariable(Clause, Var, Term);
/* The clause literals aren't reoriented here. For the detection of */
/* definitions it suffices to know the non-oriented literals in the */
/* original clause. */
litsToRemove = list_Cons((POINTER)i, litsToRemove);
applied = TRUE;
}
}
}
if (applied) {
/* Now remove the definition literals. */
clause_DeleteLiterals(Clause, litsToRemove, Flags, Precedence);
list_Delete(litsToRemove);
/* Equations have to be reoriented. */
clause_OrientEqualities(Clause, Flags, Precedence);
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_PropagateDefinitions: clause is corrupted ");
misc_ErrorReport("after propagation of definitions");
misc_FinishErrorReport();
}
#endif
}
return applied;
}
static CLAUSE red_CRwLitTautologyCheck(PROOFSEARCH Search, CLAUSE RedClause,
int Except, CLAUSE RuleClause, int i,
TERM LeadingTerm, NAT Mode)
/**************************************************************
INPUT: A proof search object, two clauses, two literal indices
(one per clause), a mode defining the clause index used
for intermediate reductions.
RETURNS: NULL, if the tautology check for literal <i> in <RuleClause>
failed.
If the test succeeds an auxiliary clause is returned that
contains part of the splitting information for the current
rewriting step. If the 'DocProof' flag is set, the necessary
parent information is set, too.
MEMORY: Remember to delete the returned clause!
***************************************************************/
{
FLAGSTORE Flags;
PRECEDENCE Precedence;
CLAUSE aux, NewClause;
LITERAL Lit;
TERM Atom;
BOOL DocProof, Negative, Redundant;
LIST NegLits, PosLits, RedundantList;
int OrigNum;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
DocProof = flag_GetFlagValue(Flags, flag_DOCPROOF);
Lit = clause_GetLiteral(RuleClause, i);
Atom = clause_LiteralAtom(Lit);
Negative = clause_LiteralIsNegative(Lit);
#ifdef CRW_DEBUG
printf("\n ----------\n ");
if (Negative)
printf((i <= clause_LastConstraintLitIndex(RuleClause)) ? "Cons" : "Ante");
else
printf("Succ");
printf(" aux = ");
#endif
if (i <= clause_LastConstraintLitIndex(RuleClause)) {
/* Apply Sort Simplification for constraint literals only */
NegLits = list_List(term_Copy(Atom));
aux = clause_Create(NegLits, list_Nil(), list_Nil(), Flags, Precedence);
clause_SetTemporary(aux);
list_Delete(NegLits);
#ifdef CRW_DEBUG
clause_Print(aux);
#endif
NewClause = NULL;
OrigNum = clause_Number(aux);
if (red_SortSimplification(prfs_DynamicSortTheory(Search), aux, NAT_MAX,
DocProof, Flags, Precedence, &NewClause)) {
/* Sort Simplification was possible, so the unit clause was reduced */
/* to the empty clause. */
/* The splitting information is already set in <aux> or <NewClause>. */
if (DocProof)
/* If 'DocProof' is turned on, a copy was created and assigned */
/* to <NewClause>. */
red_CRwCalculateAdditionalParents(NewClause, list_Nil(), NULL, OrigNum);
if (NewClause != NULL) {
clause_Delete(aux);
return NewClause;
} else
return aux;
}
clause_Delete(aux);
#ifdef CRW_DEBUG
printf("\n Cons aux2 = ");
#endif
}
/* Collect literals for tautology test */
if (Negative) {
if (i <= clause_LastConstraintLitIndex(RuleClause))
NegLits = clause_CopyConstraint(RedClause);
else
NegLits = clause_CopyAntecedentExcept(RedClause, Except);
PosLits = list_List(term_Copy(Atom));
} else {
NegLits = list_List(term_Copy(Atom));
PosLits = clause_CopySuccedentExcept(RedClause, Except);
}
/* Create clause for tautology test */
aux = clause_Create(list_Nil(), NegLits, PosLits, Flags, Precedence);
clause_SetTemporary(aux);
list_Delete(NegLits);
list_Delete(PosLits);
#ifdef CRW_DEBUG
clause_Print(aux);
#endif
/* Apply special reduction. Propagate definitions x=t if for all literals */
/* u=v (A=tt) of the resulting clause the conditions holds: */
/* LeadingTerm > u{x->t} and LeadingTerm > v{x->t} (LeadingTerm > A{x->t}. */
if (red_PropagateDefinitions(aux, LeadingTerm, Flags, Precedence)) {
#ifdef CRW_DEBUG
printf("\n After propagation of definitions:\n aux = ");
clause_Print(aux);
#endif
}
/* Invoke forward reduction and tautology test */
NewClause = NULL;
RedundantList = list_Nil();
OrigNum = clause_Number(aux);
Redundant = red_SelectedStaticReductions(Search, &aux, &NewClause,
&RedundantList, Mode);
clause_SetTemporary(aux);
/* <aux> was possibly changed by some reductions, so mark it as */
/* temporary again. */
/* Invoke tautology test if <aux> isn't redundant. */
if (Redundant || (!clause_IsEmptyClause(aux) && cc_Tautology(aux))) {
if (NewClause != NULL)
/* <aux> is subsumed by <NewClause> */
clause_UpdateSplitDataFromPartner(aux, NewClause);
if (DocProof)
red_CRwCalculateAdditionalParents(aux, RedundantList, NewClause, OrigNum);
} else {
/* test failed */
clause_Delete(aux);
aux = NULL;
}
#ifdef CRW_DEBUG
if (aux != NULL) {
if (NewClause != NULL) {
printf("\n Subsumer = ");
clause_Print(NewClause);
}
if (!list_Empty(RedundantList)) {
printf("\n RedundantList: ");
clause_ListPrint(RedundantList);
}
printf("\n aux reduced = ");
clause_Print(aux);
}
printf("\n ----------");
#endif
/* Delete list of redundant clauses */
clause_DeleteClauseList(RedundantList);
return aux;
}
static BOOL red_CRwTautologyCheck(PROOFSEARCH Search, CLAUSE RedClause, int i,
TERM TermSInstance, CLAUSE RuleClause,
int j, NAT Mode, CLAUSE *Result)
/**************************************************************
INPUT: A proof search object, two clauses, two literal indices
(one per clause), <TermSInstance> is a subterm of
literal <i> in <RedClause>, a mode defining the clause
index used for intermediate reductions, and a pointer
to a clause used as return value.
RETURNS: FALSE, if the clauses failed some tautology test or
the literal <i> in <RedClause> is not greater than literal
<j> in <RedClause> with the substitution <sigma> applied.
In this case <Result> is set to NULL.
TRUE is returned if the clauses passed all tautology tests
and literal <i> in <RedClause> is greater than literal <j>
in <RuleClause> with the substitution <sigma> applied.
In some cases <Result> is set to some auxiliary clause.
This is done if some clauses from the index were used to
reduce the intermediate clauses before the tautology test.
The auxiliary clause is used to return the necessary splitting
information for the current rewriting step.
If the <DocProof> flag is true, the information about
parent clauses is set in <Result>, too.
MEMORY: Remember to delete the <Result> clause if it is not NULL.
***************************************************************/
{
FLAGSTORE Flags, BackupFlags;
PRECEDENCE Precedence;
CLAUSE RuleCopy, aux;
TERM TermS;
int last, h;
BOOL Rewrite;
#ifdef CHECK
if (!clause_LiteralIsOrientedEquality(clause_GetLiteral(RuleClause, j))) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_CRwTautologyCheck:");
misc_ErrorReport(" literal %d in <RuleClause> %d", j,
clause_Number(RuleClause));
misc_ErrorReport(" isn't an oriented equation");
misc_FinishErrorReport();
}
#endif
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
*Result = NULL;
/* copy <RuleClause> and rename variables in copy */
RuleCopy = clause_Copy(RuleClause);
clause_RenameVarsBiggerThan(RuleCopy, clause_MaxVar(RedClause));
TermS = term_FirstArgument(clause_GetLiteralAtom(RuleCopy, j));
/* Remove parent information of copied clause and mark it as temporary */
list_Delete(clause_ParentClauses(RuleCopy));
clause_SetParentClauses(RuleCopy, list_Nil());
list_Delete(clause_ParentLiterals(RuleCopy));
clause_SetParentLiterals(RuleCopy, list_Nil());
clause_SetTemporary(RuleCopy);
/* establish bindings */
cont_StartBinding();
if (!unify_MatchBindings(cont_LeftContext(), TermS, TermSInstance)) {
#ifdef CHECK
misc_StartErrorReport();
misc_ErrorReport("\n In red_CRwTautologyCheck: terms aren't matchable");
misc_FinishErrorReport();
#endif
}
/* Apply bindings to equation s=t, where s > t. Here the strict version */
/* of cont_Apply... can be applied, because all variables in s and t */
/* are bound. */
cont_ApplyBindingsModuloMatching(cont_LeftContext(),
clause_GetLiteralAtom(RuleCopy, j),
TRUE);
/* Check whether E > (s=t)sigma. It suffices to check only positive */
/* equations. All other cases imply the condition. */
if (i >= clause_FirstSuccedentLitIndex(RedClause) &&
clause_LiteralIsEquality(clause_GetLiteral(RedClause, i)) &&
ord_LiteralCompare(clause_GetLiteralTerm(RedClause, i),
clause_LiteralIsOrientedEquality(clause_GetLiteral(RedClause, i)),
clause_GetLiteralTerm(RuleCopy, j), TRUE,
FALSE, Flags, Precedence) != ord_GREATER_THAN) {
cont_BackTrack();
clause_Delete(RuleCopy);
return FALSE;
}
/* if (subs_SubsumesBasic(RuleClause, RedClause, j, i)) { Potential improvement, not completely
cont_BackTrack(); developed ....
return TRUE;
} else */
{
int OldClauseCounter;
/* Apply bindings to the rest of <RuleCopy> */
last = clause_LastLitIndex(RuleCopy);
for (h = clause_FirstLitIndex(); h <= last; h++) {
if (h != j)
cont_ApplyBindingsModuloMatching(cont_LeftContext(),
clause_GetLiteralAtom(RuleCopy, h),
FALSE);
}
/* Backtrack bindings before reduction rules are invoked */
cont_BackTrack();
/* Create new flag store and save current settings. Must be improved **** */
/* Then turn off flags for printing and contextual rewriting. */
/* IMPORTANT: the DocProof flag mustn't be changed! */
BackupFlags = flag_CreateStore();
flag_TransferAllFlags(Flags, BackupFlags);
#ifndef CRW_DEBUG
flag_ClearPrinting(Flags);
#else
{ /* HACK: turn on all printing flags for debugging */
FLAG_ID f;
for (f = (FLAG_ID) 0; f < flag_MAXFLAG; f++) {
if (flag_IsPrinting(f))
flag_SetFlagValue(Flags, f, flag_ON);
}
}
#endif
/* ATTENTION: to apply CRw recursively, uncomment the following */
/* line and comment out the following two lines! */
/* flag_SetFlagValue(Flags, flag_RFCRW, flag_RFCRWON); */
flag_SetFlagValue(Flags, flag_RBCRW, flag_RBCRWOFF);
flag_SetFlagValue(Flags, flag_RFCRW, flag_RFCRWOFF);
/* Examine all literals of <RuleCopy> except <j> */
Rewrite = TRUE;
last = clause_LastLitIndex(RuleCopy);
OldClauseCounter = clause_Counter();
for (h = clause_FirstLitIndex(); Rewrite && h <= last; h++) {
if (h != j) {
aux = red_CRwLitTautologyCheck(Search, RedClause, i, RuleCopy, h,
TermSInstance, Mode);
if (aux == NULL)
Rewrite = FALSE;
else {
/* Store splitting data of <aux> in RuleCopy */
clause_UpdateSplitDataFromPartner(RuleCopy, aux);
/* Collect additonal parent information, if <DocProof> is turned on */
if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
clause_SetParentClauses(RuleCopy,
list_Nconc(clause_ParentClauses(aux),
clause_ParentClauses(RuleCopy)));
clause_SetParentLiterals(RuleCopy,
list_Nconc(clause_ParentLiterals(aux),
clause_ParentLiterals(RuleCopy)));
clause_SetParentClauses(aux, list_Nil());
clause_SetParentLiterals(aux, list_Nil());
}
clause_Delete(aux);
}
}
}
/* restore clause counter */
clause_SetCounter(OldClauseCounter);
/* reset flag store of proof search object and free backup store */
flag_TransferAllFlags(BackupFlags, Flags);
flag_DeleteStore(BackupFlags);
}
if (Rewrite)
*Result = RuleCopy;
else
/* cleanup */
clause_Delete(RuleCopy);
return Rewrite;
}
static void red_DocumentContextualRewriting(CLAUSE Clause, int i,
CLAUSE RuleClause, int ri,
LIST AdditionalPClauses,
LIST AdditionalPLits)
/**************************************************************
INPUT: Two clauses and two literal indices (one per clause),
and two lists of additional parent clause numbers and
parent literals.
RETURNS: Nothing.
EFFECT: <Clause> is rewritten for the first time by
Contextual Rewriting. This function sets the parent
clause and parent literal information in <Clause>.
<Clause> gets a new clause number.
CAUTION: The lists are not copied!
***************************************************************/
{
#ifdef CHECK
if (list_Length(AdditionalPClauses) != list_Length(AdditionalPLits)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_DocumentContextualRewriting: lists of parent ");
misc_ErrorReport("clauses\n and literals have different length.");
misc_FinishErrorReport();
}
#endif
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
clause_SetParentClauses(Clause, AdditionalPClauses);
clause_SetParentLiterals(Clause, AdditionalPLits);
/* Add the old number of <Clause> as parent clause, */
/* before it gets a new clause number. */
clause_AddParentClause(Clause, clause_Number(Clause));
clause_AddParentLiteral(Clause, i);
clause_AddParentClause(Clause, clause_Number(RuleClause));
clause_AddParentLiteral(Clause, ri);
clause_NewNumber(Clause);
clause_SetFromContextualRewriting(Clause);
}
static void red_DocumentFurtherCRw(CLAUSE Clause, int i, CLAUSE RuleClause,
int ri, LIST AdditionalPClauses,
LIST AdditionalPLits)
/**************************************************************
INPUT: Two clauses, two literal indices (one per clause),
and two lists of additional parent clause numbers and
parent literal indices.
RETURNS: Nothing.
EFFECT: <Clause> is a clause, that was rewritten before by
Contextual Rewriting. This function adds the parent
clause and parent literal information from one more
rewriting step to <Clause>. The information is added
to the front of the respective lists.
CAUTION: The lists are not copied!
***************************************************************/
{
int PClauseNum;
#ifdef CHECK
if (list_Length(AdditionalPClauses) != list_Length(AdditionalPLits)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_DocumentFurtherCRw: lists of parent ");
misc_ErrorReport("clauses\n and literals have different length.");
misc_FinishErrorReport();
}
#endif
PClauseNum = (int)list_Second(clause_ParentClauses(Clause));
clause_SetParentClauses(Clause, list_Nconc(AdditionalPClauses,
clause_ParentClauses(Clause)));
clause_SetParentLiterals(Clause, list_Nconc(AdditionalPLits,
clause_ParentLiterals(Clause)));
clause_AddParentClause(Clause, PClauseNum);
clause_AddParentLiteral(Clause, i);
clause_AddParentClause(Clause, clause_Number(RuleClause));
clause_AddParentLiteral(Clause, ri);
}
static BOOL red_ContextualRewriting(PROOFSEARCH Search, CLAUSE RedClause,
NAT Mode, int Level, CLAUSE *Changed)
/**************************************************************
INPUT: A proof search object, a clause to reduce, the
reduction mode which defines the clause set used for
reduction, a split level indicating the need of a copy
if <Clause> is reduced by a clause of higher split level
than <Level>, and a pointer to a clause used as return value.
RETURNS: TRUE, if contextual rewriting was possible, FALSE otherwise.
If rewriting was possible and the <DocProof> flag is true
or the split level of the rewrite rule is higher than
<Level>, a copy of <RedClause> that is rewritten wrt.
the indexed clauses is returned in <*Changed>.
Otherwise the clause is destructively rewritten and
returned.
CAUTION: If rewriting wasn't applied, the value of <*Changed>
isn't set explicitely in this function.
***************************************************************/
{
TERM RedAtom, RedTermS;
int B_Stack;
int ri, last;
BOOL Rewritten, Result, Document;
TERM TermS, PartnerEq;
LIST Gen, EqScan, LitScan;
CLAUSE Copy;
FLAGSTORE Flags;
PRECEDENCE Precedence;
SHARED_INDEX ShIndex;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ContextualRewriting: Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
/* Select clause index */
if (red_WorkedOffMode(Mode))
ShIndex = prfs_WorkedOffSharingIndex(Search);
else
ShIndex = prfs_UsableSharingIndex(Search);
last = clause_LastSuccedentLitIndex(RedClause);
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
Result = FALSE;
Copy = RedClause;
/* Don't apply this rule on constraint literals! */
for (ri = clause_FirstAntecedentLitIndex(RedClause); ri <= last; ri++) {
if (!list_Empty(term_ArgumentList(clause_GetLiteralAtom(Copy, ri)))) {
Rewritten = TRUE;
while (Rewritten) {
Rewritten = FALSE;
RedAtom = clause_GetLiteralAtom(Copy, ri);
B_Stack = stack_Bottom();
/* push subterms on stack except variables */
sharing_PushListReverseOnStack(term_ArgumentList(RedAtom));
while (!stack_Empty(B_Stack)) {
RedTermS = (TERM)stack_PopResult();
Gen = st_GetGen(cont_LeftContext(), sharing_Index(ShIndex), RedTermS);
for ( ; !list_Empty(Gen) && !Rewritten; Gen = list_Pop(Gen)) {
TermS = list_Car(Gen);
/* A variable can't be greater than any other term, */
/* so don't consider any variables here. */
if (!term_IsVariable(TermS)) {
EqScan = term_SupertermList(TermS);
for ( ; !list_Empty(EqScan) && !Rewritten;
EqScan = list_Cdr(EqScan)) {
PartnerEq = list_Car(EqScan);
if (fol_IsEquality(PartnerEq) &&
(term_FirstArgument(PartnerEq) == TermS)) {
CLAUSE RuleClause, HelpClause;
LITERAL RuleLit;
int i;
for (LitScan = sharing_NAtomDataList(PartnerEq);
!list_Empty(LitScan) && !Rewritten;
LitScan = list_Cdr(LitScan)) {
RuleLit = list_Car(LitScan);
RuleClause = clause_LiteralOwningClause(RuleLit);
i = clause_LiteralGetIndex(RuleLit);
HelpClause = NULL;
#ifdef CRW_DEBUG
if (clause_LiteralIsPositive(RuleLit) &&
clause_LiteralGetFlag(RuleLit,STRICTMAXIMAL) &&
clause_LiteralIsOrientedEquality(RuleLit) &&
red_LeftTermOfEquationIsStrictlyMaximalTerm(RuleClause,
RuleLit,
Flags,
Precedence)) {
printf("\n------\nFCRw: %s\n%d ", red_WorkedOffMode(Mode)
? "WorkedOff" : "Usable", i);
clause_Print(RuleClause);
printf("\n%d ", ri);
clause_Print(RedClause);
}
#endif
if (clause_LiteralIsPositive(RuleLit) &&
clause_LiteralGetFlag(RuleLit,STRICTMAXIMAL) &&
clause_LiteralIsOrientedEquality(RuleLit) &&
red_LeftTermOfEquationIsStrictlyMaximalTerm(RuleClause,
RuleLit,
Flags,
Precedence) &&
red_CRwTautologyCheck(Search, Copy, ri, RedTermS,
RuleClause, i, Mode,
&HelpClause)) {
TERM TermT;
if (RedClause == Copy &&
(Document ||
prfs_SplitLevelCondition(clause_SplitLevel(RuleClause),
clause_SplitLevel(RedClause),Level) ||
prfs_SplitLevelCondition(clause_SplitLevel(HelpClause),
clause_SplitLevel(RedClause),
Level))) {
Copy = clause_Copy(RedClause);
RedAtom = clause_GetLiteralAtom(Copy, ri);
}
if (!Result && flag_GetFlagValue(Flags, flag_PCRW)) {
/* Clause is rewitten for the first time and */
/* printing is turned on. */
fputs("\nFContRewriting: ", stdout);
clause_Print(Copy);
fputs(" ==>[ ", stdout);
}
if (Document) {
LIST PClauses, PLits;
/* Get additional parent information from */
/* <HelpClause> */
PClauses = PLits = list_Nil();
if (HelpClause != NULL) {
PClauses = clause_ParentClauses(HelpClause);
PLits = clause_ParentLiterals(HelpClause);
clause_SetParentClauses(HelpClause, list_Nil());
clause_SetParentLiterals(HelpClause, list_Nil());
} else
PClauses = PLits = list_Nil();
if (!Result)
red_DocumentContextualRewriting(Copy, ri,
RuleClause, i,
PClauses, PLits);
else
red_DocumentFurtherCRw(Copy, ri, RuleClause, i,
PClauses, PLits);
}
Result = TRUE;
cont_StartBinding();
unify_MatchBindings(cont_LeftContext(), TermS, RedTermS);
TermT = cont_ApplyBindingsModuloMatching(cont_LeftContext(),
term_Copy(term_SecondArgument(PartnerEq)),
TRUE);
cont_BackTrack();
term_ReplaceSubtermBy(RedAtom, RedTermS, TermT);
Rewritten = TRUE;
/* Set splitting data from parents */
clause_UpdateSplitDataFromPartner(Copy, RuleClause);
if (HelpClause != NULL) {
/* Store splitting data from intermediate clauses */
clause_UpdateSplitDataFromPartner(Copy, HelpClause);
clause_Delete(HelpClause);
}
term_Delete(TermT);
stack_SetBottom(B_Stack);
if (flag_GetFlagValue(Flags, flag_PCRW))
printf("%d.%d ",clause_Number(RuleClause), i);
clause_UpdateWeight(Copy, Flags);
}
}
}
}
}
}
list_Delete(Gen);
}
}
}
}
if (Result) {
clause_OrientAndReInit(Copy, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PCRW)) {
fputs("] ", stdout);
clause_Print(Copy);
}
if (Copy != RedClause) {
clause_OrientAndReInit(RedClause, Flags, Precedence);
*Changed = Copy;
}
}
#ifdef CHECK
if (Copy != RedClause)
clause_Check(Copy, Flags, Precedence);
clause_Check(RedClause, Flags, Precedence);
#endif
return Result;
}
static LIST red_BackSubsumption(CLAUSE RedCl, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**********************************************************
INPUT: A pointer to a non-empty clause, an index of
clauses, a flag store and a precedence.
RETURNS: The list of clauses that are subsumed by the
clause RedCl.
***********************************************************/
{
TERM Atom,CandTerm;
CLAUSE SubsumedCl;
LITERAL CandLit;
LIST CandLits, Scan, SubsumedList;
int i, j, lc, fa, la, fs, l;
#ifdef CHECK
if (!clause_IsClause(RedCl, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackSubsumption :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedCl, Flags, Precedence);
#endif
/* Special case: clause is empty */
if (clause_IsEmptyClause(RedCl))
return list_Nil();
SubsumedList = list_Nil();
lc = clause_LastConstraintLitIndex(RedCl);
fa = clause_FirstAntecedentLitIndex(RedCl);
la = clause_LastAntecedentLitIndex(RedCl);
fs = clause_FirstSuccedentLitIndex(RedCl);
l = clause_LastLitIndex(RedCl);
/* Choose the literal with the greatest weight to start the search */
i = clause_FirstLitIndex();
for (j = i + 1; j <= l; j++) {
if (clause_LiteralWeight(clause_GetLiteral(RedCl, j)) >
clause_LiteralWeight(clause_GetLiteral(RedCl, i)))
i = j;
}
Atom = clause_GetLiteralAtom(RedCl, i);
CandTerm = st_ExistInstance(cont_LeftContext(), sharing_Index(ShIndex), Atom);
while (CandTerm) {
CandLits = sharing_NAtomDataList(CandTerm);
for (Scan = CandLits; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
CandLit = list_Car(Scan);
SubsumedCl = clause_LiteralOwningClause(CandLit);
j = clause_LiteralGetIndex(CandLit);
if (RedCl != SubsumedCl &&
/* Literals must be from same part of the clause */
((i<=lc && clause_LiteralIsFromConstraint(CandLit)) ||
(i>=fa && i<=la && clause_LiteralIsFromAntecedent(CandLit)) ||
(i>=fs && clause_LiteralIsFromSuccedent(CandLit))) &&
!list_PointerMember(SubsumedList, SubsumedCl) &&
subs_SubsumesBasic(RedCl, SubsumedCl, i, j))
SubsumedList = list_Cons(SubsumedCl, SubsumedList);
}
CandTerm = st_NextCandidate();
}
if (fol_IsEquality(Atom) &&
clause_LiteralIsNotOrientedEquality(clause_GetLiteral(RedCl, i))) {
Atom = term_Create(fol_Equality(),
list_Reverse(term_ArgumentList(Atom)));
CandTerm = st_ExistInstance(cont_LeftContext(), sharing_Index(ShIndex), Atom);
while (CandTerm) {
CandLits = sharing_NAtomDataList(CandTerm);
for (Scan = CandLits; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
CandLit = list_Car(Scan);
SubsumedCl = clause_LiteralOwningClause(list_Car(Scan));
/* if (!clause_GetFlag(SubsumedCl, BLOCKED)) { */
j = clause_LiteralGetIndex(list_Car(Scan));
if ((RedCl != SubsumedCl) &&
/* Literals must be from same part of the clause */
((i<=lc && clause_LiteralIsFromConstraint(CandLit)) ||
(i>=fa && i<=la && clause_LiteralIsFromAntecedent(CandLit)) ||
(i>=fs && clause_LiteralIsFromSuccedent(CandLit))) &&
!list_PointerMember(SubsumedList, SubsumedCl) &&
subs_SubsumesBasic(RedCl, SubsumedCl, i, j))
SubsumedList = list_Cons(SubsumedCl, SubsumedList);
/* } */
}
CandTerm = st_NextCandidate();
}
list_Delete(term_ArgumentList(Atom));
term_Free(Atom);
}
if (flag_GetFlagValue(Flags, flag_PSUB)) {
for (Scan = SubsumedList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
SubsumedCl = list_Car(Scan);
fputs("\nBSubsumption: ", stdout);
clause_Print(SubsumedCl);
printf(" by %d ",clause_Number(RedCl));
}
}
return SubsumedList;
}
static LIST red_GetBackMRResLits(CLAUSE Clause, LITERAL ActLit, SHARED_INDEX ShIndex)
/**************************************************************
INPUT: A clause, one of its literals and an Index.
RETURNS: A list of clauses with a complementary literal instance
that are subsumed if these literals are ignored.
the empty list if no such clause exists.
MEMORY: Allocates the needed listnodes.
***************************************************************/
{
CLAUSE PClause;
LITERAL PLit;
LIST LitScan, PClLits;
TERM CandTerm;
int i;
PClLits = list_Nil();
i = clause_LiteralGetIndex(ActLit);
CandTerm = st_ExistInstance(cont_LeftContext(),
sharing_Index(ShIndex),
clause_LiteralAtom(ActLit));
while (CandTerm) {
LitScan = sharing_NAtomDataList(CandTerm); /* CAUTION ! */
for ( ; !list_Empty(LitScan); LitScan = list_Cdr(LitScan)) {
PLit = list_Car(LitScan);
PClause = clause_LiteralOwningClause(PLit);
if (PClause != Clause &&
clause_LiteralsAreComplementary(ActLit,PLit) &&
subs_SubsumesBasic(Clause,PClause,i,clause_LiteralGetIndex(PLit)))
PClLits = list_Cons(PLit, PClLits);
}
CandTerm = st_NextCandidate();
}
return PClLits;
}
static LIST red_BackMatchingReplacementResolution(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
LIST* Result)
/**************************************************************
INPUT: A clause, a shared index, a flag store, a
precedence, and a pointer to a result list.
RETURNS: The return value itself contains a list of clauses
from <ShIndex> that is reducible by <RedClause> via
clause reduction.
The return value stored in <*Result> contains the
result of this operation.
If the <DocProof> flag is true then the clauses in
<*Result> contain information about the reduction.
***************************************************************/
{
LIST Blocked;
CLAUSE Copy;
BOOL Document;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackMatchingReplacementResolution:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Blocked = list_Nil();
Document = flag_GetFlagValue(Flags, flag_DOCPROOF);
if (clause_Length(RedClause) == 1) {
LITERAL ActLit, PLit;
LIST LitList, Scan, Iter;
TERM CandTerm;
int RedClNum;
ActLit = clause_GetLiteral(RedClause, clause_FirstLitIndex());
if (!fol_IsEquality(clause_LiteralAtom(ActLit)) || /* Reduce with negative equations too */
clause_LiteralIsNegative(ActLit)) {
CLAUSE PClause;
LIST PIndL;
CandTerm = st_ExistInstance(cont_LeftContext(), sharing_Index(ShIndex), clause_LiteralAtom(ActLit));
RedClNum = clause_Number(RedClause);
LitList = list_Nil();
while (CandTerm) {
for (Iter = sharing_NAtomDataList(CandTerm); !list_Empty(Iter); Iter = list_Cdr(Iter))
if (clause_LiteralsAreComplementary(ActLit,list_Car(Iter)))
LitList = list_Cons(list_Car(Iter),LitList);
CandTerm = st_NextCandidate();
}
/* It is important to get all literals first,
because there may be several literals in the same clause which can be reduced by <ActLit> */
while (!list_Empty(LitList)) {
PLit = list_Car(LitList);
PIndL = list_List(PLit);
PClause = clause_LiteralOwningClause(PLit);
Blocked = list_Cons(PClause, Blocked);
if (flag_GetFlagValue(Flags, flag_PMRR)) {
fputs("\nBMatchingReplacementResolution: ", stdout);
clause_Print(PClause);
printf(" ==>[ %d.%d ] ",clause_Number(RedClause),clause_FirstLitIndex());
}
Iter = LitList;
for (Scan=list_Cdr(LitList);!list_Empty(Scan);Scan=list_Cdr(Scan)) /* Get brothers of PLit */
if (PClause == clause_LiteralOwningClause(list_Car(Scan))) {
list_Rplacd(Iter,list_Cdr(Scan));
list_Rplacd(Scan,PIndL);
PIndL = Scan;
Scan = Iter;
}
else
Iter = Scan;
Iter = LitList;
LitList = list_Cdr(LitList);
list_Free(Iter);
Copy = clause_Copy(PClause);
clause_RemoveFlag(Copy,WORKEDOFF);
clause_UpdateSplitDataFromPartner(Copy, RedClause);
for(Scan=PIndL;!list_Empty(Scan);Scan=list_Cdr(Scan)) /* Change lits to indexes */
list_Rplaca(Scan,(POINTER)clause_LiteralGetIndex(list_Car(Scan)));
clause_DeleteLiterals(Copy, PIndL, Flags, Precedence);
if (Document)
/* Lists are consumed */
red_DocumentMatchingReplacementResolution(Copy, PIndL, list_List((POINTER)RedClNum),
list_List((POINTER)clause_FirstLitIndex()));
else
list_Delete(PIndL);
if (flag_GetFlagValue(Flags, flag_PMRR))
clause_Print(Copy);
*Result = list_Cons(Copy, *Result);
}
}
return Blocked;
}
else {
CLAUSE PClause;
LITERAL ActLit, PLit;
LIST LitScan,LitList;
int i,length,RedClNum,PInd;
RedClNum = clause_Number(RedClause);
length = clause_Length(RedClause);
for (i = clause_FirstLitIndex(); i < length; i++) {
ActLit = clause_GetLiteral(RedClause, i);
if (!fol_IsEquality(clause_LiteralAtom(ActLit))) {
LitList = red_GetBackMRResLits(RedClause, ActLit, ShIndex);
for (LitScan = LitList;!list_Empty(LitScan);LitScan = list_Cdr(LitScan)) {
PLit = list_Car(LitScan);
PClause = clause_LiteralOwningClause(PLit);
PInd = clause_LiteralGetIndex(PLit);
Copy = clause_Copy(PClause);
if (list_PointerMember(Blocked,PClause)) {
if (!flag_GetFlagValue(Flags, flag_DOCPROOF))
clause_NewNumber(Copy);
}
else
Blocked = list_Cons(PClause, Blocked);
clause_RemoveFlag(Copy,WORKEDOFF);
clause_UpdateSplitDataFromPartner(Copy, RedClause);
clause_DeleteLiteral(Copy, PInd, Flags, Precedence);
if (Document)
red_DocumentMatchingReplacementResolution(Copy, list_List((POINTER)PInd),
list_List((POINTER)RedClNum),
list_List((POINTER)i));
if (flag_GetFlagValue(Flags, flag_PMRR)) {
fputs("\nBMatchingReplacementResolution: ", stdout);
clause_Print(PClause);
printf(" ==>[ %d.%d ] ",clause_Number(RedClause),i);
clause_Print(Copy);
}
*Result = list_Cons(Copy, *Result);
}
list_Delete(LitList);
}
}
return Blocked;
}
}
static void red_ApplyRewriting(CLAUSE RuleCl, int ri, CLAUSE PartnerClause,
int pli, TERM PartnerTermS, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause to use for rewriting, the index of a
positive equality literal where the first equality
argument is greater, a clause, the index of a
literal with subterm <PartnerTermS> that can be
rewritten, a flag store and a precedence.
RETURNS: Nothing.
EFFECT: The atom of literal pli in PartnerClause is
destructively changed !!!
The <DocProof> flag is considered.
***************************************************************/
{
LITERAL PartnerLit;
TERM ReplaceTermT, NewAtom;
#ifdef CHECK
clause_Check(PartnerClause, Flags, Precedence);
clause_Check(RuleCl, Flags, Precedence);
#endif
if (flag_GetFlagValue(Flags, flag_DOCPROOF))
red_DocumentRewriting(PartnerClause, pli, RuleCl, ri);
if (flag_GetFlagValue(Flags, flag_PREW)) {
fputs("\nBRewriting: ", stdout);
clause_Print(PartnerClause);
printf(" ==>[ %d.%d ] ", clause_Number(RuleCl), ri);
}
PartnerLit = clause_GetLiteral(PartnerClause, pli);
ReplaceTermT =
cont_ApplyBindingsModuloMatchingReverse(cont_LeftContext(),
term_Copy(term_SecondArgument(clause_GetLiteralTerm(RuleCl, ri))));
NewAtom = clause_LiteralSignedAtom(PartnerLit);
term_ReplaceSubtermBy(NewAtom, PartnerTermS, ReplaceTermT);
term_Delete(ReplaceTermT);
clause_OrientAndReInit(PartnerClause, Flags, Precedence);
clause_UpdateSplitDataFromPartner(PartnerClause, RuleCl);
if (flag_GetFlagValue(Flags, flag_PREW))
clause_Print(PartnerClause);
}
static LIST red_LiteralRewriting(CLAUSE RedClause, LITERAL ActLit, int ri,
SHARED_INDEX ShIndex, FLAGSTORE Flags,
PRECEDENCE Precedence, LIST* Result)
/**************************************************************
INPUT: A clause, a positive equality literal where the
first equality argument is greater, its index, an
index of clauses, a flag store, a precedence and a
pointer to a list of clauses that were rewritten.
RETURNS: The list of clauses from the index that can be
rewritten by <ActLit> and <RedClause>.
The rewritten clauses are stored in <*Result>.
EFFECT: The <DocProof> flag is considered.
***************************************************************/
{
TERM TermS, CandTerm;
LIST Blocked;
#ifdef CHECK
if (!clause_LiteralIsLiteral(ActLit) || !clause_LiteralIsEquality(ActLit) ||
!clause_LiteralIsOrientedEquality(ActLit)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_LiteralRewriting: Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Blocked = list_Nil();
TermS = term_FirstArgument(clause_LiteralSignedAtom(ActLit)); /* Vars can't be greater ! */
CandTerm = st_ExistInstance(cont_LeftContext(), sharing_Index(ShIndex), TermS);
while (CandTerm) {
if (!term_IsVariable(CandTerm) &&
!symbol_IsPredicate(term_TopSymbol(CandTerm))) {
LIST LitList;
LitList = sharing_GetDataList(CandTerm, ShIndex);
for ( ; !list_Empty(LitList); LitList = list_Pop(LitList)){
LITERAL PartnerLit;
CLAUSE PartnerClause;
int pli;
PartnerLit = list_Car(LitList);
pli = clause_LiteralGetIndex(PartnerLit);
PartnerClause = clause_LiteralOwningClause(PartnerLit);
/* Partner literal must be from antecedent or succedent */
if (clause_Number(RedClause) != clause_Number(PartnerClause) &&
pli >= clause_FirstAntecedentLitIndex(PartnerClause) &&
!list_PointerMember(Blocked, PartnerClause) &&
subs_SubsumesBasic(RedClause, PartnerClause, ri, pli)) {
CLAUSE Copy;
Blocked = list_Cons(PartnerClause, Blocked);
Copy = clause_Copy(PartnerClause);
clause_RemoveFlag(Copy, WORKEDOFF);
red_ApplyRewriting(RedClause, ri, Copy, pli, CandTerm,
Flags, Precedence);
*Result = list_Cons(Copy, *Result);
}
}
}
CandTerm = st_NextCandidate();
}
return Blocked;
}
static LIST red_BackRewriting(CLAUSE RedClause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence,
LIST* Result)
/**************************************************************
INPUT: A clause, and Index, a flag store, a precedence and
a pointer to the list of rewritten clauses.
RETURNS: A list of clauses that can be rewritten with
<RedClause> and the result of this operation is
stored in <*Result>.
EFFECT: The <DocProof> flag is considered.
***************************************************************/
{
int i,length;
LITERAL ActLit;
LIST Blocked;
#ifdef CHECK
if (!(clause_IsClause(RedClause, Flags, Precedence))) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackRewriting :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
Blocked = list_Nil();
length = clause_Length(RedClause);
for (i=clause_FirstSuccedentLitIndex(RedClause); i < length; i++) {
ActLit = clause_GetLiteral(RedClause, i);
if (clause_LiteralIsOrientedEquality(ActLit)) {
Blocked = list_Nconc(red_LiteralRewriting(RedClause, ActLit, i,
ShIndex, Flags, Precedence,
Result),
Blocked);
}
#ifdef CHECK
if (fol_IsEquality(clause_LiteralSignedAtom(ActLit))) {
ord_RESULT HelpRes;
HelpRes =
ord_Compare(term_FirstArgument(clause_LiteralSignedAtom(ActLit)),
term_SecondArgument(clause_LiteralSignedAtom(ActLit)),
Flags, Precedence);
if (ord_IsSmallerThan(HelpRes)){ /* For Debugging */
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackRewriting:");
misc_ErrorReport("First Argument smaller than second in RedClause.\n");
misc_FinishErrorReport();
}
} /* end of if (fol_IsEquality). */
#endif
} /* end of for 'all succedent literals'. */
Blocked = list_PointerDeleteDuplicates(Blocked);
return Blocked;
}
/**************************************************************/
/* BACKWARD CONTEXTUAL REWRITING */
/**************************************************************/
static LIST red_BackCRwOnLiteral(PROOFSEARCH Search, CLAUSE RuleClause,
LITERAL Lit, int i, NAT Mode, LIST* Result)
/**************************************************************
INPUT: A proof search object, a clause that is used to rewrite
other clauses, a positive literal from the clause,
that is a strictly maximal, oriented equation, the index
of the literal, a mode defining which clause index
is used to find rewritable clauses, and a pointer
to a list that is used as return value.
The left term of the equation has to be the strictly
maximal term in the clause, i.e. it is bigger than
any other term.
RETURNS: The list of clauses from the clause index that can be
rewritten by <Lit> and <RuleClause>.
The rewritten clauses are stored in <*Result>.
EFFECT: The <DocProof> flag is considered.
***************************************************************/
{
TERM TermS, CandTerm, ReplaceTermT;
LIST Inst, Blocked;
FLAGSTORE Flags;
PRECEDENCE Precedence;
SHARED_INDEX ShIndex;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
if (red_WorkedOffMode(Mode))
ShIndex = prfs_WorkedOffSharingIndex(Search);
else
ShIndex = prfs_UsableSharingIndex(Search);
#ifdef CHECK
if (!clause_LiteralIsLiteral(Lit) || !clause_LiteralIsEquality(Lit) ||
!clause_LiteralGetFlag(Lit, STRICTMAXIMAL) ||
!clause_LiteralIsOrientedEquality(Lit)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackCRwOnLiteral: Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RuleClause, Flags, Precedence);
#endif
Blocked = list_Nil();
TermS = term_FirstArgument(clause_LiteralSignedAtom(Lit));
/* Get all instances of <TermS> at once. This can't be done iteratively */
/* since other reduction rules are invoked within the following loop. */
Inst = st_GetInstance(cont_LeftContext(), sharing_Index(ShIndex), TermS);
for ( ; !list_Empty(Inst); Inst = list_Pop(Inst)) {
CandTerm = list_Car(Inst);
if (!term_IsVariable(CandTerm) &&
!symbol_IsPredicate(term_TopSymbol(CandTerm))) {
LIST LitList;
LitList = sharing_GetDataList(CandTerm, ShIndex);
for ( ; !list_Empty(LitList); LitList = list_Pop(LitList)){
LITERAL RedLit;
CLAUSE RedClause, HelpClause;
int ri;
RedLit = list_Car(LitList);
ri = clause_LiteralGetIndex(RedLit);
RedClause = clause_LiteralOwningClause(RedLit);
HelpClause = NULL;
#ifdef CRW_DEBUG
if (clause_Number(RuleClause) != clause_Number(RedClause) &&
ri >= clause_FirstAntecedentLitIndex(RedClause) &&
!list_PointerMember(Blocked, RedClause)) {
printf("\n------\nBCRw: %s\n%d ", red_WorkedOffMode(Mode) ?
"WorkedOff" : "Usable", i);
clause_Print(RuleClause);
printf("\n%d ", ri);
clause_Print(RedClause);
}
#endif
/* Partner literal must be from antecedent or succedent */
if (clause_Number(RuleClause) != clause_Number(RedClause) &&
ri >= clause_FirstAntecedentLitIndex(RedClause) &&
/* Check that clause wasn't already rewritten by this literal. */
/* Necessary because then the old version of the clause is still */
/* in the index, but the rewritten version in not in the index. */
!list_PointerMember(Blocked, RedClause) &&
red_CRwTautologyCheck(Search, RedClause, ri, CandTerm,
RuleClause, i, Mode, &HelpClause)) {
CLAUSE Copy;
/* The <PartnerClause> has to be copied because it's indexed. */
Blocked = list_Cons(RedClause, Blocked);
Copy = clause_Copy(RedClause);
clause_RemoveFlag(Copy, WORKEDOFF);
/* Establish bindings */
cont_StartBinding();
if (!unify_MatchBindings(cont_LeftContext(), TermS, CandTerm)) {
#ifdef CHECK
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackCRwOnLiteral: terms aren't ");
misc_ErrorReport("matchable.");
misc_FinishErrorReport();
#endif
}
/* The variable check in cont_ApplyBindings... is turned on here */
/* because all variables is s are bound, and s > t. So all */
/* variables in t are bound, too. */
ReplaceTermT =
cont_ApplyBindingsModuloMatching(cont_LeftContext(),
term_Copy(term_SecondArgument(clause_GetLiteralTerm(RuleClause, i))),
TRUE);
cont_BackTrack();
/* Modify copied clause */
term_ReplaceSubtermBy(clause_GetLiteralAtom(Copy, ri), CandTerm,
ReplaceTermT);
term_Delete(ReplaceTermT);
/* Proof documentation */
if (flag_GetFlagValue(Flags, flag_DOCPROOF)) {
LIST PClauses, PLits;
if (HelpClause != NULL) {
/* Get additional parent clauses and literals from the */
/* tautology check. */
PClauses = clause_ParentClauses(HelpClause);
PLits = clause_ParentLiterals(HelpClause);
clause_SetParentClauses(HelpClause, list_Nil());
clause_SetParentLiterals(HelpClause, list_Nil());
} else
PClauses = PLits = list_Nil();
red_DocumentContextualRewriting(Copy, ri, RuleClause, i,
PClauses, PLits);
}
/* Set splitting data according to all parents */
clause_UpdateSplitDataFromPartner(Copy, RuleClause);
if (HelpClause != NULL) {
clause_UpdateSplitDataFromPartner(Copy, HelpClause);
clause_Delete(HelpClause);
}
clause_OrientAndReInit(Copy, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PCRW)) {
fputs("\nBContRewriting: ", stdout);
clause_Print(RedClause);
printf(" ==>[ %d.%d ] ", clause_Number(RuleClause), i);
clause_Print(Copy);
}
*Result = list_Cons(Copy, *Result);
}
}
}
}
return Blocked;
}
static LIST red_BackContextualRewriting(PROOFSEARCH Search, CLAUSE RuleClause,
NAT Mode, LIST* Result)
/**************************************************************
INPUT: A proof search object, a clause that is used to rewrite
other clauses, a mode flag that indicates which clause
index is used to find rewritable clauses, and a pointer
to a list that is used as return value.
RETURNS: A list of clauses that can be reduced
with Contextual Rewriting with <RuleClause>.
The clauses resulting from the rewriting steps are
stored in <*Result>.
EFFECT: The <DocProof> flag is considered. Every rewritable clause
is copied before rewriting is applied! This has to be done,
because the rewritable clauses are indexed.
***************************************************************/
{
BOOL found;
int i, ls;
LITERAL Lit;
LIST Blocked;
FLAGSTORE Flags;
PRECEDENCE Precedence;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
#ifdef CHECK
if (!clause_IsClause(RuleClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_BackContextualRewriting: Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RuleClause, Flags, Precedence);
#endif
Blocked = list_Nil();
ls = clause_LastSuccedentLitIndex(RuleClause);
found = FALSE;
for (i = clause_FirstSuccedentLitIndex(RuleClause); i <= ls && !found; i++) {
Lit = clause_GetLiteral(RuleClause, i);
if (clause_LiteralIsOrientedEquality(Lit) &&
clause_LiteralGetFlag(Lit, STRICTMAXIMAL) &&
red_LeftTermOfEquationIsStrictlyMaximalTerm(RuleClause, Lit, Flags,
Precedence)) {
Blocked = list_Nconc(red_BackCRwOnLiteral(Search, RuleClause, Lit, i,
Mode, Result),
Blocked);
/* Stop loop: there's only one strictly maximal term per clause */
found = TRUE;
}
}
Blocked = list_PointerDeleteDuplicates(Blocked);
return Blocked;
}
static void red_DocumentSortSimplification(CLAUSE Clause, LIST Indexes,
LIST Clauses)
/*********************************************************
INPUT: A clause and the literal indices and clauses
involved in sort simplification.
RETURNS: Nothing.
MEMORY: Consumes the input lists.
**********************************************************/
{
LIST Scan,Declarations,Self;
Declarations = list_Nil();
Self = list_Nil();
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
for(Scan=Indexes;!list_Empty(Scan);Scan=list_Cdr(Scan))
Self = list_Cons((POINTER)clause_Number(Clause),Self);
for(Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) {
Declarations = list_Cons((POINTER)clause_FirstSuccedentLitIndex(list_Car(Scan)),Declarations);
list_Rplaca(Scan,(POINTER)clause_Number(list_Car(Scan)));
}
clause_SetParentLiterals(Clause, list_Nconc(Indexes,Declarations));
clause_SetParentClauses(Clause, list_Nconc(Self,Clauses));
clause_SetNumber(Clause, clause_IncreaseCounter());
clause_SetFromSortSimplification(Clause);
}
static BOOL red_SortSimplification(SORTTHEORY Theory, CLAUSE Clause, NAT Level,
BOOL Document, FLAGSTORE Flags,
PRECEDENCE Precedence, CLAUSE *Changed)
/**********************************************************
INPUT: A sort theory, a clause, the last backtrack
level of the current proof search, a boolean
flag concerning proof documentation, a flag
store and a precedence.
RETURNS: TRUE iff sort simplification was possible.
If <Document> is true or the split level of the
used declaration clauses requires copying a
simplified copy of the clause is returned in
<*Changed>.
Otherwise the clause is destructively
simplified.
***********************************************************/
{
if (Theory != (SORTTHEORY)NULL) {
TERM Atom,Term;
SOJU SortPair;
SORT TermSort,LitSort;
LIST Indexes,NewClauses,Clauses,Scan;
int i,lc,j,OldSplitLevel;
CLAUSE Copy;
CONDITION Cond;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_SortSimplification :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
lc = clause_LastConstraintLitIndex(Clause);
i = clause_FirstLitIndex();
j = 0;
OldSplitLevel = clause_SplitLevel(Clause);
Copy = Clause;
Indexes = list_Nil();
Clauses = list_Nil();
while (i <= lc) {
Atom = clause_LiteralAtom(clause_GetLiteral(Copy, i));
Term = term_FirstArgument(Atom);
SortPair = sort_ComputeSortNoResidues(Theory, Term, Copy, i,
Flags, Precedence);
TermSort = sort_PairSort(SortPair);
NewClauses = sort_ConditionClauses(sort_PairCondition(SortPair));
sort_ConditionPutClauses(sort_PairCondition(SortPair),list_Nil());
LitSort = sort_TheorySortOfSymbol(Theory,term_TopSymbol(Atom));
if ((Cond = sort_TheoryIsSubsortOfNoResidues(Theory, TermSort, LitSort)) != (CONDITION)NULL) {
if (j == 0 && flag_GetFlagValue(Flags, flag_PSSI)) {
fputs("\nSortSimplification: ", stdout);
clause_Print(Copy);
fputs(" ==>[ ", stdout);
}
NewClauses = list_Nconc(NewClauses,sort_ConditionClauses(Cond));
sort_ConditionPutClauses(Cond,list_Nil());
sort_ConditionDelete(Cond);
for (Scan = NewClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
if (Clause == Copy &&
(Document ||
prfs_SplitLevelCondition(clause_SplitLevel(list_Car(Scan)),OldSplitLevel,Level)))
Copy = clause_Copy(Clause);
clause_UpdateSplitDataFromPartner(Copy, list_Car(Scan));
if (flag_GetFlagValue(Flags, flag_PSSI))
printf("%d ",clause_Number(list_Car(Scan)));
}
if (Document)
Indexes = list_Cons((POINTER)(i+j), Indexes);
clause_DeleteLiteral(Copy, i, Flags, Precedence);
Clauses = list_Nconc(NewClauses,Clauses);
j++;
lc--;
}
else {
list_Delete(NewClauses);
i++;
}
sort_DeleteSortPair(SortPair);
sort_Delete(LitSort);
}
#ifdef CHECK
clause_Check(Copy, Flags, Precedence);
#endif
if (j > 0) {
if (Document)
red_DocumentSortSimplification(Copy,Indexes,Clauses);
else
list_Delete(Clauses);
clause_ReInit(Copy, Flags, Precedence);
if (flag_GetFlagValue(Flags, flag_PSSI)) {
fputs("] ", stdout);
clause_Print(Copy);
}
if (Copy != Clause)
*Changed = Copy;
return TRUE;
}
}
return FALSE;
}
static void red_ExchangeClauses(CLAUSE *RedClause, CLAUSE *Copy, LIST *Result)
/**********************************************************
INPUT: Two pointers to clauses and a pointer to a list.
RETURNS: Nothing.
EFFECT: If *Copy is NULL, nothing is done. Otherwise *RedClause
is added to the list, *Copy is assigned to *RedClause,
and NULL is assigned to *Copy.
***********************************************************/
{
if (*Copy) {
*Result = list_Cons(*RedClause,*Result);
*RedClause = *Copy;
*Copy = (CLAUSE)NULL;
}
}
static BOOL red_SimpleStaticReductions(CLAUSE *RedClause, FLAGSTORE Flags,
PRECEDENCE Precedence, LIST* Result)
/**********************************************************
INPUT: A clause (by reference), a flag store and a
precedence.
RETURNS: TRUE if <*RedClause> is redundant.
If the <DocProof> flag is false and no copying is necessary
with respect to splitting, the clause is destructively changed,
otherwise (intermediate) copies are made and returned in <*Result>.
EFFECT: Used reductions are tautology deletion and
obvious reductions.
***********************************************************/
{
CLAUSE Copy;
BOOL DocProof;
#ifdef CHECK
if (!clause_IsClause(*RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_SimpleStaticReductions :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(*RedClause, Flags, Precedence);
#endif
Copy = (CLAUSE)NULL;
DocProof = flag_GetFlagValue(Flags, flag_DOCPROOF);
if (flag_GetFlagValue(Flags, flag_RTAUT) != flag_RTAUTOFF &&
red_Tautology(*RedClause, Flags, Precedence))
return TRUE;
if (flag_GetFlagValue(Flags, flag_ROBV)) {
red_ObviousReductions(*RedClause, DocProof, Flags, Precedence, &Copy);
red_ExchangeClauses(RedClause, &Copy, Result);
}
if (flag_GetFlagValue(Flags, flag_RCON)) {
red_Condensing(*RedClause, DocProof, Flags, Precedence, &Copy);
red_ExchangeClauses(RedClause, &Copy, Result);
}
return FALSE;
}
static BOOL red_StaticReductions(PROOFSEARCH Search, CLAUSE *Clause,
CLAUSE *Subsumer, LIST* Result, NAT Mode)
/**********************************************************
INPUT: A proof search object, a clause (by reference) to be reduced,
a shared index of clauses and the mode of the reductions,
determining which sets (Usable, WorkedOff) in <Search>
are considered for reductions.
RETURNS: TRUE iff the clause is redundant.
If the <DocProof> flag is false and no copying is necessary
with respect to splitting, the clause is destructively changed,
otherwise (intermediate) copies are made and returned in <*Result>.
If <Clause> gets redundant with respect to forward subsumption,
the subsuming clause is returned in <*Subsumer>.
EFFECT: Used reductions are tautology deletion, obvious reductions,
forward subsumption, forward rewriting, forward contextual
rewriting, forward matching replacement resolution,
sort simplification, unit conflict and static soft typing.
Depending on <Mode>, then clauses are reduced with respect
to WorkedOff or Usable Clauses.
***********************************************************/
{
CLAUSE Copy;
BOOL Redundant;
SHARED_INDEX Index;
FLAGSTORE Flags;
PRECEDENCE Precedence;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
#ifdef CHECK
if (!clause_IsClause(*Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_StaticReductions:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(*Clause, Flags, Precedence);
#endif
Index = (red_OnlyWorkedOffMode(Mode) ?
prfs_WorkedOffSharingIndex(Search) : prfs_UsableSharingIndex(Search));
Copy = (CLAUSE)NULL;
Redundant = red_SimpleStaticReductions(Clause, Flags, Precedence, Result);
if (Redundant)
return Redundant;
/* Assignment Equation Deletion */
if (flag_GetFlagValue(Flags, flag_RAED) != flag_RAEDOFF &&
red_AssignmentEquationDeletion(*Clause, Flags, Precedence, &Copy,
prfs_NonTrivClauseNumber(Search),
(flag_GetFlagValue(Flags, flag_RAED) == flag_RAEDPOTUNSOUND))) {
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
}
/* Subsumption */
if (flag_GetFlagValue(Flags, flag_RFSUB)) {
*Subsumer = red_ForwardSubsumption(*Clause, Index, Flags, Precedence);
if ((Redundant = (*Subsumer != (CLAUSE)NULL)))
return Redundant;
}
/* Forward Rewriting and Forward Contextual Rewriting */
if ((flag_GetFlagValue(Flags, flag_RFREW) &&
red_RewriteRedClause(*Clause, Index, Flags, Precedence,
&Copy, prfs_LastBacktrackLevel(Search))) ||
(flag_GetFlagValue(Flags, flag_RFCRW) &&
red_ContextualRewriting(Search, *Clause, Mode,
prfs_LastBacktrackLevel(Search), &Copy))) {
red_ExchangeClauses(Clause, &Copy, Result);
Redundant = red_SimpleStaticReductions(Clause, Flags, Precedence, Result);
if (Redundant)
return Redundant;
if (clause_IsEmptyClause(*Clause))
return FALSE;
if (flag_GetFlagValue(Flags, flag_RFSUB)) {
*Subsumer = red_ForwardSubsumption(*Clause, Index, Flags, Precedence);
if ((Redundant = (*Subsumer != (CLAUSE)NULL)))
return Redundant;
}
}
/* Sort Simplification */
if (red_OnlyWorkedOffMode(Mode) && flag_GetFlagValue(Flags, flag_RSSI)) {
red_SortSimplification(prfs_DynamicSortTheory(Search), *Clause,
prfs_LastBacktrackLevel(Search),
flag_GetFlagValue(Flags, flag_DOCPROOF),
Flags, Precedence, &Copy);
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
}
/* Matching Replacement Resolution */
if (flag_GetFlagValue(Flags, flag_RFMRR)) {
red_MatchingReplacementResolution(*Clause, Index, Flags, Precedence,
&Copy, prfs_LastBacktrackLevel(Search));
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
}
/* Unit Conflict */
if (flag_GetFlagValue(Flags, flag_RUNC)) {
red_UnitConflict(*Clause, Index, Flags, Precedence,
&Copy, prfs_LastBacktrackLevel(Search));
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
}
/* Static Soft Typing */
if (red_OnlyWorkedOffMode(Mode) && flag_GetFlagValue(Flags, flag_RSST))
Redundant = red_ClauseDeletion(prfs_StaticSortTheory(Search),*Clause,
Flags, Precedence);
#ifdef CHECK
clause_Check(*Clause, Flags, Precedence);
#endif
return Redundant;
}
static BOOL red_SelectedStaticReductions(PROOFSEARCH Search, CLAUSE *Clause,
CLAUSE *Subsumer, LIST* Result,
NAT Mode)
/**********************************************************
INPUT: A proof search object, a clause (by reference) to be reduced,
and the mode of the reductions, determining which sets
(Usable, WorkedOff) in <Search> are considered for reductions.
EFFECT: Used reductions are tautology deletion, obvious reductions,
forward subsumption, forward rewriting, forward matching
replacement resolution, sort simplification, unit conflict
and static soft typing.
Depending on <Mode>, the clauses are reduced with respect
to WorkedOff and/or Usable Clauses.
RETURNS: TRUE iff the clause is redundant.
If the <DocProof> flag is false and no copying is necessary
with respect to splitting, the clause is destructively changed,
otherwise (intermediate) copies are made and returned in <*Result>.
If <Clause> gets redundant with respect to forward subsumption,
the subsuming clause is returned in <*Subsumer>.
***********************************************************/
{
CLAUSE Copy;
BOOL Redundant ,Rewritten, Tried, ContextualRew, StandardRew;
SHARED_INDEX WoIndex,UsIndex;
FLAGSTORE Flags;
PRECEDENCE Precedence;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
#ifdef CHECK
if (!clause_IsClause(*Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_SelectedStaticReductions:");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(*Clause, Flags, Precedence);
#endif
WoIndex = (SHARED_INDEX)NULL;
UsIndex = (SHARED_INDEX)NULL;
if (red_WorkedOffMode(Mode))
WoIndex = prfs_WorkedOffSharingIndex(Search);
if (red_UsableMode(Mode))
UsIndex = prfs_UsableSharingIndex(Search);
Copy = (CLAUSE)NULL;
Redundant = red_SimpleStaticReductions(Clause, Flags, Precedence, Result);
if (Redundant)
return Redundant;
if (flag_GetFlagValue(Flags, flag_RAED) != flag_RAEDOFF &&
red_AssignmentEquationDeletion(*Clause, Flags, Precedence, &Copy,
prfs_NonTrivClauseNumber(Search),
(flag_GetFlagValue(Flags, flag_RAED)==flag_RAEDPOTUNSOUND))) {
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
}
if (flag_GetFlagValue(Flags, flag_RFSUB)) {
*Subsumer = (CLAUSE)NULL;
if (WoIndex != NULL) {
*Subsumer = red_ForwardSubsumption(*Clause, WoIndex, Flags, Precedence);
if (*Subsumer != (CLAUSE)NULL)
return TRUE;
}
if (UsIndex != NULL) {
*Subsumer = red_ForwardSubsumption(*Clause, UsIndex, Flags, Precedence);
if (*Subsumer != (CLAUSE)NULL)
return TRUE;
}
}
StandardRew = flag_GetFlagValue(Flags, flag_RFREW);
ContextualRew = flag_GetFlagValue(Flags, flag_RFCRW);
Rewritten = (StandardRew || ContextualRew);
Tried = FALSE;
while (Rewritten) {
Rewritten = FALSE;
if (WoIndex != NULL &&
((StandardRew &&
red_RewriteRedClause(*Clause, WoIndex, Flags, Precedence, &Copy,
prfs_LastBacktrackLevel(Search))) ||
(ContextualRew &&
red_ContextualRewriting(Search, *Clause, red_WORKEDOFF,
prfs_LastBacktrackLevel(Search), &Copy)))) {
Rewritten = TRUE;
red_ExchangeClauses(Clause, &Copy, Result);
Redundant = red_SimpleStaticReductions(Clause, Flags,
Precedence, Result);
if (Redundant)
return Redundant;
if (clause_IsEmptyClause(*Clause))
return FALSE;
if (flag_GetFlagValue(Flags, flag_RFSUB)) {
*Subsumer = (CLAUSE)NULL;
*Subsumer = red_ForwardSubsumption(*Clause, WoIndex,
Flags, Precedence);
if (*Subsumer != (CLAUSE)NULL)
return TRUE; /* Clause is redundant */
if (UsIndex != NULL) {
*Subsumer = red_ForwardSubsumption(*Clause, UsIndex,
Flags, Precedence);
if (*Subsumer != (CLAUSE)NULL)
return TRUE;
}
}
}
if (UsIndex != NULL &&
(!Tried || Rewritten) &&
((StandardRew &&
red_RewriteRedClause(*Clause, UsIndex, Flags, Precedence,
&Copy, prfs_LastBacktrackLevel(Search))) ||
(ContextualRew &&
red_ContextualRewriting(Search, *Clause, red_USABLE,
prfs_LastBacktrackLevel(Search), &Copy)))) {
Rewritten = TRUE;
red_ExchangeClauses(Clause, &Copy, Result);
Redundant = red_SimpleStaticReductions(Clause, Flags,
Precedence, Result);
if (Redundant)
return Redundant;
if (clause_IsEmptyClause(*Clause))
return FALSE;
if (flag_GetFlagValue(Flags, flag_RFSUB)) {
*Subsumer = (CLAUSE)NULL;
if (WoIndex != NULL)
*Subsumer = red_ForwardSubsumption(*Clause, WoIndex,
Flags, Precedence);
if (*Subsumer != (CLAUSE)NULL)
return TRUE;
*Subsumer = red_ForwardSubsumption(*Clause, UsIndex,
Flags, Precedence);
if (*Subsumer != (CLAUSE)NULL)
return TRUE;
}
}
Tried = TRUE;
} /* end of while(Rewritten) */
if (flag_GetFlagValue(Flags, flag_RSSI)) {
red_SortSimplification(prfs_DynamicSortTheory(Search), *Clause,
prfs_LastBacktrackLevel(Search),
flag_GetFlagValue(Flags, flag_DOCPROOF),
Flags, Precedence, &Copy);
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
}
if (flag_GetFlagValue(Flags, flag_RFMRR)) {
if (WoIndex)
red_MatchingReplacementResolution(*Clause, WoIndex, Flags, Precedence,
&Copy, prfs_LastBacktrackLevel(Search));
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
if (UsIndex)
red_MatchingReplacementResolution(*Clause, UsIndex, Flags, Precedence,
&Copy, prfs_LastBacktrackLevel(Search));
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
}
if (flag_GetFlagValue(Flags, flag_RUNC)) {
if (WoIndex)
red_UnitConflict(*Clause, WoIndex, Flags, Precedence,
&Copy, prfs_LastBacktrackLevel(Search));
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
if (UsIndex)
red_UnitConflict(*Clause, UsIndex, Flags, Precedence,
&Copy, prfs_LastBacktrackLevel(Search));
red_ExchangeClauses(Clause, &Copy, Result);
if (clause_IsEmptyClause(*Clause))
return FALSE;
}
if (flag_GetFlagValue(Flags, flag_RSST))
Redundant = red_ClauseDeletion(prfs_StaticSortTheory(Search),*Clause,
Flags, Precedence);
#ifdef CHECK
clause_Check(*Clause, Flags, Precedence);
#endif
return Redundant;
}
CLAUSE red_ReductionOnDerivedClause(PROOFSEARCH Search, CLAUSE Clause,
NAT Mode)
/**************************************************************
INPUT: A proof search object, a derived clause and a mode
indicating which indexes should be used for reductions.
RETURNS: The non-redundant clause after reducing <Clause>,
NULL if <Clause> is redundant.
EFFECT: Clauses probably generated, but redundant are kept according
to the <DocProof> flag and the split level of involved clauses.
depending on <Mode>, then clauses are reduced
with respect to WorkedOff and/or Usable Clauses.
***************************************************************/
{
CLAUSE RedClause;
LIST Redundant;
#ifdef CHECK
cont_SaveState();
#endif
Redundant = list_Nil();
RedClause = (CLAUSE)NULL;
if (red_StaticReductions(Search,&Clause,&RedClause,&Redundant,Mode)) {
/* Clause is redundant */
red_HandleRedundantDerivedClauses(Search, Redundant, Clause);
list_Delete(Redundant);
if (RedClause &&
prfs_SplitLevelCondition(clause_SplitLevel(RedClause),clause_SplitLevel(Clause),
prfs_LastBacktrackLevel(Search))) {
split_KeepClauseAtLevel(Search,Clause,clause_SplitLevel(RedClause));
}
else
if (flag_GetFlagValue(prfs_Store(Search), flag_DOCPROOF))
prfs_InsertDocProofClause(Search,Clause);
else
clause_Delete(Clause);
Clause = (CLAUSE)NULL;
}
else {
red_HandleRedundantDerivedClauses(Search, Redundant, Clause);
list_Delete(Redundant);
}
#ifdef CHECK
cont_CheckState();
#endif
return Clause;
}
CLAUSE red_CompleteReductionOnDerivedClause(PROOFSEARCH Search, CLAUSE Clause,
NAT Mode)
/**************************************************************
INPUT: A proof search object, a derived clause and a mode determining
which clauses to consider for reduction.
RETURNS: The non-redundant clause after reducing <Clause>,
NULL if <Clause> is redundant.
EFFECT: Clauses probably generated, but redundant are kept according
to the <DocProof> flag and the split level of involved clauses.
The clause is reduced with respect to all indexes determined
by <Mode>
***************************************************************/
{
CLAUSE RedClause;
LIST Redundant;
#ifdef CHECK
cont_SaveState();
#endif
Redundant = list_Nil();
RedClause = (CLAUSE)NULL;
if (red_SelectedStaticReductions(Search,&Clause,&RedClause,&Redundant,Mode)) {
/* <Clause> is redundant */
red_HandleRedundantDerivedClauses(Search, Redundant, Clause);
list_Delete(Redundant);
if (RedClause &&
prfs_SplitLevelCondition(clause_SplitLevel(RedClause),clause_SplitLevel(Clause),
prfs_LastBacktrackLevel(Search))) {
split_KeepClauseAtLevel(Search, Clause, clause_SplitLevel(RedClause));
}
else
if (flag_GetFlagValue(prfs_Store(Search), flag_DOCPROOF))
prfs_InsertDocProofClause(Search, Clause);
else
clause_Delete(Clause);
Clause = (CLAUSE)NULL;
}
else {
red_HandleRedundantDerivedClauses(Search, Redundant, Clause);
list_Delete(Redundant);
}
#ifdef CHECK
cont_CheckState();
#endif
return Clause;
}
LIST red_BackReduction(PROOFSEARCH Search, CLAUSE Clause, NAT Mode)
/**************************************************************
INPUT: A proof search object, a clause and a mode flag.
RETURNS: A list of reduced clauses in usable and worked-off
(depending on <Mode>) in <Search> with respect to <Clause>.
The original clauses that become redundant are either deleted
or kept for proof documentation or splitting.
EFFECT: The original clauses that become redundant are either deleted
or kept for proof documentation or splitting.
***************************************************************/
{
LIST Result, Redundant;
FLAGSTORE Flags;
PRECEDENCE Precedence;
#ifdef CHECK
cont_SaveState();
#endif
Result = list_Nil();
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
/* Subsumption */
if (flag_GetFlagValue(Flags, flag_RBSUB)) {
Redundant = list_Nil();
if (red_WorkedOffMode(Mode))
Redundant = red_BackSubsumption(Clause,
prfs_WorkedOffSharingIndex(Search),
Flags, Precedence);
if (red_UsableMode(Mode))
Redundant = list_Nconc(Redundant,
red_BackSubsumption(Clause,
prfs_UsableSharingIndex(Search),
Flags, Precedence));
red_HandleRedundantIndexedClauses(Search, Redundant, Clause);
list_Delete(Redundant);
}
/* Matching Replacement Resolution */
if (flag_GetFlagValue(Flags, flag_RBMRR)) {
Redundant = list_Nil();
if (red_WorkedOffMode(Mode))
Redundant = red_BackMatchingReplacementResolution(Clause,
prfs_WorkedOffSharingIndex(Search),
Flags, Precedence, &Result);
if (red_UsableMode(Mode))
Redundant = list_Nconc(Redundant,
red_BackMatchingReplacementResolution(Clause,
prfs_UsableSharingIndex(Search),
Flags, Precedence, &Result));
red_HandleRedundantIndexedClauses(Search, Redundant, Clause);
list_Delete(Redundant);
}
/* Standard Rewriting */
if (flag_GetFlagValue(Flags, flag_RBREW)) {
Redundant = list_Nil();
if (red_WorkedOffMode(Mode))
Redundant = red_BackRewriting(Clause,prfs_WorkedOffSharingIndex(Search),
Flags, Precedence, &Result);
if (red_UsableMode(Mode))
Redundant = list_Nconc(Redundant,
red_BackRewriting(Clause,
prfs_UsableSharingIndex(Search),
Flags, Precedence, &Result));
red_HandleRedundantIndexedClauses(Search, Redundant, Clause);
list_Delete(Redundant);
}
/* Contextual Rewriting */
if (flag_GetFlagValue(Flags, flag_RBCRW)) {
Redundant = list_Nil();
if (red_WorkedOffMode(Mode))
Redundant = red_BackContextualRewriting(Search, Clause, red_WORKEDOFF,
&Result);
if (red_UsableMode(Mode))
Redundant = list_Nconc(Redundant,
red_BackContextualRewriting(Search, Clause,
red_USABLE, &Result));
red_HandleRedundantIndexedClauses(Search, Redundant, Clause);
list_Delete(Redundant);
}
#ifdef CHECK
cont_CheckState();
#endif
return Result;
}
static __inline__ LIST red_MergeClauseListsByWeight(LIST L1, LIST L2)
/**************************************************************
INPUT: Two lists of clauses, sorted by weight.
RETURNS:
EFFECT:
***************************************************************/
{
return list_NNumberMerge(L1, L2, (NAT (*)(POINTER))clause_Weight);
}
LIST red_CompleteReductionOnDerivedClauses(PROOFSEARCH Search,
LIST DerivedClauses, NAT Mode,
int Bound, NAT BoundMode,
int *BoundApplied)
/**************************************************************
INPUT: A proof search object, a list of newly derived (unshared) clauses,
a mode determining which clause lists to consider for reduction,
a bound and a bound mode to cut off generated clauses.
RETURNS: A list of empty clauses that may be derived during the
reduction process.
<*BoundApplied> is set to the mode dependent value of the
smallest clause if a clause is deleted because of a bound.
EFFECT: The <DerivedClauses> are destructively reduced and reduced clauses
from the indexes are checked out and all finally reduced clauses
are checked into the indexes. Depending on <Mode> either the
WorkedOff, Usable or both indexes are considered.
The <DocProof> Flag is considered.
***************************************************************/
{
LIST EmptyClauses,NewClauses,Scan;
NAT ClauseBound;
CLAUSE Clause;
FLAGSTORE Flags;
#ifdef CHECK
cont_SaveState();
#endif
EmptyClauses = list_Nil();
DerivedClauses = clause_ListSortWeighed(DerivedClauses);
ClauseBound = 0;
Flags = prfs_Store(Search);
while (!list_Empty(DerivedClauses)) {
#ifdef WIN
clock_PingOneSecond();
#endif
Clause = list_NCar(&DerivedClauses);
if (prfs_SplitStackEmpty(Search)) /* Otherwise splitting not compatible with bound deletion */
Clause = red_CompleteReductionOnDerivedClause(Search, Clause, Mode);
if (Clause != NULL && BoundMode != flag_BOUNDMODEUNLIMITED &&
Bound != flag_BOUNDSTARTUNLIMITED && !clause_IsFromInput(Clause) &&
!clause_IsFromSplitting(Clause)) {
switch (BoundMode) {
case flag_BOUNDMODERESTRICTEDBYWEIGHT:
ClauseBound = clause_Weight(Clause);
break;
case flag_BOUNDMODERESTRICTEDBYDEPTH:
ClauseBound = clause_ComputeTermDepth(Clause);
break;
default:
misc_StartUserErrorReport();
misc_UserErrorReport("\n Error while applying bound restrictions:");
misc_UserErrorReport("\n You selected an unknown bound mode.\n");
misc_FinishUserErrorReport();
}
if (ClauseBound > Bound) {
if (flag_GetFlagValue(Flags, flag_PBDC)) {
fputs("\nDeleted by bound: ", stdout);
clause_Print(Clause);
}
clause_Delete(Clause);
if (*BoundApplied == -1 || ClauseBound < *BoundApplied)
*BoundApplied = ClauseBound;
Clause = (CLAUSE)NULL;
}
}
if (Clause != (CLAUSE)NULL && /* For clauses below bound, splitting is */
!prfs_SplitStackEmpty(Search)) /* compatible with bound deletion */
Clause = red_CompleteReductionOnDerivedClause(Search, Clause, Mode);
if (Clause) {
prfs_IncKeptClauses(Search);
if (flag_GetFlagValue(Flags, flag_PKEPT)) {
fputs("\nKept: ", stdout);
clause_Print(Clause);
}
if (clause_IsEmptyClause(Clause))
EmptyClauses = list_Cons(Clause,EmptyClauses);
else {
NewClauses = red_BackReduction(Search, Clause, Mode);
prfs_IncDerivedClauses(Search, list_Length(NewClauses));
if (flag_GetFlagValue(Flags, flag_PDER))
for (Scan=NewClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) {
fputs("\nDerived: ", stdout);
clause_Print(list_Car(Scan));
}
NewClauses = split_ExtractEmptyClauses(NewClauses,&EmptyClauses);
prfs_InsertUsableClause(Search,Clause);
NewClauses = list_NumberSort(NewClauses, (NAT (*) (POINTER)) clause_Weight);
DerivedClauses = red_MergeClauseListsByWeight(DerivedClauses,NewClauses);
}
}
}
#ifdef CHECK
cont_CheckState();
#endif
return EmptyClauses;
}
static CLAUSE red_CDForwardSubsumer(CLAUSE RedCl, st_INDEX Index,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**********************************************************
INPUT: A pointer to a non-empty clause, an index of
clauses, a flag store and a precedence.
RETURNS: The first clause from the Approx Set which
subsumes 'RedCl'.
***********************************************************/
{
TERM Atom,AtomGen;
LIST LitScan;
int i,length;
CLAUSE CandCl;
#ifdef CHECK
if (!clause_IsClause(RedCl, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_CDForwardSubsumer :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedCl, Flags, Precedence);
#endif
length = clause_Length(RedCl);
for (i = 0; i < length; i++) {
Atom = clause_GetLiteralAtom(RedCl, i);
AtomGen = st_ExistGen(cont_LeftContext(), Index, Atom);
while (AtomGen) {
for (LitScan = term_SupertermList(AtomGen);
!list_Empty(LitScan); LitScan = list_Cdr(LitScan)) {
CandCl = clause_LiteralOwningClause(list_Car(LitScan));
if (clause_GetLiteral(CandCl,clause_FirstLitIndex()) == (LITERAL)list_Car(LitScan) &&
subs_Subsumes(CandCl, RedCl, clause_FirstLitIndex(), i)) {
st_CancelExistRetrieval();
return CandCl;
}
}
AtomGen = st_NextCandidate();
}
}
return (CLAUSE)NULL;
}
static BOOL red_CDForwardSubsumption(CLAUSE RedClause, st_INDEX Index,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**********************************************************
INPUT: A clause, an index of clauses, a flag store and
a precedence.
RETURNS: The boolean value TRUE if the clause is subsumed
by an indexed clause, if so, the clause is deleted,
either really or locally.
***********************************************************/
{
BOOL IsSubsumed;
CLAUSE Subsumer;
#ifdef CHECK
if (!clause_IsClause(RedClause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_CDForwardSubSumption :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
IsSubsumed = FALSE;
Subsumer = red_CDForwardSubsumer(RedClause, Index, Flags, Precedence);
if (clause_Exists(Subsumer)) {
IsSubsumed = TRUE;
if (flag_GetFlagValue(Flags, flag_DOCSST) &&
flag_GetFlagValue(Flags, flag_PSUB)) {
fputs("\nFSubsumption:", stdout);
clause_Print(RedClause);
printf(" by %d ",clause_Number(Subsumer));
}
}
return IsSubsumed;
}
static void red_CDBackSubsumption(CLAUSE RedCl, FLAGSTORE Flags,
PRECEDENCE Precedence,
LIST* UsListPt, LIST* WOListPt,
st_INDEX Index)
/**********************************************************
INPUT: A pointer to a non-empty clause, a flag store,
a precedence, and an index of clauses.
RETURNS: Nothing.
***********************************************************/
{
TERM Atom,AtomInst;
CLAUSE SubsumedCl;
LIST Scan, SubsumedList;
#ifdef CHECK
if (!clause_IsClause(RedCl, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_CDBackupSubSumption :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedCl, Flags, Precedence);
#endif
SubsumedList = list_Nil();
if (!clause_IsEmptyClause(RedCl)) {
Atom = clause_GetLiteralAtom(RedCl, clause_FirstLitIndex());
AtomInst = st_ExistInstance(cont_LeftContext(), Index, Atom);
while(AtomInst) {
for (Scan = term_SupertermList(AtomInst); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
SubsumedCl = clause_LiteralOwningClause(list_Car(Scan));
if ((RedCl != SubsumedCl) &&
subs_Subsumes(RedCl, SubsumedCl, clause_FirstLitIndex(),
clause_LiteralGetIndex(list_Car(Scan))) &&
!list_PointerMember(SubsumedList, SubsumedCl))
SubsumedList = list_Cons(SubsumedCl, SubsumedList);
}
AtomInst = st_NextCandidate();
}
for (Scan = SubsumedList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
SubsumedCl = list_Car(Scan);
if (flag_GetFlagValue(Flags, flag_DOCSST) && flag_GetFlagValue(Flags, flag_PSUB)) {
fputs("\nBSubsumption: ", stdout);
clause_Print(SubsumedCl);
printf(" by %d ",clause_Number(RedCl));
}
if (clause_GetFlag(SubsumedCl,WORKEDOFF)) {
*WOListPt = list_PointerDeleteOneElement(*WOListPt, SubsumedCl);
}else {
*UsListPt = list_PointerDeleteOneElement(*UsListPt, SubsumedCl);
}
clause_DeleteFlatFromIndex(SubsumedCl, Index);
}
list_Delete(SubsumedList);
}
}
static LIST red_CDDerivables(SORTTHEORY Theory, CLAUSE GivenClause,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: A sort theory, a clause, a flag store and a
precedence.
RETURNS: A list of clauses derivable from <GivenClause> and
the declaration clauses in <Theory>.
***************************************************************/
{
LIST ListOfDerivedClauses;
#ifdef CHECK
if (!(clause_IsClause(GivenClause, Flags, Precedence))) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_CDDeriveables :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(GivenClause, Flags, Precedence);
#endif
if (clause_HasTermSortConstraintLits(GivenClause))
ListOfDerivedClauses = inf_ForwardSortResolution(GivenClause,
sort_TheoryIndex(Theory),
Theory, TRUE,
Flags, Precedence);
else
ListOfDerivedClauses = inf_ForwardEmptySort(GivenClause,
sort_TheoryIndex(Theory),
Theory, TRUE,
Flags, Precedence);
return ListOfDerivedClauses;
}
static BOOL red_CDReduce(SORTTHEORY Theory, CLAUSE RedClause,
FLAGSTORE Flags, PRECEDENCE Precedence,
LIST *ApproxUsListPt, LIST *ApproxWOListPt,
st_INDEX Index)
/**************************************************************
INPUT: A sort theory, an unshared clause, a flag store,
a precedence, their index and two pointers to the
sort reduction subproof usable and worked off list.
RETURNS: TRUE iff <RedClause> is redundant with respect to
clauses in the index or theory.
EFFECT: <RedClause> is destructively changed.
The <DocProof> flag is changed temporarily.
***************************************************************/
{
CLAUSE Copy;
#ifdef CHECK
clause_Check(RedClause, Flags, Precedence);
#endif
Copy = (CLAUSE)NULL; /* Only needed for interface */
red_ObviousReductions(RedClause, FALSE, Flags, Precedence, &Copy);
red_SortSimplification(Theory, RedClause, NAT_MAX, FALSE,
Flags, Precedence, &Copy);
if (clause_IsEmptyClause(RedClause))
return FALSE;
red_Condensing(RedClause, FALSE, Flags, Precedence, &Copy);
if (red_CDForwardSubsumption(RedClause, Index, Flags, Precedence))
return TRUE;
else { /* RedClause isn't subsumed! */
red_CDBackSubsumption(RedClause, Flags, Precedence,
ApproxUsListPt, ApproxWOListPt, Index);
clause_InsertFlatIntoIndex(RedClause, Index);
*ApproxUsListPt = list_Cons(RedClause, *ApproxUsListPt);
}
#ifdef CHECK
clause_Check(RedClause, Flags, Precedence);
if (Copy != (CLAUSE)NULL) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_CDReduce :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
#endif
return FALSE;
}
BOOL red_ClauseDeletion(SORTTHEORY Theory, CLAUSE RedClause, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A sort theory, a clause (unshared), a flag store
and a precedence.
RETURNS: TRUE iff the sort constraint of the clause is
unsolvable with respect to the sort theory.
***************************************************************/
{
if (Theory != (SORTTHEORY)NULL) {
CLAUSE ConstraintClause, GivenClause;
LIST ApproxUsableList, ApproxWOList, EmptyClauses, ApproxDerivables, Scan;
int i,nc, Count, OldClauseCounter;
st_INDEX Index;
#ifdef CHECK
if (!(clause_IsClause(RedClause, Flags, Precedence))) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ClauseDeletion :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
clause_Check(RedClause, Flags, Precedence);
#endif
if (clause_HasEmptyConstraint(RedClause) || !flag_GetFlagValue(Flags, flag_RSST))
return FALSE;
if (flag_GetFlagValue(Flags, flag_DOCSST)) {
fputs("\n\nStatic Soft Typing tried on: ", stdout);
clause_Print(RedClause);
}
Index = st_IndexCreate();
Scan = list_Nil();
nc = clause_NumOfConsLits(RedClause);
OldClauseCounter = clause_Counter();
/* Make constraint clause, insert it into the Approx-usable-list: */
for (i = clause_FirstLitIndex(); i < nc; i++)
Scan = list_Cons(term_Copy(clause_LiteralAtom(
clause_GetLiteral(RedClause, i))), Scan);
Scan = list_NReverse(Scan);
ConstraintClause = clause_Create(Scan, list_Nil(), list_Nil(),
Flags, Precedence);
list_Delete(Scan);
clause_InitSplitData(ConstraintClause);
clause_AddParentClause(ConstraintClause, clause_Number(RedClause));
clause_AddParentLiteral(ConstraintClause, clause_FirstLitIndex());
clause_SetFromClauseDeletion(ConstraintClause);
clause_InsertFlatIntoIndex(ConstraintClause, Index);
ApproxUsableList = list_List(ConstraintClause);
ApproxWOList = list_Nil();
/* fputs("\nConstraint clause: ",stdout); clause_Print(ConstraintClause); */
/* Now the lists are initialized, the subproof is started: */
EmptyClauses = list_Nil();
Count = 0;
if (flag_GetFlagValue(Flags, flag_DOCSST)) {
puts("\n*************** Static Soft Typing Subproof: ***************");
puts("The usable list:");
clause_ListPrint(ApproxUsableList);
puts("\nThe worked-off list:");
clause_ListPrint(ApproxWOList);
/* fputs("\nAll indexed clauses: ", stdout);
clause_PrintAllIndexedClauses(ShIndex); */
}
while (!list_Empty(ApproxUsableList) && list_Empty(EmptyClauses)) {
GivenClause = list_Car(ApproxUsableList);
clause_SetFlag(GivenClause,WORKEDOFF);
if (flag_GetFlagValue(Flags, flag_DOCSST)) {
fputs("\n\tSubproof Given clause: ", stdout);
clause_Print(GivenClause); fflush(stdout);
}
ApproxWOList = list_Cons(GivenClause, ApproxWOList);
ApproxUsableList = list_PointerDeleteOneElement(ApproxUsableList,GivenClause);
ApproxDerivables = red_CDDerivables(Theory,GivenClause, Flags, Precedence);
ApproxDerivables = split_ExtractEmptyClauses(ApproxDerivables, &EmptyClauses);
if (!list_Empty(EmptyClauses)) { /* Exit while loop! */
if (flag_GetFlagValue(Flags, flag_DOCSST)) {
fputs("\nStatic Soft Typing not successful: ", stdout);
clause_Print(list_Car(EmptyClauses));
}
clause_DeleteClauseList(ApproxDerivables);
ApproxDerivables = list_Nil();
}
else {
CLAUSE DerClause;
for (Scan = ApproxDerivables; !list_Empty(Scan) && list_Empty(EmptyClauses);
Scan = list_Cdr(Scan)) {
DerClause = (CLAUSE)list_Car(Scan);
if (red_CDReduce(Theory, DerClause, Flags, Precedence,
&ApproxUsableList, &ApproxWOList, Index))
clause_Delete(DerClause);
else{
Count++;
if (flag_GetFlagValue(Flags, flag_DOCSST)) {
putchar('\n');
clause_Print(DerClause);
}
if (clause_IsEmptyClause(DerClause))
EmptyClauses = list_Cons(DerClause,EmptyClauses);
}
list_Rplaca(Scan,(CLAUSE)NULL);
}
if (!list_Empty(EmptyClauses)) {
if (flag_GetFlagValue(Flags, flag_DOCSST)) {
fputs(" Static Soft Typing not successful!", stdout);
clause_Print(list_Car(EmptyClauses));
}
clause_DeleteClauseList(ApproxDerivables); /* There still may be clauses in the list */
ApproxDerivables = list_Nil();
}
else {
list_Delete(ApproxDerivables);
ApproxDerivables = list_Nil();
}
}
}
if (!list_Empty(EmptyClauses)) {
if (flag_GetFlagValue(Flags, flag_DOCSST)) {
puts("\nStatic Soft Typing failed, constraint solvable.");
puts("************ Static Soft Typing Subproof finished. ************");
}
}
else
if (flag_GetFlagValue(Flags, flag_PSST)) {
fputs("\nStatic Soft Typing deleted: ", stdout);
clause_Print(RedClause);
}
/* Cleanup */
clause_DeleteClauseListFlatFromIndex(ApproxUsableList, Index);
clause_DeleteClauseListFlatFromIndex(ApproxWOList, Index);
st_IndexDelete(Index);
clause_SetCounter(OldClauseCounter);
if (!list_Empty(EmptyClauses)) {
clause_DeleteClauseList(EmptyClauses);
return FALSE;
}
return TRUE;
#ifdef CHECK
clause_Check(RedClause, Flags, Precedence);
#endif
}
return FALSE;
}
LIST red_SatUnit(PROOFSEARCH Search, LIST ClauseList)
/*********************************************************
INPUT: A proof search object and a list of unshared clauses.
RETURNS: A possibly empty list of empty clauses.
EFFECT: Does a shallow saturation of the conclauses depending on the
flag_SATUNIT flag.
The <DocProof> flag is considered.
**********************************************************/
{
CLAUSE Given,Clause;
LIST Scan, Derivables, EmptyClauses, BackReduced;
NAT n, Derived;
FLAGSTORE Flags;
PRECEDENCE Precedence;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
Derived = flag_GetFlagValue(Flags, flag_CNFPROOFSTEPS);
EmptyClauses = list_Nil();
ClauseList = clause_ListSortWeighed(ClauseList);
while (!list_Empty(ClauseList) && list_Empty(EmptyClauses)) {
Given = (CLAUSE)list_NCar(&ClauseList);
Given = red_ReductionOnDerivedClause(Search, Given, red_USABLE);
if (Given) {
if (clause_IsEmptyClause(Given))
EmptyClauses = list_List(Given);
else {
BackReduced = red_BackReduction(Search, Given, red_USABLE);
if (Derived != 0) {
Derivables = inf_BoundedDepthUnitResolution(Given,
prfs_UsableSharingIndex(Search),
FALSE, Flags, Precedence);
n = list_Length(Derivables);
if (n > Derived)
Derived = 0;
else
Derived = Derived - n;
}
else
Derivables = list_Nil();
Derivables = list_Nconc(BackReduced,Derivables);
Derivables = split_ExtractEmptyClauses(Derivables, &EmptyClauses);
prfs_InsertUsableClause(Search, Given);
for(Scan = Derivables; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
Clause = (CLAUSE)list_Car(Scan);
clause_SetDepth(Clause,0);
}
ClauseList = list_Nconc(ClauseList,Derivables);
Derivables = list_Nil();
}
}
}
for(Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan))
prfs_InsertUsableClause(Search, list_Car(Scan));
list_Delete(ClauseList);
return EmptyClauses;
}
static CLAUSE red_SpecialInputReductions(CLAUSE Clause, FLAGSTORE Flags,
PRECEDENCE Precedence)
/*********************************************************
INPUT: A clause and a flag store.
RETURNS: The clause where the logical constants TRUE, FALSE
are removed.
EFFECT: The clause is destructively changed.
**********************************************************/
{
int i,end;
LIST Indexes;
TERM Atom;
#ifdef CHECK
clause_Check(Clause, Flags, Precedence);
#endif
Indexes = list_Nil();
end = clause_LastAntecedentLitIndex(Clause);
for (i = clause_FirstConstraintLitIndex(Clause); i <= end; i++) {
Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i));
if (fol_IsTrue(Atom))
Indexes = list_Cons((POINTER)i,Indexes);
}
end = clause_LastSuccedentLitIndex(Clause);
for (i = clause_FirstSuccedentLitIndex(Clause); i <= end; i++) {
Atom = clause_LiteralAtom(clause_GetLiteral(Clause,i));
if (fol_IsFalse(Atom))
Indexes = list_Cons((POINTER)i,Indexes);
}
clause_DeleteLiterals(Clause,Indexes, Flags, Precedence);
list_Delete(Indexes);
return Clause;
}
LIST red_ReduceInput(PROOFSEARCH Search, LIST ClauseList)
/*********************************************************
INPUT: A proof search object and a list of unshared clauses.
RETURNS: A list of empty clauses.
EFFECT: Interreduces the clause list and inserts the clauses into <Search>.
Keeps track of derived and kept clauses.
Time limits and the DocProof flag are considered.
**********************************************************/
{
CLAUSE Given;
LIST Scan, EmptyClauses, BackReduced;
FLAGSTORE Flags;
PRECEDENCE Precedence;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
EmptyClauses = list_Nil();
ClauseList = clause_ListSortWeighed(list_Copy(ClauseList));
ClauseList = split_ExtractEmptyClauses(ClauseList, &EmptyClauses);
while (!list_Empty(ClauseList) && list_Empty(EmptyClauses) &&
(flag_GetFlagValue(Flags,flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED ||
flag_GetFlagValue(Flags, flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) {
Given = (CLAUSE)list_NCar(&ClauseList);
#ifdef CHECK
if (!clause_IsClause(Given, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_ReduceInput :");
misc_ErrorReport(" Illegal input.\n");
misc_FinishErrorReport();
}
#endif
Given = red_SpecialInputReductions(Given, Flags, Precedence);
Given = red_ReductionOnDerivedClause(Search, Given, red_USABLE);
if (Given) {
prfs_IncKeptClauses(Search);
if (clause_IsEmptyClause(Given))
EmptyClauses = list_List(Given);
else {
BackReduced = red_BackReduction(Search, Given, red_USABLE);
prfs_IncDerivedClauses(Search, list_Length(BackReduced));
BackReduced = split_ExtractEmptyClauses(BackReduced, &EmptyClauses);
prfs_InsertUsableClause(Search, Given);
BackReduced = clause_ListSortWeighed(BackReduced);
ClauseList = red_MergeClauseListsByWeight(ClauseList, BackReduced);
}
}
}
for(Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan))
prfs_InsertUsableClause(Search, list_Car(Scan));
list_Delete(ClauseList);
return EmptyClauses;
}
LIST red_SatInput(PROOFSEARCH Search)
/*********************************************************
INPUT: A proof search object.
RETURNS: A list of derived empty clauses.
EFFECT: Does a saturation from the conjectures into the axioms/conjectures
Keeps track of derived and kept clauses. Keeps track of a possible
time limit.
Considers the Usable clauses in <Search> and a possible time limit.
**********************************************************/
{
CLAUSE Given;
LIST Scan, ClauseList, Derivables, EmptyClauses;
int n;
FLAGSTORE Flags;
PRECEDENCE Precedence;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
EmptyClauses = list_Nil();
ClauseList = list_Nil();
Scan = prfs_UsableClauses(Search);
n = list_Length(Scan);
while(!list_Empty(Scan) &&
n > 0 &&
(flag_GetFlagValue(Flags,flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED ||
flag_GetFlagValue(Flags, flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) {
Given = (CLAUSE)list_Car(Scan);
if (clause_GetFlag(Given,CONCLAUSE)) {
Derivables = inf_BoundedDepthUnitResolution(Given,
prfs_UsableSharingIndex(Search),
FALSE, Flags, Precedence);
n -= list_Length(Derivables);
ClauseList = list_Nconc(Derivables,ClauseList);
}
Scan = list_Cdr(Scan);
}
prfs_IncDerivedClauses(Search, list_Length(ClauseList));
EmptyClauses = red_ReduceInput(Search, ClauseList);
list_Delete(ClauseList);
ClauseList = list_Nil();
if (list_Empty(EmptyClauses)) {
Scan=prfs_UsableClauses(Search);
while (!list_Empty(Scan) &&
n > 0 &&
(flag_GetFlagValue(Flags,flag_TIMELIMIT)==flag_TIMELIMITUNLIMITED ||
flag_GetFlagValue(Flags, flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) {
Given = (CLAUSE)list_Car(Scan);
if (clause_GetFlag(Given,CONCLAUSE) && clause_IsFromInput(Given)) {
Derivables = inf_BoundedDepthUnitResolution(Given,
prfs_UsableSharingIndex(Search),
TRUE, Flags, Precedence);
n -= list_Length(Derivables);
ClauseList = list_Nconc(Derivables,ClauseList);
}
Scan = list_Cdr(Scan);
}
prfs_IncDerivedClauses(Search, list_Length(ClauseList));
EmptyClauses = red_ReduceInput(Search, ClauseList);
list_Delete(ClauseList);
}
return EmptyClauses;
}
void red_CheckSplitSubsumptionCondition(PROOFSEARCH Search)
/*********************************************************
INPUT: A proof search object.
EFFECT: For all deleted clauses in the split stack, it
is checked whether they are subsumed by some
existing clause. If they are not, a core is dumped.
Used for debugging.
**********************************************************/
{
LIST Scan1,Scan2;
CLAUSE Clause;
FLAGSTORE Flags;
PRECEDENCE Precedence;
Flags = prfs_Store(Search);
Precedence = prfs_Precedence(Search);
for (Scan1=prfs_SplitStack(Search);!list_Empty(Scan1);Scan1=list_Cdr(Scan1))
for (Scan2=prfs_SplitDeletedClauses(list_Car(Scan1));!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) {
Clause = (CLAUSE)list_Car(Scan2);
if (!red_ForwardSubsumer(Clause, prfs_WorkedOffSharingIndex(Search),
Flags, Precedence) &&
!red_ForwardSubsumer(Clause, prfs_UsableSharingIndex(Search),
Flags, Precedence) &&
!red_ClauseDeletion(prfs_StaticSortTheory(Search),Clause,
Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In red_CheckSplitSubsumptionCondition: No clause found implying ");
clause_Print(Clause);
misc_ErrorReport("\n Current Split: ");
prfs_PrintSplit(list_Car(Scan1));
misc_FinishErrorReport();
}
}
}