Fixing a memory leak in the eager bitblaster.

2 files changed, 69 insertions, 73 deletions

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 929bccada..0a7d165a2 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -266,7 +266,8 @@ class EagerBitblaster : public TBitblaster<Node> {
   TNodeSet d_bbAtoms;
   TNodeSet d_variables;
 
-  MinisatEmptyNotify d_notify;
+  // This is either an MinisatEmptyNotify or NULL.
+  MinisatEmptyNotify* d_notify;
 
   Node getModelFromSatSolver(TNode a, bool fullModel);
   bool isSharedTerm(TNode node);
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index e66b7f621..2ceca7423 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -17,59 +17,54 @@
 #include "cvc4_private.h"
 
 #include "options/bv_options.h"
+#include "proof/bitvector_proof.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"
 
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-void BitblastingRegistrar::preRegister(Node n) {
-  d_bitblaster->bbAtom(n);
-};
+void BitblastingRegistrar::preRegister(Node n) { d_bitblaster->bbAtom(n); }
 
 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
-  : TBitblaster<Node>()
-  , d_satSolver(NULL)
-  , d_bitblastingRegistrar(NULL)
-  , d_nullContext(NULL)
-  , d_cnfStream(NULL)
-  , d_bv(theory_bv)
-  , d_bbAtoms()
-  , d_variables()
-  , d_notify()
-{
+    : TBitblaster<Node>(),
+      d_satSolver(NULL),
+      d_bitblastingRegistrar(NULL),
+      d_nullContext(NULL),
+      d_cnfStream(NULL),
+      d_bv(theory_bv),
+      d_bbAtoms(),
+      d_variables(),
+      d_notify(NULL) {
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
-  
-  switch(options::bvSatSolver()) {
-  case SAT_SOLVER_MINISAT: {
-    prop::BVSatSolverInterface* minisat =
-      prop::SatSolverFactory::createMinisat(d_nullContext,
-                                            smtStatisticsRegistry(),
-                                            "EagerBitblaster");
-    MinisatEmptyNotify* notify = new MinisatEmptyNotify();
-    minisat->setNotify(notify);
-    d_satSolver = minisat;
-    break;
-  }
-  case SAT_SOLVER_CRYPTOMINISAT:
-    d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(),
-                                                              "EagerBitblaster");
-    break;
-  default:
-    Unreachable("Unknown SAT solver type");
+
+  switch (options::bvSatSolver()) {
+    case SAT_SOLVER_MINISAT: {
+      prop::BVSatSolverInterface* minisat =
+          prop::SatSolverFactory::createMinisat(
+              d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
+      d_notify = new MinisatEmptyNotify();
+      minisat->setNotify(d_notify);
+      d_satSolver = minisat;
+      break;
+    }
+    case SAT_SOLVER_CRYPTOMINISAT:
+      d_satSolver = prop::SatSolverFactory::createCryptoMinisat(
+          smtStatisticsRegistry(), "EagerBitblaster");
+      break;
+    default:
+      Unreachable("Unknown SAT solver type");
   }
 
-  d_cnfStream = new prop::TseitinCnfStream(
-      d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(),
-      "EagerBitblaster");
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
+                                           d_nullContext, options::proof(),
+                                           "EagerBitblaster");
 
   d_bvp = NULL;
 }
@@ -77,12 +72,14 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
 EagerBitblaster::~EagerBitblaster() {
   delete d_cnfStream;
   delete d_satSolver;
+  delete d_notify;
   delete d_nullContext;
   delete d_bitblastingRegistrar;
 }
 
 void EagerBitblaster::bbFormula(TNode node) {
-  d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, TNode::null());
+  d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID,
+                                TNode::null());
 }
 
 /**
@@ -92,20 +89,20 @@ void EagerBitblaster::bbFormula(TNode node) {
  *
  */
 void EagerBitblaster::bbAtom(TNode node) {
-  node = node.getKind() == kind::NOT?  node[0] : node;
-  if (node.getKind() == kind::BITVECTOR_BITOF)
-    return;
+  node = node.getKind() == kind::NOT ? node[0] : node;
+  if (node.getKind() == kind::BITVECTOR_BITOF) return;
   if (hasBBAtom(node)) {
     return;
   }
 
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+  Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
 
   // the bitblasted definition of the atom
   Node normalized = Rewriter::rewrite(node);
-  Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
-    d_atomBBStrategies[normalized.getKind()](normalized, this) :
-    normalized;
+  Node atom_bb =
+      normalized.getKind() != kind::CONST_BOOLEAN
+          ? d_atomBBStrategies[normalized.getKind()](normalized, this)
+          : normalized;
 
   if (!options::proof()) {
     atom_bb = Rewriter::rewrite(atom_bb);
@@ -114,42 +111,44 @@ void EagerBitblaster::bbAtom(TNode node) {
   // 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);
+  AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   storeBBAtom(node, atom_bb);
-  d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
+  d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID,
+                                TNode::null());
 }
 
 void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
-  if( d_bvp ){
+  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()); }
+  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();
 }
 
 void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
-  Assert( node.getType().isBitVector() );
-  
+  Assert(node.getType().isBitVector());
+
   if (hasBBTerm(node)) {
     getBBTerm(node, bits);
     return;
   }
 
   d_bv->spendResource(options::bitblastStep());
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+  Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
 
-  d_termBBStrategies[node.getKind()] (node, bits, this);
+  d_termBBStrategies[node.getKind()](node, bits, this);
 
-  Assert (bits.size() == utils::getSize(node));
+  Assert(bits.size() == utils::getSize(node));
 
   storeBBTerm(node, bits);
 }
@@ -162,10 +161,7 @@ void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
   d_variables.insert(var);
 }
 
-Node EagerBitblaster::getBBAtom(TNode node) const {
-  return node;
-}
-
+Node EagerBitblaster::getBBAtom(TNode node) const { return node; }
 
 /**
  * Calls the solve method for the Sat Solver.
@@ -187,7 +183,6 @@ bool EagerBitblaster::solve() {
   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
-
 /**
  * Returns the value a is currently assigned to in the SAT solver
  * or null if the value is completely unassigned.
@@ -200,52 +195,52 @@ bool EagerBitblaster::solve() {
  */
 Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
   if (!hasBBTerm(a)) {
-    return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
+    return fullModel ? utils::mkConst(utils::getSize(a), 0u) : Node();
   }
 
   Bits bits;
   getBBTerm(a, bits);
   Integer value(0);
-  for (int i = bits.size() -1; i >= 0; --i) {
+  for (int i = bits.size() - 1; i >= 0; --i) {
     prop::SatValue bit_value;
     if (d_cnfStream->hasLiteral(bits[i])) {
       prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
-      Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
+      Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
     } else {
       if (!fullModel) return Node();
       // unconstrained bits default to false
       bit_value = prop::SAT_VALUE_FALSE;
     }
-    Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+    Integer bit_int =
+        bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
     value = value * 2 + bit_int;
   }
   return utils::mkConst(BitVector(bits.size(), value));
 }
 
-
 void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   TNodeSet::iterator it = d_variables.begin();
-  for (; it!= d_variables.end(); ++it) {
+  for (; it != d_variables.end(); ++it) {
     TNode var = *it;
     if (d_bv->isLeaf(var) || isSharedTerm(var) ||
-        (var.isVar() && var.getType().isBoolean()))  {
+        (var.isVar() && var.getType().isBoolean())) {
       // only shared terms could not have been bit-blasted
-      Assert (hasBBTerm(var) || isSharedTerm(var));
+      Assert(hasBBTerm(var) || isSharedTerm(var));
 
       Node const_value = getModelFromSatSolver(var, true);
 
-      if(const_value != Node()) {
-        Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= "
-                                 << var << " "
-                                 << const_value << "))\n";
+      if (const_value != Node()) {
+        Debug("bitvector-model")
+            << "EagerBitblaster::collectModelInfo (assert (= " << var << " "
+            << const_value << "))\n";
         m->assertEquality(var, const_value, true);
       }
     }
   }
 }
 
-void EagerBitblaster::setProofLog( BitVectorProof * bvp ) {
+void EagerBitblaster::setProofLog(BitVectorProof* bvp) {
   d_bvp = bvp;
   d_satSolver->setProofLog(bvp);
   bvp->initCnfProof(d_cnfStream, d_nullContext);