1 files changed, 19 insertions, 39 deletions

diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h
index ccb288f6e..6c2ae589f 100644
--- a/src/proof/resolution_bitvector_proof.h
+++ b/src/proof/resolution_bitvector_proof.h
@@ -24,32 +24,16 @@
 #include "context/context.h"
 #include "expr/expr.h"
 #include "proof/bitvector_proof.h"
+#include "proof/sat_proof.h"
 #include "proof/theory_proof.h"
 #include "prop/bvminisat/core/Solver.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_types.h"
+#include "theory/bv/bitblast/bitblaster.h"
+#include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
 
-namespace theory {
-namespace bv {
-class TheoryBV;
-template <class T>
-class TBitblaster;
-}  // namespace bv
-}  // namespace theory
-
-// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream
-// header cycle and remove this.
-namespace prop {
-class CnfStream;
-}
-
-} /* namespace CVC4 */
-
-
-namespace CVC4 {
-
-template <class Solver>
-class TSatProof;
 typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof;
 
 namespace proof {
@@ -76,13 +60,7 @@ class ResolutionBitVectorProof : public BitVectorProof
 
   BVSatProof* getSatProof();
 
-  /**
-   * Kind of a mess.
-   * In eager mode this must be invoked before printing a proof of the empty
-   * clause. In lazy mode the behavior is ???
-   * TODO(aozdemir) clean this up.
-   */
-  void finalizeConflicts(std::vector<Expr>& conflicts);
+  void finalizeConflicts(std::vector<Expr>& conflicts) override;
 
   void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
   void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
@@ -91,13 +69,14 @@ class ResolutionBitVectorProof : public BitVectorProof
   void markAssumptionConflict() { d_isAssumptionConflict = true; }
   bool isAssumptionConflict() const { return d_isAssumptionConflict; }
 
-  virtual void printResolutionProof(std::ostream& os,
-                                    std::ostream& paren,
-                                    ProofLetMap& letMap) = 0;
-
-  void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override;
+  void initCnfProof(prop::CnfStream* cnfStream,
+                    context::Context* cnf,
+                    prop::SatVariable trueVar,
+                    prop::SatVariable falseVar) override;
 
  protected:
+  void attachToSatSolver(prop::SatSolver& sat_solver) override;
+
   context::Context d_fakeContext;
 
   // The CNF formula that results from bit-blasting will need a proof.
@@ -106,13 +85,13 @@ class ResolutionBitVectorProof : public BitVectorProof
 
   bool d_isAssumptionConflict;
 
-  theory::TheoryId getTheoryId() override;
 };
 
-class LFSCBitVectorProof : public ResolutionBitVectorProof
+class LfscResolutionBitVectorProof : public ResolutionBitVectorProof
 {
  public:
-  LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+  LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv,
+                               TheoryProofEngine* proofEngine)
       : ResolutionBitVectorProof(bv, proofEngine)
   {
   }
@@ -120,9 +99,10 @@ class LFSCBitVectorProof : public ResolutionBitVectorProof
                              std::ostream& os,
                              std::ostream& paren,
                              const ProofLetMap& map) override;
-  void printResolutionProof(std::ostream& os,
-                            std::ostream& paren,
-                            ProofLetMap& letMap) override;
+  void printBBDeclarationAndCnf(std::ostream& os,
+                                std::ostream& paren,
+                                ProofLetMap& letMap) override;
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
   void calculateAtomsInBitblastingProof() override;
 };