diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-27 14:47:10 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-27 14:47:10 +0000 |
commit | f813ed144b0945334e03bfd769ea3c2cf8b75843 (patch) | |
tree | e70c9bddf5445aac50b5080c2b1719e6ffb478e0 /src/util/dense_map.h | |
parent | 68237f7d39a03905be4cc133a42083fc3342adb4 (diff) |
This merges in the branch cvc4/branches/arithmetic/matrix into trunk.
- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!
Diffstat (limited to 'src/util/dense_map.h')
-rw-r--r-- | src/util/dense_map.h | 294 |
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 */ |