summaryrefslogtreecommitdiff
path: root/src/util/dense_map.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/dense_map.h')
-rw-r--r--src/util/dense_map.h294
1 files changed, 294 insertions, 0 deletions
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
new file mode 100644
index 000000000..a687985f9
--- /dev/null
+++ b/src/util/dense_map.h
@@ -0,0 +1,294 @@
+/********************* */
+/*! \file dense_map.h
+ ** \verbatim
+ ** Original author: taking
+ ** 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 This is an abstraction of a Map from unsigned integers to elements of type T.
+ **
+ ** This is an abstraction of a Map from an unsigned integer to elements of type T.
+ ** This class is designed to provide constant time insertion, deletion, element_of,
+ ** and fast iteration. This is done by storing backing vectors of size greater than
+ ** the maximum key. This datastructure is appropraite for heavy use datastructures
+ ** where the Keys are a dense set of integers.
+ **
+ ** T must support T(), and operator=().
+ **
+ ** The derived utility classes DenseSet and DenseMultiset are also defined.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+#include <boost/integer_traits.hpp>
+#include "util/index.h"
+
+namespace CVC4 {
+
+template <class T>
+class DenseMap {
+public:
+ typedef Index Key;
+ typedef std::vector<Key> KeyList;
+ typedef KeyList::const_iterator const_iterator;
+
+private:
+ //List of the keys in the dense map.
+ KeyList d_list;
+
+ typedef Index Position;
+ typedef std::vector<Position> PositionMap;
+ static const Position POSITION_SENTINEL = boost::integer_traits<Position>::const_max;
+
+ //Each Key in the set is mapped to its position in d_list.
+ //Each Key not in the set is mapped to KEY_SENTINEL
+ PositionMap d_posVector;
+
+ typedef std::vector<T> ImageMap;
+ //d_image : Key |-> T
+ ImageMap d_image;
+
+public:
+
+ DenseMap() : d_list(), d_posVector(), d_image() {}
+
+ /** Returns the number of elements in the set. */
+ size_t size() const {
+ return d_list.size();
+ }
+
+ /** Returns true if the map is empty(). */
+ bool empty() const {
+ return d_list.empty();
+ }
+
+ /**
+ * Similar to a std::vector::clear().
+ *
+ * Invalidates iterators.
+ */
+ void clear() {
+ d_list.clear();
+ d_posVector.clear();
+ d_image.clear();
+ Assert(empty());
+ }
+
+ /**
+ * Similar to a clear(), but the datastructures are not reset in size.
+ * Invalidates iterators.
+ */
+ void purge() {
+ while(!empty()){
+ pop_back();
+ }
+ Assert(empty());
+ }
+
+ /** Returns true if k is a key of this datastructure. */
+ bool isKey(Key x) const{
+ if( x >= allocated()){
+ return false;
+ }else{
+ Assert(x < allocated());
+ return d_posVector[x] != POSITION_SENTINEL;
+ }
+ }
+
+ /**
+ * Maps the key to value in the map.
+ * Invalidates iterators.
+ */
+ void set(Key key, const T& value){
+ if( key >= allocated()){
+ increaseSize(key);
+ }
+
+ if(!isKey(key)){
+ d_posVector[key] = size();
+ d_list.push_back(key);
+ }
+ d_image[key] = value;
+ }
+
+ /** Returns a mutable reference to the element mapped by key. */
+ T& get(Key key){
+ Assert(isKey(key));
+ return d_image[key];
+ }
+
+ /** Returns a const reference to the element mapped by key.*/
+ const T& operator[](Key key) const {
+ Assert(isKey(key));
+ return d_image[key];
+ }
+
+ /** Returns an iterator over the keys of the map. */
+ const_iterator begin() const{ return d_list.begin(); }
+ const_iterator end() const{ return d_list.end(); }
+
+ const KeyList& getKeys() const{
+ return d_list;
+ }
+
+ /**
+ * Removes the mapping associated with key.
+ * This changes the order of the keys.
+ *
+ * Invalidates iterators.
+ */
+ void remove(Key x){
+ Assert(isKey(x));
+ swapToBack(x);
+ Assert(d_list.back() == x);
+ pop_back();
+ }
+
+ Key back() const {
+ return d_list.back();
+ }
+
+ /** Removes the element associated with the last Key from the map. */
+ void pop_back() {
+ Assert(!empty());
+ Key atBack = back();
+ d_posVector[atBack] = POSITION_SENTINEL;
+ d_image[atBack] = T();
+ d_list.pop_back();
+ }
+
+ private:
+
+ size_t allocated() const {
+ Assert(d_posVector.size() == d_image.size());
+ return d_posVector.size();
+ }
+
+ void increaseSize(Key max){
+ Assert(max >= allocated());
+ d_posVector.resize(max+1, POSITION_SENTINEL);
+ d_image.resize(max+1);
+ }
+
+ /** Swaps a member x to the back of d_list. */
+ void swapToBack(Key x){
+ Assert(isKey(x));
+
+ Position currentPos = d_posVector[x];
+ Key atBack = back();
+
+ d_list[currentPos] = atBack;
+ d_posVector[atBack] = currentPos;
+
+ Position last = size() - 1;
+
+ d_list[last] = x;
+ d_posVector[x] = last;
+ }
+}; /* class DenseMap<T> */
+
+/**
+ * This provides an abstraction for a set of unsigned integers with similar capabilities
+ * as DenseMap. This is implemented as a light wrapper for DenseMap<bool> with an
+ * interface designed for use as a set instead of a map.
+ */
+class DenseSet {
+private:
+ typedef DenseMap<bool> BackingMap;
+ BackingMap d_map;
+public:
+ typedef BackingMap::const_iterator const_iterator;
+ typedef BackingMap::Key Element;
+
+ size_t size() const { return d_map.size(); }
+ bool empty() const { return d_map.empty(); }
+
+ /** See DenseMap's documentation. */
+ void purge() { d_map.purge(); }
+ void clear() { d_map.clear(); }
+
+ bool isMember(Element x) const{ return d_map.isKey(x); }
+
+ /**
+ * Adds an element that is not a member of the set to the set.
+ */
+ void add(Element x){
+ Assert(!isMember(x));
+ d_map.set(x, true);
+ }
+
+ /** Adds an element to the set even if it is already an element of the set. */
+ void softAdd(Element x){ d_map.set(x, true); }
+
+ /** Removes an element from the set. */
+ void remove(Element x){ d_map.remove(x); }
+
+ const_iterator begin() const{ return d_map.begin(); }
+ const_iterator end() const{ return d_map.end(); }
+
+ Element back() { return d_map.back(); }
+ void pop_back() { d_map.pop_back(); }
+}; /* class DenseSet */
+
+/**
+ * This provides an abstraction for a multiset of unsigned integers with similar
+ * capabilities as DenseMap.
+ * This is implemented as a light wrapper for DenseMap<bool> with an
+ * interface designed for use as a set instead of a map.
+ */
+class DenseMultiset {
+public:
+ typedef uint32_t CountType;
+
+private:
+ typedef DenseMap<CountType> BackingMap;
+ BackingMap d_map;
+
+public:
+ typedef BackingMap::const_iterator const_iterator;
+ typedef BackingMap::Key Element;
+
+ DenseMultiset() : d_map() {}
+
+ size_t size() const { return d_map.size(); }
+ bool empty() const { return d_map.empty(); }
+
+ void purge() { d_map.purge(); }
+ void clear() { d_map.clear(); }
+
+ bool isMember(Element x) const{ return d_map.isKey(x); }
+
+ void add(Element x){
+ if(d_map.isKey(x)){
+ d_map.set(x, d_map.get(x)+1);
+ }else{
+ d_map.set(x,1);
+ }
+ }
+
+ void remove(Element x){ return d_map.remove(x); }
+
+ CountType count(Element x) const {
+ if(d_map.isKey(x)){
+ return d_map[x];
+ }else {
+ return 0;
+ }
+ }
+
+ const_iterator begin() const{ return d_map.begin(); }
+ const_iterator end() const{ return d_map.end(); }
+ Element back() { return d_map.back(); }
+ void pop_back() { d_map.pop_back(); }
+}; /* class DenseMultiset */
+
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback