Move ownership of theory preprocessor to TheoryProxy (#5690)

With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.

No significant behavior changes in this PR.

The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.

1 files changed, 104 insertions, 26 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index a8a92096c..8352373c5 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -36,6 +36,7 @@
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
 #include "util/resource_manager.h"
@@ -94,8 +95,14 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::CnfStream(
       d_satSolver, d_registrar, userContext, &d_outMgr, rm, true);
-  d_theoryProxy = new TheoryProxy(
-      this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
+
+  d_theoryProxy = new TheoryProxy(this,
+                                  d_theoryEngine,
+                                  d_decisionEngine.get(),
+                                  d_context,
+                                  userContext,
+                                  d_cnfStream,
+                                  pnm);
   d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
 
   d_decisionEngine->setSatSolver(d_satSolver);
@@ -143,6 +150,16 @@ PropEngine::~PropEngine() {
   delete d_theoryProxy;
 }
 
+theory::TrustNode PropEngine::preprocess(
+    TNode node,
+    std::vector<theory::TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems,
+    bool doTheoryPreprocess)
+{
+  return d_theoryProxy->preprocess(
+      node, newLemmas, newSkolems, doTheoryPreprocess);
+}
+
 void PropEngine::notifyPreprocessedAssertions(
     const preprocessing::AssertionPipeline& ap)
 {
@@ -168,7 +185,6 @@ void PropEngine::notifyPreprocessedAssertions(
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << endl;
-  // Assert as non-removable
   if (isProofEnabled())
   {
     d_pfCnfStream->convertAndAssert(node, false, false, nullptr);
@@ -181,35 +197,47 @@ void PropEngine::assertFormula(TNode node) {
   }
 }
 
-void PropEngine::assertLemma(theory::TrustNode trn, bool removable)
+Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
 {
-  Node node = trn.getNode();
-  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
-  Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
-  // Assert as (possibly) removable
-  if (isProofEnabled())
+  bool removable = isLemmaPropertyRemovable(p);
+  bool preprocess = isLemmaPropertyPreprocess(p);
+
+  // call preprocessor
+  std::vector<theory::TrustNode> ppLemmas;
+  std::vector<Node> ppSkolems;
+  theory::TrustNode tplemma =
+      d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems, preprocess);
+
+  Assert(ppSkolems.size() == ppLemmas.size());
+
+  // do final checks on the lemmas we are about to send
+  if (isProofEnabled() && options::proofNewEagerChecking())
   {
-    Assert(trn.getGenerator());
-    d_pfCnfStream->convertAndAssert(
-        node, negated, removable, trn.getGenerator());
+    Assert(tplemma.getGenerator() != nullptr);
+    // ensure closed, make the proof node eagerly here to debug
+    tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
+    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+    {
+      Assert(ppLemmas[i].getGenerator() != nullptr);
+      ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new");
+    }
   }
-  else
+
+  if (Trace.isOn("te-lemma"))
   {
-    d_cnfStream->convertAndAssert(node, removable, negated);
+    Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
+    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+    {
+      Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven()
+                        << " (skolem is " << ppSkolems[i] << ")" << std::endl;
+    }
   }
-}
 
-void PropEngine::assertLemmas(theory::TrustNode lem,
-                              std::vector<theory::TrustNode>& ppLemmas,
-                              std::vector<Node>& ppSkolems,
-                              bool removable)
-{
-  Assert(ppSkolems.size() == ppLemmas.size());
-  // assert the lemmas
-  assertLemma(lem, removable);
+  // now, assert the lemmas
+  assertLemmaInternal(tplemma, removable);
   for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
   {
-    assertLemma(ppLemmas[i], removable);
+    assertLemmaInternal(ppLemmas[i], removable);
   }
 
   // assert to decision engine
@@ -217,7 +245,7 @@ void PropEngine::assertLemmas(theory::TrustNode lem,
   {
     // also add to the decision engine, where notice we don't need proofs
     std::vector<Node> assertions;
-    assertions.push_back(lem.getProven());
+    assertions.push_back(tplemma.getProven());
     std::vector<Node> ppLemmasF;
     for (const theory::TrustNode& tnl : ppLemmas)
     {
@@ -225,6 +253,38 @@ void PropEngine::assertLemmas(theory::TrustNode lem,
     }
     d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
   }
+
+  // make the return lemma, which the theory engine will use
+  Node retLemma = tplemma.getProven();
+  if (!ppLemmas.empty())
+  {
+    std::vector<Node> lemmas{retLemma};
+    for (const theory::TrustNode& tnl : ppLemmas)
+    {
+      lemmas.push_back(tnl.getProven());
+    }
+    // the returned lemma is the conjunction of all additional lemmas.
+    retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
+  }
+  return retLemma;
+}
+
+void PropEngine::assertLemmaInternal(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
+  if (isProofEnabled())
+  {
+    Assert(trn.getGenerator());
+    d_pfCnfStream->convertAndAssert(
+        node, negated, removable, trn.getGenerator());
+  }
+  else
+  {
+    d_cnfStream->convertAndAssert(node, removable, negated);
+  }
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
@@ -361,7 +421,25 @@ void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const
   d_cnfStream->getBooleanVariables(outputVariables);
 }
 
-void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); }
+Node PropEngine::ensureLiteral(TNode n)
+{
+  // must preprocess
+  std::vector<theory::TrustNode> newLemmas;
+  std::vector<Node> newSkolems;
+  theory::TrustNode tpn =
+      d_theoryProxy->preprocess(n, newLemmas, newSkolems, true);
+  // send lemmas corresponding to the skolems introduced by preprocessing n
+  for (const theory::TrustNode& tnl : newLemmas)
+  {
+    Trace("ensureLiteral") << "  lemma: " << tnl.getNode() << std::endl;
+    assertLemma(tnl, theory::LemmaProperty::NONE);
+  }
+  Node preprocessed = tpn.isNull() ? Node(n) : tpn.getNode();
+  Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
+                         << std::endl;
+  d_cnfStream->ensureLiteral(preprocessed);
+  return preprocessed;
+}
 
 void PropEngine::push()
 {