From d5eabdff2f68dcc3da96c2651976172fc181f074 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 24 May 2018 14:00:29 +0000
Subject: [PATCH] expr_iterator: use a std::deque to implement the stack

operator++ mostly spent its time doing re-allocations. Using a
std::deque reduces the runtime across >1 billion calls from 20s to less
than 1s.
---
 src/util/expr_iterator.h | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h
index b72bd02b1c4..132a1784d7b 100644
--- a/src/util/expr_iterator.h
+++ b/src/util/expr_iterator.h
@@ -9,6 +9,7 @@
 #ifndef CPROVER_UTIL_EXPR_ITERATOR_H
 #define CPROVER_UTIL_EXPR_ITERATOR_H
 
+#include <deque>
 #include <iterator>
 #include <functional>
 #include <set>
@@ -39,7 +40,7 @@ class const_unique_depth_iteratort;
 /// Helper class for depth_iterator_baset
 struct depth_iterator_expr_statet final
 {
-  typedef std::vector<exprt>::const_iterator operands_iteratort;
+  typedef exprt::operandst::const_iterator operands_iteratort;
   inline depth_iterator_expr_statet(
     const exprt &expr,
     operands_iteratort it,
@@ -213,7 +214,7 @@ class depth_iterator_baset
   }
 
 private:
-  std::vector<depth_iterator_expr_statet> m_stack;
+  std::deque<depth_iterator_expr_statet> m_stack;
 
   depth_iterator_t &downcast()
   { return static_cast<depth_iterator_t &>(*this); }