(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, 11 insertions, 0 deletions

diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 8d0644800..07d81f92b 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -28,6 +28,7 @@ namespace CVC4 {
 class SmtEngine;
 class TheoryEngine;
 class ResourceManager;
+class ProofNodeManager;
 
 namespace prop {
 class PropEngine;
@@ -108,6 +109,11 @@ class SmtSolver
    * into the SMT solver, and clears the buffer.
    */
   void processAssertions(Assertions& as);
+  /**
+   * Set proof node manager. Enables proofs in this SmtSolver. Should be
+   * called before finishInit.
+   */
+  void setProofNodeManager(ProofNodeManager* pnm);
   //------------------------------------------ access methods
   /** Get a pointer to the TheoryEngine owned by this solver. */
   TheoryEngine* getTheoryEngine();
@@ -125,6 +131,11 @@ class SmtSolver
   Preprocessor& d_pp;
   /** Reference to the statistics of SmtEngine */
   SmtEngineStatistics& d_stats;
+  /**
+   * Pointer to the proof node manager used by this SmtSolver. A non-null
+   * proof node manager indicates that proofs are enabled.
+   */
+  ProofNodeManager* d_pnm;
   /** The theory engine */
   std::unique_ptr<TheoryEngine> d_theoryEngine;
   /** The propositional engine */