From 46e7f7ef87edf0228f98f8892bcd9643eecb3651 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 3 Jun 2016 11:39:12 -0500 Subject: [PATCH] Simple memory fixes, minor cleanup in quantifiers. --- src/smt/smt_engine.cpp | 14 +++--- src/theory/datatypes/theory_datatypes.cpp | 2 + .../quantifiers/inst_match_generator.cpp | 35 +++++++++++---- src/theory/quantifiers/inst_match_generator.h | 10 +++-- src/theory/quantifiers/term_database.cpp | 44 +++++-------------- src/theory/quantifiers/trigger.cpp | 2 +- 6 files changed, 54 insertions(+), 53 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8f282b413..6f4135af2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -552,10 +552,10 @@ class SmtEnginePrivate : public NodeManagerListener { */ unsigned d_simplifyAssertionsDepth; - /** whether certain preprocess steps are necessary */ - bool d_needsExpandDefs; - bool d_needsRewriteBoolTerms; - bool d_needsConstrainSubTypes; + /** TODO: whether certain preprocess steps are necessary */ + //bool d_needsExpandDefs; + //bool d_needsRewriteBoolTerms; + //bool d_needsConstrainSubTypes; public: /** @@ -684,9 +684,9 @@ public: d_abstractValueMap(&d_fakeContext), d_abstractValues(), d_simplifyAssertionsDepth(0), - d_needsExpandDefs(true), - d_needsRewriteBoolTerms(true), - d_needsConstrainSubTypes(true), //TODO + //d_needsExpandDefs(true), + //d_needsRewriteBoolTerms(true), + //d_needsConstrainSubTypes(true), //TODO d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_pbsProcessor(smt.d_userContext), diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 95d704a0e..7994351ee 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -82,6 +82,8 @@ TheoryDatatypes::~TheoryDatatypes() { Assert(current != NULL); delete current; } + delete d_sygus_split; + delete d_sygus_sym_break; } void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) { diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index bd5100a2e..2d3bf76f6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -32,6 +32,7 @@ namespace theory { namespace inst { InstMatchGenerator::InstMatchGenerator( Node pat ){ + d_cg = NULL; d_needsReset = true; d_active_add = false; Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); @@ -43,12 +44,20 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ } InstMatchGenerator::InstMatchGenerator() { + d_cg = NULL; d_needsReset = true; d_active_add = false; d_next = NULL; d_matchPolicy = MATCH_GEN_DEFAULT; } +InstMatchGenerator::~InstMatchGenerator() throw() { + for( unsigned i=0; ireset( t[ d_children_index[i] ], qe ); } Trace("matching-debug2") << "Continue next " << d_next << std::endl; @@ -484,7 +493,7 @@ d_f( q ){ } Debug("smart-multi-trigger") << std::endl; } - for( int i=0; i<(int)pats.size(); i++ ){ + for( unsigned i=0; i unique_vars; std::map< int, bool > shared_vars; int numSharedVars = 0; - for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ + for( unsigned j=0; j vars; - int index = i==0 ? (int)(pats.size()-1) : (i-1); + unsigned index = i==0 ? pats.size()-1 : (i-1); while( numSharedVars>0 && index!=i ){ for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){ if( it->second ){ @@ -519,16 +528,24 @@ d_f( q ){ } vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() ); Debug("smart-multi-trigger") << " Index[" << i << "]: "; - for( int i=0; i<(int)vars.size(); i++ ){ - Debug("smart-multi-trigger") << vars[i] << " "; + for( unsigned j=0; jd_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() ); - d_children_trie.push_back( InstMatchTrieOrdered( imtio ) ); + d_imtio[i] = new InstMatchTrie::ImtIndexOrder; + d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() ); + d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) ); } +} +InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() { + for( unsigned i=0; i::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){ + delete it->second; + } } /** reset instantiation round (call this whenever equivalence classes have changed) */ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 49e3c1ec5..096774c51 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -91,7 +91,7 @@ public: InstMatchGenerator( Node pat ); InstMatchGenerator(); /** destructor */ - ~InstMatchGenerator() throw() {} + virtual ~InstMatchGenerator() throw(); /** The pattern we are producing matches for. If null, this is a multi trigger that is merging matches from d_children. */ @@ -125,7 +125,7 @@ public: class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { public: VarMatchGeneratorBooleanTerm( Node var, Node comp ); - ~VarMatchGeneratorBooleanTerm() throw() {} + virtual ~VarMatchGeneratorBooleanTerm() throw() {} Node d_comp; bool d_rm_prev; /** reset instantiation round (call this at beginning of instantiation round) */ @@ -142,7 +142,7 @@ public: class VarMatchGeneratorTermSubs : public InstMatchGenerator { public: VarMatchGeneratorTermSubs( Node var, Node subs ); - ~VarMatchGeneratorTermSubs() throw() {} + virtual ~VarMatchGeneratorTermSubs() throw() {} TNode d_var; TypeNode d_var_type; Node d_subs; @@ -183,6 +183,8 @@ private: int d_matchPolicy; /** children generators */ std::vector< InstMatchGenerator* > d_children; + /** order */ + std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio; /** inst match tries for each child */ std::vector< InstMatchTrieOrdered > d_children_trie; /** calculate matches */ @@ -191,7 +193,7 @@ public: /** constructors */ InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ); /** destructor */ - ~InstMatchGeneratorMulti() throw() {} + virtual ~InstMatchGeneratorMulti() throw(); /** reset instantiation round (call this whenever equivalence classes have changed) */ void resetInstantiationRound( QuantifiersEngine* qe ); /** reset, eqc is the equivalence class to search in (any if eqc=null) */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5645c3401..c34d86497 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -238,10 +238,15 @@ void TermDb::computeUfTerms( TNode f ) { if( it!=d_op_map.end() ){ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); Trace("term-db-debug") << "Adding terms for operator " << f << std::endl; + unsigned congruentCount = 0; + unsigned nonCongruentCount = 0; + unsigned alreadyCongruentCount = 0; + unsigned relevantCount = 0; for( unsigned i=0; isecond.size(); i++ ){ Node n = it->second[i]; //to be added to term index, term must be relevant, and exist in EE if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ + relevantCount++; if( isTermActive( n ) ){ computeArgReps( n ); @@ -260,7 +265,7 @@ void TermDb::computeUfTerms( TNode f ) { if( at!=n && ee->areEqual( at, n ) ){ setTermInactive( n ); Trace("term-db-debug") << n << " is redundant." << std::endl; - //congruentCount++; + congruentCount++; }else{ if( at!=n && ee->areDisequal( at, n, false ) ){ std::vector< Node > lits; @@ -282,29 +287,22 @@ void TermDb::computeUfTerms( TNode f ) { d_consistent_ee = false; return; } - //nonCongruentCount++; + nonCongruentCount++; d_op_nonred_count[ f ]++; } }else{ Trace("term-db-debug") << n << " is already redundant." << std::endl; - //congruentCount++; - //alreadyCongruentCount++; + alreadyCongruentCount++; } }else{ Trace("term-db-debug") << n << " is not relevant." << std::endl; - //nonRelevantCount++; } } - - /* - if( Trace.isOn("term-db-index") ){ - Trace("term-db-index") << "Term index for " << f << " : " << std::endl; - Trace("term-db-index") << "- " << it->first << std::endl; - d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]); - Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = "; - Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; + if( Trace.isOn("tdb") ){ + Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / "; + Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / "; + Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl; } - */ } } } @@ -676,10 +674,6 @@ void TermDb::presolve() { } bool TermDb::reset( Theory::Effort effort ){ - //int nonCongruentCount = 0; - //int congruentCount = 0; - //int alreadyCongruentCount = 0; - //int nonRelevantCount = 0; d_op_nonred_count.clear(); d_arg_reps.clear(); d_func_map_trie.clear(); @@ -743,20 +737,6 @@ bool TermDb::reset( Theory::Effort effort ){ } } */ - /* - Trace("term-db-stats") << "TermDb: Reset" << std::endl; - Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = "; - Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; - if( Trace.isOn("term-db-index") ){ - Trace("term-db-index") << "functions : " << std::endl; - for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - if( it->second.size()>0 ){ - Trace("term-db-index") << "- " << it->first << std::endl; - d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]); - } - } - } - */ return true; } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 214a4d055..802acc089 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -86,7 +86,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) } Trigger::~Trigger() { - if(d_mg != NULL) { delete d_mg; } + delete d_mg; } void Trigger::resetInstantiationRound(){ -- 2.30.2