diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
commit | 9098391fe334d829ec4101f190b8f1fa21c30752 (patch) | |
tree | b134fc1fe1c767a50013e1449330ca6a7ee18a3d /src/util/dense_map.h | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/util/dense_map.h')
-rw-r--r-- | src/util/dense_map.h | 30 |
1 files changed, 26 insertions, 4 deletions
diff --git a/src/util/dense_map.h b/src/util/dense_map.h index b8acf1556..8f8b63668 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -29,6 +29,7 @@ #include <vector> #include <boost/integer_traits.hpp> #include "util/index.h" +#include "util/cvc4_assert.h" namespace CVC4 { @@ -287,15 +288,36 @@ public: bool isMember(Element x) const{ return d_map.isKey(x); } - void add(Element x){ + void add(Element x, CountType c = 1u){ + Assert(c > 0); if(d_map.isKey(x)){ - d_map.set(x, d_map.get(x)+1); + d_map.set(x, d_map.get(x)+c); }else{ - d_map.set(x,1); + d_map.set(x,c); } } - void remove(Element x){ return d_map.remove(x); } + void setCount(Element x, CountType c){ + d_map.set(x, c); + } + + void removeAll(Element x){ return d_map.remove(x); } + + void removeOne(Element x){ + CountType c = count(x); + switch(c){ + case 0: break; // do nothing + case 1: removeAll(x); break; // remove + default: d_map.set(x, c-1); break; // decrease + } + } + + void removeOneOfEverything(){ + BackingMap::KeyList keys(d_map.begin(), d_map.end()); + for(BackingMap::const_iterator i=keys.begin(), i_end = keys.end(); i != i_end; ++i){ + removeOne(*i); + } + } CountType count(Element x) const { if(d_map.isKey(x)){ |