diff options
| author | Tim King <taking@google.com> | 2017-03-27 22:15:23 -0700 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2017-03-27 22:15:23 -0700 |
| commit | 10a9f52fcb1aedd662c87a394a3df76a4d66b5c9 (patch) | |
| tree | f1c1a3689daa8367cbca1223d9b441e3913534c4 /src/theory/strings | |
| parent | 0a0600ef6705f9d4265057fef307bc49f54bfa35 (diff) | |
Minor cleanups to ExtTheory.
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index bb226e962..930520725 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -798,8 +798,7 @@ void TheoryStrings::checkExtfReductions( int effort ) { //std::vector< Node > nred; //getExtTheory()->doReductions( effort, nred, false ); - std::vector< Node > extf; - getExtTheory()->getActive( extf ); + std::vector< Node > extf = getExtTheory()->getActive(); Trace("strings-process") << "checking " << extf.size() << " active extf" << std::endl; for( unsigned i=0; i<extf.size(); i++ ){ Node n = extf[i]; @@ -1306,10 +1305,9 @@ void TheoryStrings::checkExtfEval( int effort ) { Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl; d_extf_info_tmp.clear(); bool has_nreduce = false; - std::vector< Node > terms; + std::vector< Node > terms = getExtTheory()->getActive(); std::vector< Node > sterms; std::vector< std::vector< Node > > exp; - getExtTheory()->getActive( terms ); getExtTheory()->getSubstitutedTerms( effort, terms, sterms, exp ); for( unsigned i=0; i<terms.size(); i++ ){ Node n = terms[i]; @@ -4288,9 +4286,8 @@ bool TheoryStrings::checkMemberships2() { void TheoryStrings::checkMemberships() { //add the memberships - std::vector< Node > mems; - getExtTheory()->getActive( mems, kind::STRING_IN_REGEXP ); - for( unsigned i=0; i<mems.size(); i++ ){ + std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP); + for (unsigned i = 0; i < mems.size(); i++) { Node n = mems[i]; Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); if( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 ){ |