FP converter: convert: Use std::vector as instead of std::stack. (#3563)
authorAina Niemetz <aina.niemetz@gmail.com>
Fri, 13 Dec 2019 05:05:49 +0000 (21:05 -0800)
committerAndres Noetzli <andres.noetzli@gmail.com>
Fri, 13 Dec 2019 05:05:49 +0000 (21:05 -0800)
commit8afa8a89101743915fe6b94dabd18797a55b3e55
treed705a94914f106eefa62652f037243c2fbc83628
parent87602bc6d010eea33b8db93e80a79dcf99d230b5
 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>>`.
src/theory/fp/fp_converter.cpp