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).

2 files changed, 74 insertions, 12 deletions

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