Minor cleanups to ExtTheory.

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<Node> 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<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 ){
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<n.getNumChildren(); i++ ){
-          collectVars( n[i], vars, visited );
-        }
-      }else{
-        vars.push_back( n );
-      }
+// Gets all leaf terms in n.
+std::vector<Node> ExtTheory::collectVars(Node n) {
+  std::vector<Node> vars;
+  std::set<Node> visited;
+  std::vector<Node> 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<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;
   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<Node>& terms,
+                                     std::vector<Node>& nred, bool batch,
+                                     bool isRed) {
+  if (batch) {
     bool addedLemma = false;
     if( isRed ){
       for( unsigned i=0; i<terms.size(); i++ ){
@@ -533,8 +546,9 @@ bool ExtTheory::sendLemma( Node lem, bool preprocess ) {
   return false;
 }
 
-bool ExtTheory::doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) {
-  if( !terms.empty() ){
+bool ExtTheory::doInferences(int effort, const std::vector<Node>& terms,
+                             std::vector<Node>& 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<Node>& terms,
+                             std::vector<Node>& 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<Node>& nred, bool batch) {
+  const std::vector<Node> 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<Node> 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<n.getNumChildren(); i++ ){
-      registerTermRec( n[i], visited );
+void ExtTheory::registerTermRec(Node n, std::set<Node>* 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<Node> ExtTheory::getActive() const {
+  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);
     }
   }
+  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<Node> ExtTheory::getActive(Kind k) const {
+  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).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 <ext/hash_set>
 #include <iosfwd>
+#include <map>
+#include <set>
 #include <string>
 
 #include "context/cdlist.h"
@@ -913,7 +915,19 @@ public:
 class ExtTheory {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-protected:
+private:
+  // collect variables
+  static std::vector<Node> collectVars(Node n);
+  // is context dependent inactive
+  bool isContextIndependentInactive( Node n ) const;
+  //do inferences internal
+  bool doInferencesInternal(int effort, const 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::set<Node>* 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<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
   //  * 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<Node>& terms,
+                    std::vector<Node>& nred, bool batch = true);
+  bool doInferences(int effort, std::vector<Node>& 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<Node>& terms,
+                    std::vector<Node>& nred, bool batch = true);
+  bool doReductions(int effort, std::vector<Node>& 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<Node> getActive() const;
+  // get the set of active terms from d_ext_func_terms of kind k
+  std::vector<Node> getActive(Kind k) const;
 };
 
 }/* CVC4::theory namespace */