From 7f52115ab0dcba4c8ba9403a5f25b8e8c588911a Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 5 Dec 2012 19:06:21 +0000 Subject: [PATCH] This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsertHashMap. CDHashSet have been changed to CDHashSet. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap. --- src/context/Makefile.am | 4 + src/context/cdhashmap.h | 41 +- src/context/cdhashmap_forward.h | 16 +- src/context/cdhashset.h | 57 ++- src/context/cdinsert_hashmap.h | 402 +++++++++++++++ src/context/cdinsert_hashmap_forward.h | 38 ++ src/context/cdtrail_hashmap.h | 571 ++++++++++++++++++++++ src/context/cdtrail_hashmap_forward.h | 38 ++ src/decision/justification_heuristic.h | 6 +- src/decision/relevancy.h | 2 +- src/prop/cnf_stream.cpp | 33 +- src/prop/cnf_stream.h | 5 +- src/theory/arith/arith_static_learner.cpp | 12 +- src/theory/arith/arith_static_learner.h | 8 +- src/theory/arith/theory_arith.cpp | 2 +- src/theory/arith/theory_arith.h | 3 +- src/theory/arrays/theory_arrays.cpp | 6 +- src/theory/arrays/theory_arrays.h | 6 +- src/theory/booleans/circuit_propagator.h | 2 +- src/theory/bv/theory_bv.h | 4 +- src/theory/shared_terms_database.h | 2 +- src/theory/theory_engine.h | 2 +- 22 files changed, 1158 insertions(+), 102 deletions(-) create mode 100644 src/context/cdinsert_hashmap.h create mode 100644 src/context/cdinsert_hashmap_forward.h create mode 100644 src/context/cdtrail_hashmap.h create mode 100644 src/context/cdtrail_hashmap_forward.h diff --git a/src/context/Makefile.am b/src/context/Makefile.am index e7f1dc68b..a63c990cc 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -16,6 +16,10 @@ libcontext_la_SOURCES = \ cdlist_forward.h \ cdqueue.h \ cdtrail_queue.h \ + cdtrail_hashmap.h \ + cdtrail_hashmap_forward.h \ + cdinsert_hashmap.h \ + cdinsert_hashmap_forward.h \ cdhashmap.h \ cdhashmap_forward.h \ cdhashset.h \ diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index a37fd2f23..e2ede0603 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -17,14 +17,19 @@ ** and operator== for the key class. For key types that don't have a ** __gnu_cxx::hash<>, you should provide an explicit HashFcn. ** + ** See also: + ** CDInsertHashMap : An "insert-once" CD hash map. + ** CDTrailHashMap : A lightweight CD hash map with poor iteration + ** characteristics and some quirks in usage. + ** ** Internal documentation: ** - ** CDMap<> is something of a work in progress at present (26 May + ** CDHashMap<> is something of a work in progress at present (26 May ** 2010), due to some recent discoveries of problems with its ** internal state. Here are some notes on the internal use of ** CDOhash_maps that may be useful in figuring out this mess: ** - ** So you have a CDMap<>. + ** So you have a CDHashMap<>. ** ** You insert some (key,value) pairs. Each allocates a CDOhash_map<> ** and goes on a doubly-linked list headed by map.d_first and @@ -36,7 +41,7 @@ ** map pointer at level 0, and a non-NULL map pointer in the ** current context level. (Remember that for later.) ** - ** When a key is associated to a new value in a CDMap, its + ** When a key is associated to a new value in a CDHashMap, its ** associated CDOhash_map calls makeCurrent(), then sets the new ** value. The save object is also a CDOhash_map (allocated in context ** memory). @@ -62,21 +67,21 @@ ** obliterate() removes it from the map and frees the CDOhash_map's ** memory. ** - ** Fourth, you might delete the cdhashmap(calling CDMap::~CDMap()). + ** Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). ** This first calls destroy(), as per ContextObj contract, but ** cdhashmapdoesn't save/restore itself, so that does nothing at the - ** CDMap-level. Then it empties the trash. Then, for each + ** CDHashMap-level. Then it empties the trash. Then, for each ** element in the map, it marks it as being "part of a complete ** map destruction", which essentially short-circuits ** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates ** it. Finally it asserts that the trash is empty (which it ** should be, since restore() was short-circuited). ** - ** Fifth, you might clear() the CDMap. This does exactly the - ** same as CDMap::~CDMap(), except that it doesn't call destroy() + ** Fifth, you might clear() the CDHashMap. This does exactly the + ** same as CDHashMap::~CDHashMap(), except that it doesn't call destroy() ** on itself. ** - ** CDMap::emptyTrash() simply goes through and calls + ** CDHashMap::emptyTrash() simply goes through and calls ** ->deleteSelf() on all elements in the trash. ** ContextObj::deleteSelf() calls the CDOhash_map destructor, then ** frees the memory associated to the CDOhash_map. CDOhash_map::~CDOhash_map() @@ -87,8 +92,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__CONTEXT__CDMAP_H -#define __CVC4__CONTEXT__CDMAP_H +#ifndef __CVC4__CONTEXT__CDHASHMAP_H +#define __CVC4__CONTEXT__CDHASHMAP_H #include #include @@ -148,9 +153,9 @@ class CDOhash_map : public ContextObj { d_next->d_prev = d_prev; d_prev->d_next = d_next; if(d_noTrash) { - Debug("gc") << "CDMap<> no-trash " << this << std::endl; + Debug("gc") << "CDHashMap<> no-trash " << this << std::endl; } else { - Debug("gc") << "CDMap<> trash push_back " << this << std::endl; + Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl; //this->deleteSelf(); d_map->d_trash.push_back(this); } @@ -190,7 +195,7 @@ public: // "Initializing" map insertion: this entry will never be // removed from the map, it's inserted at level 0 as an // "initializing" element. See - // CDMap<>::insertAtContextLevelZero(). + // CDHashMap<>::insertAtContextLevelZero(). d_data = data; } else { // Normal map insertion: first makeCurrent(), then set the data @@ -417,7 +422,7 @@ public: } /** - * Version of insert() for CDMap<> that inserts data value d at + * Version of insert() for CDHashMap<> that inserts data value d at * context level zero. This is a special escape hatch for inserting * "initializing" data into the map. Imagine something happens at a * deep context level L that causes insertion into a map, such that @@ -538,7 +543,7 @@ public: const std::pair& operator*() const { return *d_pair; } - };/* class CDMap<>::iterator::Proxy */ + };/* class CDHashMap<>::iterator::Proxy */ // Actual postfix increment: returns Proxy with the old value. // Now, an expression like *i++ will return the current *i, and @@ -549,7 +554,7 @@ public: ++(*this); return e; } - };/* class CDMap<>::iterator */ + };/* class CDHashMap<>::iterator */ typedef iterator const_iterator; @@ -576,9 +581,9 @@ public: return const_cast(this)->find(k); } -};/* class CDMap<> */ +};/* class CDHashMap<> */ }/* CVC4::context namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__CONTEXT__CDMAP_H */ +#endif /* __CVC4__CONTEXT__CDHashMAP_H */ diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h index d81f5345d..60291af07 100644 --- a/src/context/cdhashmap_forward.h +++ b/src/context/cdhashmap_forward.h @@ -9,22 +9,22 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief This is a forward declaration header to declare the CDMap<> + ** \brief This is a forward declaration header to declare the CDHashMap<> ** template ** - ** This is a forward declaration header to declare the CDMap<> - ** template. It's useful if you want to forward-declare CDMap<> - ** without including the full cdmap.h header, for example, in a + ** This is a forward declaration header to declare the CDHashMap<> + ** template. It's useful if you want to forward-declare CDHashMap<> + ** without including the full cdhashmap.h header, for example, in a ** public header context. ** - ** For CDMap<> in particular, it's difficult to forward-declare it + ** For CDHashMap<> in particular, it's difficult to forward-declare it ** yourself, because it has a default template argument. **/ #include "cvc4_public.h" -#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H -#define __CVC4__CONTEXT__CDMAP_FORWARD_H +#ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H +#define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H /// \cond internals @@ -41,4 +41,4 @@ namespace CVC4 { /// \endcond -#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */ +#endif /* __CVC4__CONTEXT__CDHASHMAP_FORWARD_H */ diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index e885b7729..d7957cf3f 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -20,16 +20,15 @@ #define __CVC4__CONTEXT__CDSET_H #include "context/context.h" -#include "context/cdhashset_forward.h" -#include "context/cdhashmap.h" +#include "context/cdinsert_hashmap.h" #include "util/cvc4_assert.h" namespace CVC4 { namespace context { template -class CDHashSet : protected CDHashMap { - typedef CDHashMap super; +class CDHashSet : protected CDInsertHashMap { + typedef CDInsertHashMap super; public: @@ -58,40 +57,30 @@ public: return super::size(); } - size_t count(const V& v) const { - return super::count(v); - } - bool insert(const V& v) { - return super::insert(v, v); - } - - void insertAtContextLevelZero(const V& v) { - return super::insertAtContextLevelZero(v, v); + return super::insert_safe(v, true); } bool contains(const V& v) { - return find(v) != end(); + return super::contains(v); } - // FIXME: no erase(), too much hassle to implement efficiently... - - class iterator { - typename super::iterator d_it; + class const_iterator { + typename super::const_iterator d_it; public: - iterator(const typename super::iterator& it) : d_it(it) {} - iterator(const iterator& it) : d_it(it.d_it) {} + const_iterator(const typename super::const_iterator& it) : d_it(it) {} + const_iterator(const const_iterator& it) : d_it(it.d_it) {} // Default constructor - iterator() {} + const_iterator() {} // (Dis)equality - bool operator==(const iterator& i) const { + bool operator==(const const_iterator& i) const { return d_it == i.d_it; } - bool operator!=(const iterator& i) const { + bool operator!=(const const_iterator& i) const { return d_it != i.d_it; } @@ -101,7 +90,7 @@ public: } // Prefix increment - iterator& operator++() { + const_iterator& operator++() { ++d_it; return *this; } @@ -131,18 +120,28 @@ public: } };/* class CDSet<>::iterator */ - typedef iterator const_iterator; - const_iterator begin() const { - return iterator(super::begin()); + return const_iterator(super::begin()); } const_iterator end() const { - return iterator(super::end()); + return const_iterator(super::end()); } const_iterator find(const V& v) const { - return iterator(super::find(v)); + return const_iterator(super::find(v)); + } + + typedef typename super::key_iterator key_iterator; + key_iterator key_begin() const { + return super::key_begin(); + } + key_iterator key_end() const { + return super::key_end(); + } + + void insertAtContextLevelZero(const V& v) { + return super::insertAtContextLevelZero(v, true); } };/* class CDSet */ diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h new file mode 100644 index 000000000..0c84eda80 --- /dev/null +++ b/src/context/cdinsert_hashmap.h @@ -0,0 +1,402 @@ +/********************* */ +/*! \file cdinsert_hashmap.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-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Context-dependent insert only hashmap built using trail of edits + ** + ** Context-dependent hashmap that only allows for one insertion per element. + ** This can be viewed as a highly restricted version of CDHashMap. + ** It is significantly lighter in memory usage than CDHashMap. + ** + ** See also: + ** CDTrailHashMap : A lightweight CD hash map with poor iteration + ** characteristics and some quirks in usage. + ** CDHashMap : A fully featured CD hash map. (The closest to ) + ** + ** Notes: + ** - To iterate efficiently over the elements use the key_iterators. + ** - operator[] is only supported as a const derefence (must succeed). + ** - insert(k) must always work. + ** - Use insert_safe if you want to check if the element has been inserted + ** and only insert if it has not yet been. + ** - Does not accept TNodes as keys. + ** - Supports insertAtContextLevelZero() if the element is not in the map. + **/ + + +#include "cvc4_private.h" + +#include "context/context.h" +#include "context/cdinsert_hashmap_forward.h" +#include +#include +#include +#include "util/cvc4_assert.h" +#include "util/output.h" + +#include "expr/node.h" +#include + +#pragma once + +namespace CVC4 { +namespace context { + + +template > +class InsertHashMap { +private: + typedef std::deque KeyVec; + /** A list of the keys in the map maintained as a stack. */ + KeyVec d_keys; + + typedef __gnu_cxx::hash_map HashMap; + /** The hash_map used for element lookup. */ + HashMap d_hashMap; + +public: + /** + * An iterator over a list of keys. + * Use this to efficiently iterate over the elements. + * (See std::deque<>::iterator). + */ + typedef typename KeyVec::const_iterator key_iterator; + + /**An iterator over the elements in the hash_map. */ + typedef typename HashMap::const_iterator const_iterator; + + + /** + * Returns an iterator to the begining of the HashMap. + * Acts like a hash_map::const_iterator. + */ + const_iterator begin() const{ + return d_hashMap.begin(); + } + /** + * Returns an iterator to the end of the HashMap. + * Acts like a hash_map::const_iterator. + */ + const_iterator end() const{ + return d_hashMap.end(); + } + + /** + * Returns an iterator to the Key k of the map. + * See hash_map::find() + */ + const_iterator find(const Key& k) const{ + return d_hashMap.find(k); + } + + /** Returns an iterator to the start of the set of keys. */ + key_iterator key_begin() const{ + return d_keys.begin(); + } + /** Returns an iterator to the end of the set of keys. */ + key_iterator key_end() const{ + return d_keys.end(); + } + + /** Returns true if the map is empty. */ + bool empty() const { return d_keys.empty(); } + /** Returns the number of elements in the map. */ + size_t size() const { return d_keys.size(); } + + /** Returns true if k is a mapped key. */ + bool contains(const Key& k) const { + return find(k) != end(); + } + + /** + * Returns a reference the data mapped by k. + * This must succeed. + */ + const Data& operator[](const Key& k) const { + const_iterator ci = find(k); + Assert(ci != end()); + return (*ci).second; + } + + /** + * Inserts an element into the map, and pushes its key to the front + * of the stack. The key inserted must be not be currently mapped. + */ + void push_front(const Key& k, const Data& d){ + Assert(!contains(k)); + d_hashMap.insert(std::make_pair(k, d)); + d_keys.push_front(k); + } + + /** + * Inserts an element into the map, and pushes its key onto the + * back on the stack. The key inserted must be not be currently mapped. + */ + void push_back(const Key& k, const Data& d){ + Assert(!contains(k)); + d_hashMap.insert(std::make_pair(k, d)); + d_keys.push_back(k); + } + + /** + * Pops the key at the front of the list off and removes its key from the map. + */ + void pop_front(){ + Assert(!empty()); + const Key& front = d_keys.front(); + d_hashMap.erase(front); + + Debug("TrailHashMap") <<"TrailHashMap pop_front " << size() << std::endl; + d_keys.pop_front(); + } + + /** + * Pops the key at the back of the stack off and removes its key from the map. + */ + void pop_back(){ + Assert(!empty()); + const Key& back = d_keys.back(); + d_hashMap.erase(back); + + Debug("TrailHashMap") <<"TrailHashMap pop_back " << size() << std::endl; + d_keys.pop_back(); + } + + /** + * Pops the back of the stack until the size is below s. + */ + void pop_to_size(size_t s){ + while(size() > s){ + pop_back(); + } + } +};/* class TrailHashMap<> */ + +template +class CDInsertHashMap : public ContextObj { +private: + typedef InsertHashMap IHM; + + /** An InsertHashMap that backs all of the data. */ + IHM* d_insertMap; + + /** For restores, we need to keep track of the previous size. */ + size_t d_size; + + /** + * To support insertAtContextLevelZero() and restores, + * we have called d_insertMap->d_pushFront(). + */ + size_t d_pushFronts; + + /** + * Private copy constructor used only by save(). d_insertMap is + * not copied: only the base class information and + * d_size and d_pushFronts are needed in restore. + */ + CDInsertHashMap(const CDInsertHashMap& l) : + ContextObj(l), + d_insertMap(NULL), + d_size(l.d_size), + d_pushFronts(l.d_pushFronts) + { + Debug("CDInsertHashMap") << "copy ctor: " << this + << " from " << &l + << " size " << d_size << std::endl; + } + + /** + * Implementation of mandatory ContextObj method save: simply copies + * the current size information to a copy using the copy constructor (the + * pointer and the allocated size are *not* copied as they are not + * restored on a pop). The saved information is allocated using the + * ContextMemoryManager. + */ + ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* data = new(pCMM) CDInsertHashMap(*this); + Debug("CDInsertHashMap") << "save " << this + << " at level " << this->getContext()->getLevel() + << " size at " << this->d_size + << " d_list is " << this->d_insertMap + << " data:" << data << std::endl; + return data; + } +protected: + /** + * Implementation of mandatory ContextObj method restore: + * restore to the previous size taking into account the number + * of new pushFront calls have happened since saving. + * The d_insertMap is untouched and d_pushFronts is also kept. + */ + void restore(ContextObj* data) { + Debug("CDInsertHashMap") << "restore " << this + << " level " << this->getContext()->getLevel() + << " data == " << data + << " d_insertMap == " << this->d_insertMap << std::endl; + size_t oldSize = ((CDInsertHashMap*)data)->d_size; + size_t oldPushFronts = ((CDInsertHashMap*)data)->d_pushFronts; + Assert(oldPushFronts <= d_pushFronts); + + // The size to restore to. + size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts); + d_insertMap->pop_to_size(restoreSize); + d_size = restoreSize; + Assert(d_insertMap->size() == d_size); + Debug("CDInsertHashMap") << "restore " << this + << " level " << this->getContext()->getLevel() + << " size back to " << this->d_size << std::endl; + } +public: + + /** + * Main constructor: d_insertMap starts as an empty map, with the size is 0 + */ + CDInsertHashMap(Context* context) : + ContextObj(context), + d_insertMap(new IHM()), + d_size(0), + d_pushFronts(0){ + Assert(d_insertMap->size() == d_size); + } + + /** + * Destructor: delete the d_insertMap + */ + ~CDInsertHashMap() throw(AssertionException) { + this->destroy(); + delete d_insertMap; + } + + /** An iterator over the elements in the hash_map. */ + typedef typename IHM::const_iterator const_iterator; + + /** + * An iterator over a list of keys. + * Use this to efficiently iterate over the elements. + * (See std::deque<>::iterator). + */ + typedef typename IHM::key_iterator key_iterator; + + /** Returns true if the map is empty in the current context. */ + bool empty() const{ + return d_size == 0; + } + + /** Returns true the size of the map in the current context. */ + size_t size() const { + return d_size; + } + + /** + * Inserts an element into the map. + * The key inserted must be not be currently mapped. + * This is implemented using d_insertMap.push_back(). + */ + void insert(const Key& k, const Data& d){ + makeCurrent(); + ++d_size; + d_insertMap->push_back(k, d); + Assert(d_insertMap->size() == d_size); + } + + /** + * Checks if the key k is mapped already. + * If it is, this returns false. + * Otherwise it is inserted and this returns true. + */ + bool insert_safe(const Key& k, const Data& d){ + if(contains(k)){ + return false; + }else{ + insert(k,d); + return true; + } + } + + /** + * Version of insert() for CDMap<> that inserts data value d at + * context level zero. + * + * It is an error to insertAtContextLevelZero() + * a key that already is in the map. + */ + void insertAtContextLevelZero(const Key& k, const Data& d){ + makeCurrent(); + ++d_size; + ++d_pushFronts; + d_insertMap->push_front(k, d); + } + + /** Returns true if k is a mapped key in the context. */ + bool contains(const Key& k) const { + return d_insertMap->contains(k); + } + + /** + * Returns a reference the data mapped by k. + * k must be in the map in this context. + */ + const Data& operator[](const Key& k) const { + return (*d_insertMap)[k]; + } + + /** + * Returns a const_iterator to the value_type if k is a mapped key in + * the context. + */ + const_iterator find(const Key& k) const { + return d_insertMap->find(k); + } + + /** + * Returns an iterator to the begining of the map. + * Acts like a hash_map::const_iterator. + */ + const_iterator begin() const{ + return d_insertMap->begin(); + } + + /** + * Returns an iterator to the end of the map. + * Acts like a hash_map::const_iterator. + */ + const_iterator end() const{ + return d_insertMap->end(); + } + + /** Returns an iterator to the start of the set of keys. */ + key_iterator key_begin() const{ + return d_insertMap->key_begin(); + } + /** Returns an iterator to the end of the set of keys. */ + key_iterator key_end() const{ + return d_insertMap->key_end(); + } +};/* class CDInsertHashMap<> */ + + +template +class CDInsertHashMap : public ContextObj { + /* CDInsertHashMap is challenging to get working with TNode. + * Consider using CDHashMap instead. + * + * Explanation: + * CDInsertHashMap uses keys for deallocation. + * If the key is a TNode and the backing (the hard node reference) + * for the key in another data structure removes the key at the same context + * the ref count could drop to 0. The key would then not be eligible to be + * hashed. Getting the order right with a guarentee is to hard. + */ + + BOOST_STATIC_ASSERT(sizeof(Data) == 0); +}; + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ diff --git a/src/context/cdinsert_hashmap_forward.h b/src/context/cdinsert_hashmap_forward.h new file mode 100644 index 000000000..638607840 --- /dev/null +++ b/src/context/cdinsert_hashmap_forward.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file cdinsert_hashmap_forward.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-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a forward declaration header to declare the CDInsertHashMap<> + ** template + ** + ** This is a forward declaration header to declare the CDInsertHashMap<> + ** template. It's useful if you want to forward-declare CDInsertHashMap<> + ** without including the full cdinsert_hashmap.h header, for example, in a + ** public header context. + ** + ** For CDInsertHashMap<> in particular, it's difficult to forward-declare it + ** yourself, because it has a default template argument. + **/ + +#include "cvc4_public.h" + +#pragma once + +namespace __gnu_cxx { + template struct hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template > + class CDInsertHashMap; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h new file mode 100644 index 000000000..5f090341d --- /dev/null +++ b/src/context/cdtrail_hashmap.h @@ -0,0 +1,571 @@ +/********************* */ +/*! \file cdtrail_hashmap.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-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Context-dependent hashmap built using trail of elements + ** + ** Context-dependent hashmap that explicitly keeps track of its edit history. + ** This is similar in functionality to CDHashMap with fewer capabilites and + ** slight changes in the interface. It has the advantage of being lighter in + ** memory usage. + ** + ** See also: + ** CDInsertHashMap : An "insert-once" CD hash map. + ** CDHashMap : A fully featured CD hash map. (The closest to ) + ** + ** Notes: + ** - To iterate efficiently over the elements use the key_iterators. + ** - operator[] is only supported as a const derefence (must succeed). + ** - Insertions to the map are done with respect to a context. + ** - Insertions can be done in two manors either with insert() or + ** insert_no_overwrite(). + ** - insert(k,d) inserts the key data pair into the hashtable and returns a + ** false if it overwrote the previous value. + ** - insert_no_overwrite(k,d) inserts key data pair into the hashtable only + ** if the value is not already there. It returns true, if an element was + ** added. This conditionally extends the trail length if it returns true. + ** - inserts are compacting. If there is another insert to the same key + ** at the same context, the memory is reused. + ** - Iterating over const_iterators has amortized time proportional to + ** O(trail length). (If this needs to be improved, please bug Tim.) + ** - contains() and operator[] are slightly faster than using stl style + ** iterator comparisons: find(), end(), etc. + **/ + + +#include "cvc4_private.h" + +#pragma once + +#include "context/context.h" +#include "context/cdtrail_hashmap_forward.h" +#include +#include +#include +#include "util/cvc4_assert.h" +#include "util/output.h" + +#include "expr/node.h" +#include + + +namespace CVC4 { +namespace context { + + +template > +class TrailHashMap { +public: + /** A pair of Key and Data that mirrors hash_map::value_type. */ + typedef std::pair value_type; + +private: + + /** The trail information from an insert. */ + struct KDT { + /** The Key Data pair. */ + value_type d_kd; + + /** + * The previous trail entry with the same key. + * On a pop, this is the element to revert to. + * This value is a self loop if there is no previous entry. + */ + size_t d_prevKey; + + /** The whether the trail element is current. */ + bool d_current; + + KDT(const Key& key, const Data& data, size_t prev, bool cur = true): + d_kd(std::make_pair(key, data)), d_prevKey(prev), d_current(cur){ } + KDT(){} + }; + + typedef std::deque KDTVec; + typedef typename KDTVec::const_iterator KDTVec_const_iterator; + /** The trail of elements. */ + KDTVec d_kdts; + + + typedef __gnu_cxx::hash_map PositionMap; + typedef typename PositionMap::iterator PM_iterator; + typedef typename PositionMap::const_iterator PM_const_iterator; + + /** A map of keys to their positions in the trail. */ + PositionMap d_posMap; + + + /** The number of unique keys in the map. */ + size_t d_uniqueKeys; + + /** Internal utility class. NonConstant find on the position map.*/ + inline PM_iterator ncfind(const Key& k) { + return d_posMap.find(k); + } + + /** Internal utility class. Position Map Find.*/ + inline PM_const_iterator pmfind(const Key& k) const{ + return d_posMap.find(k); + } + /** Internal utility class. Position Map End.*/ + inline PM_const_iterator pmend() const{ + return d_posMap.end(); + } + + /** This is true if the previous entry in the trail points at itself.*/ + inline bool selfLoop(size_t pos, const KDT& kdt) const { + return pos == kdt.d_prevKey; + } + +public: + /** + * Constant iterator for TrailHashMap. + * Only supports forward iteration. + * This always points at the end or a current element in the trail. + * This is done by iterating over the trail. + */ + class const_iterator { + private: + /** A vector iterator. */ + KDTVec_const_iterator d_it; + + /** A pointer to the end of the vector.*/ + KDTVec_const_iterator d_end; + + /** Move the iterator to the end or the next current element.*/ + void findCurrent(){ + while(d_it != d_end && !(*d_it).d_current){ + ++d_it; + } + } + + public: + + /** Constructs an iterator for a TrailHashMap. */ + const_iterator(KDTVec_const_iterator it, KDTVec_const_iterator end) : + d_it(it), + d_end(end){ + findCurrent(); + } + + /** Copy constructor for an iterator for a TrailHashMap. */ + const_iterator(const const_iterator& other) : + d_it(other.d_it), d_end(other.d_end){ + // Do not need to findCurrent() + } + + /** Returns true if the iterators are the same. */ + inline bool operator==(const const_iterator& other) const { + return d_it == other.d_it; + } + + /** Returns true if the iterators are the same. */ + inline bool operator!=(const const_iterator& other) const { + return d_it != other.d_it; + } + + /** Returns a pair. */ + inline const value_type& operator*() const { + return (*d_it).d_kd; + } + + /** Prefix increment */ + const_iterator& operator++() { + ++d_it; + findCurrent(); + return *this; + } + }; + + /** Returns a beginning iterator.*/ + inline const_iterator begin() const{ + return const_iterator(d_kdts.begin(), d_kdts.end()); + } + + /** Returns an end iterator.*/ + inline const_iterator end() const{ + return const_iterator(d_kdts.end(), d_kdts.end()); + } + + /** Returns true if the trail is empty.*/ + inline bool empty() const { return d_kdts.empty(); } + + /** Returns the size of the trail.*/ + inline size_t trailSize() const { return d_kdts.size(); } + + /** Returns the number of unique keys in the map.*/ + inline size_t uniqueKeys() const { return d_uniqueKeys; } + + /** Returns true if the key is in the map.*/ + inline bool contains(const Key& k) const { + return pmfind(k) != pmend(); + } + + /** + * Returns a NON const reference to an element in the Map. + * k must be a key in the Map. + * DO NOT USE THIS UNLESS YOU ARE CONFIDENT THE CHANGES MAKE SENSE. + */ + Data& lookup(const Key& k){ + Assert(contains(k)); + PM_iterator ci = ncfind(k); + KDT& kdt = d_kdts[(*ci).second]; + return kdt.d_kd.second; + } + + /** + * Returns a const reference to an element mapped by a Key k. + * k must be a key in the Map. + */ + const Data& operator[](const Key& k) const { + PM_const_iterator pci = pmfind(k); + Assert(pci != pmend()); + return d_kdts[(*pci).second].d_kd.second; + } + + /** + * If the key k is in the map, this returns a const_iterator pointing at this + * element. Otherwise, this returns end(). + */ + const_iterator find(const Key& k) const { + PM_const_iterator pci = pmfind(k); + if(pci == pmend()){ + return end(); + }else{ + size_t pos = (*pci).second; + return const_iterator(d_kdts.begin() + pos, d_kdts.end()); + } + } + + /** + * Similar to contains, but includes a notion of trail position. + * Returns if contains(k) and the current position of k + * in the map is greater than or equal to pos. + * Returns if it contains(k) but not the previous condition. + * Returns if it does not contains(k). + */ + std::pair hasAfter(const Key& k, size_t pos) { + PM_iterator it = ncfind(k); + if(it != d_posMap.end()){ + return std::make_pair(true, (*it).second >= pos ); + } + return std::make_pair(false, false); + } + + /** + * Inserts an element unconditionally. + * Always increases the trail size. + * Returns true if the key count increased. + */ + bool push_back(const Key& k, const Data& d){ + std::pair res = compacting_push_back(k, d, trailSize()); + return res.first; + } + + /** + * This inserts an element into the trail. + * This insert can reuse the same trail element if the postion of the element + * is >= threshold. + * + * Return values: + * If pair res = compacting_push_back(..), + * then res.first is true if this is a new unique key, and + * res.second is true if the trail length increased. + * + */ + std::pair compacting_push_back(const Key& k, const Data& d, size_t threshold){ + size_t backPos = d_kdts.size(); + std::pair res = d_posMap.insert(std::make_pair(k, backPos)); + if(!res.second){ + size_t& prevPosInPM = (*res.first).second; + + Assert(d_kdts[prevPosInPM].d_current); + + if(prevPosInPM < threshold){ + d_kdts.push_back(KDT(k,d, prevPosInPM)); + d_kdts[prevPosInPM].d_current = false; + prevPosInPM = backPos; + + return std::make_pair(false, true); + }else{ + d_kdts[prevPosInPM].d_kd.second = d; + return std::make_pair(false, false); + } + }else{ + d_kdts.push_back(KDT(k,d, backPos)); + ++d_uniqueKeys; + return std::make_pair(true, true); + } + } + + /** + * Inserts an element if the key is not already in the map. + * Returns true if the element was inserted. + */ + bool insert_no_overwrite(const Key& k, const Data& d){ + size_t backPos = d_kdts.size(); + std::pair res = d_posMap.insert(std::make_pair(k, backPos)); + if(res.second){ + d_kdts.push_back(KDT(k,d, backPos)); + ++d_uniqueKeys; + } + Debug("TrailHashMap") <<"TrailHashMap insert" << k << " d " << d << " " << backPos << std::endl; + return res.second; + } + + /** Pops the element at the back of the trail. */ + void pop_back(){ + Assert(!empty()); + const KDT& back = d_kdts.back(); + const Key& k = back.d_kd.first; + if(selfLoop(trailSize()-1, back)){ + d_posMap.erase(k); + --d_uniqueKeys; + Debug("TrailHashMap") <<"TrailHashMap pop_back erase " << trailSize() <<" " << std::endl; + + }else{ + Debug("TrailHashMap") <<"TrailHashMap reset " << trailSize() <<" " << " " << back.d_prevKey << std::endl; + d_posMap[k] = back.d_prevKey; + d_kdts[back.d_prevKey].d_current = true; + } + d_kdts.pop_back(); + } + + /** Pops the element at the back of the trail until the trailSize is <= s. */ + void pop_to_size(size_t s){ + while(trailSize() > s){ + pop_back(); + } + } +};/* class TrailHashMap<> */ + +template +class CDTrailHashMap : public ContextObj { +private: + /** A short name for the templatized TrailMap that backs the CDTrailMap. */ + typedef TrailHashMap THM; + + /** The trail map that backs the CDTrailMap. */ + THM* d_trailMap; +public: + /** Iterator for the CDTrailHashMap. */ + typedef typename THM::const_iterator const_iterator; + + /** Return value of operator* on a const_iterator (pair).*/ + typedef typename THM::value_type value_type; + +private: + /** + * The length of the trail in the current context. + * This is used to support reverting. + */ + size_t d_trailSize; + + /** + * The length of the trail immediately after the previous makeCurrent(). + * This is used to support compacting inserts. + */ + size_t d_prevTrailSize; + + /** + * Private copy constructor used only by save(). d_trailMap is not copied: + * only the base class information, d_trailSize, and d_prevTrailSize + * are needed in restore. + */ + CDTrailHashMap(const CDTrailHashMap& l) : + ContextObj(l), + d_trailMap(NULL), + d_trailSize(l.d_trailSize), + d_prevTrailSize(l.d_prevTrailSize){ + Debug("CDTrailHashMap") << "copy ctor: " << this + << " from " << &l + << " size " << d_trailSize << std::endl; + } + + /** + * Implementation of mandatory ContextObj method save: simply copies + * the current sizes to a copy using the copy constructor, + * The saved information is allocated using the ContextMemoryManager. + */ + ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* data = new(pCMM) CDTrailHashMap(*this); + Debug("CDTrailHashMap") << "save " << this + << " at level " << this->getContext()->getLevel() + << " size at " << this->d_trailSize + << " d_list is " << this->d_trailMap + << " data:" << data << std::endl; + return data; + } +protected: + /** + * Implementation of mandatory ContextObj method restore: simply + * restores the previous size. Note that the list pointer and the + * allocated size are not changed. + */ + void restore(ContextObj* data) { + Debug("CDTrailHashMap") << "restore " << this + << " level " << this->getContext()->getLevel() + << " data == " << data + << " d_trailMap == " << this->d_trailMap << std::endl; + size_t oldSize = ((CDTrailHashMap*)data)->d_trailSize; + d_trailMap->pop_to_size(oldSize); + d_trailSize = oldSize; + Assert(d_trailMap->trailSize() == d_trailSize); + + d_prevTrailSize = ((CDTrailHashMap*)data)->d_prevTrailSize; + Debug("CDTrailHashMap") << "restore " << this + << " level " << this->getContext()->getLevel() + << " size back to " << this->d_trailSize << std::endl; + } + + /** + * We need to save the d_trailSize immediately after a successful makeCurrent. + * So this version needs to be used everywhere instead of maekCurrent() + * internally. + */ + void internalMakeCurrent () { + if(!isCurrent()){ + makeCurrent(); + d_prevTrailSize = d_trailSize; + } + } + +public: + + /** + * Main constructor: d_trailMap starts as an empty map, with the sizes are 0 + */ + CDTrailHashMap(Context* context) : + ContextObj(context), + d_trailMap(new THM()), + d_trailSize(0), + d_prevTrailSize(0){ + Assert(d_trailMap->trailSize() == d_trailSize); + } + + /** + * Destructor: delete the map + */ + ~CDTrailHashMap() throw(AssertionException) { + this->destroy(); + delete d_trailMap; + } + + /** Returns true if the map is empty in the current context. */ + bool empty() const{ + return d_trailSize == 0; + } + + /** Returns true the size of the map in the current context. */ + size_t size() const { + return d_trailMap->uniqueKeys(); + } + + /** + * Inserts an element into the map. + * This always succeeds. + * Returns true if the key is new. + */ + bool insert(const Key& k, const Data& d){ + internalMakeCurrent(); + std::pair res = d_trailMap->compacting_push_back(k, d, d_prevTrailSize); + if(res.second){ + ++d_trailSize; + } + Assert(d_trailMap->trailSize() == d_trailSize); + return res.first; + } + + /** + * Inserts an element into the map if the key is not already there. + * This has no side effects if the insert does not happen. + * Returns true if the element was inserted. + */ + bool insert_no_overwrite(const Key& k, const Data& d){ + bool res = d_trailMap->insert_no_overwrite(k, d); + if(res){ + internalMakeCurrent(); + ++d_trailSize; + } + Assert(d_trailMap->trailSize() == d_trailSize); + return res; + } + + /** Returns true if k is a mapped key in the context. */ + bool contains(const Key& k) const { + return d_trailMap->contains(k); + } + + /** + * Returns a reference the data mapped by k. + * k must be in the map in this context. + */ + const Data& operator[](const Key& k) const { + return (*d_trailMap)[k]; + } + /* +// While the following code "works", I wonder if it is not better to disable it? +// Non-const operator[] has strange semantics for a context-dependent +// data structure. + Data& operator[](const Key& k) { + internalMakeCurrent(); + std::pair res = d_trailMap->hasAfter(k, d_prevTrailSize); + if(!res.first){ + std::pair res = d_trailMap->compacting_push_back(k, Data(), d_prevTrailSize); + if(res.second){ + ++d_trailSize; + } + }else if(!res.second){ + std::pair res = d_trailMap->compacting_push_back(k, (*d_trailMap)[k], d_prevTrailSize); + if(res.second){ + ++d_trailSize; + } + } + return d_trailMap->lookup(k); + } + */ + + /** + * Returns a const_iterator to the value_type if k is a mapped key in + * the context. + */ + const_iterator find(const Key& k) const { + return d_trailMap->find(k); + } + + /** Returns an iterator to the begining of the map. */ + const_iterator begin() const{ + return d_trailMap->begin(); + } + /** Returns an iterator to the end of the map. */ + const_iterator end() const{ + return d_trailMap->end(); + } + +};/* class CDTrailHashMap<> */ + +template +class CDTrailHashMap : public ContextObj { + /* CDTrailHashMap is challenging to get working with TNode. + * Consider using CDHashMap instead. + * + * Explanation: + * CDTrailHashMap uses keys during deallocation. + * If the key is a TNode and the backing (the hard node reference) + * for the key in another data structure removes the key at the same context + * the ref count could drop to 0. The key would then not be eligible to be + * hashed. Getting the order right with a guarentee is to hard. + */ + + BOOST_STATIC_ASSERT(sizeof(Data) == 0); +}; + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ diff --git a/src/context/cdtrail_hashmap_forward.h b/src/context/cdtrail_hashmap_forward.h new file mode 100644 index 000000000..549ecd738 --- /dev/null +++ b/src/context/cdtrail_hashmap_forward.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file cdtrail_hashmap_forward.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-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a forward declaration header to declare the + ** CDTrailHashMap<> template + ** + ** This is a forward declaration header to declare the CDTrailHashMap<> + ** template. It's useful if you want to forward-declare CDTrailHashMap<> + ** without including the full cdtrail_hash_map.h header, for example, in a + ** public header context. + ** + ** For CDTrailHashMap<> in particular, it's difficult to forward-declare it + ** yourself, because it has a default template argument. + **/ + +#include "cvc4_public.h" + +#pragma once + +namespace __gnu_cxx { + template struct hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template > + class CDTrailHashMap; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index adccc0d55..a1b29ed47 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -49,7 +49,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { typedef context::CDHashMap SkolemMap; // being 'justified' is monotonic with respect to decisions - typedef context::CDHashSet JustifiedSet; + typedef context::CDHashSet JustifiedSet; JustifiedSet d_justified; context::CDO d_prvsIndex; @@ -107,8 +107,8 @@ public: d_visited.clear(); if(Trace.isOn("justified")) { - for(JustifiedSet::iterator i = d_justified.begin(); - i != d_justified.end(); ++i) { + for(JustifiedSet::key_iterator i = d_justified.key_begin(); + i != d_justified.key_end(); ++i) { TNode n = *i; SatLiteral l = d_decisionEngine->hasSatLiteral(n) ? d_decisionEngine->getSatLiteral(n) : -1; diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h index 8a6eb54ef..bfd30ddde 100644 --- a/src/decision/relevancy.h +++ b/src/decision/relevancy.h @@ -60,7 +60,7 @@ class Relevancy : public RelevancyStrategy { typedef hash_map PolarityCache; // being 'justified' is monotonic with respect to decisions - context::CDHashSet d_justified; + context::CDHashSet d_justified; context::CDO d_prvsIndex; IntStat d_helfulness; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9f2138e9d..89cd731e9 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -108,11 +108,10 @@ void TseitinCnfStream::ensureLiteral(TNode n) { Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { SatLiteral lit = getLiteral(n); - LiteralToNodeMap::iterator i = d_literalToNodeMap.find(lit); - if(i == d_literalToNodeMap.end()) { + if(!d_literalToNodeMap.contains(lit)){ // Store backward-mappings - d_literalToNodeMap[lit] = n; - d_literalToNodeMap[~lit] = n.notNode(); + d_literalToNodeMap.insert(lit, n); + d_literalToNodeMap.insert(~lit, n.notNode()); } return; } @@ -140,8 +139,9 @@ void TseitinCnfStream::ensureLiteral(TNode n) { lit = toCNF(n, false); // Store backward-mappings - d_literalToNodeMap[lit] = n; - d_literalToNodeMap[~lit] = n.notNode(); + // These may already exist + d_literalToNodeMap.insert_safe(lit, n); + d_literalToNodeMap.insert_safe(~lit, n.notNode()); } else { // We have a theory atom or variable. lit = convertAtom(n); @@ -168,8 +168,8 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { } else { lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); } - d_nodeToLiteralMap[node] = lit; - d_nodeToLiteralMap[node.notNode()] = ~lit; + d_nodeToLiteralMap.insert(node, lit); + d_nodeToLiteralMap.insert(node.notNode(), ~lit); } else { lit = getLiteral(node); } @@ -178,8 +178,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { if ( theoryLiteral || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && options::replayLog() != NULL ) || (Dump.isOn("clauses")) ) { - d_literalToNodeMap[lit] = node; - d_literalToNodeMap[~lit] = node.notNode(); + + d_literalToNodeMap.insert_safe(lit, node); + d_literalToNodeMap.insert_safe(~lit, node.notNode()); } // If a theory literal, we pre-register it @@ -197,11 +198,8 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { TNode CnfStream::getNode(const SatLiteral& literal) { Debug("cnf") << "getNode(" << literal << ")" << endl; - LiteralToNodeMap::iterator find = d_literalToNodeMap.find(literal); - Assert(find != d_literalToNodeMap.end()); - Assert(d_nodeToLiteralMap.find((*find).second) != d_nodeToLiteralMap.end()); - Debug("cnf") << "getNode(" << literal << ") => " << (*find).second << endl; - return (*find).second; + Debug("cnf") << "getNode(" << literal << ") => " << d_literalToNodeMap[literal] << endl; + return d_literalToNodeMap[literal]; } void CnfStream::getBooleanVariables(std::vector& outputVariables) const { @@ -229,10 +227,9 @@ SatLiteral CnfStream::convertAtom(TNode node) { } SatLiteral CnfStream::getLiteral(TNode node) { - NodeToLiteralMap::iterator find = d_nodeToLiteralMap.find(node); Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node"); - Assert(find != d_nodeToLiteralMap.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); - SatLiteral literal = (*find).second; + Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); + SatLiteral literal = d_nodeToLiteralMap[node]; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 6ab639712..042cccd56 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -29,6 +29,7 @@ #include "prop/theory_proxy.h" #include "prop/registrar.h" #include "context/cdlist.h" +#include "context/cdinsert_hashmap.h" #include @@ -47,10 +48,10 @@ class CnfStream { public: /** Cache of what nodes have been registered to a literal. */ - typedef context::CDHashMap LiteralToNodeMap; + typedef context::CDInsertHashMap LiteralToNodeMap; /** Cache of what literals have been registered to a node. */ - typedef context::CDHashMap NodeToLiteralMap; + typedef context::CDInsertHashMap NodeToLiteralMap; protected: diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 5b8d3befc..9ae7cd1c2 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -145,8 +145,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet break; case CONST_RATIONAL: // Mark constants as minmax - d_minMap[n] = n.getConst(); - d_maxMap[n] = n.getConst(); + d_minMap.insert(n, n.getConst()); + d_maxMap.insert(n, n.getConst()); break; case OR: { // Look for things like "x = 0 OR x = 1" (that are defTrue) and @@ -248,7 +248,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ DeltaRational min = std::min(first, second); CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n); if (minFind == d_minMap.end() || (*minFind).second < min) { - d_minMap[n] = min; + d_minMap.insert(n, min); Node nGeqMin; if (min.getInfinitesimalPart() == 0) { nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart()); @@ -267,7 +267,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ DeltaRational max = std::max(first, second); CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n); if (maxFind == d_maxMap.end() || (*maxFind).second > max) { - d_maxMap[n] = max; + d_maxMap.insert(n, max); Node nLeqMax; if (max.getInfinitesimalPart() == 0) { nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart()); @@ -398,7 +398,7 @@ void ArithStaticLearner::addBound(TNode n) { /* fall through */ case kind::LEQ: if (maxFind == d_maxMap.end() || (*maxFind).second > bound) { - d_maxMap[n[0]] = bound; + d_maxMap.insert(n[0], bound); Debug("arith::static") << "adding bound " << n << endl; } break; @@ -407,7 +407,7 @@ void ArithStaticLearner::addBound(TNode n) { /* fall through */ case kind::GEQ: if (minFind == d_minMap.end() || (*minFind).second < bound) { - d_minMap[n[0]] = bound; + d_minMap.insert(n[0], bound); Debug("arith::static") << "adding bound " << n << endl; } break; diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index b047018e8..0de28c5ab 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -27,7 +27,7 @@ #include "context/context.h" #include "context/cdlist.h" -#include "context/cdhashmap.h" +#include "context/cdtrail_hashmap.h" #include namespace CVC4 { @@ -41,8 +41,7 @@ private: * (=> _ (= x c)) * where c is a constant. */ - //typedef __gnu_cxx::hash_map, NodeHashFunction> VarToNodeSetMap; - typedef context::CDHashMap CDNodeToNodeListMap; + typedef context::CDTrailHashMap CDNodeToNodeListMap; // The domain is an implicit list OR(x, OR(y, ..., FALSE )) // or FALSE CDNodeToNodeListMap d_miplibTrick; @@ -50,8 +49,7 @@ private: /** * Map from a node to it's minimum and maximum. */ - //typedef __gnu_cxx::hash_map NodeToMinMaxMap; - typedef context::CDHashMap CDNodeToMinMaxMap; + typedef context::CDTrailHashMap CDNodeToMinMaxMap; CDNodeToMinMaxMap d_minMap; CDNodeToMinMaxMap d_maxMap; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6ec6c7090..d2814348a 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1369,7 +1369,7 @@ Constraint TheoryArith::constraintFromFactQueue(){ if(assertion != reAssertion){ Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " << reAssertion << endl; Assert(constraint != NullConstraint); - d_assertionsThatDoNotMatchTheirLiterals[assertion] = constraint; + d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint); } } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 6a83c501b..b791186cf 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -22,6 +22,7 @@ #include "context/context.h" #include "context/cdlist.h" #include "context/cdhashset.h" +#include "context/cdinsert_hashmap.h" #include "context/cdqueue.h" #include "expr/node.h" @@ -135,7 +136,7 @@ private: * A superset of all of the assertions that currently are not the literal for * their constraint do not match constraint literals. Not just the witnesses. */ - context::CDHashMap d_assertionsThatDoNotMatchTheirLiterals; + context::CDInsertHashMap d_assertionsThatDoNotMatchTheirLiterals; /** * (For the moment) the type hierarchy goes as: diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index a05d30517..aabd3a62d 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -537,7 +537,7 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) { void TheoryArrays::computeCareGraph() { if (d_sharedArrays.size() > 0) { - context::CDHashSet::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end(); + CDNodeSet::key_iterator it1 = d_sharedArrays.key_begin(), it2, iend = d_sharedArrays.key_end(); for (; it1 != iend; ++it1) { for (it2 = it1, ++it2; it2 != iend; ++it2) { if ((*it1).getType() != (*it2).getType()) { @@ -1261,7 +1261,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) void TheoryArrays::queueRowLemma(RowLemmaType lem) { - if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) { + if (d_conflict || d_RowAlreadyAdded.contains(lem)) { return; } TNode a = lem.first; @@ -1407,7 +1407,7 @@ void TheoryArrays::dischargeLemmas() for (unsigned count = 0; count < sz; ++count) { RowLemmaType l = d_RowQueue.front(); d_RowQueue.pop(); - if (d_RowAlreadyAdded.count(l) != 0) { + if (d_RowAlreadyAdded.contains(l)) { continue; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 240cfad9a..172482e71 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -333,8 +333,10 @@ class TheoryArrays : public Theory { context::CDQueue d_RowQueue; context::CDHashSet d_RowAlreadyAdded; - context::CDHashSet d_sharedArrays; - context::CDHashSet d_sharedOther; + typedef context::CDHashSet CDNodeSet; + + CDNodeSet d_sharedArrays; + CDNodeSet d_sharedOther; context::CDO d_sharedTerms; context::CDList d_reads; std::hash_map d_diseqCache; diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index e62f9b7a1..aec0cff58 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -118,7 +118,7 @@ private: /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far - context::CDHashSet d_seen; + context::CDHashSet d_seen; /** * Assignment status of each node. diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 0c8df3fca..e38f3568c 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -40,8 +40,8 @@ class TheoryBV : public Theory { context::Context* d_context; /** Context dependent set of atoms we already propagated */ - context::CDHashSet d_alreadyPropagatedSet; - context::CDHashSet d_sharedTermsSet; + context::CDHashSet d_alreadyPropagatedSet; + context::CDHashSet d_sharedTermsSet; BitblastSolver d_bitblastSolver; EqualitySolver d_equalitySolver; diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 655918986..c7036a9ad 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -66,7 +66,7 @@ private: AlreadyNotifiedMap d_alreadyNotifiedMap; /** The registered equalities for propagation */ - typedef context::CDHashSet RegisteredEqualitiesSet; + typedef context::CDHashSet RegisteredEqualitiesSet; RegisteredEqualitiesSet d_registeredEqualities; private: diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 063943056..27371eac3 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -190,7 +190,7 @@ class TheoryEngine { * context-dependent set of those theory-propagable literals that * have been propagated. */ - context::CDHashSet d_hasPropagated; + context::CDHashSet d_hasPropagated; /** * Statistics for a particular theory. -- 2.30.2