From 60cd271c46e7b250e3799f1c3b1fc20015723999 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 4 Nov 2016 16:28:20 -0500 Subject: [PATCH] Fix a few more minor memory leaks. --- src/smt/smt_engine.cpp | 40 ++++++++++++-------------- src/smt/smt_engine.h | 7 ++--- src/theory/quantifiers/anti_skolem.cpp | 11 ++++++- src/theory/quantifiers/anti_skolem.h | 3 +- src/theory/theory_engine.cpp | 2 +- 5 files changed, 34 insertions(+), 29 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c9484dbf0..46469fb0d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -989,8 +989,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_propEngine(NULL), d_proofManager(NULL), d_definedFunctions(NULL), - d_fmfRecFunctionsAbs(NULL), - d_fmfRecFunctionsConcrete(NULL), + d_fmfRecFunctionsDefined(NULL), d_assertionList(NULL), d_assignments(NULL), d_modelGlobalCommands(), @@ -1059,8 +1058,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); if( options::fmfFunWellDefined() || options::fmfFunWellDefinedRelevant() ){ - d_fmfRecFunctionsAbs = new(true) TypeNodeMap(d_userContext); - d_fmfRecFunctionsConcrete = new(true) NodeListMap(d_userContext); + d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext); } d_modelCommands = new(true) smt::CommandList(d_userContext); } @@ -1206,13 +1204,10 @@ SmtEngine::~SmtEngine() throw() { d_definedFunctions->deleteSelf(); - if( d_fmfRecFunctionsAbs != NULL ){ - d_fmfRecFunctionsAbs->deleteSelf(); + if( d_fmfRecFunctionsDefined != NULL ){ + d_fmfRecFunctionsDefined->deleteSelf(); } - if( d_fmfRecFunctionsConcrete != NULL ){ - d_fmfRecFunctionsConcrete->deleteSelf(); - } - + delete d_theoryEngine; d_theoryEngine = NULL; delete d_propEngine; @@ -3998,27 +3993,28 @@ void SmtEnginePrivate::processAssertions() { if( options::fmfFunWellDefined() ){ quantifiers::FunDefFmf fdf; //must carry over current definitions (for incremental) - for( SmtEngine::TypeNodeMap::const_iterator fit = d_smt.d_fmfRecFunctionsAbs->begin(); fit != d_smt.d_fmfRecFunctionsAbs->end(); ++fit ){ - Node f = (*fit).first; - TypeNode ft = (*fit).second; + for( context::CDList::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin(); + fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) { + Node f = (*fit); + Assert( d_smt.d_fmfRecFunctionsAbs.find( f )!=d_smt.d_fmfRecFunctionsAbs.end() ); + TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f]; fdf.d_sorts[f] = ft; - SmtEngine::NodeListMap::const_iterator fcit = d_smt.d_fmfRecFunctionsConcrete->find( f ); - Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete->end() ); - SmtEngine::NodeList* cl = (*fcit).second; - for( SmtEngine::NodeList::const_iterator cit = cl->begin(); cit != cl->end(); ++cit ){ - fdf.d_input_arg_inj[f].push_back( *cit ); + std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f ); + Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete.end() ); + for( unsigned j=0; jsecond.size(); j++ ){ + fdf.d_input_arg_inj[f].push_back( fcit->second[j] ); } } fdf.simplify( d_assertions.ref() ); //must store new definitions (for incremental) for( unsigned i=0; iinsert( f, fdf.d_sorts[f] ); - SmtEngine::NodeList* cl = new(true) SmtEngine::NodeList( d_smt.d_userContext ); + d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f]; + d_smt.d_fmfRecFunctionsConcrete[f].clear(); for( unsigned j=0; jpush_back( fdf.d_input_arg_inj[f][j] ); + d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] ); } - d_smt.d_fmfRecFunctionsConcrete->insert( f, cl ); + d_smt.d_fmfRecFunctionsDefined->push_back( f ); } } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 760c7c071..f1ce2e0e9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -130,9 +130,7 @@ class CVC4_PUBLIC SmtEngine { /** The type of our internal assignment set */ typedef context::CDHashSet AssignmentSet; /** The types for the recursive function definitions */ - typedef context::CDHashMap< Node, TypeNode, NodeHashFunction > TypeNodeMap; typedef context::CDList NodeList; - typedef context::CDHashMap NodeListMap; /** Expr manager context */ context::Context* d_context; @@ -157,8 +155,9 @@ class CVC4_PUBLIC SmtEngine { /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; /** recursive function definition abstractions for --fmf-fun */ - TypeNodeMap* d_fmfRecFunctionsAbs; - NodeListMap* d_fmfRecFunctionsConcrete; + std::map< Node, TypeNode > d_fmfRecFunctionsAbs; + std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; + NodeList* d_fmfRecFunctionsDefined; /** * The assertion list (before any conversion) for supporting diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index 9ccba38cd..908aeecfd 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Implementation of anti-skolemization + ** \brief Implementation of anti-skolemization, e.g.: ** ( forall x. P[ f( x ) ] ^ forall x. Q[ f( x ) ] ) => forall x. exists y. ( P[ y ] ^ Q[ y ] ) **/ @@ -75,6 +75,15 @@ bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Nod } } +QuantAntiSkolem::CDSkQuantCache::~CDSkQuantCache() { + for(std::map< Node, CDSkQuantCache* >::iterator i = d_data.begin(), iend = d_data.end(); + i != iend; ++i){ + CDSkQuantCache* current = (*i).second; + Assert(current != NULL); + delete current; + } +} + QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe) : QuantifiersModule(qe) { d_sqc = new CDSkQuantCache(qe->getUserContext()); diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 48205db9d..c996b171e 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief dynamic quantifiers splitting + ** \brief anti-skolemization **/ #include "cvc4_private.h" @@ -71,6 +71,7 @@ public: class CDSkQuantCache { public: CDSkQuantCache( context::Context* c ) : d_valid( c, false ){} + ~CDSkQuantCache(); std::map< Node, CDSkQuantCache* > d_data; context::CDO< bool > d_valid; bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 ); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9de8fa0dd..cf7611dab 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -739,7 +739,7 @@ void TheoryEngine::propagate(Theory::Effort effort) { Node TheoryEngine::getNextDecisionRequest() { // Definition of the statement that is to be run by every theory - unsigned min_priority; + unsigned min_priority = 0; Node dec; #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT -- 2.30.2