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

1 files changed, 50 insertions, 4 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) {