From ef0e0ad3826c87219b5b36336563e51992e46551 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Sep 2013 17:03:37 -0700
Subject: [PATCH] Add (optional) performance tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/queue.cpp | 80 ++++++++++++++++++++++++++++++++++++++++
 src/util/queue.h         |  8 ++--
 2 files changed, 84 insertions(+), 4 deletions(-)

diff --git a/src/tests/util/queue.cpp b/src/tests/util/queue.cpp
index b2ebba3b0..f52aa6904 100644
--- a/src/tests/util/queue.cpp
+++ b/src/tests/util/queue.cpp
@@ -122,9 +122,89 @@ static void tst3() {
     lean_assert(pop_back(pop_back(q).first).second == 3);
 }
 
+// #define QUEUE_PERF_TEST
+#ifdef QUEUE_PERF_TEST
+#include "timeit.h"
+
+static void perf_deque(unsigned n) {
+    std::deque<int> q;
+    for (unsigned i = 0; i < n; i++) {
+        q.push_back(i);
+    }
+    for (unsigned i = 0; i < n; i++) {
+        q.pop_front();
+    }
+}
+
+static void perf_queue(unsigned n) {
+    queue<int> q;
+    for (unsigned i = 0; i < n; i++) {
+        q = push_back(q, i);
+    }
+    for (unsigned i = 0; i < n; i++) {
+        q = pop_front(q).first;
+    }
+}
+
+static void tst4() {
+    unsigned N = 100000;
+    unsigned M = 100;
+    {
+        timeit t(std::cout, "deque time");
+        for (unsigned i = 0; i < N; i++) perf_deque(M);
+    }
+    {
+        timeit t(std::cout, "queue time");
+        for (unsigned i = 0; i < N; i++) perf_queue(M);
+    }
+}
+
+
+static void perf_deque2(std::deque<int> q, unsigned n) {
+    for (unsigned i = 0; i < n; i++) {
+        q.push_back(i);
+    }
+    for (unsigned i = 0; i < n; i++) {
+        q.pop_front();
+    }
+}
+
+static void perf_queue2(queue<int> q, unsigned n) {
+    for (unsigned i = 0; i < n; i++) {
+        q = push_back(q, i);
+    }
+    for (unsigned i = 0; i < n; i++) {
+        q = pop_front(q).first;
+    }
+}
+
+static void tst5() {
+    unsigned N = 100000;
+    unsigned SZ1 = 10000;
+    unsigned M   = 5;
+    {
+        timeit t(std::cout, "deque time");
+        std::deque<int> q;
+        for (unsigned i = 0; i < SZ1; i++) { q.push_back(i); }
+        for (unsigned i = 0; i < N; i++) perf_deque2(q, M);
+    }
+    {
+        timeit t(std::cout, "queue time");
+        queue<int> q;
+        for (unsigned i = 0; i < SZ1 + 1; i++) { q = push_back(q, i); }
+        q = pop_front(q).first;
+        for (unsigned i = 0; i < N; i++) perf_queue2(q, M);
+    }
+}
+#endif
+
 int main() {
     tst1();
     tst2();
     tst3();
+#ifdef QUEUE_PERF_TEST
+    tst4();
+    tst5();
+#endif
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/queue.h b/src/util/queue.h
index 5d3d2edc9..761b662cb 100644
--- a/src/util/queue.h
+++ b/src/util/queue.h
@@ -28,10 +28,10 @@ public:
     unsigned size() const { return length(m_front) + length(m_rear); }
 
     /** \brief Return the queue <tt>(v :: q)</tt> (complexity O(1)) */
-    friend queue push_front(queue const & q, T const & v) { return queue(cons(v, q.m_front), q.m_rear); }
+    friend queue push_front(queue<T> const & q, T const & v) { return queue(cons(v, q.m_front), q.m_rear); }
 
     /** \brief Return the queue <tt>(q :: v)</tt> (complexity O(1)) */
-    friend queue push_back(queue const & q, T const & v) { return queue(q.m_front, cons(v, q.m_rear)); }
+    friend queue push_back(queue<T> const & q, T const & v) { return queue(q.m_front, cons(v, q.m_rear)); }
 
     /**
         \brief Return the pair <tt>(q, v)</tt> for a queue <tt>(v :: q)</tt>.
@@ -39,7 +39,7 @@ public:
 
         \pre !is_empty(q)
     */
-    friend std::pair<queue, T> pop_front(queue const & q) {
+    friend std::pair<queue<T>, T> pop_front(queue<T> const & q) {
         lean_assert(!q.is_empty());
         if (is_nil(q.m_front)) {
             if (is_nil(cdr(q.m_rear))) {
@@ -59,7 +59,7 @@ public:
 
         \pre !is_empty(q)
     */
-    friend std::pair<queue, T> pop_back(queue const & q) {
+    friend std::pair<queue<T>, T> pop_back(queue<T> const & q) {
         lean_assert(!q.is_empty());
         if (is_nil(q.m_rear)) {
             if (is_nil(cdr(q.m_front))) {