From: Tim King Date: Mon, 7 Nov 2016 18:24:11 +0000 (-0800) Subject: Fixing a memory leak in the eager bitblaster. X-Git-Tag: cvc5-1.0.0~5999 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6364f7d8f368f9c03857fa433ea452b58e54514;p=cvc5.git Fixing a memory leak in the eager bitblaster. --- 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 { 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() - , d_satSolver(NULL) - , d_bitblastingRegistrar(NULL) - , d_nullContext(NULL) - , d_cnfStream(NULL) - , d_bv(theory_bv) - , d_bbAtoms() - , d_variables() - , d_notify() -{ + : TBitblaster(), + 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);