Add (optional) performance tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-11 17:03:37 -07:00
parent 572c7ced2a
commit ef0e0ad382
2 changed files with 84 additions and 4 deletions

View file

@ -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;
}

View file

@ -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))) {