(proof-new) Update preprocessing pass context for proofs (#5298)

This sets up the preprocessing pass context in preparation for proof production.

This PR makes the top level substitutions map into a TrustSubstitutionMap, the data structure that applies substitutions in a way that tracks proofs.

This PR also makes the "apply subst" preprocessing pass proof producing.

10 files changed, 66 insertions, 32 deletions

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index cd92e5f3d..4529ad5e1 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -104,7 +104,12 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
 }
 
 void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
-{
+{  
+  if (trn.isNull())
+  {
+    // null trust node denotes no change, nothing to do
+    return;
+  }
   Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
   replace(i, trn.getNode(), trn.getGenerator());
 }
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 0ce3f20b2..06821ab56 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -41,7 +41,7 @@ PreprocessingPassResult ApplySubsts::applyInternal(
     // TODO(#1255): Substitutions in incremental mode should be managed with a
     // proper data structure.
 
-    theory::SubstitutionMap& substMap =
+    theory::TrustSubstitutionMap& tlsm =
         d_preprocContext->getTopLevelSubstitutions();
     unsigned size = assertionsToPreprocess->size();
     for (unsigned i = 0; i < size; ++i)
@@ -54,9 +54,8 @@ PreprocessingPassResult ApplySubsts::applyInternal(
                         << std::endl;
       d_preprocContext->spendResource(
           ResourceManager::Resource::PreprocessStep);
-      assertionsToPreprocess->replace(i,
-                                      theory::Rewriter::rewrite(substMap.apply(
-                                          (*assertionsToPreprocess)[i])));
+      assertionsToPreprocess->replaceTrusted(
+          i, tlsm.apply((*assertionsToPreprocess)[i]));
       Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
                         << std::endl;
     }
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 3d7fd120a..f55665bc5 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -189,8 +189,9 @@ PreprocessingPassResult MipLibTrick::applyInternal(
       propagator->getBackEdges();
   unordered_set<unsigned long> removeAssertions;
 
-  SubstitutionMap& top_level_substs =
+  theory::TrustSubstitutionMap& tlsm =
       d_preprocContext->getTopLevelSubstitutions();
+  SubstitutionMap& top_level_substs = tlsm.get();
 
   NodeManager* nm = NodeManager::currentNM();
   Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 823e93f52..a3650c988 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -114,8 +114,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       << "Iterate through " << propagator->getLearnedLiterals().size()
       << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
-  SubstitutionMap& top_level_substs =
-      d_preprocContext->getTopLevelSubstitutions();
+  TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
+  CVC4_UNUSED SubstitutionMap& top_level_substs = ttls.get();
   SubstitutionMap constantPropagations(d_preprocContext->getUserContext());
   TrustSubstitutionMap tnewSubstituions(d_preprocContext->getUserContext(),
                                         nullptr);
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 65e26cabb..5893635cf 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -14,7 +14,7 @@
  ** The preprocessing pass context for passes.
  **/
 
-#include "preprocessing_pass_context.h"
+#include "preprocessing/preprocessing_pass_context.h"
 
 #include "expr/node_algorithm.h"
 
@@ -24,12 +24,14 @@ namespace preprocessing {
 PreprocessingPassContext::PreprocessingPassContext(
     SmtEngine* smt,
     RemoveTermFormulas* iteRemover,
-    theory::booleans::CircuitPropagator* circuitPropagator)
+    theory::booleans::CircuitPropagator* circuitPropagator,
+    ProofNodeManager* pnm)
     : d_smt(smt),
       d_resourceManager(smt->getResourceManager()),
       d_iteRemover(iteRemover),
-      d_topLevelSubstitutions(smt->getUserContext()),
+      d_topLevelSubstitutions(smt->getUserContext(), pnm),
       d_circuitPropagator(circuitPropagator),
+      d_pnm(pnm),
       d_symsInAssertions(smt->getUserContext())
 {
 }
@@ -40,6 +42,12 @@ void PreprocessingPassContext::widenLogic(theory::TheoryId id)
   req.widenLogic(id);
 }
 
+theory::TrustSubstitutionMap&
+PreprocessingPassContext::getTopLevelSubstitutions()
+{
+  return d_topLevelSubstitutions;
+}
+
 void PreprocessingPassContext::enableIntegers()
 {
   LogicRequest req(*d_smt);
@@ -61,5 +69,10 @@ void PreprocessingPassContext::recordSymbolsInAssertions(
   }
 }
 
+ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
+{
+  return d_pnm;
+}
+
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index f93c96fde..d0747b5d9 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -29,6 +29,7 @@
 #include "smt/term_formula_removal.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "theory/theory_engine.h"
+#include "theory/trust_substitutions.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
@@ -40,7 +41,8 @@ class PreprocessingPassContext
   PreprocessingPassContext(
       SmtEngine* smt,
       RemoveTermFormulas* iteRemover,
-      theory::booleans::CircuitPropagator* circuitPropagator);
+      theory::booleans::CircuitPropagator* circuitPropagator,
+      ProofNodeManager* pnm);
 
   SmtEngine* getSmt() { return d_smt; }
   TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); }
@@ -70,10 +72,7 @@ class PreprocessingPassContext
   void widenLogic(theory::TheoryId id);
 
   /** Gets a reference to the top-level substitution map */
-  theory::SubstitutionMap& getTopLevelSubstitutions()
-  {
-    return d_topLevelSubstitutions;
-  }
+  theory::TrustSubstitutionMap& getTopLevelSubstitutions();
 
   /* Enable Integers. */
   void enableIntegers();
@@ -85,6 +84,9 @@ class PreprocessingPassContext
    */
   void recordSymbolsInAssertions(const std::vector<Node>& assertions);
 
+  /** The the proof node manager associated with this context, if it exists */
+  ProofNodeManager* getProofNodeManager();
+
  private:
   /** Pointer to the SmtEngine that this context was created in. */
   SmtEngine* d_smt;
@@ -96,10 +98,12 @@ class PreprocessingPassContext
   RemoveTermFormulas* d_iteRemover;
 
   /* The top level substitutions */
-  theory::SubstitutionMap d_topLevelSubstitutions;
+  theory::TrustSubstitutionMap d_topLevelSubstitutions;
 
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;
+  /** Pointer to the proof node manager, if it exists */
+  ProofNodeManager* d_pnm;
 
   /**
    * The (user-context-dependent) set of symbols that occur in at least one
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 02323561d..912c0ea28 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -30,12 +30,14 @@ namespace smt {
 Preprocessor::Preprocessor(SmtEngine& smt,
                            context::UserContext* u,
                            AbstractValues& abs)
-    : d_smt(smt),
+    : d_context(u),
+      d_smt(smt),
       d_absValues(abs),
       d_propagator(true, true),
       d_assertionsProcessed(u, false),
       d_processor(smt, *smt.getResourceManager()),
-      d_rtf(u)
+      d_rtf(u),
+      d_pnm(nullptr)
 {
 }
 
@@ -51,7 +53,7 @@ Preprocessor::~Preprocessor()
 void Preprocessor::finishInit()
 {
   d_ppContext.reset(new preprocessing::PreprocessingPassContext(
-      &d_smt, &d_rtf, &d_propagator));
+      &d_smt, &d_rtf, &d_propagator, d_pnm));
 
   // initialize the preprocessing passes
   d_processor.finishInit(d_ppContext.get());
@@ -62,7 +64,8 @@ bool Preprocessor::process(Assertions& as)
   preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
 
   // should not be called if empty
-  Assert(ap.size() != 0) << "Can only preprocess a non-empty list of assertions";
+  Assert(ap.size() != 0)
+      << "Can only preprocess a non-empty list of assertions";
 
   if (d_assertionsProcessed && options::incrementalSolving())
   {
@@ -140,7 +143,8 @@ Node Preprocessor::simplify(const Node& node, bool removeItes)
   }
   std::unordered_map<Node, Node, NodeHashFunction> cache;
   Node n = d_processor.expandDefinitions(nas, cache);
-  Node ns = applySubstitutions(n);
+  TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n);
+  Node ns = ts.isNull() ? n : ts.getNode();
   if (removeItes)
   {
     // also remove ites if asked
@@ -149,9 +153,11 @@ Node Preprocessor::simplify(const Node& node, bool removeItes)
   return ns;
 }
 
-Node Preprocessor::applySubstitutions(TNode node)
+void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
 {
-  return Rewriter::rewrite(d_ppContext->getTopLevelSubstitutions().apply(node));
+  Assert(pppg != nullptr);
+  d_pnm = pppg->getManager();
+  d_rtf.setProofNodeManager(d_pnm);
 }
 
 }  // namespace smt
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 81757de37..b07e7ec97 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -100,12 +100,14 @@ class Preprocessor
    */
   RemoveTermFormulas& getTermFormulaRemover();
 
- private:
   /**
-   * Apply substitutions that have been inferred by preprocessing, return the
-   * substituted form of node.
+   * Set proof node manager. Enables proofs in this preprocessor.
    */
-  Node applySubstitutions(TNode node);
+  void setProofGenerator(PreprocessProofGenerator* pppg);
+
+ private:
+  /** A copy of the current context */
+  context::Context* d_context;
   /** Reference to the parent SmtEngine */
   SmtEngine& d_smt;
   /** Reference to the abstract values utility */
@@ -130,6 +132,8 @@ class Preprocessor
    * in term contexts.
    */
   RemoveTermFormulas d_rtf;
+  /** Proof node manager */
+  ProofNodeManager* d_pnm;
 };
 
 }  // namespace smt
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 719165048..f8af72c3a 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -105,9 +105,6 @@ bool ProcessAssertions::apply(Assertions& as)
     return true;
   }
 
-  SubstitutionMap& top_level_substs =
-      d_preprocessingPassContext->getTopLevelSubstitutions();
-
   if (options::bvGaussElim())
   {
     d_passes["bv-gauss"]->apply(&assertions);
@@ -330,6 +327,8 @@ bool ProcessAssertions::apply(Assertions& as)
       // First, find all skolems that appear in the substitution map - their
       // associated iteExpr will need to be moved to the main assertion set
       set<TNode> skolemSet;
+      SubstitutionMap& top_level_substs =
+          d_preprocessingPassContext->getTopLevelSubstitutions().get();
       SubstitutionMap::iterator pos = top_level_substs.begin();
       for (; pos != top_level_substs.end(); ++pos)
       {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2a771ce76..2f9918486 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -259,14 +259,17 @@ void SmtEngine::finishInit()
   if (options::proofNew())
   {
     d_pfManager.reset(new PfManager(getUserContext(), this));
+    PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
     // use this proof node manager
     pnm = d_pfManager->getProofNodeManager();
     // enable proof support in the rewriter
     d_rewriter->setProofNodeManager(pnm);
     // enable it in the assertions pipeline
-    d_asserts->setProofGenerator(d_pfManager->getPreprocessProofGenerator());
+    d_asserts->setProofGenerator(pppg);
     // enable it in the SmtSolver
     d_smtSolver->setProofNodeManager(pnm);
+    // enabled proofs in the preprocessor
+    d_pp->setProofGenerator(pppg);
   }
 
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;