diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-05 21:45:12 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-05 21:45:12 +0000 |
commit | bd0a6c39c56c6ad2bf12e7b9fd41db1772fed9cd (patch) | |
tree | 51f4bc5994a0716e6f4cfeed136360954ce505ac /src/util | |
parent | 356a8b6e5ea2622d0fef5cf209159caf08ba5297 (diff) |
Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/dense_map.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/util/dense_map.h b/src/util/dense_map.h index fa78e6787..222a761c3 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -151,6 +151,7 @@ public: pop_back(); } + /** Returns the key at the back of a non-empty list.*/ Key back() const { return d_list.back(); } @@ -164,6 +165,27 @@ public: d_list.pop_back(); } + + /** Adds at least a constant fraction of the elements in the current map to another map. */ + void splitInto(DenseMap<T>& target){ + uint32_t targetSize = size()/2; + while(size() > targetSize){ + Key key = back(); + target.set(key, get(key)); + pop_back(); + } + } + + /** Adds the current target map to the current map.*/ + void addAll(const DenseMap<T>& target){ + for(const_iterator i = target.begin(), e = target.end(); i != e; ++i){ + Key k = *i; + set(k, target[k]); + } + } + + + private: size_t allocated() const { |