coroutines for clause generation

Inferences/Factoring.cpp

@@ -31,89 +31,6 @@
 namespace Inferences
 {
 
-/**
- * This functor given a pair of literal indices
- * removes the second literal from the clause specified in constructor,
- * applies the substitution, and returns resulting clause.
- * (Also it records this to statistics as factoring.)
- */
-class Factoring::ResultsFn
-{
-public:
-  ResultsFn(Clause* cl, bool afterCheck, LiteralSelector &sel, Ordering& ord)
-  : _cl(cl), _cLen(cl->length()), _afterCheck(afterCheck), _sel(sel), _ord(ord) {}
-  Clause* operator() (std::pair<unsigned,unsigned> nums)
-  {
-    Literal* l1 = (*_cl)[nums.first];
-    Literal* l2 = (*_cl)[nums.second];
-
-    //we assume there are no duplicate literals
-    ASS(l1!=l2);
-
-    if(l1->isEquality())
-      //We don't perform factoring with equalities
-      return nullptr;
-
-    // check polarity and functor matches
-    if(!Literal::headersMatch(l1, l2, false))
-      return nullptr;
-
-    if(_sel.isNegativeForSelection(l1)) {
-      //We don't perform factoring on negative literals
-      // (this check only becomes relevant, when there is more than one literal selected
-      // and yet the selected ones are not all positive -- see the check in generateClauses)
-      return nullptr;
-    }
-
-    subst.reset();
-    if(!subst.unify(TermList(l1), 0, TermList(l2), 0))
-      return nullptr;
-
-    RStack<Literal*> resLits;
-
-    Literal *skipped = l2;
-
-    Literal* skippedAfter = 0;
-    if (_afterCheck && _cl->numSelected() > 1) {
-      TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
-
-      skippedAfter = subst.apply(skipped, 0);
-    }
-
-    for(unsigned i=0;i<_cLen;i++) {
-      Literal* curr=(*_cl)[i];
-      if(curr!=skipped) {
-        Literal* currAfter = subst.apply(curr, 0);
-
-        if (skippedAfter) {
-          TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
-
-          if (i < _cl->numSelected() && _ord.compare(currAfter,skippedAfter) == Ordering::GREATER) {
-            env.statistics->inferencesBlockedDueToOrderingAftercheck++;
-            return nullptr;
-          }
-        }
-
-        resLits->push(currAfter);
-      }
-    }
-
-    Clause *cl = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::FACTORING,_cl));
-    if(env.options->proofExtra() == Options::ProofExtra::FULL)
-      env.proofExtra.insert(cl, new FactoringExtra(l1, l2));
-    return cl;
-  }
-private:
-  static RobSubstitution subst;
-  Clause* _cl;
-  ///length of the premise clause
-  unsigned _cLen;
-  bool _afterCheck;
-  LiteralSelector& _sel;
-  Ordering& _ord;
-};
-RobSubstitution Factoring::ResultsFn::subst;
-
 /**
  * Return ClauseIterator, that yields clauses generated from
  * @b premise by the factoring inference rule.
@@ -132,22 +49,99 @@ RobSubstitution Factoring::ResultsFn::subst;
  */
 ClauseIterator Factoring::generateClauses(Clause* premise)
 {
+  // bail out before even creating a coroutine frame
   if(premise->length()<=1) {
     return ClauseIterator::getEmpty();
   }
   if(premise->numSelected()==1 && _salg.getLiteralSelector().isNegativeForSelection((*premise)[0])) {
     return ClauseIterator::getEmpty();
   }
 
-  auto it1 = getCombinationIterator(0u,premise->numSelected(),premise->length());
+  return pvi(factorings(premise));
+}
 
-  auto it2 = getMappingIterator(it1,ResultsFn(premise,
-      _salg.getOptions().literalMaximalityAftercheck() && _salg.getLiteralSelector().isBGComplete(),
-      _salg.getLiteralSelector(), _salg.getOrdering()));
+/**
+ * For each unordered pair of literals of @b premise with at least one of them selected,
+ * unify them, drop the second, apply the substitution to the rest, and yield the result.
+ */
+Generator<Clause*> Factoring::factorings(Clause* premise)
+{
+  LiteralSelector& sel = _salg.getLiteralSelector();
+  const Ordering& ord = _salg.getOrdering();
+  bool afterCheck = _salg.getOptions().literalMaximalityAftercheck() && sel.isBGComplete();
+  unsigned cLen = premise->length();
+
+  RobSubstitution subst;
+
+  for(unsigned fst=0; fst<premise->numSelected(); fst++) {
+    Literal* l1 = (*premise)[fst];
+
+    //We don't perform factoring with equalities
+    if(l1->isEquality())
+      continue;
+
+    //We don't perform factoring on negative literals
+    // (this check only becomes relevant, when there is more than one literal selected
+    // and yet the selected ones are not all positive -- see the check in generateClauses)
+    if(sel.isNegativeForSelection(l1))
+      continue;
+
+    for(unsigned snd=fst+1; snd<cLen; snd++) {
+      Literal* skipped = (*premise)[snd];
+
+      //we assume there are no duplicate literals
+      ASS(l1!=skipped);
+
+      // check polarity and functor matches
+      if(!Literal::headersMatch(l1, skipped, false))
+        continue;
+
+      subst.reset();
+      if(!subst.unify(TermList(l1), 0, TermList(skipped), 0))
+        continue;
+
+      Clause* factor;
+      {
+        RStack<Literal*> resLits;
+
+        Literal* skippedAfter = 0;
+        if (afterCheck && premise->numSelected() > 1) {
+          TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
+
+          skippedAfter = subst.apply(skipped, 0);
+        }
+
+        bool blocked = false;
+        for(unsigned i=0;i<cLen;i++) {
+          Literal* curr=(*premise)[i];
+          if(curr!=skipped) {
+            Literal* currAfter = subst.apply(curr, 0);
 
-  auto it3 = getFilteredIterator(it2, NonzeroFn());
+            if (skippedAfter) {
+              TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
 
-  return pvi( it3 );
+              if (i < premise->numSelected() && ord.compare(currAfter,skippedAfter) == Ordering::GREATER) {
+                env.statistics->inferencesBlockedDueToOrderingAftercheck++;
+                blocked = true;
+                break;
+              }
+            }
+
+            resLits->push(currAfter);
+          }
+        }
+        if(blocked)
+          continue;
+
+        factor = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::FACTORING,premise));
+      }
+
+      if(env.options->proofExtra() == Options::ProofExtra::FULL)
+        env.proofExtra.insert(factor, new FactoringExtra(l1, skipped));
+
+      co_yield factor;
+    }
+  }
 }
 
 }

Inferences/Factoring.hpp

@@ -17,6 +17,7 @@
 #define __Factoring__
 
 #include "Forwards.hpp"
+#include "Lib/Generator.hpp"
 
 #include "InferenceEngine.hpp"
 #include "ProofExtra.hpp"
@@ -30,7 +31,9 @@ class Factoring
   Factoring(SaturationAlgorithm& salg) : _salg(salg) {}
   ClauseIterator generateClauses(Kernel::Clause* premise) override;
 private:
-  class ResultsFn;
+  /** every factor of @b premise, yielded lazily */
+  Lib::Generator<Kernel::Clause*> factorings(Kernel::Clause* premise);
+
   const SaturationAlgorithm& _salg;
 };
 

Inferences/Superposition.cpp

@@ -17,7 +17,6 @@
 #include "Forwards.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Metaiterators.hpp"
-#include "Lib/PairUtils.hpp"
 #include "Lib/Recycled.hpp"
 #include "Lib/VirtualIterator.hpp"
 
@@ -50,7 +49,6 @@ using namespace Lib;
 using namespace Kernel;
 using namespace Indexing;
 using namespace Saturation;
-using std::pair;
 
 namespace Inferences {
 
@@ -64,60 +62,53 @@ Superposition<higherOrder>::Superposition(SaturationAlgorithm& salg)
 template<bool higherOrder>
 ClauseIterator Superposition<higherOrder>::generateClauses(Clause* premise)
 {
-  auto itf = premise->getSelectedLiteralIterator()
-    // Get an iterator of pairs of selected literals and rewritable subterms of those literals
-    // A subterm is rewritable (see EqHelper) if it is a non-variable subterm of either
-    // a maximal side of an equality or of a non-equational literal
-    .flatMap([this](Literal* lit)
-      // returns an iterator over the rewritable subterms
-      { return pushPairIntoRightIterator(lit, EqHelper::getSubtermIterator<higherOrder>(lit, _salg.getOrdering())); })
-
-    // Get clauses with a literal whose complement unifies with the rewritable subterm,
-    // returns a pair with the original pair and the unification result (includes substitution)
-    .flatMap([this](pair<Literal*, TypedTermList> arg)
-      { return pushPairIntoRightIterator(arg, _lhsIndex->getUwa<higherOrder>(arg.second, _salg.getOptions())); })
-
-    // Perform forward superposition
-    .map([this,premise](pair<pair<Literal*, TypedTermList>, QueryRes<AbstractingUnifier*, TermLiteralClause>> arg)
-      {
-        auto& qr = arg.second;
-        return performSuperposition(premise, arg.first.first, arg.first.second,
-	        qr.data->clause, qr.data->literal, qr.data->term, qr.unifier, true);
-      });
-
-  auto itb = premise->getSelectedLiteralIterator()
-    // Get LHSs of all selected positive literals for superposition
-    .flatMap([this](Literal* lit)
-      { return pvi( pushPairIntoRightIterator(lit, EqHelper::getSuperpositionLHSIterator(lit, _salg.getOrdering(), _salg.getOptions())) ); })
-
-    // Get clauses that unify with these LHSs, modulo abstraction
-    .flatMap([this] (pair<Literal*, TermList> arg)
-      { return pushPairIntoRightIterator(arg,
-          _subtermIndex->template getUwa<higherOrder>(TypedTermList(arg.second, SortHelper::getEqualityArgumentSort(arg.first)), _salg.getOptions())); })
-
-    // Perform backward superposition
-    .map([this,premise](pair<pair<Literal*, TermList>, QueryRes<AbstractingUnifier*, TermLiteralClause>> arg) -> Clause*
-    {
-      // Self-superpositions are only done in forwards mode
-      if (premise == arg.second.data->clause) {
-        return nullptr;
-      }
-
-      auto& qr = arg.second;
-      return performSuperposition(qr.data->clause, qr.data->literal, qr.data->term,
-        premise, arg.first.first, arg.first.second, qr.unifier, false);
-    });
-
-  // Add the results of forward and backward together
-  auto it1 = concatIters(std::move(itf),std::move(itb));
-
-  // Remove null elements - these can come from performSuperposition
-  auto it2 = getFilteredIterator(std::move(it1),NonzeroFn());
+  // the outer iterator ensures we update the time counter for superposition
+  return pvi(TIME_TRACE_ITER("superposition", superpositions(premise)));
+}
 
-  // The outer iterator ensures we update the time counter for superposition
-  auto it3 = TIME_TRACE_ITER("superposition", std::move(it2));
+/**
+ * Yield the result of every superposition that can be performed with @b premise as one of
+ * the two parents: first forwards (equations from the index rewrite @b premise), then
+ * backwards (equations of @b premise rewrite clauses from the index).
+ *
+ * @warning @b qr.unifier below aliases state owned by the index query iterator that is
+ * still being walked, and that state is undone as soon as the query iterator is advanced
+ * -- which is exactly what happens when this coroutine is resumed. So the clause must be
+ * built *before* the co_yield; never carry a QueryRes across one.
+ */
+template<bool higherOrder>
+Generator<Clause*> Superposition<higherOrder>::superpositions(Clause* premise)
+{
+  for (Literal* lit : premise->getSelectedLiteralIterator()) {
+    // a subterm is rewritable (see EqHelper) if it is a non-variable subterm of either
+    // a maximal side of an equality or of a non-equational literal
+    for (Term* rw : iterTraits(EqHelper::getSubtermIterator<higherOrder>(lit, _salg.getOrdering()))) {
+      TypedTermList rwTerm(rw);
+      // clauses with a literal whose complement unifies with the rewritable subterm,
+      // modulo abstraction
+      for (auto qr : iterTraits(_lhsIndex->template getUwa<higherOrder>(rwTerm, _salg.getOptions())))
+        if (Clause* generated = performSuperposition(premise, lit, rwTerm,
+              qr.data->clause, qr.data->literal, qr.data->term, qr.unifier, /*eqIsResult=*/true))
+          co_yield generated;
+    }
+  }
 
-  return pvi( std::move(it3) );
+  for (Literal* lit : premise->getSelectedLiteralIterator()) {
+    // LHSs of the selected positive literals to superpose from
+    for (TermList eqLHS : iterTraits(EqHelper::getSuperpositionLHSIterator(lit, _salg.getOrdering(), _salg.getOptions()))) {
+      TypedTermList query(eqLHS, SortHelper::getEqualityArgumentSort(lit));
+      // clauses that unify with these LHSs, modulo abstraction
+      for (auto qr : iterTraits(_subtermIndex->template getUwa<higherOrder>(query, _salg.getOptions()))) {
+        // self-superpositions are only done in forwards mode
+        if (premise == qr.data->clause)
+          continue;
+
+        if (Clause* generated = performSuperposition(qr.data->clause, qr.data->literal, qr.data->term,
+              premise, lit, eqLHS, qr.unifier, /*eqIsResult=*/false))
+          co_yield generated;
+      }
+    }
+  }
 }
 
 /**

Inferences/Superposition.hpp

@@ -18,6 +18,7 @@
 
 #include "Forwards.hpp"
 #include "Indexing/TermIndex.hpp"
+#include "Lib/Generator.hpp"
 
 #include "InferenceEngine.hpp"
 #include "Inferences/ProofExtra.hpp"
@@ -37,6 +38,9 @@ class Superposition
   ClauseIterator generateClauses(Clause* premise) override;
 
 private:
+  /** every opportunity to superpose with @b premise as a parent, yielded lazily */
+  Generator<Clause*> superpositions(Clause* premise);
+
   Clause* performSuperposition(
     Clause* rwClause, Literal* rwLiteral, TermList rwTerm,
     Clause* eqClause, Literal* eqLiteral, TermList eqLHS,