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>>`.

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index bcdebc12e4df0439b41a991b6129fd576aa2b471..e4e485fd9702f83038aa7338f5393a81dccbf0f9 100644 (file)
--- 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!
           }