1 files changed, 13 insertions, 8 deletions

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index feed945d5..824197bc5 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -5,7 +5,7 @@
  **   Aina Niemetz, Mathias Preiner, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -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(); }
@@ -64,16 +66,14 @@ class PreprocessingPassContext
     d_resourceManager->spendResource(r);
   }
 
-  const LogicInfo& getLogicInfo() { return d_smt->d_logic; }
+  /** Get the current logic info of the SmtEngine */
+  const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
 
   /* Widen the logic to include the given theory. */
   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 +85,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 +99,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