Core inference unit tests

.github/workflows/coverage.yml

@@ -42,6 +42,6 @@ jobs:
       with:
         name: vcoverage-${{ github.sha }}
         path: |
-          ${{ runner.workspace }}/vampire/build/vcoverage/*.html
+          ${{ runner.workspace }}/vampire/build/vcoverage/*
         overwrite: true
         if-no-files-found: error

Inferences/EqualityFactoring.cpp

@@ -40,9 +40,8 @@ using namespace Indexing;
 using namespace Saturation;
 using std::pair;
 
-EqualityFactoring::EqualityFactoring()
-  : _abstractionOracle(AbstractionOracle::createOnlyHigherOrder())
-  , _uwaFixedPointIteration(env.options->unificationWithAbstractionFixedPointIteration())
+EqualityFactoring::EqualityFactoring(Options::UnificationWithAbstraction uwa, bool uwaFixedPointIteration)
+  : _abstractionOracle(uwa), _uwaFixedPointIteration(uwaFixedPointIteration)
 {
 
 }

Inferences/EqualityFactoring.hpp

@@ -18,6 +18,8 @@
 
 #include "Forwards.hpp"
 
+#include "Kernel/UnificationWithAbstraction.hpp"
+
 #include "InferenceEngine.hpp"
 #include "ProofExtra.hpp"
 
@@ -31,7 +33,7 @@ class EqualityFactoring
 : public GeneratingInferenceEngine
 {
 public:
-  EqualityFactoring();
+  EqualityFactoring(Options::UnificationWithAbstraction uwa, bool uwaFixedPointIteration);
   ClauseIterator generateClauses(Clause* premise) override;
 private:
   struct IsPositiveEqualityFn;

Inferences/InferenceEngine.hpp

@@ -275,17 +275,6 @@ class BackwardSimplificationEngine
   virtual void perform(Clause* premise, BwSimplificationRecordIterator& simplifications) = 0;
 };
 
-
-class DummyGIE
-: public GeneratingInferenceEngine
-{
-public:
-  ClauseIterator generateClauses(Clause* premise) override
-  {
-    return ClauseIterator::getEmpty();
-  }
-};
-
 template<class... Args>
 class TupleISE
 : public ImmediateSimplificationEngine

Inferences/InnerRewriting.cpp

@@ -15,33 +15,31 @@
 #include "InnerRewriting.hpp"
 
 #include "Kernel/EqHelper.hpp"
-#include "Kernel/Inference.hpp"
-
-#include "Saturation/SaturationAlgorithm.hpp"
+#include "Kernel/Clause.hpp"
+#include "Lib/Environment.hpp"
+#include "Shell/Statistics.hpp"
 
 namespace Inferences {
 
 using namespace Lib;
 using namespace Kernel;
 
-bool InnerRewriting::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises)
+Clause* InnerRewriting::simplify(Clause* cl)
 {
-  Ordering& ordering = _salg->getOrdering();
-
   // look for the first equality which rewrites something and rewrite everything with it (check for EqTaut as you go)
   unsigned len = cl->length();
   for (unsigned i = 0; i < len; i++) {
     Literal* rwLit=(*cl)[i];
     TermList lhs, rhs;
-    if (rwLit->isEquality() && rwLit->isNegative() && EqHelper::hasGreaterEqualitySide(rwLit,ordering,lhs,rhs)) {
+    if (rwLit->isEquality() && rwLit->isNegative() && EqHelper::hasGreaterEqualitySide(rwLit,_ord,lhs,rhs)) {
       for (unsigned j = 0; j < len; j++) {
         if (i != j) {
           Literal* lit = (*cl)[j];
           Literal* nLit = EqHelper::replace(lit,lhs,rhs);
           if (nLit != lit) {
             if(EqHelper::isEqTautology(nLit)) {
               env.statistics->innerRewritesToEqTaut++;
-              return true;
+              return nullptr;
             }
 
             RStack<Literal*> resLits;
@@ -58,22 +56,20 @@ bool InnerRewriting::perform(Clause* cl, Clause*& replacement, ClauseIterator& p
                 Literal* rLit = EqHelper::replace(oLit,lhs,rhs);
                 if(EqHelper::isEqTautology(rLit)) {
                   env.statistics->innerRewritesToEqTaut++;
-                  return true;
+                  return nullptr;
                 }
                 resLits->push(rLit);
               }
             }
 
-            replacement = Clause::fromStack(*resLits,SimplifyingInference1(InferenceRule::INNER_REWRITING, cl));
-            return true;
+            return Clause::fromStack(*resLits,SimplifyingInference1(InferenceRule::INNER_REWRITING, cl));
           }
         }
       }
     }
   }
 
-  return false;
+  return cl;
 }
 
-
 }

Inferences/InnerRewriting.hpp

@@ -26,10 +26,15 @@ using namespace Kernel;
 using namespace Saturation;
 
 class InnerRewriting
-: public ForwardSimplificationEngine
+: public ImmediateSimplificationEngine
 {
 public:
-  bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override;
+  InnerRewriting(const Ordering& ord) : _ord(ord) {}
+
+  Clause* simplify(Clause* cl) override;
+
+private:
+  const Ordering& _ord;
 };
 
 };

Inferences/Superposition.cpp

@@ -171,7 +171,7 @@ bool Superposition::checkClauseColorCompatibility(Clause* eqClause, Clause* rwCl
  *
  * This function checks that we don't perform superpositions from
  * variables that occur in the remaining part of the clause either in
- * a literal which is not an equality, or in a as an argument of a function.
+ * a literal which is not an equality, or as an argument of a function.
  * Such situation would mean that there is no ground substitution in which
  * @c eqLHS would be the larger argument of the largest literal.
  */
@@ -189,10 +189,10 @@ bool Superposition::checkSuperpositionFromVariable(Clause* eqClause, Literal* eq
     }
     if(lit->isEquality()) {
       for(unsigned aIdx=0; aIdx<2; aIdx++) {
-	TermList arg = *lit->nthArgument(aIdx);
-	if(arg.isTerm() && arg.containsSubterm(eqLHS)) {
-	  return false;
-	}
+        TermList arg = *lit->nthArgument(aIdx);
+        if(arg.isTerm() && arg.containsSubterm(eqLHS)) {
+          return false;
+        }
       }
     }
     else if(lit->containsSubterm(eqLHS)) {

Inferences/URResolution.cpp

@@ -39,10 +39,6 @@ using namespace Kernel;
 using namespace Indexing;
 using namespace Saturation;
 
-template<bool synthesis>
-URResolution<synthesis>::URResolution(bool full)
-: _full(full), _selectedOnly(false) {}
-
 template<bool synthesis>
 void URResolution<synthesis>::attach(SaturationAlgorithm* salg)
 {
@@ -53,6 +49,7 @@ void URResolution<synthesis>::attach(SaturationAlgorithm* salg)
 
   Options::URResolution optSetting = _salg->getOptions().unitResultingResolution();
   ASS_NEQ(optSetting,  Options::URResolution::OFF);
+  _full = optSetting==Options::URResolution::FULL;
   _emptyClauseOnly = optSetting==Options::URResolution::EC_ONLY;
 }
 

Inferences/URResolution.hpp

@@ -32,8 +32,6 @@ class URResolution
 : public GeneratingInferenceEngine
 {
 public:
-  URResolution(bool full);
-
   void attach(SaturationAlgorithm* salg) override;
   void detach() override;
 
@@ -51,7 +49,7 @@ class URResolution
 
   bool _full;
   bool _emptyClauseOnly;
-  bool _selectedOnly;
+  bool _selectedOnly = false;
   using UnitIndexType = std::conditional_t<synthesis, UnitClauseWithALLiteralIndex, UnitClauseLiteralIndex>;
   using NonUnitIndexType = std::conditional_t<synthesis, NonUnitClauseWithALLiteralIndex, NonUnitClauseLiteralIndex>;
   std::shared_ptr<UnitIndexType> _unitIndex;

Saturation/SaturationAlgorithm.cpp

@@ -257,6 +257,12 @@ SaturationAlgorithm::SaturationAlgorithm(Problem& prb, const Options& opt)
     _extensionality = 0;
   }
 
+  if (opt.splitting()) {
+    _splitter = new Splitter();
+  }
+
+  _partialRedundancyHandler.reset(PartialRedundancyHandler::create(opt, _ordering.ptr(), _splitter));
+
   s_instance = this;
 }
 
@@ -1437,10 +1443,6 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
     NOT_IMPLEMENTED;
   }
 
-  if (opt.splitting()) {
-    res->_splitter = new Splitter();
-  }
-
   // create generating inference engine
   CompositeGIE *gie = new CompositeGIE();
 
@@ -1463,7 +1465,7 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
 
   if (mayHaveEquality) {
     if (!alascaTakesOver) { // in alasca we have a special equality factoring rule
-      gie->addFront(new EqualityFactoring());
+      gie->addFront(new EqualityFactoring(AbstractionOracle::createOnlyHigherOrder(), opt.unificationWithAbstractionFixedPointIteration()));
     }
     gie->addFront(new EqualityResolution());
     if(env.options->superposition() && !alascaTakesOver){ // in alasca we have a special superposition rule
@@ -1484,9 +1486,9 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
   }
   if (opt.unitResultingResolution() != Options::URResolution::OFF) {
     if (env.options->questionAnswering() == Options::QuestionAnsweringMode::SYNTHESIS) {
-      gie->addFront(new URResolution</*synthesis=*/true>(opt.unitResultingResolution() == Options::URResolution::FULL));
+      gie->addFront(new URResolution</*synthesis=*/true>());
     } else {
-      gie->addFront(new URResolution</*synthesis=*/false>(opt.unitResultingResolution() == Options::URResolution::FULL));
+      gie->addFront(new URResolution</*synthesis=*/false>());
     }
   }
   if (opt.extensionalityResolution() != Options::ExtensionalityResolution::OFF) {
@@ -1609,9 +1611,6 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
   // create simplification engine
 
   // create forward simplification engine
-  if (mayHaveEquality && opt.innerRewriting()) {
-    res->addForwardSimplifierToFront(new InnerRewriting());
-  }
   if (opt.globalSubsumption()) {
     res->addForwardSimplifierToFront(new GlobalSubsumption(opt));
   }
@@ -1693,8 +1692,6 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const
     res->_symEl = new SymElOutput();
   }
 
-  res->_partialRedundancyHandler.reset(PartialRedundancyHandler::create(opt, &ordering, res->_splitter));
-
   res->_answerLiteralManager = AnswerLiteralManager::getInstance(); // selects the right one, according to options!
   ASS(!res->_answerLiteralManager||opt.questionAnswering()!=Options::QuestionAnsweringMode::OFF);
   ASS( res->_answerLiteralManager||opt.questionAnswering()==Options::QuestionAnsweringMode::OFF);
@@ -1711,6 +1708,12 @@ std::pair<CompositeISE*, CompositeISEMany> SaturationAlgorithm::createISE(Proble
 
   bool mayHaveEquality = couldEqualityArise(prb,opt);
 
+  // InnerRewriting is relatively expensive, so let's insert it first,
+  // so that it gets applied as the last ImmediateSimplification
+  if (mayHaveEquality && opt.innerRewriting()) {
+    res->addFront(new InnerRewriting(ordering));
+  }
+
   if (mayHaveEquality && opt.equationalTautologyRemoval()) {
     res->addFront(new EquationalTautologyRemoval());
   }
@@ -1803,5 +1806,6 @@ std::pair<CompositeISE*, CompositeISEMany> SaturationAlgorithm::createISE(Proble
     // Note: SynthesisAnswerLiteralProcessor must be THE LAST added simplification-many rule.
     resMany.addFront(std::make_unique<SynthesisAnswerLiteralProcessor>());
   }
+
   return std::make_pair(res, std::move(resMany));
 }