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/theory/fp/fp_converter.cpp | |
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/theory/fp/fp_converter.cpp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 98 |
1 files changed, 49 insertions, 49 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index bcdebc12e..e4e485fd9 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -16,7 +16,7 @@ #include "theory/theory.h" // theory.h Only needed for the leaf test -#include <stack> +#include <vector> #ifdef CVC4_USE_SYMFPU #include "symfpu/core/add.h" @@ -846,17 +846,17 @@ FpConverter::uf FpConverter::buildComponents(TNode current) Node FpConverter::convert(TNode node) { #ifdef CVC4_USE_SYMFPU - std::stack<TNode> workStack; + std::vector<TNode> workStack; TNode result = node; - workStack.push(node); + workStack.push_back(node); NodeManager *nm = NodeManager::currentNM(); while (!workStack.empty()) { - TNode current = workStack.top(); - workStack.pop(); + TNode current = workStack.back(); + workStack.pop_back(); result = current; TypeNode t(current.getType()); @@ -941,8 +941,8 @@ Node FpConverter::convert(TNode node) if (arg1 == f.end()) { - workStack.push(current); - workStack.push(current[0]); + workStack.push_back(current); + workStack.push_back(current[0]); continue; // i.e. recurse! } @@ -974,14 +974,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (mode == r.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg1 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1017,14 +1017,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (arg1 == f.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg2 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1047,14 +1047,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (arg1 == f.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg2 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1098,18 +1098,18 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (mode == r.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg1 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } if (arg2 == f.end()) { - workStack.push(current[2]); + workStack.push_back(current[2]); } continue; // i.e. recurse! } @@ -1178,22 +1178,22 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (mode == r.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg1 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } if (arg2 == f.end()) { - workStack.push(current[2]); + workStack.push_back(current[2]); } if (arg3 == f.end()) { - workStack.push(current[3]); + workStack.push_back(current[3]); } continue; // i.e. recurse! } @@ -1216,14 +1216,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (mode == r.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg1 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1260,10 +1260,10 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (mode == r.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } continue; // i.e. recurse! } @@ -1335,14 +1335,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (arg1 == f.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg2 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1359,14 +1359,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (arg1 == r.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg2 == r.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1392,14 +1392,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (arg1 == f.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg2 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1438,8 +1438,8 @@ Node FpConverter::convert(TNode node) if (arg1 == f.end()) { - workStack.push(current); - workStack.push(current[0]); + workStack.push_back(current); + workStack.push_back(current[0]); continue; // i.e. recurse! } @@ -1536,14 +1536,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (mode == r.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg1 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1577,14 +1577,14 @@ Node FpConverter::convert(TNode node) if (recurseNeeded) { - workStack.push(current); + workStack.push_back(current); if (mode == r.end()) { - workStack.push(current[0]); + workStack.push_back(current[0]); } if (arg1 == f.end()) { - workStack.push(current[1]); + workStack.push_back(current[1]); } continue; // i.e. recurse! } @@ -1643,8 +1643,8 @@ Node FpConverter::convert(TNode node) if (arg1 == f.end()) { - workStack.push(current); - workStack.push(current[0]); + workStack.push_back(current); + workStack.push_back(current[0]); continue; // i.e. recurse! } |