From 3a8a27994584ca2168ef71d5eb0ce46ef558ba34 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Sep 2020 22:38:04 -0500
Subject: (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.
---
 src/smt/smt_solver.h | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/smt/smt_solver.h')

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 */
-- 
cgit v1.2.3