6 files changed, 48 insertions, 20 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 55710092b..57ef8ef30 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -104,7 +104,8 @@ void BVMinisatSatSolver::popAssumption() {
   d_minisat->popAssumption();
 }
 
-void BVMinisatSatSolver::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void BVMinisatSatSolver::setResolutionProofLog(
+    proof::ResolutionBitVectorProof* bvp)
 {
   d_minisat->setProofLog( bvp );
 }
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 16489b172..efb90a3f0 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -119,7 +119,7 @@ public:
 
   void popAssumption() override;
 
-  void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
+  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) override;
 
  private:
   /* Disable the default constructor. */
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index cdb850ce2..84c315547 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -79,19 +79,22 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
     }
   }
 
-  PROOF(if (d_cnfProof) d_cnfProof->pushCurrentDefinition(node););
+  if (PROOF_ON() && d_cnfProof)
+  {
+    d_cnfProof->pushCurrentDefinition(node);
+  }
 
   ClauseId clause_id = d_satSolver->addClause(c, d_removable);
   if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
 
-  PROOF
-    (
-     if (d_cnfProof) {
-       Assert (clause_id != ClauseIdError);
-       d_cnfProof->registerConvertedClause(clause_id);
-       d_cnfProof->popCurrentDefinition();
-     }
-    );
+  if (PROOF_ON() && d_cnfProof)
+  {
+    if (clause_id != ClauseIdError)
+    {
+      d_cnfProof->registerConvertedClause(clause_id);
+    }
+    d_cnfProof->popCurrentDefinition();
+  };
 }
 
 void CnfStream::assertClause(TNode node, SatLiteral a) {
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index df5a20791..c04fb8b56 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -62,10 +62,11 @@ void toInternalClause(SatClause& clause,
 
 CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
                                          const std::string& name)
-: d_solver(new CMSat::SATSolver())
-, d_numVariables(0)
-, d_okay(true)
-, d_statistics(registry, name)
+    : d_solver(new CMSat::SATSolver()),
+      d_bvp(nullptr),
+      d_numVariables(0),
+      d_okay(true),
+      d_statistics(registry, name)
 {
   d_true = newVar();
   d_false = newVar();
@@ -117,9 +118,17 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
   
   std::vector<CMSat::Lit> internal_clause;
   toInternalClause(clause, internal_clause);
-  bool res = d_solver->add_clause(internal_clause);
-  d_okay &= res;
-  return ClauseIdError;
+  bool nowOkay = d_solver->add_clause(internal_clause);
+  ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId());
+
+  THEORY_PROOF(
+      // If this clause results in a conflict, then `nowOkay` may be false, but
+      // we still need to register this clause as used. Thus, we look at
+      // `d_okay` instead
+      if (d_bvp && d_okay) { d_bvp->registerUsedClause(freshId, clause); })
+
+  d_okay &= nowOkay;
+  return freshId;
 }
 
 bool CryptoMinisatSolver::ok() const {
@@ -193,6 +202,12 @@ unsigned CryptoMinisatSolver::getAssertionLevel() const {
   return -1; 
 }
 
+void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp)
+{
+  d_bvp = bvp;
+  d_solver->set_drat(&bvp->getDratOstream(), false);
+}
+
 // Satistics for CryptoMinisatSolver
 
 CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index c5345cb86..17cc1568c 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -21,6 +21,7 @@
 
 #ifdef CVC4_USE_CRYPTOMINISAT
 
+#include "proof/clausal_bitvector_proof.h"
 #include "prop/sat_solver.h"
 
 // Cryptominisat has name clashes with the other Minisat implementations since
@@ -39,6 +40,7 @@ class CryptoMinisatSolver : public SatSolver {
 
 private:
   std::unique_ptr<CMSat::SATSolver> d_solver;
+  proof::ClausalBitVectorProof* d_bvp;
   unsigned d_numVariables;
   bool d_okay;
   SatVariable d_true;
@@ -71,6 +73,7 @@ public:
   SatValue modelValue(SatLiteral l) override;
 
   unsigned getAssertionLevel() const override;
+  void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override;
 
   class Statistics {
   public:
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 49064c20f..70e46eceb 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -26,7 +26,6 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "proof/resolution_bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "prop/bv_sat_solver_notify.h"
@@ -34,6 +33,11 @@
 
 namespace CVC4 {
 
+namespace proof {
+class ClausalBitVectorProof;
+class ResolutionBitVectorProof;
+}  // namespace proof
+
 namespace prop {
 
 class TheoryProxy;
@@ -97,7 +101,9 @@ public:
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
 
-  virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
+  virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {}
+
+  virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {}
 
 };/* class SatSolver */