Labeled demodulation

Inferences/BackwardDemodulation.cpp

@@ -50,7 +50,7 @@ BackwardDemodulation<higherOrder>::BackwardDemodulation(SaturationAlgorithm& sal
   : _ord(salg.getOrdering()),
     _preordered(salg.getOptions().backwardDemodulation() == Options::Demodulation::PREORDERED),
     _index(salg.getSimplifyingIndex<DemodulationSubtermIndex<higherOrder>>()),
-    _helper(DemodulationHelper(salg.getOptions(), &salg.getOrdering()))
+    _helper(salg.getOptions(), salg.getOrdering())
 {}
 
 namespace {
@@ -127,7 +127,7 @@ struct BackwardDemodulation<higherOrder>::ResultFn
     TermList rhsS=subs->applyToBoundQuery(rhs);
 
     if (_helper.redundancyCheckNeededForPremise(qr.data->clause,qr.data->literal,lhsS) &&
-      !_helper.isPremiseRedundant(qr.data->clause,qr.data->literal,lhsS,rhsS,lhs,&appl))
+      !_helper.isPremiseRedundant(qr.data->clause,qr.data->literal,lhsS,rhsS,_cl,lhs,&appl))
     {
       return BwSimplificationRecord(0);
     }

Inferences/BackwardDemodulation.hpp

@@ -42,7 +42,7 @@ class BackwardDemodulation
   const Ordering& _ord;
   const bool _preordered;
   std::shared_ptr<DemodulationSubtermIndex<higherOrder>> _index;
-  DemodulationHelper _helper;
+  const DemodulationHelper _helper;
 };
 
 using BackwardDemodulationExtra = RewriteInferenceExtra;

Inferences/DemodulationHelper.cpp

@@ -22,9 +22,10 @@ namespace Inferences {
 
 using namespace Kernel;
 
-DemodulationHelper::DemodulationHelper(const Options& opts, const Ordering* ord)
+DemodulationHelper::DemodulationHelper(const Options& opts, const Ordering& ord)
 : _redundancyCheck(opts.demodulationRedundancyCheck() != Options::DemodulationRedundancyCheck::OFF),
-  _encompassing(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS),
+  _labeled(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::LABELED),
+  _encompassing(_labeled || opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS),
   _ord(ord)
 {
 }
@@ -44,18 +45,20 @@ bool DemodulationHelper::redundancyCheckNeededForPremise(Clause* rwCl, Literal*
 }
 
 bool DemodulationHelper::isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermList rwTerm,
-  TermList tgtTerm, TermList eqLHS, const SubstApplicator* eqApplicator) const
+  TermList tgtTerm, Clause* eqCl, TermList eqLHS, const SubstApplicator* eqApplicator) const
 {
   ASS(redundancyCheckNeededForPremise(rwCl, rwLit, rwTerm));
 
   TermList other=EqHelper::getOtherEqualitySide(rwLit, rwTerm);
-  if (_ord->compare(tgtTerm, other) == Ordering::LESS) {
+  auto tord = _ord.compare(tgtTerm, other);
+  if (tord == Ordering::LESS) {
     return true;
   }
 
   if (_encompassing) {
     // under _encompassing, we know there are no other literals in rwCl
-    return !isRenamingOn(eqApplicator,eqLHS);
+    return !isRenamingOn(eqApplicator,eqLHS) ||
+      (_labeled && tord == Ordering::INCOMPARABLE && rwCl->number() > eqCl->number());
   }
 
   // return early to avoid creation of eqLitS
@@ -75,7 +78,7 @@ bool DemodulationHelper::isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermLi
   // Hence we need to check if there are any literals
   // in rwCl greater than eqLitS.
   return rwCl->iterLits().any([rwLit,this,eqLitS](Literal* lit) {
-    return lit != rwLit && _ord->compare(eqLitS, lit)==Ordering::LESS;
+    return lit != rwLit && _ord.compare(eqLitS, lit)==Ordering::LESS;
   });
 }
 

Inferences/DemodulationHelper.hpp

@@ -25,8 +25,7 @@ using namespace Shell;
 
 class DemodulationHelper {
 public:
-  DemodulationHelper() = default;
-  DemodulationHelper(const Options& opts, const Ordering* ord);
+  DemodulationHelper(const Options& opts, const Ordering& ord);
 
   template<typename Object>
   static bool isRenamingOn(const SubstApplicator* applicator, Object obj) {
@@ -53,12 +52,13 @@ class DemodulationHelper {
 
   bool redundancyCheckNeededForPremise(Clause* rwCl, Literal* rwLit, TermList rwTerm) const;
   bool isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermList rwTerm, TermList tgtTerm,
-    TermList eqLHS, const SubstApplicator* applicator) const;
+    Clause* eqCl, TermList eqLHS, const SubstApplicator* applicator) const;
 
 private:
-  bool _redundancyCheck;
-  bool _encompassing;
-  const Ordering* _ord;
+  const bool _redundancyCheck;
+  const bool _labeled;
+  const bool _encompassing;
+  const Ordering& _ord;
 };
 
 };

Inferences/ForwardDemodulation.cpp

@@ -36,8 +36,6 @@
 #include "Shell/Statistics.hpp"
 #include "Debug/TimeProfiling.hpp"
 
-#include "DemodulationHelper.hpp"
-
 #include "ForwardDemodulation.hpp"
 
 namespace Inferences {
@@ -53,7 +51,7 @@ ForwardDemodulation<higherOrder>::ForwardDemodulation(SaturationAlgorithm& salg)
     _encompassing(salg.getOptions().demodulationRedundancyCheck()==Options::DemodulationRedundancyCheck::ENCOMPASS),
     _useTermOrderingDiagrams(salg.getOptions().forwardDemodulationTermOrderingDiagrams()),
     _skipNonequationalLiterals(salg.getOptions().demodulationOnlyEquational()),
-    _helper(DemodulationHelper(salg.getOptions(), &salg.getOrdering())),
+    _helper(salg.getOptions(), salg.getOrdering()),
     _ord(salg.getOrdering()),
     _index(salg.getSimplifyingIndex<DemodulationLHSIndex>())
 {}
@@ -149,7 +147,7 @@ bool ForwardDemodulation<higherOrder>::perform(Clause* cl, Clause*& replacement,
 
         TermList rhsS = rhsApplied.apply();
 
-        if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, lhs, &subs)) {
+        if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, qr.data->clause, lhs, &subs)) {
           continue;
         }
 

Inferences/FunctionDefinitionRewriting.cpp

@@ -46,7 +46,7 @@ Clause* performRewriting(
   // This should be the case for code trees
   TermList tgtTermS = subst->apply(tgtTerm);
 
-  if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqLHS,subst)) {
+  if (helper && !helper->isPremiseRedundant(rwClause,rwLit,rwTerm,tgtTermS,eqClause,eqLHS,subst)) {
     return 0;
   }
 
@@ -92,7 +92,7 @@ Clause* performRewriting(
 }
 
 FunctionDefinitionRewriting::FunctionDefinitionRewriting(SaturationAlgorithm& salg)
-  : _salg(salg), _helper(DemodulationHelper(salg.getOptions(), &salg.getOrdering()))
+  : _salg(salg), _helper(salg.getOptions(), salg.getOrdering())
 {}
 
 Kernel::ClauseIterator FunctionDefinitionRewriting::generateClauses(Clause *premise)
@@ -117,7 +117,7 @@ Kernel::ClauseIterator FunctionDefinitionRewriting::generateClauses(Clause *prem
 }
 
 FunctionDefinitionDemodulation::FunctionDefinitionDemodulation(SaturationAlgorithm& salg)
-  : _ord(salg.getOrdering()), _helper(salg.getOptions(), &_ord), _fnDefHandler(salg.getFunctionDefinitionHandler())
+  : _ord(salg.getOrdering()), _helper(salg.getOptions(), _ord), _fnDefHandler(salg.getFunctionDefinitionHandler())
 {}
 
 bool FunctionDefinitionDemodulation::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises)

Inferences/FunctionDefinitionRewriting.hpp

@@ -47,7 +47,7 @@ class FunctionDefinitionRewriting
 
 private:
   const SaturationAlgorithm& _salg;
-  DemodulationHelper _helper;
+  const DemodulationHelper _helper;
 };
 
 /**

Shell/Options.cpp

@@ -685,14 +685,15 @@ Options::Options ()
        .description = "Perform condensation. If 'fast' is specified, we only perform condensations that are easy to check for.",
        .tag = OptionTag::INFERENCES})
   , _demodulationRedundancyCheck("demodulation_redundancy_check",this,
-       DemodulationRedundancyCheck::ENCOMPASS,{"off","ordering","encompass"},
+       DemodulationRedundancyCheck::ENCOMPASS,{"off","ordering","encompass","labeled"},
       {.short_name = "drc",
        .description = "The following cases of backward and forward demodulation do not preserve completeness:\n"
        "s = t     s = t1 \\/ C \t s = t     s != t1 \\/ C\n"
 
        "--------------------- \t ---------------------\n"
        "t = t1 \\/ C \t\t t != t1 \\/ C\n"
        "where t > t1 and s = t > C (RHS replaced)\n"
+       "With `labeled`, we have `encompass` but we also demodulate one equation with another (equally general but incomparable) equation if one was generated earlier (labeled smaller)."
        "With `encompass`, we treat demodulations (both forward and backward) as encompassment demodulations (as defined by Duarte and Korovin in 2022's IJCAR paper).\n"
        "With `ordering`, we check this condition and don't demodulate if we could violate completeness.\n"
        "With `off`, we skip the checks, save time, but become incomplete.",

Shell/Options.hpp

@@ -463,6 +463,9 @@ class Options
     ENCOMPASS, // (1) positive unit equations (PUE) are smaller than non-PUE clauses,
                // (2) more general PUE are smaller than less general PUE, and
                // (3) equally general PUEs are ordered based on term ordering.
+    LABELED,   // similar to encompass, but a PUE is smaller than another when
+               // they are equally general ordered but incomparable equations
+               // and the label (clause number) is smaller than that of the other.
   };
 
   enum class TheoryAxiomLevel : unsigned int {

Shell/PartialRedundancyHandler.cpp

@@ -523,7 +523,21 @@ bool PartialRedundancyHandlerImpl<enabled, ordC, avatarC, litC>::compareWithSupe
           return true;
         }
         // case 2.b.
-        return checkOrConstrainGreater(_ord->compare(other, tgtTermS), other, tgtTermS, cons);
+        auto tord = _ord->compare(other, tgtTermS);
+        if (_labeled) {
+          switch (tord) {
+            case Ordering::GREATER:
+              return true;
+            case Ordering::EQUAL:
+              return rwCl->number() > eqCl->number();
+            case Ordering::LESS:
+              return false;
+            case Ordering::INCOMPARABLE:
+              return rwCl->number() > eqCl->number() || checkOrConstrainGreater(tord, other, tgtTermS, cons);
+          }
+        } else {
+          return checkOrConstrainGreater(tord, other, tgtTermS, cons);
+        }
       }
       // case 2.c.
       if (!MatchingUtils::matchTerms(rwTerm, eqLHS)) {

Shell/PartialRedundancyHandler.hpp

@@ -127,7 +127,8 @@ class PartialRedundancyHandlerImpl
 public:
   PartialRedundancyHandlerImpl(const Options& opts, const Ordering* ord, Splitter* splitter)
     : _redundancyCheck(opts.demodulationRedundancyCheck() != Options::DemodulationRedundancyCheck::OFF),
-      _encompassing(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS),
+      _labeled(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::LABELED),
+      _encompassing(_labeled || opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS),
       _ord(ord), _splitter(splitter) {}
 
   /** Returns false if superposition should be skipped. */
@@ -155,6 +156,7 @@ class PartialRedundancyHandlerImpl
     LiteralSet&& lits, SplitSet* splits) const;
 
   bool _redundancyCheck;
+  bool _labeled;
   bool _encompassing;
   const Ordering* _ord;
   Splitter* _splitter;

UnitTests/tInferences_Demodulation.cpp

@@ -213,4 +213,22 @@ TEST_SIMPLIFICATION(test19,
     .justifications({ /* nothing */ })
 )
 
+// encompassment does not work with equally general but incomparable equations
+TEST_SIMPLIFICATION(test20,
+  tester()
+    .simplifyWith({ clause({ g(f(x,y)) == f(x,y) }) })
+    .toSimplify({ clause({ g(f(x,y)) == f(y,x) }) })
+    .expected({ /* nothing */ })
+    .justifications({ /* nothing */ });
+)
+
+// labeled demodulates equally general but incomparable equation
+TEST_SIMPLIFICATION(test21,
+  tester()
+    .simplifyWith({ clause({ g(f(x,y)) == f(x,y) }) })
+    .toSimplify({ clause({ g(f(x,y)) == f(y,x) }) })
+    .expected({ clause({ f(x,y) == f(y,x) }) })
+    .options({ { "term_ordering", "lpo" }, { "demodulation_redundancy_check", "labeled" } });
+)
+
 }

samplers/samplerFNT.smp

@@ -156,7 +156,7 @@ sa!=fmb > fd ~cat all:500,off:41,preordered:168
 > $drc ~cat 0:1
 fd!=off > $drc ~cat 1:1
 bd!=off > $drc ~cat 1:1
-sa!=fmb $drc=1 > drc ~cat ordering:643,encompass:554
+sa!=fmb $drc=1 > drc ~cat labeled:500,ordering:643,encompass:554
 
 # forward_demodulation_term_ordering_diagrams
 sa!=fmb fd!=off > fdtod ~cat on:1,off:1

samplers/samplerFOL.smp

@@ -208,8 +208,8 @@ sa!=fmb > fd ~cat all:500,off:41,preordered:168
 > $drc ~cat 0:1
 fd!=off > $drc ~cat 1:1
 bd!=off > $drc ~cat 1:1
-intent=unsat sa!=fmb $drc=1 > drc ~cat encompass:500,ordering:500,off:354
-intent=sat sa!=fmb $drc=1 > drc ~cat ordering:643,encompass:554
+intent=unsat sa!=fmb $drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354
+intent=sat sa!=fmb $drc=1 > drc ~cat labeled:500,ordering:643,encompass:554
 
 # forward_demodulation_term_ordering_diagrams
 sa!=fmb fd!=off > fdtod ~cat on:1,off:1

samplers/samplerHOL.smp

@@ -210,8 +210,8 @@ er!=off > erml ~cat 0:3,2:1,3:1
 > $drc ~cat 0:1
 fd!=off > $drc ~cat 1:1
 bd!=off > $drc ~cat 1:1
-intent=unsat $drc=1 > drc ~cat encompass:500,ordering:500,off:354
-intent=sat $drc=1 > drc ~cat ordering:643,encompass:554
+intent=unsat $drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354
+intent=sat $drc=1 > drc ~cat labeled:500,ordering:643,encompass:554
 
 # forward_demodulation_term_ordering_diagrams
 fd!=off > fdtod ~cat on:1,off:1

samplers/samplerIND.smp

@@ -213,7 +213,7 @@ er!=off > erml ~cat 0:3,2:1,3:1
 > $drc ~cat 0:1
 fd!=off > $drc ~cat 1:1
 bd!=off > $drc ~cat 1:1
-$drc=1 > drc ~cat encompass:500,ordering:500,off:354
+$drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354
 
 # forward_demodulation_term_ordering_diagrams
 fd!=off > fdtod ~cat on:1,off:1

samplers/samplerSMT.smp

@@ -216,7 +216,7 @@ er!=off > erml ~cat 0:3,2:1,3:1
 > $drc ~cat 0:1
 fd!=off > $drc ~cat 1:1
 bd!=off > $drc ~cat 1:1
-$drc=1 > drc ~cat encompass:500,ordering:500,off:354
+$drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354
 
 # forward_demodulation_term_ordering_diagrams
 fd!=off > fdtod ~cat on:1,off:1

samplers/samplerUEQ.smp

@@ -168,7 +168,7 @@ er!=off > erml ~cat 0:3,2:1,3:1
 > $drc ~cat 0:1
 fd!=off > $drc ~cat 1:1
 bd!=off > $drc ~cat 1:1
-$drc=1 > drc ~cat encompass:500,ordering:500,off:354
+$drc=1 > drc ~cat labeled:500,encompass:500,ordering:500,off:354
 
 # forward_demodulation_term_ordering_diagrams
 fd!=off > fdtod ~cat on:1,off:1