summaryrefslogtreecommitdiff
path: root/src/theory/theory.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r--src/theory/theory.cpp15
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback