Make decision engine independent of AssertionsPipeline (#5626)

This PR makes decision engine independent of AssertionsPipeline, which consequently allows some of the key PropEngine interfaces to be consolidated. It also modifies PropEngine to take TrustNode for assertLemma, which is the first step for making PropEngine manage proofs from TheoryEngine.

This is in preparation for modifying the interplay between PropEngine, TheoryEngine, TheoryPreprocessor, and new proposed SAT relevancy heuristic.

There are no intended behavior changes in this PR.

Marking "major" since this impacts several current directions (including proof-new integration, lazy theory preprocessing, SAT relevancy).

9 files changed, 128 insertions, 68 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 6ebd73a5f..ec8943f4a 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -113,8 +113,9 @@ SatValue DecisionEngine::getPolarity(SatVariable var)
   }
 }
 
-void DecisionEngine::addAssertions(
-    const preprocessing::AssertionPipeline& assertions)
+void DecisionEngine::addAssertions(const std::vector<Node>& assertions,
+                                   const std::vector<Node>& ppLemmas,
+                                   const std::vector<Node>& ppSkolems)
 {
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
@@ -126,7 +127,7 @@ void DecisionEngine::addAssertions(
 
   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
   {
-    d_needIteSkolemMap[i]->addAssertions(assertions);
+    d_needIteSkolemMap[i]->addAssertions(assertions, ppLemmas, ppSkolems);
   }
 }
 
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 52e1e2d1a..afa16397d 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -24,7 +24,6 @@
 #include "base/output.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
-#include "preprocessing/assertion_pipeline.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/sat_solver_types.h"
@@ -142,9 +141,12 @@ class DecisionEngine {
   // External World helping us help the Strategies
 
   /**
-   * Add a list of assertions from an AssertionPipeline.
+   * Add a list of assertions, as well as lemmas coming from preprocessing
+   * (ppLemmas) and pairwise the skolems they constrain (ppSkolems).
    */
-  void addAssertions(const preprocessing::AssertionPipeline& assertions);
+  void addAssertions(const std::vector<Node>& assertions,
+                     const std::vector<Node>& ppLemmas,
+                     const std::vector<Node>& ppSkolems);
 
   // Interface for Strategies to use stuff stored in Decision Engine
   // (which was possibly requested by them on initialization)
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index f7c28299d..ebddc659d 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -19,7 +19,9 @@
 #ifndef CVC4__DECISION__DECISION_STRATEGY_H
 #define CVC4__DECISION__DECISION_STRATEGY_H
 
-#include "preprocessing/assertion_pipeline.h"
+#include <vector>
+
+#include "expr/node.h"
 #include "prop/sat_solver_types.h"
 #include "smt/term_formula_removal.h"
 
@@ -58,8 +60,13 @@ public:
 
   bool needIteSkolemMap() override { return true; }
 
-  virtual void addAssertions(
-      const preprocessing::AssertionPipeline& assertions) = 0;
+  /**
+   * Add a list of assertions, as well as lemmas coming from preprocessing
+   * (ppLemmas) and pairwise the skolems they constrain (ppSkolems).
+   */
+  virtual void addAssertions(const std::vector<Node>& assertions,
+                             const std::vector<Node>& ppLemmas,
+                             const std::vector<Node>& ppSkolems) = 0;
 };/* class ITEDecisionStrategy */
 
 class RelevancyStrategy : public ITEDecisionStrategy {
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index baf0056e9..afbff18c1 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -164,15 +164,14 @@ inline void computeXorIffDesiredValues
   }
 }
 
-void JustificationHeuristic::addAssertions(
-    const preprocessing::AssertionPipeline &assertions)
+void JustificationHeuristic::addAssertions(const std::vector<Node>& assertions,
+                                           const std::vector<Node>& ppLemmas,
+                                           const std::vector<Node>& ppSkolems)
 {
-  size_t assertionsEnd = assertions.getRealAssertionsEnd();
-
+  Assert(ppSkolems.size() == ppLemmas.size());
   Trace("decision")
     << "JustificationHeuristic::addAssertions()"
     << " size = " << assertions.size()
-    << " assertionsEnd = " << assertionsEnd
     << std::endl;
 
   // Save all assertions locally, including the assertions generated by term
@@ -198,13 +197,11 @@ void JustificationHeuristic::addAssertions(
   }
 
   // Save mapping between ite skolems and ite assertions
-  for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap())
+  for (size_t i = 0, nlemmas = ppLemmas.size(); i < nlemmas; i++)
   {
-    Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to "
-                               << assertions[(i.second)] << std::endl;
-    Assert(i.second >= assertionsEnd && i.second < assertions.size());
-
-    d_skolemAssertions[i.first] = assertions[i.second];
+    Trace("decision::jh::ite") << " jh-ite: " << ppSkolems[i] << " maps to "
+                               << ppLemmas[i] << std::endl;
+    d_skolemAssertions[ppSkolems[i]] = ppLemmas[i];
   }
 
   // Automatic weight computation
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 5ecb5eb08..81b08f1a6 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -121,8 +121,9 @@ public:
 
   prop::SatLiteral getNext(bool &stopSearch) override;
 
-  void addAssertions(
-      const preprocessing::AssertionPipeline &assertions) override;
+  void addAssertions(const std::vector<Node>& assertions,
+                     const std::vector<Node>& ppLemmas,
+                     const std::vector<Node>& ppSkolems) override;
 
  private:
   /* getNext with an option to specify threshold */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 26d1e615b..8c1e452e7 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -123,6 +123,28 @@ PropEngine::~PropEngine() {
   delete d_theoryProxy;
 }
 
+void PropEngine::notifyPreprocessedAssertions(
+    const preprocessing::AssertionPipeline& ap)
+{
+  // notify the theory engine of preprocessed assertions
+  d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
+
+  // Add assertions to decision engine, which manually extracts what assertions
+  // corresponded to term formula removal. Note that alternatively we could
+  // delay all theory preprocessing and term formula removal to this point, in
+  // which case this method could simply take a vector of Node and not rely on
+  // assertion pipeline or its ITE skolem map.
+  std::vector<Node> ppLemmas;
+  std::vector<Node> ppSkolems;
+  for (const std::pair<const Node, unsigned>& i : ap.getIteSkolemMap())
+  {
+    Assert(i.second >= ap.getRealAssertionsEnd() && i.second < ap.size());
+    ppSkolems.push_back(i.first);
+    ppLemmas.push_back(ap[i.second]);
+  }
+  d_decisionEngine->addAssertions(ap.ref(), ppLemmas, ppSkolems);
+}
+
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << endl;
@@ -130,18 +152,42 @@ void PropEngine::assertFormula(TNode node) {
   d_cnfStream->convertAndAssert(node, false, false, true);
 }
 
-void PropEngine::assertLemma(TNode node, bool negated, bool removable)
+void PropEngine::assertLemma(theory::TrustNode trn, bool removable)
 {
+  Node node = trn.getNode();
+  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
   // Assert as (possibly) removable
   d_cnfStream->convertAndAssert(node, removable, negated);
 }
 
-void PropEngine::addAssertionsToDecisionEngine(
-    const preprocessing::AssertionPipeline& assertions)
+void PropEngine::assertLemmas(theory::TrustNode lem,
+                              std::vector<theory::TrustNode>& ppLemmas,
+                              std::vector<Node>& ppSkolems,
+                              bool removable)
 {
-  d_decisionEngine->addAssertions(assertions);
+  Assert(ppSkolems.size() == ppLemmas.size());
+  // assert the lemmas
+  assertLemma(lem, removable);
+  for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+  {
+    assertLemma(ppLemmas[i], removable);
+  }
+
+  // assert to decision engine
+  if (!removable)
+  {
+    // also add to the decision engine, where notice we don't need proofs
+    std::vector<Node> assertions;
+    assertions.push_back(lem.getProven());
+    std::vector<Node> ppLemmasF;
+    for (const theory::TrustNode& tnl : ppLemmas)
+    {
+      ppLemmasF.push_back(tnl.getProven());
+    }
+    d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
+  }
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index e4d536c29..061324947 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -88,6 +88,13 @@ class PropEngine
   void shutdown() {}
 
   /**
+   * Notify preprocessed assertions. This method is called just before the
+   * assertions are asserted to this prop engine. This method notifies the
+   * decision engine and the theory engine of the assertions in ap.
+   */
+  void notifyPreprocessedAssertions(const preprocessing::AssertionPipeline& ap);
+
+  /**
    * Converts the given formula to CNF and assert the CNF to the SAT solver.
    * The formula is asserted permanently for the current context.
    * @param node the formula to assert
@@ -99,19 +106,28 @@ class PropEngine
    * The formula can be removed by the SAT solver after backtracking lower
    * than the (SAT and SMT) level at which it was asserted.
    *
-   * @param node the formula to assert
-   * @param negated whether the node should be considered to be negated
-   * at the top level (or not)
+   * @param trn the trust node storing the formula to assert
    * @param removable whether this lemma can be quietly removed based
-   * on an activity heuristic (or not)
+   * on an activity heuristic
    */
-  void assertLemma(TNode node, bool negated, bool removable);
+  void assertLemma(theory::TrustNode trn, bool removable);
 
   /**
-   * Pass a list of assertions from an AssertionPipeline to the decision engine.
+   * Assert lemma trn with preprocessing lemmas ppLemmas which correspond
+   * to lemmas for skolems in ppSkolems.
+   *
+   * @param trn the trust node storing the formula to assert
+   * @param ppLemmas the lemmas from preprocessing and term formula removal on
+   * the proven node of trn
+   * @param ppSkolem the skolem that each lemma in ppLemma constrains. It should
+   * be the case that ppLemmas.size()==ppSkolems.size().
+   * @param removable whether this lemma can be quietly removed based
+   * on an activity heuristic
    */
-  void addAssertionsToDecisionEngine(
-      const preprocessing::AssertionPipeline& assertions);
+  void assertLemmas(theory::TrustNode trn,
+                    std::vector<theory::TrustNode>& ppLemmas,
+                    std::vector<Node>& ppSkolems,
+                    bool removable);
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 26a2ff3e1..c18dfe8ac 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -224,14 +224,11 @@ void SmtSolver::processAssertions(Assertions& as)
   // process the assertions with the preprocessor
   bool noConflict = d_pp.process(as);
 
-  // notify theory engine new preprocessed assertions
-  d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
-
   // Push the formula to decision engine
   if (noConflict)
   {
-    Chat() << "pushing to decision engine..." << endl;
-    d_propEngine->addAssertionsToDecisionEngine(ap);
+    Chat() << "notifying theory engine and decision engine..." << std::endl;
+    d_propEngine->notifyPreprocessedAssertions(ap);
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 84212fa1b..fa8960446 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -31,7 +31,6 @@
 #include "options/options.h"
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"
-#include "preprocessing/assertion_pipeline.h"
 #include "printer/printer.h"
 #include "smt/dump.h"
 #include "smt/logic_exception.h"
@@ -1495,26 +1494,18 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
     }
   }
 
-  // must use an assertion pipeline due to decision engine below
-  AssertionPipeline lemmas;
-  // make the assertion pipeline
-  lemmas.push_back(lemmap);
-  lemmas.updateRealAssertionsEnd();
   Assert(newSkolems.size() == newLemmas.size());
-  for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++)
-  {
-    // store skolem mapping here
-    IteSkolemMap& imap = lemmas.getIteSkolemMap();
-    imap[newSkolems[i]] = lemmas.size();
-    lemmas.push_back(newLemmas[i].getNode());
-  }
 
   // If specified, we must add this lemma to the set of those that need to be
   // justified, where note we pass all auxiliary lemmas in lemmas, since these
   // by extension must be justified as well.
   if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
   {
-    d_relManager->notifyPreprocessedAssertions(lemmas.ref());
+    d_relManager->notifyPreprocessedAssertion(tlemma.getProven());
+    for (const theory::TrustNode& tnl : newLemmas)
+    {
+      d_relManager->notifyPreprocessedAssertion(tnl.getProven());
+    }
   }
 
   // do final checks on the lemmas we are about to send
@@ -1531,32 +1522,34 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
     }
   }
 
-  // now, send the lemmas to the prop engine
-  Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl;
-  d_propEngine->assertLemma(tlemma.getProven(), false, removable);
-  for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
+  if (Trace.isOn("te-lemma"))
   {
-    Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven()
-                      << std::endl;
-    d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable);
+    Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl;
+    for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
+    {
+      Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven()
+                        << " (skolem is " << newSkolems[i] << ")" << std::endl;
+    }
   }
 
-  // assert to decision engine
-  if (!removable)
-  {
-    d_propEngine->addAssertionsToDecisionEngine(lemmas);
-  }
+  // now, send the lemmas to the prop engine
+  d_propEngine->assertLemmas(tlemma, newLemmas, newSkolems, removable);
 
   // Mark that we added some lemmas
   d_lemmasAdded = true;
 
   // Lemma analysis isn't online yet; this lemma may only live for this
   // user level.
-  Node retLemma = lemmas[0];
-  if (lemmas.size() > 1)
+  Node retLemma = tlemma.getNode();
+  if (!newLemmas.empty())
   {
+    std::vector<Node> lemmas{retLemma};
+    for (const theory::TrustNode& tnl : newLemmas)
+    {
+      lemmas.push_back(tnl.getProven());
+    }
     // the returned lemma is the conjunction of all additional lemmas.
-    retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref());
+    retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
   }
   return theory::LemmaStatus(retLemma, d_userContext->getLevel());
 }