diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 4 | ||||
-rw-r--r-- | src/util/dense_map.h | 294 | ||||
-rw-r--r-- | src/util/index.h | 29 |
3 files changed, 326 insertions, 1 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index d52f23a9c..4945f6339 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -52,6 +52,7 @@ libutil_la_SOURCES = \ language.h \ lemma_input_channel.h \ lemma_output_channel.h \ + dense_map.h \ channel.h \ language.cpp \ ntuple.h \ @@ -73,7 +74,8 @@ libutil_la_SOURCES = \ ite_removal.cpp \ pseudoboolean.h \ pseudoboolean.cpp \ - node_visitor.h + node_visitor.h \ + index.h libutil_la_LIBADD = \ @builddir@/libutilcudd.la 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 */ diff --git a/src/util/index.h b/src/util/index.h new file mode 100644 index 000000000..0c8b0a307 --- /dev/null +++ b/src/util/index.h @@ -0,0 +1,29 @@ +#include "cvc4_private.h" + +#pragma once + +#include <stdint.h> +#include <boost/static_assert.hpp> + +namespace CVC4 { + +/** + * Index is an unsigned integer used for array indexing. + * + * This gives a standardized type for independent pieces of code to use as an agreement. + */ +typedef uint32_t Index; + +BOOST_STATIC_ASSERT(sizeof(Index) <= sizeof(size_t)); +BOOST_STATIC_ASSERT(!std::numeric_limits<Index>::is_signed); + +/* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)? + * + * size_t is a more appropraite choice than uint32_t as the choice is dictated by + * uniqueness in arrays and vectors. These correspond to size_t. + * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticably + * slower. (Limited testing suggests a ~1/16 of running time.) + * (Interestingly, uint_fast32_t also has a sizeof == 8 on x86_64. Filthy Liars!) + */ + +}; /* namespace CVC4 */ |