(proof-new) Add SMT proof manager (#5054)

This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.

This PR includes setting up some connections into the various modules for proof production.

1 files changed, 12 insertions, 2 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5ef8b63c6..e95e36c3d 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -117,6 +117,7 @@ class DefinedFunction;
 struct SmtEngineStatistics;
 class SmtScope;
 class ProcessAssertions;
+class PfManager;
 
 ProofManager* currentProofManager();
 }/* CVC4::smt namespace */
@@ -900,7 +901,10 @@ class CVC4_PUBLIC SmtEngine
   /** Get a pointer to the PropEngine owned by this SmtEngine. */
   prop::PropEngine* getPropEngine();
 
-  /** Get a pointer to the ProofManager owned by this SmtEngine. */
+  /**
+   * Get a pointer to the ProofManager owned by this SmtEngine.
+   * TODO (project #37): this is the old proof manager and will be deleted
+   */
   ProofManager* getProofManager() { return d_proofManager.get(); };
 
   /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
@@ -1072,10 +1076,16 @@ class CVC4_PUBLIC SmtEngine
   /** The SMT solver */
   std::unique_ptr<smt::SmtSolver> d_smtSolver;
 
-  /** The proof manager */
+  /** The (old) proof manager TODO (project #37): delete this */
   std::unique_ptr<ProofManager> d_proofManager;
 
   /**
+   * The proof manager, which manages all things related to checking,
+   * processing, and printing proofs.
+   */
+  std::unique_ptr<smt::PfManager> d_pfManager;
+
+  /**
    * The rewriter associated with this SmtEngine. We have a different instance
    * of the rewriter for each SmtEngine instance. This is because rewriters may
    * hold references to objects that belong to theory solvers, which are