diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-13 17:44:19 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-13 17:44:19 -0500 |
commit | 9da056f71c0c4a8ed5afd01c300e9c86cfcf5601 (patch) | |
tree | 9cc4ed5a09640c3dbb8df9cbaf242ade0f8acc4f /src/theory/theory.cpp | |
parent | 7e750757ac9832b70b5c6ca1d15e17cddbd2e6c0 (diff) |
Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 15 |
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; |