From 7dc4bbc411cbfcafbc866d4e90d532d7c8a4178f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 3 Jun 2016 14:20:55 -0500 Subject: [PATCH] Remove NodeListMap from strings, fixes memory leaks. Fix for regexp intersection. --- src/theory/strings/regexp_operation.cpp | 4 + src/theory/strings/regexp_operation.h | 1 + src/theory/strings/theory_strings.cpp | 179 ++++++++++-------- src/theory/strings/theory_strings.h | 12 +- .../strings/theory_strings_preprocess.cpp | 4 + .../strings/theory_strings_preprocess.h | 1 + 6 files changed, 116 insertions(+), 85 deletions(-) diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 53344dd6c..a665a02c1 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -39,6 +39,10 @@ RegExpOpr::RegExpOpr() d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma ); } +RegExpOpr::~RegExpOpr(){ + +} + int RegExpOpr::gcd ( int a, int b ) { int c; while ( a != 0 ) { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index c537553f2..075391370 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -99,6 +99,7 @@ private: public: RegExpOpr(); + ~RegExpOpr(); bool checkConstRegExp( Node r ); void simplify(Node t, std::vector< Node > &new_nodes, bool polarity); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 497ce5f8c..57344236e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2726,23 +2726,17 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node void TheoryStrings::addNormalFormPair( Node n1, Node n2 ){ if( !isNormalFormPair( n1, n2 ) ){ - //Assert( !isNormalFormPair( n1, n2 ) ); - NodeList* lst; - NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); - if( nf_i == d_nf_pairs.end() ){ - if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){ - addNormalFormPair( n2, n1 ); - return; - } - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_nf_pairs.insertDataFromContextMemory( n1, lst ); - Trace("strings-nf") << "Create cache for " << n1 << std::endl; - } else { - lst = (*nf_i).second; - } - Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl; - lst->push_back( n2 ); + int index = 0; + NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + } + d_nf_pairs[n1] = index + 1; + if( index<(int)d_nf_pairs_data[n1].size() ){ + d_nf_pairs_data[n1][index] = n2; + }else{ + d_nf_pairs_data[n1].push_back( n2 ); + } Assert( isNormalFormPair( n1, n2 ) ); } else { Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl; @@ -2755,15 +2749,14 @@ bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) { } bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { - //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; - NodeList* lst; - NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); - if( nf_i != d_nf_pairs.end() ) { - lst = (*nf_i).second; - for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) { - Node n = *i; - if( n==n2 ) { - return true; + //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; + NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); + if( it!=d_nf_pairs.end() ){ + Assert( d_nf_pairs_data.find( n1 )!=d_nf_pairs_data.end() ); + for( int i=0; i<(*it).second; i++ ){ + Assert( i<(int)d_nf_pairs_data[n1].size() ); + if( d_nf_pairs_data[n1][i]==n2 ){ + return true; } } } @@ -3428,6 +3421,26 @@ void TheoryStrings::updateMpl( Node n, int b ) { } */ + +unsigned TheoryStrings::getNumMemberships( Node n, bool isPos ) { + if( isPos ){ + NodeIntMap::const_iterator it = d_pos_memberships.find( n ); + if( it!=d_pos_memberships.end() ){ + return (*it).second; + } + }else{ + NodeIntMap::const_iterator it = d_neg_memberships.find( n ); + if( it!=d_neg_memberships.end() ){ + return (*it).second; + } + } + return 0; +} + +Node TheoryStrings::getMembership( Node n, bool isPos, unsigned i ) { + return isPos ? d_pos_memberships_data[n][i] : d_neg_memberships_data[n][i]; +} + //// Regular Expressions Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) { if(d_regexp_ant.find(atom) == d_regexp_ant.end()) { @@ -3505,10 +3518,8 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl; - for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); - itr_xr != d_pos_memberships.end(); ++itr_xr ) { + for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){ Node x = (*itr_xr).first; - NodeList* lst = (*itr_xr).second; Node nf_x = x; std::vector< Node > nf_x_exp; if(d_normal_forms.find( x ) != d_normal_forms.end()) { @@ -3522,10 +3533,11 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > std::vector< Node > vec_x; std::vector< Node > vec_r; - for(NodeList::const_iterator itr_lst = lst->begin(); - itr_lst != lst->end(); ++itr_lst) { - Node r = *itr_lst; - Node nf_r = normalizeRegexp((*lst)[0]); + unsigned n_pmem = (*itr_xr).second; + Assert( getNumMemberships( x, true )==n_pmem ); + for( unsigned k=0; kmkNode(kind::STRING_IN_REGEXP, nf_x, nf_r); if(d_processed_memberships.find(memb) == d_processed_memberships.end()) { if(d_regexp_opr.checkConstRegExp(nf_r)) { @@ -3755,46 +3767,43 @@ void TheoryStrings::checkMemberships() { Trace("regexp-debug") << "Checking Memberships ... " << std::endl; //if(options::stringEIT()) { //TODO: Opt for normal forms - for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); - itr_xr != d_pos_memberships.end(); ++itr_xr ) { + for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){ bool spflag = false; Node x = (*itr_xr).first; - NodeList* lst = (*itr_xr).second; Trace("regexp-debug") << "Checking Memberships for " << x << std::endl; if(d_inter_index.find(x) == d_inter_index.end()) { d_inter_index[x] = 0; } int cur_inter_idx = d_inter_index[x]; - if(cur_inter_idx != (int)lst->size()) { - if(lst->size() == 1) { - d_inter_cache[x] = (*lst)[0]; + unsigned n_pmem = (*itr_xr).second; + Assert( getNumMemberships( x, true )==n_pmem ); + if( cur_inter_idx != (int)n_pmem ) { + if( n_pmem == 1) { + d_inter_cache[x] = getMembership( x, true, 0 ); d_inter_index[x] = 1; Trace("regexp-debug") << "... only one choice " << std::endl; - } else if(lst->size() > 1) { + } else if(n_pmem > 1) { Node r; if(d_inter_cache.find(x) != d_inter_cache.end()) { r = d_inter_cache[x]; } if(r.isNull()) { - r = (*lst)[0]; + r = getMembership( x, true, 0 ); cur_inter_idx = 1; } - NodeList::const_iterator itr_lst = lst->begin(); - for(int i=0; isize() << std::endl; - for(;itr_lst != lst->end(); ++itr_lst) { - Node r2 = *itr_lst; + + unsigned k_start = cur_inter_idx; + Trace("regexp-debug") << "... staring from : " << cur_inter_idx << ", we have " << n_pmem << std::endl; + for(unsigned k = k_start; k vec_nodes; - ++itr_lst; - for(NodeList::const_iterator itr2 = lst->begin(); - itr2 != itr_lst; ++itr2) { - Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2); + for( unsigned kk=0; kk<=k; kk++ ){ + Node rr = getMembership( x, true, kk ); + Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, rr); vec_nodes.push_back( n ); } Node conc; @@ -3809,7 +3818,7 @@ void TheoryStrings::checkMemberships() { //updates if(!d_conflict && !spflag) { d_inter_cache[x] = r; - d_inter_index[x] = (int)lst->size(); + d_inter_index[x] = (int)n_pmem; } } } @@ -4432,44 +4441,52 @@ void TheoryStrings::addMembership(Node assertion) { Node x = atom[0]; Node r = atom[1]; if(polarity) { - NodeList* lst; - NodeListMap::iterator itr_xr = d_pos_memberships.find( x ); - if( itr_xr == d_pos_memberships.end() ){ - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_pos_memberships.insertDataFromContextMemory( x, lst ); - } else { - lst = (*itr_xr).second; - } - //check - for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { - if( r == *itr ) { - return; + int index = 0; + NodeIntMap::const_iterator it = d_pos_memberships.find( x ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + for( int k=0; kpush_back( r ); + d_pos_memberships[x] = index + 1; + if( index<(int)d_pos_memberships_data[x].size() ){ + d_pos_memberships_data[x][index] = r; + }else{ + d_pos_memberships_data[x].push_back( r ); + } } else if(!options::stringIgnNegMembership()) { /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { int rt; Node r2 = d_regexp_opr.complement(r, rt); Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2); }*/ - NodeList* lst; - NodeListMap::iterator itr_xr = d_neg_memberships.find( x ); - if( itr_xr == d_neg_memberships.end() ){ - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_neg_memberships.insertDataFromContextMemory( x, lst ); - } else { - lst = (*itr_xr).second; - } - //check - for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { - if( r == *itr ) { - return; + int index = 0; + NodeIntMap::const_iterator it = d_neg_memberships.find( x ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + for( int k=0; kpush_back( r ); + d_neg_memberships[x] = index + 1; + if( index<(int)d_neg_memberships_data[x].size() ){ + d_neg_memberships_data[x][index] = r; + }else{ + d_neg_memberships_data[x].push_back( r ); + } } // old if(polarity || !options::stringIgnNegMembership()) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c9e0a29bf..2deb09654 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -50,7 +50,6 @@ typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttri class TheoryStrings : public Theory { typedef context::CDChunkList NodeList; - typedef context::CDHashMap NodeListMap; typedef context::CDHashMap NodeBoolMap; typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeNodeMap; @@ -165,7 +164,8 @@ private: std::map< Node, std::vector< Node > > d_normal_forms_exp; std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend; //map of pairs of terms that have the same normal form - NodeListMap d_nf_pairs; + NodeIntMap d_nf_pairs; + std::map< Node, std::vector< Node > > d_nf_pairs_data; void addNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair2( Node n1, Node n2 ); @@ -421,8 +421,12 @@ private: NodeSet d_regexp_ucached; NodeSet d_regexp_ccached; // stored assertions - NodeListMap d_pos_memberships; - NodeListMap d_neg_memberships; + NodeIntMap d_pos_memberships; + std::map< Node, std::vector< Node > > d_pos_memberships_data; + NodeIntMap d_neg_memberships; + std::map< Node, std::vector< Node > > d_neg_memberships_data; + unsigned getNumMemberships( Node n, bool isPos ); + Node getMembership( Node n, bool isPos, unsigned i ); // semi normal forms for symbolic expression std::map< Node, Node > d_nf_regexps; std::map< Node, std::vector< Node > > d_nf_regexps_exp; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a4f42bddd..ba811644a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -33,6 +33,10 @@ StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){ d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); } +StringsPreprocess::~StringsPreprocess(){ + +} + /* int StringsPreprocess::checkFixLenVar( Node t ) { int ret = 2; diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 5bc9667ea..abc7b5a91 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -40,6 +40,7 @@ private: Node simplify( Node t, std::vector< Node > &new_nodes ); public: StringsPreprocess( context::UserContext* u ); + ~StringsPreprocess(); Node decompose( Node t, std::vector< Node > &new_nodes ); void simplify(std::vector< Node > &vec_node); -- 2.30.2