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.

4 files changed, 192 insertions, 54 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()
 {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 55a42c2a7..ac2b35ad6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -95,6 +95,23 @@ class PropEngine
   void shutdown() {}
 
   /**
+   * Preprocess the given node. Return the REWRITE trust node corresponding to
+   * rewriting node. New lemmas and skolems are added to ppLemmas and
+   * ppSkolems respectively.
+   *
+   * @param node The assertion to preprocess,
+   * @param ppLemmas The lemmas to add to the set of assertions,
+   * @param ppSkolems The skolems that newLemmas correspond to,
+   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
+   * @return The (REWRITE) trust node corresponding to rewritten node via
+   * preprocessing.
+   */
+  theory::TrustNode preprocess(TNode node,
+                               std::vector<theory::TrustNode>& ppLemmas,
+                               std::vector<Node>& ppSkolems,
+                               bool doTheoryPreprocess);
+
+  /**
    * 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.
@@ -114,27 +131,10 @@ class PropEngine
    * than the (SAT and SMT) level at which it was asserted.
    *
    * @param trn the trust node storing the formula to assert
-   * @param removable whether this lemma can be quietly removed based
-   * on an activity heuristic
+   * @param p the properties of the lemma
+   * @return the (preprocessed) lemma
    */
-  void assertLemma(theory::TrustNode trn, bool removable);
-
-  /**
-   * 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 assertLemmas(theory::TrustNode trn,
-                    std::vector<theory::TrustNode>& ppLemmas,
-                    std::vector<Node>& ppSkolems,
-                    bool removable);
+  Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
@@ -185,10 +185,11 @@ class PropEngine
 
   /**
    * Ensure that the given node will have a designated SAT literal
-   * that is definitionally equal to it.  The result of this function
-   * is that the Node can be queried via getSatValue().
+   * that is definitionally equal to it. Note that theory preprocessing is
+   * applied to n. The node returned by this method can be subsequently queried
+   * via getSatValue().
    */
-  void ensureLiteral(TNode n);
+  Node ensureLiteral(TNode n);
 
   /**
    * Push the context level.
@@ -261,6 +262,18 @@ class PropEngine
  private:
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
+
+  /**
+   * Converts the given formula to CNF and asserts the CNF to the SAT solver.
+   * The formula can be removed by the SAT solver after backtracking lower
+   * than the (SAT and SMT) level at which it was asserted.
+   *
+   * @param trn the trust node storing the formula to assert
+   * @param removable whether this lemma can be quietly removed based
+   * on an activity heuristic
+   */
+  void assertLemmaInternal(theory::TrustNode trn, bool removable);
+
   /**
    * Indicates that the SAT solver is currently solving something and we should
    * not mess with it's internal state.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 1b9e78d80..23405675a 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -19,15 +19,14 @@
 #include "context/context.h"
 #include "decision/decision_engine.h"
 #include "options/decision_options.h"
+#include "proof/cnf_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
-#include "proof/cnf_proof.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "util/statistics_registry.h"
 
-
 namespace CVC4 {
 namespace prop {
 
@@ -35,12 +34,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          TheoryEngine* theoryEngine,
                          DecisionEngine* decisionEngine,
                          context::Context* context,
-                         CnfStream* cnfStream)
+                         context::UserContext* userContext,
+                         CnfStream* cnfStream,
+                         ProofNodeManager* pnm)
     : d_propEngine(propEngine),
       d_cnfStream(cnfStream),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
-      d_queue(context)
+      d_queue(context),
+      d_tpp(*theoryEngine, userContext, pnm)
 {
 }
 
@@ -165,5 +167,25 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
 
 CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
 
+theory::TrustNode TheoryProxy::preprocessLemma(
+    theory::TrustNode trn,
+    std::vector<theory::TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems,
+    bool doTheoryPreprocess)
+{
+  return d_tpp.preprocessLemma(trn, newLemmas, newSkolems, doTheoryPreprocess);
+}
+
+theory::TrustNode TheoryProxy::preprocess(
+    TNode node,
+    std::vector<theory::TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems,
+    bool doTheoryPreprocess)
+{
+  theory::TrustNode pnode =
+      d_tpp.preprocess(node, newLemmas, newSkolems, doTheoryPreprocess);
+  return pnode;
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index e16728d0d..4d460434d 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -26,10 +26,13 @@
 #include <iosfwd>
 #include <unordered_set>
 
+#include "context/cdhashmap.h"
 #include "context/cdqueue.h"
 #include "expr/node.h"
 #include "prop/sat_solver.h"
 #include "theory/theory.h"
+#include "theory/theory_preprocessor.h"
+#include "theory/trust_node.h"
 #include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
@@ -53,7 +56,9 @@ class TheoryProxy
               TheoryEngine* theoryEngine,
               DecisionEngine* decisionEngine,
               context::Context* context,
-              CnfStream* cnfStream);
+              context::UserContext* userContext,
+              CnfStream* cnfStream,
+              ProofNodeManager* pnm);
 
   ~TheoryProxy();
 
@@ -90,6 +95,23 @@ class TheoryProxy
 
   CnfStream* getCnfStream();
 
+  /**
+   * Call the preprocessor on node, return trust node corresponding to the
+   * rewrite.
+   */
+  theory::TrustNode preprocessLemma(theory::TrustNode trn,
+                                    std::vector<theory::TrustNode>& newLemmas,
+                                    std::vector<Node>& newSkolems,
+                                    bool doTheoryPreprocess);
+  /**
+   * Call the preprocessor on node, return trust node corresponding to the
+   * rewrite.
+   */
+  theory::TrustNode preprocess(TNode node,
+                               std::vector<theory::TrustNode>& newLemmas,
+                               std::vector<Node>& newSkolems,
+                               bool doTheoryPreprocess);
+
  private:
   /** The prop engine we are using. */
   PropEngine* d_propEngine;
@@ -111,6 +133,9 @@ class TheoryProxy
    * all imported and exported lemmas.
    */
   std::unordered_set<Node, NodeHashFunction> d_shared;
+
+  /** The theory preprocessor */
+  theory::TheoryPreprocessor d_tpp;
 }; /* class TheoryProxy */
 
 }/* CVC4::prop namespace */