[proof-new] Updating interfaces between prop engine and minisat (#5664)

This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface".

Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code.

15 files changed, 258 insertions, 136 deletions

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index afa16397d..15dbf0d79 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -46,7 +46,7 @@ class DecisionEngine {
 
   // PropEngine* d_propEngine;
   CnfStream* d_cnfStream;
-  DPLLSatSolverInterface* d_satSolver;
+  CDCLTSatSolverInterface* d_satSolver;
 
   context::Context* d_satContext;
   context::UserContext* d_userContext;
@@ -75,7 +75,8 @@ class DecisionEngine {
     Trace("decision") << "Destroying decision engine" << std::endl;
   }
 
-  void setSatSolver(DPLLSatSolverInterface* ss) {
+  void setSatSolver(CDCLTSatSolverInterface* ss)
+  {
     // setPropEngine should not be called more than once
     Assert(d_satSolver == NULL);
     Assert(ss != NULL);
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index e769ba6cc..c5158bb4f 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -148,11 +148,14 @@ class ScopedBool
 
 Solver::Solver(CVC4::prop::TheoryProxy* proxy,
                CVC4::context::Context* context,
-               bool enable_incremental)
+               CVC4::context::UserContext* userContext,
+               ProofNodeManager* pnm,
+               bool enableIncremental)
     : d_proxy(proxy),
       d_context(context),
       assertionLevel(0),
-      d_enable_incremental(enable_incremental),
+      d_pfManager(nullptr),
+      d_enable_incremental(enableIncremental),
       minisat_busy(false)
       // Parameters (user settable):
       //
@@ -209,7 +212,7 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
       simpDB_props(0),
       order_heap(VarOrderLt(activity)),
       progress_estimate(0),
-      remove_satisfied(!enable_incremental)
+      remove_satisfied(!enableIncremental)
 
       // Resource constraints:
       //
@@ -2118,5 +2121,15 @@ inline bool Solver::withinBudget(ResourceManager::Resource r) const
   return within_budget;
 }
 
+SatProofManager* Solver::getProofManager()
+{
+  return d_pfManager ? d_pfManager.get() : nullptr;
+}
+
+std::shared_ptr<ProofNode> Solver::getProof()
+{
+  return d_pfManager ? d_pfManager->getProof() : nullptr;
+}
+
 } /* CVC4::Minisat namespace */
 } /* CVC4 namespace */
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index f3bcfb67e..270cc9308 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "base/output.h"
 #include "context/context.h"
+#include "expr/proof_node_manager.h"
 #include "proof/clause_id.h"
 #include "prop/minisat/core/SolverTypes.h"
 #include "prop/minisat/mtl/Alg.h"
@@ -36,12 +37,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/sat_proof_manager.h"
 #include "theory/theory.h"
 
-
 namespace CVC4 {
 template <class Solver> class TSatProof;
 
 namespace prop {
-  class TheoryProxy;
+class PropEngine;
+class TheoryProxy;
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
@@ -55,6 +56,7 @@ namespace Minisat {
 class Solver {
 
   /** The only two CVC4 entry points to the private solver data */
+  friend class CVC4::prop::PropEngine;
   friend class CVC4::prop::TheoryProxy;
   friend class CVC4::prop::SatProofManager;
   friend class CVC4::TSatProof<Minisat::Solver>;
@@ -85,6 +87,9 @@ public:
   /** Variable representing false */
   Var varFalse;
 
+  /** The resolution proof manager */
+  std::unique_ptr<CVC4::prop::SatProofManager> d_pfManager;
+
  public:
   /** Returns the current user assertion level */
   int getAssertionLevel() const { return assertionLevel; }
@@ -129,51 +134,66 @@ public:
 
     // Constructor/Destructor:
     //
-    Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental = false);
-    CVC4_PUBLIC virtual ~Solver();
-
-    // Problem specification:
-    //
-    Var     newVar    (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); // Add a new variable with parameters specifying variable mode.
-    Var     trueVar() const { return varTrue; }
-    Var     falseVar() const { return varFalse; }
-
-    // Less than for literals in a lemma
-    struct lemma_lt {
-      Solver& d_solver;
-      lemma_lt(Solver& solver) : d_solver(solver) {}
-      bool operator()(Lit x, Lit y)
-      {
-        lbool x_value = d_solver.value(x);
-        lbool y_value = d_solver.value(y);
-        // Two unassigned literals are sorted arbitrarily
-        if (x_value == l_Undef && y_value == l_Undef)
-        {
-          return x < y;
-        }
-        // Unassigned literals are put to front
-        if (x_value == l_Undef) return true;
-        if (y_value == l_Undef) return false;
-        // Literals of the same value are sorted by decreasing levels
-        if (x_value == y_value)
-        {
-          return d_solver.trail_index(var(x)) > d_solver.trail_index(var(y));
-        }
-        else
-        {
-          // True literals go up front
-          if (x_value == l_True)
-          {
-            return true;
-          }
-          else
-          {
-            return false;
-          }
-        }
-      }
-    };
-
+ Solver(CVC4::prop::TheoryProxy* proxy,
+        CVC4::context::Context* context,
+        CVC4::context::UserContext* userContext,
+        ProofNodeManager* pnm,
+        bool enableIncremental = false);
+ CVC4_PUBLIC virtual ~Solver();
+
+ // Problem specification:
+ //
+ Var newVar(bool polarity = true,
+            bool dvar = true,
+            bool isTheoryAtom = false,
+            bool preRegister = false,
+            bool canErase = true);  // Add a new variable with parameters
+                                    // specifying variable mode.
+ Var trueVar() const { return varTrue; }
+ Var falseVar() const { return varFalse; }
+
+ /** Retrive the SAT proof manager */
+ CVC4::prop::SatProofManager* getProofManager();
+
+ /** Retrive the refutation proof */
+ std::shared_ptr<ProofNode> getProof();
+
+ // Less than for literals in a lemma
+ struct lemma_lt
+ {
+   Solver& d_solver;
+   lemma_lt(Solver& solver) : d_solver(solver) {}
+   bool operator()(Lit x, Lit y)
+   {
+     lbool x_value = d_solver.value(x);
+     lbool y_value = d_solver.value(y);
+     // Two unassigned literals are sorted arbitrarily
+     if (x_value == l_Undef && y_value == l_Undef)
+     {
+       return x < y;
+     }
+     // Unassigned literals are put to front
+     if (x_value == l_Undef) return true;
+     if (y_value == l_Undef) return false;
+     // Literals of the same value are sorted by decreasing levels
+     if (x_value == y_value)
+     {
+       return d_solver.trail_index(var(x)) > d_solver.trail_index(var(y));
+     }
+     else
+     {
+       // True literals go up front
+       if (x_value == l_True)
+       {
+         return true;
+       }
+       else
+       {
+         return false;
+       }
+     }
+   }
+ };
 
     // CVC4 context push/pop
     void          push                     ();
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index aae347caf..8af73140e 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -102,8 +102,11 @@ void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
   Assert((unsigned)clause.size() == sat_clause.size());
 }
 
-void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) {
-
+void MinisatSatSolver::initialize(context::Context* context,
+                                  TheoryProxy* theoryProxy,
+                                  context::UserContext* userContext,
+                                  ProofNodeManager* pnm)
+{
   d_context = context;
 
   if (options::decisionMode() != options::DecisionMode::INTERNAL)
@@ -116,6 +119,8 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory
   d_minisat = new Minisat::SimpSolver(
       theoryProxy,
       d_context,
+      userContext,
+      pnm,
       options::incrementalSolving()
           || options::decisionMode() != options::DecisionMode::INTERNAL);
 
@@ -218,6 +223,16 @@ bool MinisatSatSolver::isDecision(SatVariable decn) const {
   return d_minisat->isDecision( decn );
 }
 
+SatProofManager* MinisatSatSolver::getProofManager()
+{
+  return d_minisat->getProofManager();
+}
+
+std::shared_ptr<ProofNode> MinisatSatSolver::getProof()
+{
+  return d_minisat->getProof();
+}
+
 /** Incremental interface */
 
 unsigned MinisatSatSolver::getAssertionLevel() const {
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index e2b5699f7..959095757 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -23,9 +23,9 @@
 namespace CVC4 {
 namespace prop {
 
-class MinisatSatSolver : public DPLLSatSolverInterface {
-public:
-
+class MinisatSatSolver : public CDCLTSatSolverInterface
+{
+ public:
   MinisatSatSolver(StatisticsRegistry* registry);
   ~MinisatSatSolver() override;
 
@@ -38,7 +38,10 @@ public:
 
   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
-  void initialize(context::Context* context, TheoryProxy* theoryProxy) override;
+  void initialize(context::Context* context,
+                  TheoryProxy* theoryProxy,
+                  CVC4::context::UserContext* userContext,
+                  ProofNodeManager* pnm) override;
 
   ClauseId addClause(SatClause& clause, bool removable) override;
   ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
@@ -79,6 +82,15 @@ public:
 
   bool isDecision(SatVariable decn) const override;
 
+  /** Retrieve a pointer to the unerlying solver. */
+  Minisat::SimpSolver* getSolver() { return d_minisat; }
+
+  /** Retrieve the proof manager of this SAT solver. */
+  SatProofManager* getProofManager();
+
+  /** Retrieve the refutation proof of this SAT solver. */
+  std::shared_ptr<ProofNode> getProof() override;
+
  private:
 
   /** The SatSolver used */
@@ -104,7 +116,7 @@ public:
   };/* class MinisatSatSolver::Statistics */
   Statistics d_statistics;
 
-};/* class MinisatSatSolver */
+}; /* class MinisatSatSolver */
 
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 0ec8981ca..5c8922360 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -49,8 +49,10 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 
 SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
                        CVC4::context::Context* context,
+                       CVC4::context::UserContext* userContext,
+                       ProofNodeManager* pnm,
                        bool enableIncremental)
-    : Solver(proxy, context, enableIncremental),
+    : Solver(proxy, context, userContext, pnm, enableIncremental),
       grow(opt_grow),
       clause_lim(opt_clause_lim),
       subsumption_lim(opt_subsumption_lim),
@@ -62,10 +64,9 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
       asymm_lits(0),
       eliminated_vars(0),
       elimorder(1),
-      use_simplification(
-          !enableIncremental
-          && !options::unsatCores())  // TODO: turn off simplifications if
-                                      // proofs are on initially
+      use_simplification(!enableIncremental && !options::unsatCores()
+                         && !pnm)  // TODO: turn off simplifications if
+                                   // proofs are on initially
       ,
       occurs(ClauseDeleted(ca)),
       elim_heap(ElimLt(n_occ)),
@@ -733,7 +734,6 @@ void SimpSolver::cleanUpClauses()
     clauses_persistent.shrink(i - j);
 }
 
-
 //=================================================================================================
 // Garbage Collection methods:
 
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index c13ee5583..f952aee1e 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -43,41 +43,66 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-    SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental = false);
-    CVC4_PUBLIC ~SimpSolver();
-
-    // Problem specification:
-    //
-    Var     newVar    (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
-    bool    addClause (const vec<Lit>& ps, bool removable, ClauseId& id);
-    bool    addEmptyClause(bool removable); // Add the empty clause to the solver.
-    bool    addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
-    bool    addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
-    bool    substitute(Var v, Lit x);  // Replace all occurrences of v with x (may cause a contradiction).
-
-    // Variable mode:
-    // 
-    void    setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
-    bool    isEliminated(Var v) const;
-
-    // Solving:
-    //
-    lbool    solve       (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
-    lbool    solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
-    lbool    solve       (                     bool do_simp = true, bool turn_off_simp = false);
-    lbool    solve       (Lit p       ,        bool do_simp = true, bool turn_off_simp = false);       
-    lbool    solve       (Lit p, Lit q,        bool do_simp = true, bool turn_off_simp = false);
-    lbool    solve       (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
-    bool    eliminate   (bool turn_off_elim = false);  // Perform variable elimination based simplification. 
-
-    // Memory managment:
-    //
-    void garbageCollect() override;
-
-    // Generate a (possibly simplified) DIMACS file:
-    //
+  SimpSolver(CVC4::prop::TheoryProxy* proxy,
+             CVC4::context::Context* context,
+             CVC4::context::UserContext* userContext,
+             ProofNodeManager* pnm,
+             bool enableIncremental = false);
+  CVC4_PUBLIC ~SimpSolver();
+
+  // Problem specification:
+  //
+  Var newVar(bool polarity = true,
+             bool dvar = true,
+             bool isTheoryAtom = false,
+             bool preRegister = false,
+             bool canErase = true);
+  bool addClause(const vec<Lit>& ps, bool removable, ClauseId& id);
+  bool addEmptyClause(bool removable);  // Add the empty clause to the solver.
+  bool addClause(Lit p,
+                 bool removable,
+                 ClauseId& id);  // Add a unit clause to the solver.
+  bool addClause(Lit p,
+                 Lit q,
+                 bool removable,
+                 ClauseId& id);  // Add a binary clause to the solver.
+  bool addClause(Lit p,
+                 Lit q,
+                 Lit r,
+                 bool removable,
+                 ClauseId& id);  // Add a ternary clause to the solver.
+  bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
+  bool substitute(Var v, Lit x);  // Replace all occurrences of v with x (may
+                                  // cause a contradiction).
+
+  // Variable mode:
+  //
+  void setFrozen(Var v,
+                 bool b);  // If a variable is frozen it will not be eliminated.
+  bool isEliminated(Var v) const;
+
+  // Solving:
+  //
+  lbool solve(const vec<Lit>& assumps,
+              bool do_simp = true,
+              bool turn_off_simp = false);
+  lbool solveLimited(const vec<Lit>& assumps,
+                     bool do_simp = true,
+                     bool turn_off_simp = false);
+  lbool solve(bool do_simp = true, bool turn_off_simp = false);
+  lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false);
+  lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
+  lbool solve(
+      Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
+  bool eliminate(bool turn_off_elim = false);  // Perform variable elimination
+                                               // based simplification.
+
+  // Memory managment:
+  //
+  void garbageCollect() override;
+
+  // Generate a (possibly simplified) DIMACS file:
+  //
 #if 0
     void    toDimacs  (const char* file, const vec<Lit>& assumps);
     void    toDimacs  (const char* file);
@@ -118,11 +143,13 @@ class SimpSolver : public Solver {
 
         // old ordering function
         // bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
-        
-         bool operator()(Var x, Var y) const { 
-             int c_x = cost(x);
-             int c_y = cost(y);
-             return c_x < c_y || (c_x == c_y && x < y); }
+
+        bool operator()(Var x, Var y) const
+        {
+          int c_x = cost(x);
+          int c_y = cost(y);
+          return c_x < c_y || (c_x == c_y && x < y);
+        }
     };
 
     struct ClauseDeleted {
@@ -200,14 +227,14 @@ inline lbool SimpSolver::solve        (                     bool do_simp, bool t
   assumptions.clear();
   return solve_(do_simp, turn_off_simp);
  }
- 
+
 inline lbool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  {
   budgetOff();
   assumptions.clear();
   assumptions.push(p);
   return solve_(do_simp, turn_off_simp);
  }
- 
+
 inline lbool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  {
   budgetOff();
   assumptions.clear();
@@ -215,7 +242,7 @@ inline lbool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool t
   assumptions.push(q);
   return solve_(do_simp, turn_off_simp);
  }
- 
+
 inline lbool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  {
   budgetOff();
   assumptions.clear();
@@ -225,16 +252,24 @@ inline lbool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool t
   return solve_(do_simp, turn_off_simp);
  }
 
- inline lbool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
+ inline lbool SimpSolver::solve(const vec<Lit>& assumps,
+                                bool do_simp,
+                                bool turn_off_simp)
+ {
    budgetOff();
     assumps.copyTo(assumptions);
     return solve_(do_simp, turn_off_simp);
  }
 
-inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
-    assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
+ inline lbool SimpSolver::solveLimited(const vec<Lit>& assumps,
+                                       bool do_simp,
+                                       bool turn_off_simp)
+ {
+   assumps.copyTo(assumptions);
+   return solve_(do_simp, turn_off_simp);
+ }
 
-//=================================================================================================
+ //=================================================================================================
 } /* CVC4::Minisat namespace */
 } /* CVC4 namespace */
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e5efcbf8f..fee73babb 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -70,7 +70,8 @@ PropEngine::PropEngine(TheoryEngine* te,
                        Context* satContext,
                        UserContext* userContext,
                        ResourceManager* rm,
-                       OutputManager& outMgr)
+                       OutputManager& outMgr,
+                       ProofNodeManager* pnm)
     : d_inCheckSat(false),
       d_theoryEngine(te),
       d_context(satContext),
@@ -79,6 +80,7 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_registrar(NULL),
       d_cnfStream(NULL),
       d_pfCnfStream(nullptr),
+      d_ppm(nullptr),
       d_interrupted(false),
       d_resourceManager(rm),
       d_outMgr(outMgr)
@@ -89,7 +91,7 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
   d_decisionEngine->init();  // enable appropriate strategies
 
-  d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry());
+  d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());
 
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::CnfStream(
@@ -97,7 +99,7 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   d_theoryProxy = new TheoryProxy(
       this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
-  d_satSolver->initialize(d_context, d_theoryProxy);
+  d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
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 */
diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index 3b1df8a00..3c18dc896 100644
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -22,11 +22,11 @@ namespace prop {
 
 PropPfManager::PropPfManager(context::UserContext* userContext,
                              ProofNodeManager* pnm,
-                             SatProofManager* satPM,
+                             CDCLTSatSolverInterface* satSolver,
                              ProofCnfStream* cnfProof)
     : d_pnm(pnm),
       d_pfpp(new ProofPostproccess(pnm, cnfProof)),
-      d_satPM(satPM),
+      d_satSolver(satSolver),
       d_assertions(userContext)
 {
   // add trivial assumption. This is so that we can check the that the prop
@@ -47,7 +47,7 @@ void PropPfManager::checkProof(context::CDList<Node>* assertions)
 {
   Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution "
                         "proof of false is closed\n";
-  std::shared_ptr<ProofNode> conflictProof = d_satPM->getProof();
+  std::shared_ptr<ProofNode> conflictProof = d_satSolver->getProof();
   Assert(conflictProof);
   // connect it with CNF proof
   d_pfpp->process(conflictProof);
@@ -66,7 +66,7 @@ std::shared_ptr<ProofNode> PropPfManager::getProof()
   // retrieve the SAT solver's refutation proof
   Trace("sat-proof")
       << "PropPfManager::getProof: Getting resolution proof of false\n";
-  std::shared_ptr<ProofNode> conflictProof = d_satPM->getProof();
+  std::shared_ptr<ProofNode> conflictProof = d_satSolver->getProof();
   Assert(conflictProof);
   if (Trace.isOn("sat-proof"))
   {
diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h
index f3deee5bc..fc0151bcd 100644
--- a/src/prop/prop_proof_manager.h
+++ b/src/prop/prop_proof_manager.h
@@ -39,7 +39,7 @@ class PropPfManager
  public:
   PropPfManager(context::UserContext* userContext,
                 ProofNodeManager* pnm,
-                SatProofManager* satPM,
+                CDCLTSatSolverInterface* satSolver,
                 ProofCnfStream* cnfProof);
 
   /** Saves assertion for later checking whether refutation proof is closed.
@@ -78,9 +78,9 @@ class PropPfManager
   /** The proof post-processor */
   std::unique_ptr<prop::ProofPostproccess> d_pfpp;
   /**
-   * The SAT solver's proof manager, which will provide a refutation
-   * proofresolution proof when requested */
-  SatProofManager* d_satPM;
+   * The SAT solver of this prop engine, which should provide a refutation
+   * proof when requested */
+  CDCLTSatSolverInterface* d_satSolver;
   /** Assertions corresponding to the leaves of the prop engine's proof.
    *
    * These are kept in a context-dependent manner since the prop engine's proof
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index a842647bd..10ee843df 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -24,9 +24,10 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "expr/proof_node_manager.h"
 #include "proof/clause_id.h"
-#include "prop/sat_solver_types.h"
 #include "prop/bv_sat_solver_notify.h"
+#include "prop/sat_solver_types.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -122,13 +123,15 @@ public:
 
 };/* class BVSatSolverInterface */
 
-class DPLLSatSolverInterface : public SatSolver
+class CDCLTSatSolverInterface : public SatSolver
 {
  public:
-  virtual ~DPLLSatSolverInterface(){};
+  virtual ~CDCLTSatSolverInterface(){};
 
   virtual void initialize(context::Context* context,
-                          prop::TheoryProxy* theoryProxy) = 0;
+                          prop::TheoryProxy* theoryProxy,
+                          CVC4::context::UserContext* userContext,
+                          ProofNodeManager* pnm) = 0;
 
   virtual void push() = 0;
 
@@ -145,7 +148,10 @@ class DPLLSatSolverInterface : public SatSolver
   virtual void requirePhase(SatLiteral lit) = 0;
 
   virtual bool isDecision(SatVariable decn) const = 0;
-}; /* class DPLLSatSolverInterface */
+
+  virtual std::shared_ptr<ProofNode> getProof() = 0;
+
+}; /* class CDCLTSatSolverInterface */
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
   out << lit.toString();
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index cfdbc8b04..c6213f5a0 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -33,7 +33,7 @@ BVSatSolverInterface* SatSolverFactory::createMinisat(
   return new BVMinisatSatSolver(registry, mainSatContext, name);
 }
 
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
+MinisatSatSolver* SatSolverFactory::createCDCLTMinisat(
     StatisticsRegistry* registry)
 {
   return new MinisatSatSolver(registry);
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 75069e63b..0bf6116cb 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "context/context.h"
+#include "prop/minisat/minisat.h"
 #include "prop/sat_solver.h"
 #include "util/statistics_registry.h"
 
@@ -36,8 +37,7 @@ class SatSolverFactory
                                              StatisticsRegistry* registry,
                                              const std::string& name = "");
 
-  static DPLLSatSolverInterface* createDPLLMinisat(
-      StatisticsRegistry* registry);
+  static MinisatSatSolver* createCDCLTMinisat(StatisticsRegistry* registry);
 
   static SatSolver* createCryptoMinisat(StatisticsRegistry* registry,
                                         const std::string& name = "");
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index c18dfe8ac..e53401f79 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -71,7 +71,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
                                     d_smt.getContext(),
                                     d_smt.getUserContext(),
                                     d_rm,
-                                    d_smt.getOutputManager()));
+                                    d_smt.getOutputManager(),
+                                    d_pnm));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -91,7 +92,8 @@ void SmtSolver::resetAssertions()
                                     d_smt.getContext(),
                                     d_smt.getUserContext(),
                                     d_rm,
-                                    d_smt.getOutputManager()));
+                                    d_smt.getOutputManager(),
+                                    d_pnm));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not