diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-03 16:57:54 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-03 16:57:54 -0600 |
commit | 35cf275a068f28c518acaab456ece16e19b6959c (patch) | |
tree | 71c8aecf13f5006db21c4058b8925f158a82bca9 /src/expr/node_algorithm.cpp | |
parent | 1c55227e6ef30149e6a008fdea56573f67244a61 (diff) |
Utility function for getting component types (#3703)
Diffstat (limited to 'src/expr/node_algorithm.cpp')
-rw-r--r-- | src/expr/node_algorithm.cpp | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index eda4dadd2..9721845f7 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -18,6 +18,7 @@ #include "expr/node_algorithm.h" #include "expr/attribute.h" +#include "expr/dtype.h" namespace CVC4 { namespace expr { @@ -522,5 +523,27 @@ Node substituteCaptureAvoiding(TNode n, return visited[n]; } +void getComponentTypes( + TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types) +{ + std::vector<TypeNode> toProcess; + toProcess.push_back(t); + do + { + TypeNode curr = toProcess.back(); + toProcess.pop_back(); + // if not already visited + if (types.find(t) == types.end()) + { + types.insert(t); + // get component types from the children + for (unsigned i = 0, nchild = t.getNumChildren(); i < nchild; i++) + { + toProcess.push_back(t[i]); + } + } + } while (!toProcess.empty()); +} + } // namespace expr } // namespace CVC4 |