summaryrefslogtreecommitdiff
path: root/src/expr/node.h
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2019-12-12 21:05:49 -0800
committerAndres Noetzli <andres.noetzli@gmail.com>2019-12-12 21:05:49 -0800
commit8afa8a89101743915fe6b94dabd18797a55b3e55 (patch)
treed705a94914f106eefa62652f037243c2fbc83628 /src/expr/node.h
parent87602bc6d010eea33b8db93e80a79dcf99d230b5 (diff)
FP converter: convert: Use std::vector as instead of std::stack. (#3563)
The word-blasting function `FpConverter::convert` used a `std::stack` with `deque` as an underlying data structure (default) for node traversal. Previous experiments suggested that using `std::stack<T, std::deque<T>>` performs worse than using `std::vector<T>`, and we decided, as a guideline, to always use `std::vector` for stacks: https://github.com/CVC4/CVC4/wiki/Code-Style-Guidelines#stack. This PR refactors `FpConverter::convert` to use `std::vector`. Runs on all incremental and non-incremental FP logics in SMT-LIB showed a slight improvement over the previous (`std::stack<T, std::deque<T>>`) implementation, and an even greater (albeit still slight) improvement over using `std::stack<T, std::vector<T>>`.
Diffstat (limited to 'src/expr/node.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback