summaryrefslogtreecommitdiff
path: root/test/spass/rules-red.c
diff options
context:
space:
mode:
Diffstat (limited to 'test/spass/rules-red.c')
-rw-r--r--test/spass/rules-red.c4508
1 files changed, 4508 insertions, 0 deletions
diff --git a/test/spass/rules-red.c b/test/spass/rules-red.c
new file mode 100644
index 0000000..609b3cf
--- /dev/null
+++ b/test/spass/rules-red.c
@@ -0,0 +1,4508 @@
+/**************************************************************/
+/* ********************************************************** */
+/* * * */
+/* * 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: 21527 $ * */
+/* $State$ * */
+/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */
+/* $Author: duraid $ * */
+/* * * */
+/* * 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();
+ }
+ }
+}