Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.

1 files changed, 15 insertions, 0 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9e71a1ddf..1c0a03e9c 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -527,6 +527,21 @@ void ExtTheory::registerTerm( Node n ) {
   }
 }
 
+void ExtTheory::registerTermRec( Node n ) {
+  std::map< Node, bool > 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 );
+    }
+  }
+}
+
 //mark reduced
 void ExtTheory::markReduced( Node n, bool contextDepend ) {
   d_ext_func_terms[n] = false;