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

6 files changed, 39 insertions, 17 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