diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-06-19 22:45:32 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-19 22:45:32 -0700 |
| commit | 3bc4a541b6c3a35fae987cc068e0e01937d5c4b1 (patch) | |
| tree | 56f19ac241b31904cf52f46c60c1798fadc4c18f /src/expr/node_traversal.cpp | |
| parent | 3d44636a3080831bd8ea4c6b2d4f60adf6b37e9d (diff) | |
Use traversal iterators in IntToBv (#4169)
This commit rips the traversal machinery out of Int-to-Bv, replacing it with traversal iterators.
Also, cleaned `childrenTypesChanged` a bit.
While basically I just cut out some lines, the diff is rather messy (I think the diffing tool doesn't like indentation changes).
Diffstat (limited to 'src/expr/node_traversal.cpp')
| -rw-r--r-- | src/expr/node_traversal.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp index 0d207b302..5968c4348 100644 --- a/src/expr/node_traversal.cpp +++ b/src/expr/node_traversal.cpp @@ -63,8 +63,11 @@ TNode& NodeDfsIterator::operator*() return d_current; } -bool NodeDfsIterator::operator==(const NodeDfsIterator& other) const +bool NodeDfsIterator::operator==(NodeDfsIterator& other) { + // Unitialize this node, and the other, before comparing. + initializeIfUninitialized(); + other.initializeIfUninitialized(); // The stack and current node uniquely represent traversal state. We need not // use the scheduled node set. // @@ -74,7 +77,7 @@ bool NodeDfsIterator::operator==(const NodeDfsIterator& other) const return d_stack == other.d_stack && d_current == other.d_current; } -bool NodeDfsIterator::operator!=(const NodeDfsIterator& other) const +bool NodeDfsIterator::operator!=(NodeDfsIterator& other) { return !(*this == other); } |