From f49ddf87046793972a7f6a1bdae15003709f08d2 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 27 Mar 2017 12:26:14 -0700 Subject: Making the ExtTheory object a private member of Theory. --- src/theory/strings/theory_strings.cpp | 59 +++++++++++++++++------------------ 1 file changed, 29 insertions(+), 30 deletions(-) (limited to 'src/theory/strings/theory_strings.cpp') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5f05003c6..bb226e962 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -97,18 +97,18 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, d_cardinality_lits(u), d_curr_cardinality(c, 0) { - d_extt = new ExtTheory( this ); - d_extt->addFunctionKind( kind::STRING_SUBSTR ); - d_extt->addFunctionKind( kind::STRING_STRIDOF ); - d_extt->addFunctionKind( kind::STRING_ITOS ); - d_extt->addFunctionKind( kind::STRING_U16TOS ); - d_extt->addFunctionKind( kind::STRING_U32TOS ); - d_extt->addFunctionKind( kind::STRING_STOI ); - d_extt->addFunctionKind( kind::STRING_STOU16 ); - d_extt->addFunctionKind( kind::STRING_STOU32 ); - d_extt->addFunctionKind( kind::STRING_STRREPL ); - d_extt->addFunctionKind( kind::STRING_STRCTN ); - d_extt->addFunctionKind( kind::STRING_IN_REGEXP ); + setupExtTheory(); + getExtTheory()->addFunctionKind(kind::STRING_SUBSTR); + getExtTheory()->addFunctionKind(kind::STRING_STRIDOF); + getExtTheory()->addFunctionKind(kind::STRING_ITOS); + getExtTheory()->addFunctionKind(kind::STRING_U16TOS); + getExtTheory()->addFunctionKind(kind::STRING_U32TOS); + getExtTheory()->addFunctionKind(kind::STRING_STOI); + getExtTheory()->addFunctionKind(kind::STRING_STOU16); + getExtTheory()->addFunctionKind(kind::STRING_STOU32); + getExtTheory()->addFunctionKind(kind::STRING_STRREPL); + getExtTheory()->addFunctionKind(kind::STRING_STRCTN); + getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); @@ -142,7 +142,6 @@ TheoryStrings::~TheoryStrings() { for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){ delete it->second; } - delete d_extt; } Node TheoryStrings::getRepresentative( Node t ) { @@ -644,7 +643,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { if( options::stringExp() ){ //collect extended functions here: some may not be asserted to strings (such as those with return type Int), // but we need to record them so they are treated properly - d_extt->registerTermRec( n ); + getExtTheory()->registerTermRec( n ); } } //concat terms do not contribute to theory combination? TODO: verify @@ -797,10 +796,10 @@ bool TheoryStrings::needsCheckLastEffort() { void TheoryStrings::checkExtfReductions( int effort ) { //standardize this? //std::vector< Node > nred; - //d_extt->doReductions( effort, nred, false ); + //getExtTheory()->doReductions( effort, nred, false ); std::vector< Node > extf; - d_extt->getActive( extf ); + getExtTheory()->getActive( extf ); Trace("strings-process") << "checking " << extf.size() << " active extf" << std::endl; for( unsigned i=0; imarkReduced( extf[i] ); + getExtTheory()->markReduced( extf[i] ); if( options::stringOpt1() && hasProcessed() ){ return; } @@ -859,7 +858,7 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ //we care about the length of this string registerTerm( t[0], 1 ); }else{ - //d_extt->registerTerm( t ); + //getExtTheory()->registerTerm( t ); } } @@ -1017,11 +1016,11 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { } } //register the atom here, since it may not create a new equivalence class - //d_extt->registerTerm( atom ); + //getExtTheory()->registerTerm( atom ); } Trace("strings-pending-debug") << " Now collect terms" << std::endl; //collect extended function terms in the atom - d_extt->registerTermRec( atom ); + getExtTheory()->registerTermRec( atom ); Trace("strings-pending-debug") << " Finished collect terms" << std::endl; } @@ -1148,9 +1147,9 @@ void TheoryStrings::checkInit() { } //infer the equality sendInference( exp, n.eqNode( nc ), "I_Norm" ); - }else if( d_extt->hasFunctionKind( n.getKind() ) ){ + }else if( getExtTheory()->hasFunctionKind( n.getKind() ) ){ //mark as congruent : only process if neither has been reduced - d_extt->markCongruent( nc, n ); + getExtTheory()->markCongruent( nc, n ); } //this node is congruent to another one, we can ignore it Trace("strings-process-debug") << " congruent term : " << n << std::endl; @@ -1310,8 +1309,8 @@ void TheoryStrings::checkExtfEval( int effort ) { std::vector< Node > terms; std::vector< Node > sterms; std::vector< std::vector< Node > > exp; - d_extt->getActive( terms ); - d_extt->getSubstitutedTerms( effort, terms, sterms, exp ); + getExtTheory()->getActive( terms ); + getExtTheory()->getSubstitutedTerms( effort, terms, sterms, exp ); for( unsigned i=0; imarkReduced( n ); + getExtTheory()->markReduced( n ); Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; std::vector< Node > exps; Trace("strings-extf-debug") << " get symbolic definition..." << std::endl; @@ -1395,7 +1394,7 @@ void TheoryStrings::checkExtfEval( int effort ) { //if it reduces to a conjunction, infer each and reduce }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){ Assert( effort<3 ); - d_extt->markReduced( n ); + getExtTheory()->markReduced( n ); itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n ); Trace("strings-extf-debug") << " decomposable..." << std::endl; Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl; @@ -1425,7 +1424,7 @@ void TheoryStrings::checkExtfEval( int effort ) { } Trace("strings-extf-list") << std::endl; } - if( d_extt->isActive( n ) && itit->second.d_model_active ){ + if( getExtTheory()->isActive( n ) && itit->second.d_model_active ){ has_nreduce = true; } } @@ -1457,7 +1456,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef children[index] = nr[index][i]; Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, children ); //can mark as reduced, since model for n => model for conc - d_extt->markReduced( conc ); + getExtTheory()->markReduced( conc ); sendInference( in.d_exp, in.d_pol==1 ? conc : conc.negate(), "CTN_Decompose" ); } @@ -1494,7 +1493,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef } }else{ Trace("strings-extf-debug") << " redundant." << std::endl; - d_extt->markReduced( n ); + getExtTheory()->markReduced( n ); } } } @@ -4290,7 +4289,7 @@ bool TheoryStrings::checkMemberships2() { void TheoryStrings::checkMemberships() { //add the memberships std::vector< Node > mems; - d_extt->getActive( mems, kind::STRING_IN_REGEXP ); + getExtTheory()->getActive( mems, kind::STRING_IN_REGEXP ); for( unsigned i=0; i