summaryrefslogtreecommitdiff
path: root/src/expr/node_traversal.h
AgeCommit message (Collapse)Author
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
2020-11-19Include stddef.h (needed for size_t) in cvc4_public.h (#5476)Aina Niemetz
This further removes obsolete explicit includes of stdint.h.
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-06-19Use traversal iterators in IntToBv (#4169)Alex Ozdemir
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).
2020-06-16Update copyright headers.Aina Niemetz
2020-06-05Fix lifetime and copy issues with NodeDfsIterable (#4569)Andres Noetzli
When running node_traversal_black with ASan and UBSan, there were two distinct issues being reported. UBSan was complaining that we were assigning an invalid value to a Boolean. This happened because d_initialized in NodeDfsIterator was uninitialized and the default copy constructor tried to copy it. This commit removes that data member. ASan was complainig that NodeDfsIterator::begin() was trying to access a skip function that had been freed. In particular, this happened when NodeDfsIterable was used in a range-based for loop like so: for (auto n : NodeDfsIterable(n).inPostorder()) { ... } The problem here is that the lifetime of a temporary within the range expression is not extended (the lifetime of the result of the range expression is extended, however) [0]. This is a problem because NodeDfsIterable(n) is a temporary and inPostorder() returns a reference to that temporary. It makes sense that the compiler cannot possibly know that the reference from inPostorder() corresponds to NodeDfsIterable(n), so it cannot extend its lifetime. See [1] for more details on the problem with chained functions. This commit fixes the issue by replacing the fluent interface of NodeDfsIterable by a constructor with default arguments. Additionally, it introduces an enum to represent the visit order to avoid having a nondescript Boolean argument. [0] https://en.cppreference.com/w/cpp/language/range-for#Temporary_range_expression [1] http://cpptruths.blogspot.com/2018/10/chained-functions-break-reference.html?m=1
2020-04-11Add skip predicate to node traversal. (#4222)Alex Ozdemir
Sometime you want to skip specific sub-DAGs when traversing a node. For example, you might be doing a transformation with a cache, and want to skip sub-DAGs that you've already processed. This PR would add a skipIf builder method to NodeDfsIterable, which allows the user to provide a predicate according to which nodes will be omitted from the subsequent traversal.
2020-03-27Node traversal iterator (#3845)Alex Ozdemir
Implement an iterator for pre- and post-order traversals. I believe that this will be useful in pre-processing passes, many of which do postorder traversals that they implement by hand. Right now this iterator does not support modification of the traversal pattern, but we could add this later on, if we want it. Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com> Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback