From 10a9f52fcb1aedd662c87a394a3df76a4d66b5c9 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 27 Mar 2017 22:15:23 -0700 Subject: [PATCH] Minor cleanups to ExtTheory. --- src/theory/bv/theory_bv.cpp | 7 +- src/theory/strings/theory_strings.cpp | 11 +- src/theory/theory.cpp | 138 +++++++++++++++----------- src/theory/theory.h | 82 ++++++++------- 4 files changed, 134 insertions(+), 104 deletions(-) diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index ca7c037ef..651d44841 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -396,10 +396,9 @@ void TheoryBV::check(Effort e) } //last call : do reductions on extended bitvector functions - if( e==Theory::EFFORT_LAST_CALL ){ - std::vector< Node > nred; - getExtTheory()->getActive( nred ); - doExtfReductions( nred ); + if (e == Theory::EFFORT_LAST_CALL) { + std::vector nred = getExtTheory()->getActive(); + doExtfReductions(nred); return; } 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 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 mems; - getExtTheory()->getActive( mems, kind::STRING_IN_REGEXP ); - for( unsigned i=0; i 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 ){ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 3aa468e01..021aa61c6 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -365,27 +365,38 @@ d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_has_extf( d_true = NodeManager::currentNM()->mkConst( true ); } -//gets all leaf terms in n -void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) { - if( !n.isConst() ){ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - //treat terms not belonging to this theory as leaf - // AJR TODO : should include terms not belonging to this theory (commented below) - if( n.getNumChildren()>0 ){//&& Theory::theoryOf(n)==d_parent->getId() ){ - for( unsigned i=0; i ExtTheory::collectVars(Node n) { + std::vector vars; + std::set visited; + std::vector worklist; + worklist.push_back(n); + while (!worklist.empty()) { + Node current = worklist.back(); + worklist.pop_back(); + if (current.isConst() || visited.count(current) <= 0) { + continue; + } + visited.insert(current); + // Treat terms not belonging to this theory as leaf + // AJR TODO : should include terms not belonging to this theory + // (commented below) + if (current.getNumChildren() > 0) { + //&& Theory::theoryOf(n)==d_parent->getId() ){ + worklist.insert(worklist.end(), current.begin(), current.end()); + } else { + vars.push_back(current); } } + return vars; } -//do inferences -void ExtTheory::getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) { - Trace("extt-debug") << "Currently " << d_ext_func_terms.size() << " extended functions." << std::endl; +//do inferences +void ExtTheory::getSubstitutedTerms(int effort, const std::vector& terms, + std::vector& sterms, + std::vector >& exp) { + Trace("extt-debug") << "Currently " << d_ext_func_terms.size() + << " extended functions." << std::endl; Trace("extt-debug") << "..." << terms.size() << " to reduce." << std::endl; if( !terms.empty() ){ //all variables we need to find a substitution for @@ -441,8 +452,10 @@ void ExtTheory::getSubstitutedTerms( int effort, std::vector< Node >& terms, std } } -bool ExtTheory::doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ) { - if( batch ){ +bool ExtTheory::doInferencesInternal(int effort, const std::vector& terms, + std::vector& nred, bool batch, + bool isRed) { + if (batch) { bool addedLemma = false; if( isRed ){ for( unsigned i=0; i& terms, std::vector< Node >& nred, bool batch ) { - if( !terms.empty() ){ +bool ExtTheory::doInferences(int effort, const std::vector& terms, + std::vector& nred, bool batch) { + if (!terms.empty()) { return doInferencesInternal( effort, terms, nred, batch, false ); }else{ return false; @@ -542,50 +556,48 @@ bool ExtTheory::doInferences( int effort, std::vector< Node >& terms, std::vecto } bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) { - std::vector< Node > terms; - getActive( terms ); + std::vector< Node > terms = getActive(); return doInferencesInternal( effort, terms, nred, batch, false ); } -bool ExtTheory::doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) { - if( !terms.empty() ){ +bool ExtTheory::doReductions(int effort, const std::vector& terms, + std::vector& nred, bool batch) { + if (!terms.empty()) { return doInferencesInternal( effort, terms, nred, batch, true ); }else{ return false; } } -bool ExtTheory::doReductions( int effort, std::vector< Node >& nred, bool batch ) { - std::vector< Node > terms; - getActive( terms ); - return doInferencesInternal( effort, terms, nred, batch, true ); +bool ExtTheory::doReductions(int effort, std::vector& nred, bool batch) { + const std::vector terms = getActive(); + return doInferencesInternal(effort, terms, nred, batch, true); } - -//register term -void ExtTheory::registerTerm( Node n ) { - if( d_extf_kind.find( n.getKind() )!=d_extf_kind.end() ){ - if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){ - Trace("extt-debug") << "Found extended function : " << n << " in " << d_parent->getId() << std::endl; +// Register term. +void ExtTheory::registerTerm(Node n) { + if (d_extf_kind.find(n.getKind()) != d_extf_kind.end()) { + if (d_ext_func_terms.find(n) == d_ext_func_terms.end()) { + Trace("extt-debug") << "Found extended function : " << n << " in " + << d_parent->getId() << std::endl; d_ext_func_terms[n] = true; d_has_extf = n; - std::map< Node, bool > visited; - collectVars( n, d_extf_info[n].d_vars, visited ); + d_extf_info[n].d_vars = collectVars(n); } } } -void ExtTheory::registerTermRec( Node n ) { - std::map< Node, bool > visited; - registerTermRec( n, visited ); +void ExtTheory::registerTermRec(Node n) { + std::set visited; + registerTermRec(n, &visited); } -void ExtTheory::registerTermRec( Node n, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - registerTerm( n ); - for( unsigned i=0; i* visited) { + if (visited->find(n) == visited->end()) { + visited->insert(n); + registerTerm(n); + for (unsigned i = 0; i < n.getNumChildren(); i++) { + registerTermRec(n[i], visited); } } } @@ -629,8 +641,8 @@ void ExtTheory::markCongruent( Node a, Node b ) { } } -bool ExtTheory::isContextIndependentInactive( Node n ) { - return d_ci_inactive.find( n )!=d_ci_inactive.end(); +bool ExtTheory::isContextIndependentInactive(Node n) const { + return d_ci_inactive.find(n) != d_ci_inactive.end(); } bool ExtTheory::hasActiveTerm() { @@ -646,23 +658,31 @@ bool ExtTheory::isActive( Node n ) { return false; } } -//get active -void ExtTheory::getActive( std::vector< Node >& active ) { - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - //if not already reduced - if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ - active.push_back( (*it).first ); + +// get active +std::vector ExtTheory::getActive() const { + std::vector active; + for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); + it != d_ext_func_terms.end(); ++it) { + // if not already reduced + if ((*it).second && !isContextIndependentInactive((*it).first)) { + active.push_back((*it).first); } } + return active; } -void ExtTheory::getActive( std::vector< Node >& active, Kind k ) { - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - //if not already reduced - if( (*it).first.getKind()==k && (*it).second && !isContextIndependentInactive( (*it).first ) ){ - active.push_back( (*it).first ); +std::vector ExtTheory::getActive(Kind k) const { + std::vector active; + for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); + it != d_ext_func_terms.end(); ++it) { + // if not already reduced + if ((*it).first.getKind() == k && (*it).second && + !isContextIndependentInactive((*it).first)) { + active.push_back((*it).first); } } + return active; } }/* CVC4::theory namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index d34d3c549..d50d6b3f9 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -21,6 +21,8 @@ #include #include +#include +#include #include #include "context/cdlist.h" @@ -913,7 +915,19 @@ public: class ExtTheory { typedef context::CDHashMap NodeBoolMap; typedef context::CDHashSet NodeSet; -protected: +private: + // collect variables + static std::vector collectVars(Node n); + // is context dependent inactive + bool isContextIndependentInactive( Node n ) const; + //do inferences internal + bool doInferencesInternal(int effort, const std::vector& terms, + std::vector& nred, bool batch, bool isRed); + // send lemma + bool sendLemma( Node lem, bool preprocess = false ); + // register term (recursive) + void registerTermRec(Node n, std::set* visited); + Theory * d_parent; Node d_true; //extended string terms, map to whether they are active @@ -935,23 +949,16 @@ protected: std::vector< Node > d_vars; }; std::map< Node, ExtfInfo > d_extf_info; - //collect variables - void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); - // is context dependent inactive - bool isContextIndependentInactive( Node n ); - //do inferences internal - bool doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ); - //send lemma - bool sendLemma( Node lem, bool preprocess = false ); - //register term (recursive) - void registerTermRec( Node n, std::map< Node, bool >& visited ); -public: - ExtTheory( Theory * p ); - virtual ~ExtTheory(){} - //add extf kind - void addFunctionKind( Kind k ) { d_extf_kind[k] = true; } - bool hasFunctionKind( Kind k ) { return d_extf_kind.find( k )!=d_extf_kind.end(); } - //register term + + public: + ExtTheory(Theory* p); + virtual ~ExtTheory() {} + // add extf kind + void addFunctionKind(Kind k) { d_extf_kind[k] = true; } + bool hasFunctionKind(Kind k) const { + return d_extf_kind.find(k) != d_extf_kind.end(); + } + // register term // adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called void registerTerm( Node n ); void registerTermRec( Node n ); @@ -964,27 +971,34 @@ public: //getSubstitutedTerms // input : effort, terms // output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i - void getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ); - //doInferences - // * input : effort, terms, batch (whether to send one lemma or lemmas for all terms) - // * sends rewriting lemmas of the form ( exp => t = c ) where t is in terms and c is a constant, c = rewrite( t*sigma ) where exp |= sigma + void getSubstitutedTerms(int effort, const std::vector& terms, + std::vector& sterms, + std::vector >& exp); + // doInferences + // * input : effort, terms, batch (whether to send one lemma or lemmas for + // all terms) + // * sends rewriting lemmas of the form ( exp => t = c ) where t is in terms + // and c is a constant, c = rewrite( t*sigma ) where exp |= sigma // * output : nred (the terms that are still active) // * return : true iff lemma is sent - bool doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch=true ); - bool doInferences( int effort, std::vector< Node >& nred, bool batch=true ); + bool doInferences(int effort, const std::vector& terms, + std::vector& nred, bool batch = true); + bool doInferences(int effort, std::vector& nred, bool batch = true); //doReductions - // same as doInferences, but will send reduction lemmas of the form ( t = t' ) where t is in terms, t' is equivalent, reduced term - bool doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch=true ); - bool doReductions( int effort, std::vector< Node >& nred, bool batch=true ); + // same as doInferences, but will send reduction lemmas of the form ( t = t' ) + // where t is in terms, t' is equivalent, reduced term. + bool doReductions(int effort, const std::vector& terms, + std::vector& nred, bool batch = true); + bool doReductions(int effort, std::vector& nred, bool batch = true); - //has active term + // has active term bool hasActiveTerm(); - //is n active - bool isActive( Node n ); - //get the set of active terms from d_ext_func_terms - void getActive( std::vector< Node >& active ); - //get the set of active terms from d_ext_func_terms of kind k - void getActive( std::vector< Node >& active, Kind k ); + // is n active + bool isActive(Node n); + // get the set of active terms from d_ext_func_terms + std::vector getActive() const; + // get the set of active terms from d_ext_func_terms of kind k + std::vector getActive(Kind k) const; }; }/* CVC4::theory namespace */ -- 2.30.2