diff options
Diffstat (limited to 'src/prop/minisat/mtl/Map.h')
| -rw-r--r-- | src/prop/minisat/mtl/Map.h | 128 |
1 files changed, 0 insertions, 128 deletions
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h deleted file mode 100644 index 715b84da4..000000000 --- a/src/prop/minisat/mtl/Map.h +++ /dev/null @@ -1,128 +0,0 @@ -/*******************************************************************************************[Map.h] -MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#include "cvc4_private.h" - -#ifndef CVC4_MiniSat_Map_h -#define CVC4_MiniSat_Map_h - -#include <stdint.h> - -#include "Vec.h" - -namespace CVC4 { -namespace prop { -namespace minisat { - -//================================================================================================= -// Default hash/equals functions -// - -template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; -template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; - -template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; -template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; - -//================================================================================================= -// Some primes -// - -static const int nprimes = 25; -static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 }; - -//================================================================================================= -// Hash table implementation of Maps -// - -template<class K, class D, class H = Hash<K>, class E = Equal<K> > -class Map { - struct Pair { K key; D data; }; - - H hash; - E equals; - - vec<Pair>* table; - int cap; - int size; - - // Don't allow copying (error prone): - Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); } - Map (Map<K,D,H,E>& other) { assert(0); } - - int32_t index (const K& k) const { return hash(k) % cap; } - void _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; } - void rehash () { - const vec<Pair>* old = table; - - int newsize = primes[0]; - for (int i = 1; newsize <= cap && i < nprimes; i++) - newsize = primes[i]; - - table = new vec<Pair>[newsize]; - - for (int i = 0; i < cap; i++){ - for (int j = 0; j < old[i].size(); j++){ - _insert(old[i][j].key, old[i][j].data); }} - - delete [] old; - - cap = newsize; - } - - - public: - - Map () : table(NULL), cap(0), size(0) {} - Map (const H& h, const E& e) : Map(), hash(h), equals(e) {} - ~Map () { delete [] table; } - - void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; } - bool peek (const K& k, D& d) { - if (size == 0) return false; - const vec<Pair>& ps = table[index(k)]; - for (int i = 0; i < ps.size(); i++) - if (equals(ps[i].key, k)){ - d = ps[i].data; - return true; } - return false; - } - - void remove (const K& k) { - assert(table != NULL); - vec<Pair>& ps = table[index(k)]; - int j = 0; - for (; j < ps.size() && !equals(ps[j].key, k); j++); - assert(j < ps.size()); - ps[j] = ps.last(); - ps.pop(); - } - - void clear () { - cap = size = 0; - delete [] table; - table = NULL; - } -}; - -}/* CVC4::prop::minisat namespace */ -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4_MiniSat_Map_h */ |