1 files changed, 19 insertions, 3 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index b36b9d22a..b311558ab 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -28,7 +28,12 @@
 #include "options/options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_manager.h"
+#include "prop/minisat/core/Solver.h"
+#include "prop/minisat/minisat.h"
 #include "prop/proof_cnf_stream.h"
+#include "prop/prop_proof_manager.h"
+#include "prop/sat_solver_types.h"
+#include "theory/trust_node.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
 #include "util/unsafe_interrupt_exception.h"
@@ -47,7 +52,7 @@ namespace theory {
 namespace prop {
 
 class CnfStream;
-class DPLLSatSolverInterface;
+class CDCLTSatSolverInterface;
 
 class PropEngine;
 
@@ -65,7 +70,8 @@ class PropEngine
              context::Context* satContext,
              context::UserContext* userContext,
              ResourceManager* rm,
-             OutputManager& outMgr);
+             OutputManager& outMgr,
+             ProofNodeManager* pnm);
 
   /**
    * Destructor.
@@ -239,6 +245,10 @@ class PropEngine
   /** Retrieve this modules proof CNF stream. */
   ProofCnfStream* getProofCnfStream();
 
+  /** Checks that the proof is closed w.r.t. asserted formulas to this engine as
+   * well as to the given assertions. */
+  void checkProof(context::CDList<Node>* assertions);
+
   /**
    * Return the prop engine proof. This should be called only when proofs are
    * enabled. Returns a proof of false whose free assumptions are the
@@ -268,7 +278,7 @@ class PropEngine
   TheoryProxy* d_theoryProxy;
 
   /** The SAT solver proxy */
-  DPLLSatSolverInterface* d_satSolver;
+  CDCLTSatSolverInterface* d_satSolver;
 
   /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;
@@ -276,11 +286,17 @@ class PropEngine
   /** Theory registrar; kept around for destructor cleanup */
   theory::TheoryRegistrar* d_registrar;
 
+  /** A pointer to the proof node maneger to be used by this engine. */
+  ProofNodeManager* d_pnm;
+
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
   /** Proof-producing CNF converter */
   std::unique_ptr<ProofCnfStream> d_pfCnfStream;
 
+  /** The proof manager for prop engine */
+  std::unique_ptr<PropPfManager> d_ppm;
+
   /** Whether we were just interrupted (or not) */
   bool d_interrupted;
   /** Pointer to resource manager for associated SmtEngine */