diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
commit | 068107e1d1f705eb9054b4309a26236230687d80 (patch) | |
tree | 4c422f3efd6a8319abe426c518f9d2feb7ab5a6d /src/context/cdhashset.h | |
parent | 53176a3d39935bd77f1c057d0b806c380b346e23 (diff) |
CDMap -> CDHashMap
CDSet -> CDHashSet
Diffstat (limited to 'src/context/cdhashset.h')
-rw-r--r-- | src/context/cdhashset.h | 151 |
1 files changed, 151 insertions, 0 deletions
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h new file mode 100644 index 000000000..777bbc94b --- /dev/null +++ b/src/context/cdhashset.h @@ -0,0 +1,151 @@ +/********************* */ +/*! \file cdset.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Context-dependent set class. + ** + ** Context-dependent set class. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDSET_H +#define __CVC4__CONTEXT__CDSET_H + +#include "context/context.h" +#include "context/cdhashset_forward.h" +#include "context/cdhashmap.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +template <class V, class HashFcn> +class CDHashSet : protected CDHashMap<V, V, HashFcn> { + typedef CDHashMap<V, V, HashFcn> super; + +public: + + // ensure these are publicly accessible + static void* operator new(size_t size, bool b) { + return ContextObj::operator new(size, b); + } + + static void operator delete(void* pMem, bool b) { + return ContextObj::operator delete(pMem, b); + } + + void deleteSelf() { + this->ContextObj::deleteSelf(); + } + + static void operator delete(void* pMem) { + AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); + } + + CDHashSet(Context* context) : + super(context) { + } + + size_t size() const { + return super::size(); + } + + size_t count(const V& v) const { + return super::count(v); + } + + bool insert(const V& v) { + return super::insert(v, v); + } + + bool contains(const V& v) { + return find(v) != end(); + } + + // 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 */ + +#endif /* __CVC4__CONTEXT__CDSET_H */ |