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.h | |
| 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.h')
| -rw-r--r-- | src/expr/node_traversal.h | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h index 1398f6485..586cbb64d 100644 --- a/src/expr/node_traversal.h +++ b/src/expr/node_traversal.h @@ -67,9 +67,13 @@ class NodeDfsIterator // Dereference reference operator*(); // Equals - bool operator==(const NodeDfsIterator&) const; + // It is not constant, because an unitilized node must be initialized before + // comparison + bool operator==(NodeDfsIterator&); // Not equals - bool operator!=(const NodeDfsIterator&) const; + // It is not constant, because an unitilized node must be initialized before + // comparison + bool operator!=(NodeDfsIterator&); private: // While we're not at an appropriate visit (see d_postorder), advance. |