diff options
Diffstat (limited to 'src/context/cdset.h')
-rw-r--r-- | src/context/cdset.h | 96 |
1 files changed, 94 insertions, 2 deletions
diff --git a/src/context/cdset.h b/src/context/cdset.h index 48ad12daa..f51e689d5 100644 --- a/src/context/cdset.h +++ b/src/context/cdset.h @@ -24,8 +24,100 @@ namespace CVC4 { namespace context { -template <class K, class HashFcn> -class CDSet; +template <class V, class HashFcn> +class CDSet : protected CDMap<V, V, HashFcn> { + typedef CDMap<V, V, HashFcn> super; + +public: + + CDSet(Context* context) : + super(context) { + } + + size_t size() const { + return super::size(); + } + + size_t count(const V& v) const { + return super::count(v); + } + + void insert(const V& v) { + super::insert(v, v); + } + + // FIXME: no erase(), too much hassle to implement efficiently... + + class iterator { + typename super::iterator d_it; + + public: + + iterator(const typename super::iterator& it) : d_it(it) {} + iterator(const iterator& it) : d_it(it.d_it) {} + + // Default constructor + iterator() {} + + // (Dis)equality + bool operator==(const iterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const iterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + V operator*() const { + return (*d_it).first; + } + + // Prefix increment + iterator& operator++() { + ++d_it; + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const V& d_val; + + public: + + Proxy(const V& v) : d_val(v) {} + + V operator*() const { + return d_val; + } + };/* class CDSet<>::iterator::Proxy */ + + // Actual postfix increment: returns Proxy with the old value. + // Now, an expression like *i++ will return the current *i, and + // then advance the orderedIterator. However, don't try to use + // Proxy for anything else. + const Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDSet<>::iterator */ + + typedef iterator const_iterator; + + const_iterator begin() const { + return iterator(super::begin()); + } + + const_iterator end() const { + return iterator(super::end()); + } + + const_iterator find(const V& v) const { + return iterator(super::find(v)); + } + +};/* class CDSet */ }/* CVC4::context namespace */ }/* CVC4 namespace */ |