From 1af684a72f31f54243eca9ef902c0e7ecd8486d7 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 24 Mar 2016 10:44:05 -0700 Subject: [PATCH] Fixing a memory leak in QuantInfo::d_var_mg. --- .../quantifiers/quant_conflict_find.cpp | 37 +++++++++++++------ src/theory/quantifiers/quant_conflict_find.h | 24 +++++++++--- src/theory/quantifiers/rewrite_engine.cpp | 5 ++- 3 files changed, 47 insertions(+), 19 deletions(-) diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index ec93b96fc..ecf2f055a 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -24,14 +24,26 @@ #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; using namespace std; namespace CVC4 { +namespace theory { +namespace quantifiers { +QuantInfo::QuantInfo() + : d_mg( NULL ) +{} + +QuantInfo::~QuantInfo() { + delete d_mg; + for(std::map< int, MatchGen * >::iterator i = d_var_mg.begin(), + iend=d_var_mg.end(); i != iend; ++i) { + MatchGen* currentMatchGenerator = (*i).second; + delete currentMatchGenerator; + } + d_var_mg.clear(); +} void QuantInfo::initialize( Node q, Node qn ) { @@ -1260,12 +1272,12 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { Debug("qcf-match-debug") << "..." << std::endl; while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){ - std::map< int, MatchGen * >::iterator itm; + QuantInfo::VarMgMap::const_iterator itm; if( !doFail ){ Debug("qcf-match-debug") << " check variable " << d_binding_it->second << std::endl; - itm = qi->d_var_mg.find( d_binding_it->second ); + itm = qi->var_mg_find( d_binding_it->second ); } - if( doFail || ( d_binding_it->first!=0 && itm!=qi->d_var_mg.end() ) ){ + if( doFail || ( d_binding_it->first!=0 && itm != qi->var_mg_end() ) ){ Debug("qcf-match-debug") << " we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl; if( doReset ){ itm->second->reset( p, true, qi ); @@ -1279,7 +1291,9 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { --d_binding_it; Debug("qcf-match-debug") << " decrement..." << std::endl; } - }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) ); + }while( success && + ( d_binding_it->first==0 || + (!qi->containsVarMg(d_binding_it->second)))); doReset = false; doFail = false; }else{ @@ -2022,7 +2036,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { QuantInfo * qi = &d_qinfo[q]; Assert( d_qinfo.find( q )!=d_qinfo.end() ); - if( qi->d_mg->isValid() ){ + if( qi->matchGeneratorIsValid() ){ Trace("qcf-check") << "Check quantified formula "; debugPrintQuant("qcf-check", q); Trace("qcf-check") << " : " << q << "..." << std::endl; @@ -2031,7 +2045,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { qi->reset_round( this ); //try to make a matches making the body false Trace("qcf-check-debug") << "Get next match..." << std::endl; - while( qi->d_mg->getNextMatch( this, qi ) ){ + while( qi->getNextMatch( this ) ){ Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; qi->debugPrintMatch("qcf-inst"); Trace("qcf-inst") << std::endl; @@ -2278,5 +2292,6 @@ TNode QuantConflictFind::getZero( Kind k ) { } } - -} +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 4bcc59bde..a9fb27d26 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -115,8 +115,8 @@ private: //for completing match int d_una_index; std::vector< int > d_una_eqc_count; public: - QuantInfo() : d_mg( NULL ) {} - ~QuantInfo() { delete d_mg; } + QuantInfo(); + ~QuantInfo(); std::vector< TNode > d_vars; std::vector< TypeNode > d_var_types; std::map< TNode, int > d_var_num; @@ -128,9 +128,21 @@ public: int getNumVars() { return (int)d_vars.size(); } TNode getVar( int i ) { return d_vars[i]; } + typedef std::map< int, MatchGen * > VarMgMap; + private: MatchGen * d_mg; + VarMgMap d_var_mg; + public: + VarMgMap::const_iterator var_mg_find(int i) const { return d_var_mg.find(i); } + VarMgMap::const_iterator var_mg_end() const { return d_var_mg.end(); } + bool containsVarMg(int i) const { return var_mg_find(i) != var_mg_end(); } + + bool matchGeneratorIsValid() const { return d_mg->isValid(); } + bool getNextMatch( QuantConflictFind * p) { + return d_mg->getNextMatch(p, this); + } + Node d_q; - std::map< int, MatchGen * > d_var_mg; void reset_round( QuantConflictFind * p ); public: //initialize @@ -248,8 +260,8 @@ public: std::string identify() const { return "QcfEngine"; } }; -} -} -} +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ #endif diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 4c8050239..a8cdd2bc2 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -124,12 +124,13 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f ); if( it!=d_qinfo.end() ){ QuantInfo * qi = &it->second; - if( qi->d_mg->isValid() ){ + if( qi->matchGeneratorIsValid() ){ Node rr = TermDb::getRewriteRule( f ); Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; qi->reset_round( qcf ); Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; - while( qi->d_mg->getNextMatch( qcf, qi ) && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ + while( qi->getNextMatch( qcf ) && + ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ Trace("rewrite-engine-inst-debug") << " Got match to complete..." << std::endl; qi->debugPrintMatch( "rewrite-engine-inst-debug" ); std::vector< int > assigned; -- 2.30.2