diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-12-12 21:05:49 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-12 21:05:49 -0800 |
commit | 8afa8a89101743915fe6b94dabd18797a55b3e55 (patch) | |
tree | d705a94914f106eefa62652f037243c2fbc83628 /src/expr/node.h | |
parent | 87602bc6d010eea33b8db93e80a79dcf99d230b5 (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