From: Tim King Date: Wed, 23 Mar 2016 18:12:04 +0000 (-0700) Subject: Fixing memory leaks in Trigger and TriggerTrie. X-Git-Tag: cvc5-1.0.0~6049^2~93 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=786cd2dd5b1c53f650c891d6dfbf299a62840848;p=cvc5.git Fixing memory leaks in Trigger and TriggerTrie. --- diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 48385e28b..efffe10bd 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -21,17 +21,22 @@ #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" +#include "util/hash.h" + using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::inst; + +namespace CVC4 { +namespace theory { +namespace inst { /** trigger class constructor */ -Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : -d_quantEngine( qe ), d_f( f ){ +Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, + int matchOption, bool smartTriggers ) + : d_quantEngine( qe ), d_f( f ) +{ d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); Trace("trigger") << "Trigger for " << f << ": " << std::endl; for( int i=0; i<(int)d_nodes.size(); i++ ){ @@ -80,6 +85,10 @@ d_quantEngine( qe ), d_f( f ){ Trace("trigger-debug") << "Finished making trigger." << std::endl; } +Trigger::~Trigger() { + if(d_mg != NULL) { delete d_mg; } +} + void Trigger::resetInstantiationRound(){ d_mg->resetInstantiationRound( d_quantEngine ); } @@ -653,6 +662,12 @@ Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ if( nodes.empty() ){ + if(d_tr != NULL){ + // TODO: Andy can you look at fmf/QEpres-uf.855035.smt? + delete d_tr; + d_tr = NULL; + } + Assert(d_tr == NULL); d_tr = t; }else{ Node n = nodes.back(); @@ -663,3 +678,23 @@ void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ d_children[n]->addTrigger2( nodes, t ); } } + + +TriggerTrie::TriggerTrie() + : d_tr( NULL ) +{} + +TriggerTrie::~TriggerTrie() { + for(std::map< TNode, TriggerTrie* >::iterator i = d_children.begin(), iend = d_children.end(); + i != iend; ++i) { + TriggerTrie* current = (*i).second; + delete current; + } + d_children.clear(); + + if(d_tr != NULL) { delete d_tr; } +} + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index bbbf9495f..2ca2eb55d 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -17,11 +17,12 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H #define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H -#include "theory/quantifiers/inst_match.h" -#include "expr/node.h" -#include "util/hash.h" #include +#include "expr/node.h" +#include "theory/quantifiers/inst_match.h" + +// Forward declarations for defining the Trigger and TriggerTrie. namespace CVC4 { namespace theory { @@ -31,29 +32,27 @@ namespace inst { class IMGenerator; class InstMatchGenerator; +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + -//a collect of nodes representing a trigger +namespace CVC4 { +namespace theory { +namespace inst { + +/** A collect of nodes representing a trigger. */ class Trigger { -private: - /** the quantifiers engine */ - QuantifiersEngine* d_quantEngine; - /** the quantifier this trigger is for */ - Node d_f; - /** match generators */ - IMGenerator* d_mg; -private: - /** trigger constructor */ - Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false ); -public: - ~Trigger(){} -public: - std::vector< Node > d_nodes; -public: + public: + ~Trigger(); + IMGenerator* getGenerator() { return d_mg; } -public: - /** reset instantiation round (call this whenever equivalence classes have changed) */ + + /** reset instantiation round (call this whenever equivalence + * classes have changed) */ void resetInstantiationRound(); - /** reset, eqc is the equivalence class to search in (search in any if eqc=null) */ + /** reset, eqc is the equivalence class to search in (search in any + * if eqc=null) */ void reset( Node eqc ); /** get next match. must call reset( eqc ) once before this function. */ bool getNextMatch( Node f, InstMatch& m ); @@ -66,7 +65,7 @@ public: int addTerm( Node t ); /** return whether this is a multi-trigger */ bool isMultiTrigger() { return d_nodes.size()>1; } -public: + /** add all available instantiations exhaustively, in any equivalence class if limitInst>0, limitInst is the max # of instantiations to try */ int addInstantiations( InstMatch& baseMatch ); @@ -74,36 +73,35 @@ public: ie : quantifier engine; f : forall something .... nodes : (multi-)trigger - matchOption : which policy to use for creating matches (one of InstMatchGenerator::MATCH_GEN_* ) + matchOption : which policy to use for creating matches + (one of InstMatchGenerator::MATCH_GEN_* ) keepAll: don't remove unneeded patterns; - trOption : policy for dealing with triggers that already existed (see below) + trOption : policy for dealing with triggers that already existed + (see below) */ enum{ TR_MAKE_NEW, //make new trigger even if it already may exist TR_GET_OLD, //return a previous trigger if it had already been created TR_RETURN_NULL //return null if a duplicate is found }; - static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, - int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW, + static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, + std::vector< Node >& nodes, int matchOption = 0, + bool keepAll = true, int trOption = TR_MAKE_NEW, bool smartTriggers = false ); static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, - int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW, + int matchOption = 0, bool keepAll = true, + int trOption = TR_MAKE_NEW, bool smartTriggers = false ); -private: - /** is subterm of trigger usable */ - static bool isUsable( Node n, Node q ); - static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); - /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); -public: //different strategies for choosing trigger terms enum { TS_MAX_TRIGGER = 0, TS_MIN_TRIGGER, TS_ALL, }; - static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst = false ); -public: + static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, + std::vector< Node >& patTerms, int tstrt, + std::vector< Node >& exclude, + bool filterInst = false ); /** is usable trigger */ static bool isUsableTrigger( Node n, Node q ); static bool isAtomicTrigger( Node n ); @@ -113,13 +111,15 @@ public: static bool isBooleanTermTrigger( Node n ); static bool isPureTheoryTrigger( Node n ); static int getTriggerWeight( Node n ); - static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ); + static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, + std::vector< Node >& patTerms ); /** return data structure for producing matches for this trigger. */ static InstMatchGenerator* getInstMatchGenerator( Node q, Node n ); static Node getInversionVariable( Node n ); static Node getInversion( Node n, Node x ); /** get all variables that E-matching can possibly handle */ - static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ); + static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, + std::vector< Node >& t_vars ); void debugPrint( const char * c ) { Trace(c) << "TRIGGER( "; @@ -129,17 +129,37 @@ public: } Trace(c) << " )"; } -}; + +private: + /** trigger constructor */ + Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, + int matchOption = 0, bool smartTriggers = false ); + + /** is subterm of trigger usable */ + static bool isUsable( Node n, Node q ); + static Node getIsUsableTrigger( Node n, Node f, bool pol = true, + bool hasPol = false ); + /** collect all APPLY_UF pattern terms for f in n */ + static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, + int tstrt, std::vector< Node >& exclude, + bool pol, bool hasPol ); + + std::vector< Node > d_nodes; + + /** the quantifiers engine */ + QuantifiersEngine* d_quantEngine; + /** the quantifier this trigger is for */ + Node d_f; + /** match generators */ + IMGenerator* d_mg; +}; /* class Trigger */ /** a trie of triggers */ class TriggerTrie { -private: - inst::Trigger* getTrigger2( std::vector< Node >& nodes ); - void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t ); public: - TriggerTrie() : d_tr( NULL ){} - inst::Trigger* d_tr; - std::map< TNode, TriggerTrie* > d_children; + TriggerTrie(); + ~TriggerTrie(); + inst::Trigger* getTrigger( std::vector< Node >& nodes ){ std::vector< Node > temp; temp.insert( temp.begin(), nodes.begin(), nodes.end() ); @@ -152,7 +172,13 @@ public: std::sort( temp.begin(), temp.end() ); return addTrigger2( temp, t ); } -};/* class inst::Trigger::Trigger */ +private: + inst::Trigger* getTrigger2( std::vector< Node >& nodes ); + void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t ); + + inst::Trigger* d_tr; + std::map< TNode, TriggerTrie* > d_children; +};/* class inst::Trigger::TriggerTrie */ }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */