1 files changed, 37 insertions, 15 deletions

diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 000abe62b..2e4f06c38 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -19,16 +19,13 @@
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
+#include "proof/bitvector_proof.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -46,13 +43,19 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
 
-  d_satSolver = prop::SatSolverFactory::createMinisat(
-      d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
-                                           d_nullContext, d_bv->globals());
-
+  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext,
+                                                      smtStatisticsRegistry(),
+                                                      "EagerBitblaster");
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
+                                           d_bitblastingRegistrar,
+                                           d_nullContext,
+                                           d_bv->globals(),
+                                           options::proof(),
+                                           "EagerBitblaster");
+  
   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
   d_satSolver->setNotify(notify);
+  d_bvp = NULL;
 }
 
 EagerBitblaster::~EagerBitblaster() {
@@ -85,21 +88,34 @@ void EagerBitblaster::bbAtom(TNode node) {
   // the bitblasted definition of the atom
   Node normalized = Rewriter::rewrite(node);
   Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
-      Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
-      normalized;
+    d_atomBBStrategies[normalized.getKind()](normalized, this) :
+    normalized;
+
+  if (!options::proof()) {
+    atom_bb = Rewriter::rewrite(atom_bb);
+  }
+
   // asserting that the atom is true iff the definition holds
   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
 
-  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
-  storeBBAtom(node, atom_definition);
+  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); 
+  storeBBAtom(node, atom_bb);
   d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 }
 
 void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
-  // no need to store the definition for the lazy bit-blaster
-  d_bbAtoms.insert(atom);
+  if( d_bvp ){
+    d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
+  }
+  d_bbAtoms.insert(atom); 
 }
 
+void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
+  if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); }
+  d_termCache.insert(std::make_pair(node, bits));
+}
+
+
 bool EagerBitblaster::hasBBAtom(TNode atom) const {
   return d_bbAtoms.find(atom) != d_bbAtoms.end();
 }
@@ -211,6 +227,12 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   }
 }
 
+void EagerBitblaster::setProofLog( BitVectorProof * bvp ) {
+  d_bvp = bvp;
+  d_satSolver->setProofLog(bvp);
+  bvp->initCnfProof(d_cnfStream, d_nullContext);
+}
+
 bool EagerBitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }