michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix bugs in pvector. Improve test driver

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-12 11:01:40 -07:00
parent 55ff49d2d5
commit f972cc9aae
4 changed files with 116 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/tests/util/pdeque.cpp
View file

@ -76,6 +76,13 @@ static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double p
double f = static_cast<double>(std::rand() % 10000) / 10000.0;
if (f < copy_freq)
copies.push_back(q3);
// read random positions of q3
if (!empty(q3)) {
for (unsigned j = 0; j < rand() % 5; j++) {
unsigned idx = rand() % size(q3);
lean_assert(q3[idx] == q1[idx]);
}
}
f = static_cast<double>(std::rand() % 10000) / 10000.0;
if (f < push_freq) {
if (q1.size() >= max_sz)

64
src/tests/util/pvector.cpp
View file

@ -50,29 +50,53 @@ bool operator==(pvector<T> v1, std::vector<T> const & v2) {
return true;
}
template<typename T>
bool operator==(pvector<T> v1, pvector<T> v2) {
if (v1.size() != v2.size())
return false;
for (unsigned i = 0; i < v1.size(); i++) {
if (v1[i] != v2[i])
return false;
}
return true;
}
static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double push_freq, double copy_freq) {
std::vector<int> v1;
pvector<int> v2;
pvector<int> v3;
std::vector<pvector<int>> copies;
for (unsigned i = 0; i < num_ops; i++) {
double f = static_cast<double>(std::rand() % 10000) / 10000.0;
if (f < copy_freq)
if (f < copy_freq) {
copies.push_back(v2);
}
f = static_cast<double>(std::rand() % 10000) / 10000.0;
// read random positions of v3
if (!empty(v3)) {
for (unsigned j = 0; j < rand() % 5; j++) {
unsigned idx = rand() % size(v3);
lean_assert(v3[idx] == v1[idx]);
}
}
if (f < push_freq) {
if (v1.size() >= max_sz)
continue;
int a = std::rand() % max_val;
v1.push_back(a);
v2.push_back(a);
v3 = push_back(v3, a);
lean_assert(back(v3) == a);
} else {
if (v1.size() == 0)
continue;
lean_assert(v1.back() == v2.back());
v1.pop_back();
v2.pop_back();
v3 = pop_back(v3);
}
lean_assert(v2 == v1);
lean_assert(v3 == v1);
}
std::cout << "Copies created: " << copies.size() << "\n";
}
@ -113,6 +137,42 @@ static void tst3() {
for (unsigned i = 0; i < M; i++) { s += v2[i % v2.size()]; }
}
static void tst4() {
pvector<int> v;
lean_assert(empty(v));
lean_assert(size(v) == 0);
v = push_back(v, 1);
lean_assert(size(v) == 1);
std::cout << "v: " << v << "\n";
lean_assert(back(v) == 1);
lean_assert(!empty(v));
v = push_back(v, 2);
lean_assert(back(v) == 2);
std::cout << "v: " << v << "\n";
v = push_back(v, 3);
std::cout << "v: " << v << "\n";
lean_assert(size(v) == 3);
lean_assert(v[0] == 1);
lean_assert(back(v) == 3);
lean_assert(size(pop_back(v)) == 2);
lean_assert(back(pop_back(v)) == 2);
lean_assert(pop_back(pop_back(v))[0] == 1);
lean_assert(empty(pop_back(pop_back(pop_back(v)))));
lean_assert(pop_back(push_back(v, 3)) == v);
}
static void tst5() {
pvector<int> v;
v.push_back(0);
pvector<int> v2 = v;
for (unsigned i = 1; i < 100; i++) {
lean_assert(v2[0] == 0);
v2.push_back(i);
lean_assert(v2[0] == 0);
v = pvector<int>();
}
}
#ifdef PVECTOR_PERF_TEST
static void perf_vector(unsigned n) {
std::vector<int> q;
@ -188,6 +248,8 @@ int main() {
tst1();
tst2();
tst3();
tst4();
tst5();
#ifdef PVECTOR_PERF_TEST
tst_perf1();
tst_perf2();

6
src/util/pdeque.h
View file

@ -533,7 +533,7 @@ template<typename T>
unsigned size(pdeque<T> const & s) { return s.size(); }
template<typename T> inline std::ostream & operator<<(std::ostream & out, pdeque<T> const & d) {
out << "[";
out << "[[";
bool first = true;
auto it = d.begin();
auto end = d.end();
@ -541,10 +541,10 @@ template<typename T> inline std::ostream & operator<<(std::ostream & out, pdeque
if (first)
first = false;
else
out << " ";
out << ", ";
out << *it;
}
out << "]";
out << "]]";
return out;
}
}

53
src/util/pvector.h
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <iostream>
#include <vector>
#include "rc.h"
@ -173,12 +174,17 @@ class pvector {
}
}
/** \brief Update quota based on the cost of a read */
void update_quota_on_read(unsigned cost) {
/**
\brief Update quota based on the cost of a read
Return true if the quota was updated, and false
if the representation had to be updated.
*/
bool update_quota_on_read(unsigned cost) {
cost /= 2; // reads are cheaper than writes
if (cost > 0) {
if (cost >= m_ptr->quota()) {
flat();
return false;
} else {
if (is_shared()) {
switch (m_ptr->kind()) {
@ -193,6 +199,7 @@ class pvector {
static_cast<delta_cell*>(m_ptr)->m_quota -= cost;
}
}
return true;
}
void pop_back_core() { update_cell(new pop_cell(m_ptr)); }
@ -230,21 +237,27 @@ public:
switch (it->kind()) {
case cell_kind::PushBack:
if (i + 1 == to_push(it).m_size) {
const_cast<pvector*>(this)->update_quota_on_read(cost);
return to_push(it).m_val;
if (const_cast<pvector*>(this)->update_quota_on_read(cost))
return to_push(it).m_val;
else
return operator[](i); // representation was changed, \c it may have been deleted
}
break;
case cell_kind::PopBack:
break;
case cell_kind::Set:
if (to_set(it).m_idx == i) {
const_cast<pvector*>(this)->update_quota_on_read(cost);
return to_set(it).m_val;
if (const_cast<pvector*>(this)->update_quota_on_read(cost))
return to_set(it).m_val;
else
return operator[](i); // representation was changed, \c it may have been deleted
}
break;
case cell_kind::Root:
const_cast<pvector*>(this)->update_quota_on_read(cost);
return to_root(it).m_vector[i];
if (const_cast<pvector*>(this)->update_quota_on_read(cost))
return to_root(it).m_vector[i];
else
return operator[](i); // representation was changed, \c it may have been deleted
}
it = static_cast<delta_cell const *>(it)->m_prev;
cost++;
@ -332,6 +345,7 @@ public:
}
class iterator {
friend class pvector;
pvector const & m_vector;
unsigned m_it;
iterator(pvector const & v, unsigned it):m_vector(v), m_it(it) {}
@ -341,8 +355,8 @@ public:
iterator operator++(int) { iterator tmp(*this); operator++(); return tmp; }
bool operator==(iterator const & s) const { lean_assert(&m_vector == &(s.m_vector)); return m_it == s.m_it; }
bool operator!=(iterator const & s) const { return !operator==(s); }
T const & operator*() { lean_assert(m_it); return m_vector[m_it]; }
T const * operator->() { lean_assert(m_it); return &(m_vector[m_it]); }
T const & operator*() const { return m_vector[m_it]; }
T const * operator->() const { return &(m_vector[m_it]); }
};
/** \brief Return an iterator to the beginning */
@ -405,4 +419,23 @@ T const & back(pvector<T> const & s) { return s.back(); }
/** \brief Return true iff \c s is empty. */
template<typename T>
bool empty(pvector<T> const & s) { return s.empty(); }
/** \brief Return the size of \c s. */
template<typename T>
unsigned size(pvector<T> const & s) { return s.size(); }
template<typename T> inline std::ostream & operator<<(std::ostream & out, pvector<T> const & d) {
out << "[";
bool first = true;
auto it = d.begin();
auto end = d.end();
for (; it != end; ++it) {
if (first)
first = false;
else
out << ", ";
out << *it;
}
out << "]";
return out;
}
}