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

Add support for writing a[i] = v instead of a.set(i, v) in the pdeque class.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-12 11:18:26 -07:00
parent 74b8a4f0ac
commit bc69e7803f
2 changed files with 37 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -67,7 +67,7 @@ static void tst1() {
lean_assert(pop_back(push_back(q, 3)) == q);
}
static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double push_freq, double copy_freq) {
static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double updt_freq, double copy_freq) {
std::deque<int> q1;
pdeque<int> q2;
pdeque<int> q3;
@ -84,18 +84,31 @@ static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double p
}
}
f = static_cast<double>(std::rand() % 10000) / 10000.0;
if (f < push_freq) {
if (f < updt_freq) {
if (q1.size() >= max_sz)
continue;
int v = std::rand() % max_val;
if (std::rand() % 2 == 0) {
switch (std::rand() % 3) {
case 0:
q1.push_front(v);
q2 = push_front(q2, v);
q3.push_front(v);
} else {
break;
case 1:
q1.push_back(v);
q2 = push_back(q2, v);
q3.push_back(v);
break;
default:
if (!empty(q2)) {
unsigned idx = rand() % size(q2);
q1[idx] = v;
q2[idx] = v;
q3[idx] = v;
lean_assert(q1[idx] == q2[idx]);
lean_assert(q1[idx] == q3[idx]);
}
break;
}
} else {
if (q1.size() == 0)

25
src/util/pdeque.h
View file

@ -264,7 +264,7 @@ public:
\brief Access specified element
\pre i < size()
*/
T const & operator[](unsigned i) const {
T const & get(unsigned i) const {
lean_assert(i < size());
cell const * it = m_ptr;
unsigned input_i = i;
@ -276,7 +276,7 @@ public:
if (const_cast<pdeque*>(this)->update_quota_on_read(cost))
return to_push_back(it).m_val;
else
return operator[](input_i); // representation was updated
return get(input_i); // representation was updated
}
break;
case cell_kind::PushFront:
@ -284,7 +284,7 @@ public:
if (const_cast<pdeque*>(this)->update_quota_on_read(cost))
return to_push_front(it).m_val;
else
return operator[](input_i); // representation was updated
return get(input_i); // representation was updated
} else {
i--;
}
@ -299,14 +299,14 @@ public:
if (const_cast<pdeque*>(this)->update_quota_on_read(cost))
return to_set(it).m_val;
else
return operator[](input_i); // representation was updated
return get(input_i); // representation was updated
}
break;
case cell_kind::Root:
if (const_cast<pdeque*>(this)->update_quota_on_read(cost))
return to_root(it).m_deque[i];
else
return operator[](input_i); // representation was updated
return get(input_i); // representation was updated
}
it = static_cast<delta_cell const *>(it)->m_prev;
cost++;
@ -432,6 +432,8 @@ public:
switch (m_ptr->kind()) {
case cell_kind::PushBack:
case cell_kind::PopBack:
case cell_kind::PushFront:
case cell_kind::PopFront:
set_core(i, v);
break;
case cell_kind::Set:
@ -449,6 +451,19 @@ public:
}
}
class ref {
pdeque & m_deque;
unsigned m_idx;
public:
ref(pdeque & v, unsigned i):m_deque(v), m_idx(i) {}
ref & operator=(T const & a) { m_deque.set(m_idx, a); return *this; }
operator T const &() const { return m_deque.get(m_idx); }
};
T const & operator[](unsigned i) const { return get(i); }
ref operator[](unsigned i) { return ref(*this, i); }
class iterator {
friend class pdeque;
pdeque const & m_deque;