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

1 files changed, 6 insertions, 1 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());
 }