From: Dejan Jovanović Date: Fri, 2 Mar 2012 20:38:23 +0000 (+0000) Subject: CDMap -> CDHashMap X-Git-Tag: cvc5-1.0.0~8288 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=068107e1d1f705eb9054b4309a26236230687d80;p=cvc5.git CDMap -> CDHashMap CDSet -> CDHashSet --- diff --git a/.cproject b/.cproject index ac930d8b9..2579ef3ae 100644 --- a/.cproject +++ b/.cproject @@ -52,277 +52,278 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - make - check - true - true - true - - - make - -j2 - - true - true - true - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + make + -j10 + check + true + false + true + + + make + -j2 + true + true + true + + + diff --git a/src/context/Makefile.am b/src/context/Makefile.am index e40eac099..23607373a 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -16,10 +16,10 @@ libcontext_la_SOURCES = \ cdlist_forward.h \ cdqueue.h \ cdtrail_queue.h \ - cdmap.h \ - cdmap_forward.h \ - cdset.h \ - cdset_forward.h \ + cdhashmap.h \ + cdhashmap_forward.h \ + cdhashset.h \ + cdhashset_forward.h \ cdcirclist.h \ cdcirclist_forward.h \ cdvector.h \ diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h new file mode 100644 index 000000000..de21515c7 --- /dev/null +++ b/src/context/cdhashmap.h @@ -0,0 +1,586 @@ +/********************* */ +/*! \file cdmap.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): taking, dejan + ** 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 Context-dependent map class. + ** + ** Context-dependent map class. Generic templated class for a map + ** which must be saved and restored as contexts are pushed and + ** popped. Requires that operator= be defined for the data class, + ** and operator== for the key class. For key types that don't have a + ** __gnu_cxx::hash<>, you should provide an explicit HashFcn. + ** + ** Internal documentation: + ** + ** CDMap<> 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<>. + ** + ** You insert some (key,value) pairs. Each allocates a CDOhash_map<> + ** and goes on a doubly-linked list headed by map.d_first and + ** threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps are constructed + ** with a NULL d_map pointer, but then immediately call + ** makeCurrent() and set the d_map pointer back to the map. At + ** context level 0, this doesn't lead to anything special. In + ** higher context levels, this stores away a CDOhash_map with a NULL + ** 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 + ** associated CDOhash_map calls makeCurrent(), then sets the new + ** value. The save object is also a CDOhash_map (allocated in context + ** memory). + ** + ** Now, CDOhash_maps disappear in a variety of ways. + ** + ** First, you might pop beyond a "modification of the value" + ** scope level, requiring a re-association of the key to an old + ** value. This is easy. CDOhash_map::restore() does the work, and + ** the context memory of the save object is reclaimed as usual. + ** + ** Second, you might pop beyond a "insert the key" scope level, + ** requiring that the key be completely removed from the map and + ** its CDOhash_map object memory freed. Here, the CDOhash_map is restored + ** to a "NULL-map" state (see above), signaling it to remove + ** itself from the map completely and put itself on a "trash + ** list" for the map. + ** + ** Third, you might obliterate() the key. This calls the CDOhash_map + ** destructor, which calls destroy(), which does a successive + ** restore() until level 0. If the key was in the map since + ** level 0, the restore() won't remove it, so in that case + ** obliterate() removes it from the map and frees the CDOhash_map's + ** memory. + ** + ** Fourth, you might delete the cdhashmap(calling CDMap::~CDMap()). + ** 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 + ** 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() + ** on itself. + ** + ** CDMap::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() + ** calls destroy(), which restores as much as possible. (Note, + ** though, that since objects placed on the trash have already + ** restored to the fullest extent possible, it does nothing.) + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDMAP_H +#define __CVC4__CONTEXT__CDMAP_H + +#include +#include +#include + +#include "context/context.h" +#include "util/Assert.h" +#include "context/cdhashmap_forward.h" + +namespace CVC4 { +namespace context { + +// Auxiliary class: almost the same as CDO (see cdo.h) + +template > +class CDOhash_map : public ContextObj { + friend class CDHashMap; + + Key d_key; + Data d_data; + CDHashMap* d_map; + + /** never put this cdhashmapelement on the trash */ + bool d_noTrash; + + // Doubly-linked list for keeping track of elements in order of insertion + CDOhash_map* d_prev; + CDOhash_map* d_next; + + virtual ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDOhash_map(*this); + } + + virtual void restore(ContextObj* data) { + if(d_map != NULL) { + CDOhash_map* p = static_cast(data); + if(p->d_map == NULL) { + Assert(d_map->d_map.find(d_key) != d_map->d_map.end() && + (*d_map->d_map.find(d_key)).second == this); + // no longer in map (popped beyond first level in which it was) + d_map->d_map.erase(d_key); + // If we call deleteSelf() here, it re-enters restore(). So, + // put it on a "trash heap" instead, for later deletion. + // + // FIXME multithreading + if(d_map->d_first == this) { + Debug("gc") << "remove first-elem " << this << " from map " << d_map << " with next-elem " << d_next << std::endl; + if(d_next == this) { + Assert(d_prev == this); + d_map->d_first = NULL; + } else { + d_map->d_first = d_next; + } + } else { + Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl; + } + d_next->d_prev = d_prev; + d_prev->d_next = d_next; + if(d_noTrash) { + Debug("gc") << "CDMap<> no-trash " << this << std::endl; + } else { + Debug("gc") << "CDMap<> trash push_back " << this << std::endl; + //this->deleteSelf(); + d_map->d_trash.push_back(this); + } + } else { + d_data = p->d_data; + } + } + } + + /** ensure copy ctor is only called by us */ + CDOhash_map(const CDOhash_map& other) : + ContextObj(other), + d_key(other.d_key), + d_data(other.d_data), + d_map(other.d_map), + d_prev(NULL), + d_next(NULL) { + } + +public: + + CDOhash_map(Context* context, + CDHashMap* map, + const Key& key, + const Data& data, + bool atLevelZero = false, + bool allocatedInCMM = false) : + ContextObj(allocatedInCMM, context), + d_key(key), + d_map(NULL), + d_noTrash(allocatedInCMM) { + + // untested, probably unsafe. + Assert(!(atLevelZero && allocatedInCMM)); + + if(atLevelZero) { + // "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(). + d_data = data; + } else { + // Normal map insertion: first makeCurrent(), then set the data + // and then, later, the map. Order is important; we can't + // initialize d_map in the constructor init list above, because + // we want the restore of d_map to NULL to signal us to remove + // the element from the map. + + if(allocatedInCMM) { + // Force a save/restore point, even though the object is + // allocated here. This is so that we can detect when the + // object falls out of the map (otherwise we wouldn't get it). + makeSaveRestorePoint(); + } + + set(data); + } + d_map = map; + + CDOhash_map*& first = d_map->d_first; + if(first == NULL) { + first = d_next = d_prev = this; + Debug("gc") << "add first-elem " << this << " to map " << d_map << std::endl; + } else { + Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map << " with first-elem " << first << "[" << first->d_prev << " " << first->d_next << std::endl; + d_prev = first->d_prev; + d_next = first; + d_prev->d_next = this; + first->d_prev = this; + } + } + + ~CDOhash_map() throw(AssertionException) { + destroy(); + } + + void set(const Data& data) { + makeCurrent(); + d_data = data; + } + + const Key& getKey() const { + return d_key; + } + + const Data& get() const { + return d_data; + } + + operator Data() { + return get(); + } + + const Data& operator=(const Data& data) { + set(data); + return data; + } + + CDOhash_map* next() const { + if(d_next == d_map->d_first) { + return NULL; + } else { + return d_next; + } + } +};/* class CDOhash_map<> */ + + +/** + * Generic templated class for a map which must be saved and restored + * as contexts are pushed and popped. Requires that operator= be + * defined for the data class, and operator== for the key class. + */ +template +class CDHashMap : public ContextObj { + + typedef CDOhash_map Element; + typedef __gnu_cxx::hash_map table_type; + + friend class CDOhash_map; + + table_type d_map; + + Element* d_first; + Context* d_context; + + std::vector d_trash; + + // Nothing to save; the elements take care of themselves + virtual ContextObj* save(ContextMemoryManager* pCMM) { + Unreachable(); + } + + // Similarly, nothing to restore + virtual void restore(ContextObj* data) { + Unreachable(); + } + + void emptyTrash() { + //FIXME multithreading + for(typename std::vector::iterator i = d_trash.begin(); + i != d_trash.end(); + ++i) { + Debug("gc") << "emptyTrash(): " << *i << std::endl; + (*i)->deleteSelf(); + } + d_trash.clear(); + } + +public: + + CDHashMap(Context* context) : + ContextObj(context), + d_map(), + d_first(NULL), + d_context(context), + d_trash() { + } + + ~CDHashMap() throw(AssertionException) { + Debug("gc") << "cdhashmap" << this + << " disappearing, destroying..." << std::endl; + destroy(); + Debug("gc") << "cdhashmap" << this + << " disappearing, done destroying" << std::endl; + + Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl; + emptyTrash(); + Debug("gc") << "done emptying trash for " << this << std::endl; + + for(typename table_type::iterator i = d_map.begin(); + i != d_map.end(); + ++i) { + // mark it as being a destruction (short-circuit restore()) + (*i).second->d_map = NULL; + if(!(*i).second->d_noTrash) { + (*i).second->deleteSelf(); + } + } + d_map.clear(); + d_first = NULL; + + Assert(d_trash.empty()); + } + + void clear() throw(AssertionException) { + Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl; + emptyTrash(); + Debug("gc") << "done emptying trash for " << this << std::endl; + + for(typename table_type::iterator i = d_map.begin(); + i != d_map.end(); + ++i) { + // mark it as being a destruction (short-circuit restore()) + (*i).second->d_map = NULL; + if(!(*i).second->d_noTrash) { + (*i).second->deleteSelf(); + } + } + d_map.clear(); + d_first = NULL; + + Assert(d_trash.empty()); + } + + // The usual operators of map + + size_t size() const { + return d_map.size(); + } + + bool empty() const { + return d_map.empty(); + } + + size_t count(const Key& k) const { + return d_map.count(k); + } + + // If a key is not present, a new object is created and inserted + Element& operator[](const Key& k) { + emptyTrash(); + + typename table_type::iterator i = d_map.find(k); + + Element* obj; + if(i == d_map.end()) {// create new object + obj = new(true) Element(d_context, this, k, Data()); + d_map[k] = obj; + } else { + obj = (*i).second; + } + return *obj; + } + + bool insert(const Key& k, const Data& d) { + emptyTrash(); + + typename table_type::iterator i = d_map.find(k); + + if(i == d_map.end()) {// create new object + Element* obj = new(true) Element(d_context, this, k, d); + d_map[k] = obj; + return true; + } else { + (*i).second->set(d); + return false; + } + } + + // Use this for pointer data d allocated in context memory at this + // level. THIS IS HIGHLY EXPERIMENTAL. It seems to work if ALL + // your data objects are allocated from context memory. + void insertDataFromContextMemory(const Key& k, const Data& d) { + emptyTrash(); + + AlwaysAssert(d_map.find(k) == d_map.end()); + + Element* obj = new(d_context->getCMM()) Element(d_context, this, k, d, + false /* atLevelZero */, + true /* allocatedInCMM */); + + d_map[k] = obj; + } + + /** + * Version of insert() for CDMap<> 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 + * the object should have an "initializing" value v1 below context + * level L, and a "current" value v2 at context level L. Then you + * can (assuming key k): + * + * map.insertAtContextLevelZero(k, v1); + * map.insert(k, v2); + * + * The justification for this "escape hatch" has to do with + * variables and assignments in theories (e.g., in arithmetic). + * Let's say you introduce a new variable x at some deep decision + * level (thanks to lazy registration, or a splitting lemma, or + * whatever). x might be mapped to something, but for theory + * implementation simplicity shouldn't disappear from the map on + * backjump; rather, it can take another (legal) value, or a special + * value to indicate it needs to be recomputed. + * + * It is an error (checked via AlwaysAssert()) to + * insertAtContextLevelZero() a key that already is in the map. + */ + void insertAtContextLevelZero(const Key& k, const Data& d) { + emptyTrash(); + + AlwaysAssert(d_map.find(k) == d_map.end()); + + Element* obj = new(true) Element(d_context, this, k, d, + true /* atLevelZero */); + d_map[k] = obj; + } + + // FIXME: no erase(), too much hassle to implement efficiently... + + /** + * "Obliterating" is kind of like erasing, except it's not + * backtrackable; the key is permanently removed from the map. + * (Naturally, it can be re-added as a new element.) + */ + void obliterate(const Key& k) { + typename table_type::iterator i = d_map.find(k); + if(i != d_map.end()) { + Debug("gc") << "key " << k << " obliterated" << std::endl; + // We can't call ->deleteSelf() here, because it calls the + // ContextObj destructor, which calls CDOhash_map::destroy(), which + // restore()'s, which puts the CDOhash_map on the trash, which causes + // a double-delete. + (*i).second->~Element(); + // Writing ...->~CDOhash_map() in the above is legal (?) but breaks + // g++ 4.1, though later versions have no problem. + + typename table_type::iterator j = d_map.find(k); + // This if() succeeds for objects inserted when in the + // zero-scope: they were never save()'d there, so restore() + // never gets a NULL map and so they leak. + if(j != d_map.end()) { + Element* elt = (*j).second; + if(d_first == elt) { + if(elt->d_next == elt) { + Assert(elt->d_prev == elt); + d_first = NULL; + } else { + d_first = elt->d_next; + } + } else { + elt->d_prev->d_next = elt->d_next; + elt->d_next->d_prev = elt->d_prev; + } + d_map.erase(j);//FIXME multithreading + Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl; + // was already destructed, so don't call ->deleteSelf() + if(!elt->d_noTrash) { + ::operator delete(elt); + } + } + } + } + + class iterator { + const Element* d_it; + + public: + + iterator(const Element* p) : d_it(p) {} + iterator(const iterator& i) : d_it(i.d_it) {} + + // Default constructor + iterator() {} + + // (Dis)equality + bool operator==(const iterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const iterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + std::pair operator*() const { + return std::pair(d_it->getKey(), d_it->get()); + } + + // Prefix increment + iterator& operator++() { + d_it = d_it->next(); + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const std::pair* d_pair; + + public: + + Proxy(const std::pair& p) : d_pair(&p) {} + + const std::pair& operator*() const { + return *d_pair; + } + };/* class CDMap<>::iterator::Proxy */ + + // Actual postfix increment: returns Proxy with the old value. + // Now, an expression like *i++ will return the current *i, and + // then advance the iterator. However, don't try to use + // Proxy for anything else. + const Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDMap<>::iterator */ + + typedef iterator const_iterator; + + iterator begin() const { + return iterator(d_first); + } + + iterator end() const { + return iterator(NULL); + } + + iterator find(const Key& k) const { + typename table_type::const_iterator i = d_map.find(k); + + if(i == d_map.end()) { + return end(); + } else { + return iterator((*i).second); + } + } + + iterator find(const Key& k) { + emptyTrash(); + return const_cast(this)->find(k); + } + +};/* class CDMap<> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDMAP_H */ diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h new file mode 100644 index 000000000..f1031fec4 --- /dev/null +++ b/src/context/cdhashmap_forward.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file cdmap_forward.h + ** \verbatim + ** Original author: mdeters + ** 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 a forward declaration header to declare the CDMap<> + ** 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 + ** public header context. + ** + ** For CDMap<> in particular, it's difficult to forward-declare it + ** yourself, becase it has a default template argument. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H +#define __CVC4__CONTEXT__CDMAP_FORWARD_H + +namespace __gnu_cxx { + template struct hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template > + class CDHashMap; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */ diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h new file mode 100644 index 000000000..777bbc94b --- /dev/null +++ b/src/context/cdhashset.h @@ -0,0 +1,151 @@ +/********************* */ +/*! \file cdset.h + ** \verbatim + ** Original author: mdeters + ** 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 Context-dependent set class. + ** + ** Context-dependent set class. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDSET_H +#define __CVC4__CONTEXT__CDSET_H + +#include "context/context.h" +#include "context/cdhashset_forward.h" +#include "context/cdhashmap.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +template +class CDHashSet : protected CDHashMap { + typedef CDHashMap super; + +public: + + // ensure these are publicly accessible + static void* operator new(size_t size, bool b) { + return ContextObj::operator new(size, b); + } + + static void operator delete(void* pMem, bool b) { + return ContextObj::operator delete(pMem, b); + } + + void deleteSelf() { + this->ContextObj::deleteSelf(); + } + + static void operator delete(void* pMem) { + AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); + } + + CDHashSet(Context* context) : + super(context) { + } + + size_t size() const { + return super::size(); + } + + size_t count(const V& v) const { + return super::count(v); + } + + bool insert(const V& v) { + return super::insert(v, v); + } + + bool contains(const V& v) { + return find(v) != end(); + } + + // FIXME: no erase(), too much hassle to implement efficiently... + + class iterator { + typename super::iterator d_it; + + public: + + iterator(const typename super::iterator& it) : d_it(it) {} + iterator(const iterator& it) : d_it(it.d_it) {} + + // Default constructor + iterator() {} + + // (Dis)equality + bool operator==(const iterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const iterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + V operator*() const { + return (*d_it).first; + } + + // Prefix increment + iterator& operator++() { + ++d_it; + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const V& d_val; + + public: + + Proxy(const V& v) : d_val(v) {} + + V operator*() const { + return d_val; + } + };/* class CDSet<>::iterator::Proxy */ + + // Actual postfix increment: returns Proxy with the old value. + // Now, an expression like *i++ will return the current *i, and + // then advance the orderedIterator. However, don't try to use + // Proxy for anything else. + const Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDSet<>::iterator */ + + typedef iterator const_iterator; + + const_iterator begin() const { + return iterator(super::begin()); + } + + const_iterator end() const { + return iterator(super::end()); + } + + const_iterator find(const V& v) const { + return iterator(super::find(v)); + } + +};/* class CDSet */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDSET_H */ diff --git a/src/context/cdhashset_forward.h b/src/context/cdhashset_forward.h new file mode 100644 index 000000000..dc7da22d2 --- /dev/null +++ b/src/context/cdhashset_forward.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file cdset_forward.h + ** \verbatim + ** Original author: mdeters + ** 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 a forward declaration header to declare the CDSet<> + ** template + ** + ** This is a forward declaration header to declare the CDSet<> + ** template. It's useful if you want to forward-declare CDSet<> + ** without including the full cdset.h header, for example, in a + ** public header context. + ** + ** For CDSet<> in particular, it's difficult to forward-declare it + ** yourself, becase it has a default template argument. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CONTEXT__CDSET_FORWARD_H +#define __CVC4__CONTEXT__CDSET_FORWARD_H + +namespace __gnu_cxx { + template struct hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template > + class CDHashSet; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDSET_FORWARD_H */ diff --git a/src/context/cdmap.h b/src/context/cdmap.h deleted file mode 100644 index 2a5365082..000000000 --- a/src/context/cdmap.h +++ /dev/null @@ -1,586 +0,0 @@ -/********************* */ -/*! \file cdmap.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): taking, dejan - ** 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 Context-dependent map class. - ** - ** Context-dependent map class. Generic templated class for a map - ** which must be saved and restored as contexts are pushed and - ** popped. Requires that operator= be defined for the data class, - ** and operator== for the key class. For key types that don't have a - ** __gnu_cxx::hash<>, you should provide an explicit HashFcn. - ** - ** Internal documentation: - ** - ** CDMap<> 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 - ** CDOmaps that may be useful in figuring out this mess: - ** - ** So you have a CDMap<>. - ** - ** You insert some (key,value) pairs. Each allocates a CDOmap<> - ** and goes on a doubly-linked list headed by map.d_first and - ** threaded via cdomap.{d_prev,d_next}. CDOmaps are constructed - ** with a NULL d_map pointer, but then immediately call - ** makeCurrent() and set the d_map pointer back to the map. At - ** context level 0, this doesn't lead to anything special. In - ** higher context levels, this stores away a CDOmap with a NULL - ** 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 - ** associated CDOmap calls makeCurrent(), then sets the new - ** value. The save object is also a CDOmap (allocated in context - ** memory). - ** - ** Now, CDOmaps disappear in a variety of ways. - ** - ** First, you might pop beyond a "modification of the value" - ** scope level, requiring a re-association of the key to an old - ** value. This is easy. CDOmap::restore() does the work, and - ** the context memory of the save object is reclaimed as usual. - ** - ** Second, you might pop beyond a "insert the key" scope level, - ** requiring that the key be completely removed from the map and - ** its CDOmap object memory freed. Here, the CDOmap is restored - ** to a "NULL-map" state (see above), signaling it to remove - ** itself from the map completely and put itself on a "trash - ** list" for the map. - ** - ** Third, you might obliterate() the key. This calls the CDOmap - ** destructor, which calls destroy(), which does a successive - ** restore() until level 0. If the key was in the map since - ** level 0, the restore() won't remove it, so in that case - ** obliterate() removes it from the map and frees the CDOmap's - ** memory. - ** - ** Fourth, you might delete the CDMap (calling CDMap::~CDMap()). - ** This first calls destroy(), as per ContextObj contract, but - ** CDMap doesn't save/restore itself, so that does nothing at the - ** CDMap-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 - ** CDOmap::restore() (see CDOmap::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() - ** on itself. - ** - ** CDMap::emptyTrash() simply goes through and calls - ** ->deleteSelf() on all elements in the trash. - ** ContextObj::deleteSelf() calls the CDOmap destructor, then - ** frees the memory associated to the CDOmap. CDOmap::~CDOmap() - ** calls destroy(), which restores as much as possible. (Note, - ** though, that since objects placed on the trash have already - ** restored to the fullest extent possible, it does nothing.) - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CONTEXT__CDMAP_H -#define __CVC4__CONTEXT__CDMAP_H - -#include -#include -#include - -#include "context/context.h" -#include "util/Assert.h" -#include "context/cdmap_forward.h" - -namespace CVC4 { -namespace context { - -// Auxiliary class: almost the same as CDO (see cdo.h) - -template > -class CDOmap : public ContextObj { - friend class CDMap; - - Key d_key; - Data d_data; - CDMap* d_map; - - /** never put this cdmap element on the trash */ - bool d_noTrash; - - // Doubly-linked list for keeping track of elements in order of insertion - CDOmap* d_prev; - CDOmap* d_next; - - virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDOmap(*this); - } - - virtual void restore(ContextObj* data) { - if(d_map != NULL) { - CDOmap* p = static_cast(data); - if(p->d_map == NULL) { - Assert(d_map->d_map.find(d_key) != d_map->d_map.end() && - (*d_map->d_map.find(d_key)).second == this); - // no longer in map (popped beyond first level in which it was) - d_map->d_map.erase(d_key); - // If we call deleteSelf() here, it re-enters restore(). So, - // put it on a "trash heap" instead, for later deletion. - // - // FIXME multithreading - if(d_map->d_first == this) { - Debug("gc") << "remove first-elem " << this << " from map " << d_map << " with next-elem " << d_next << std::endl; - if(d_next == this) { - Assert(d_prev == this); - d_map->d_first = NULL; - } else { - d_map->d_first = d_next; - } - } else { - Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl; - } - d_next->d_prev = d_prev; - d_prev->d_next = d_next; - if(d_noTrash) { - Debug("gc") << "CDMap<> no-trash " << this << std::endl; - } else { - Debug("gc") << "CDMap<> trash push_back " << this << std::endl; - //this->deleteSelf(); - d_map->d_trash.push_back(this); - } - } else { - d_data = p->d_data; - } - } - } - - /** ensure copy ctor is only called by us */ - CDOmap(const CDOmap& other) : - ContextObj(other), - d_key(other.d_key), - d_data(other.d_data), - d_map(other.d_map), - d_prev(NULL), - d_next(NULL) { - } - -public: - - CDOmap(Context* context, - CDMap* map, - const Key& key, - const Data& data, - bool atLevelZero = false, - bool allocatedInCMM = false) : - ContextObj(allocatedInCMM, context), - d_key(key), - d_map(NULL), - d_noTrash(allocatedInCMM) { - - // untested, probably unsafe. - Assert(!(atLevelZero && allocatedInCMM)); - - if(atLevelZero) { - // "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(). - d_data = data; - } else { - // Normal map insertion: first makeCurrent(), then set the data - // and then, later, the map. Order is important; we can't - // initialize d_map in the constructor init list above, because - // we want the restore of d_map to NULL to signal us to remove - // the element from the map. - - if(allocatedInCMM) { - // Force a save/restore point, even though the object is - // allocated here. This is so that we can detect when the - // object falls out of the map (otherwise we wouldn't get it). - makeSaveRestorePoint(); - } - - set(data); - } - d_map = map; - - CDOmap*& first = d_map->d_first; - if(first == NULL) { - first = d_next = d_prev = this; - Debug("gc") << "add first-elem " << this << " to map " << d_map << std::endl; - } else { - Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map << " with first-elem " << first << "[" << first->d_prev << " " << first->d_next << std::endl; - d_prev = first->d_prev; - d_next = first; - d_prev->d_next = this; - first->d_prev = this; - } - } - - ~CDOmap() throw(AssertionException) { - destroy(); - } - - void set(const Data& data) { - makeCurrent(); - d_data = data; - } - - const Key& getKey() const { - return d_key; - } - - const Data& get() const { - return d_data; - } - - operator Data() { - return get(); - } - - const Data& operator=(const Data& data) { - set(data); - return data; - } - - CDOmap* next() const { - if(d_next == d_map->d_first) { - return NULL; - } else { - return d_next; - } - } -};/* class CDOmap<> */ - - -/** - * Generic templated class for a map which must be saved and restored - * as contexts are pushed and popped. Requires that operator= be - * defined for the data class, and operator== for the key class. - */ -template -class CDMap : public ContextObj { - - typedef CDOmap Element; - typedef __gnu_cxx::hash_map table_type; - - friend class CDOmap; - - table_type d_map; - - Element* d_first; - Context* d_context; - - std::vector d_trash; - - // Nothing to save; the elements take care of themselves - virtual ContextObj* save(ContextMemoryManager* pCMM) { - Unreachable(); - } - - // Similarly, nothing to restore - virtual void restore(ContextObj* data) { - Unreachable(); - } - - void emptyTrash() { - //FIXME multithreading - for(typename std::vector::iterator i = d_trash.begin(); - i != d_trash.end(); - ++i) { - Debug("gc") << "emptyTrash(): " << *i << std::endl; - (*i)->deleteSelf(); - } - d_trash.clear(); - } - -public: - - CDMap(Context* context) : - ContextObj(context), - d_map(), - d_first(NULL), - d_context(context), - d_trash() { - } - - ~CDMap() throw(AssertionException) { - Debug("gc") << "cdmap " << this - << " disappearing, destroying..." << std::endl; - destroy(); - Debug("gc") << "cdmap " << this - << " disappearing, done destroying" << std::endl; - - Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl; - emptyTrash(); - Debug("gc") << "done emptying trash for " << this << std::endl; - - for(typename table_type::iterator i = d_map.begin(); - i != d_map.end(); - ++i) { - // mark it as being a destruction (short-circuit restore()) - (*i).second->d_map = NULL; - if(!(*i).second->d_noTrash) { - (*i).second->deleteSelf(); - } - } - d_map.clear(); - d_first = NULL; - - Assert(d_trash.empty()); - } - - void clear() throw(AssertionException) { - Debug("gc") << "clearing cdmap " << this << ", emptying trash" << std::endl; - emptyTrash(); - Debug("gc") << "done emptying trash for " << this << std::endl; - - for(typename table_type::iterator i = d_map.begin(); - i != d_map.end(); - ++i) { - // mark it as being a destruction (short-circuit restore()) - (*i).second->d_map = NULL; - if(!(*i).second->d_noTrash) { - (*i).second->deleteSelf(); - } - } - d_map.clear(); - d_first = NULL; - - Assert(d_trash.empty()); - } - - // The usual operators of map - - size_t size() const { - return d_map.size(); - } - - bool empty() const { - return d_map.empty(); - } - - size_t count(const Key& k) const { - return d_map.count(k); - } - - // If a key is not present, a new object is created and inserted - Element& operator[](const Key& k) { - emptyTrash(); - - typename table_type::iterator i = d_map.find(k); - - Element* obj; - if(i == d_map.end()) {// create new object - obj = new(true) Element(d_context, this, k, Data()); - d_map[k] = obj; - } else { - obj = (*i).second; - } - return *obj; - } - - bool insert(const Key& k, const Data& d) { - emptyTrash(); - - typename table_type::iterator i = d_map.find(k); - - if(i == d_map.end()) {// create new object - Element* obj = new(true) Element(d_context, this, k, d); - d_map[k] = obj; - return true; - } else { - (*i).second->set(d); - return false; - } - } - - // Use this for pointer data d allocated in context memory at this - // level. THIS IS HIGHLY EXPERIMENTAL. It seems to work if ALL - // your data objects are allocated from context memory. - void insertDataFromContextMemory(const Key& k, const Data& d) { - emptyTrash(); - - AlwaysAssert(d_map.find(k) == d_map.end()); - - Element* obj = new(d_context->getCMM()) Element(d_context, this, k, d, - false /* atLevelZero */, - true /* allocatedInCMM */); - - d_map[k] = obj; - } - - /** - * Version of insert() for CDMap<> 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 - * the object should have an "initializing" value v1 below context - * level L, and a "current" value v2 at context level L. Then you - * can (assuming key k): - * - * map.insertAtContextLevelZero(k, v1); - * map.insert(k, v2); - * - * The justification for this "escape hatch" has to do with - * variables and assignments in theories (e.g., in arithmetic). - * Let's say you introduce a new variable x at some deep decision - * level (thanks to lazy registration, or a splitting lemma, or - * whatever). x might be mapped to something, but for theory - * implementation simplicity shouldn't disappear from the map on - * backjump; rather, it can take another (legal) value, or a special - * value to indicate it needs to be recomputed. - * - * It is an error (checked via AlwaysAssert()) to - * insertAtContextLevelZero() a key that already is in the map. - */ - void insertAtContextLevelZero(const Key& k, const Data& d) { - emptyTrash(); - - AlwaysAssert(d_map.find(k) == d_map.end()); - - Element* obj = new(true) Element(d_context, this, k, d, - true /* atLevelZero */); - d_map[k] = obj; - } - - // FIXME: no erase(), too much hassle to implement efficiently... - - /** - * "Obliterating" is kind of like erasing, except it's not - * backtrackable; the key is permanently removed from the map. - * (Naturally, it can be re-added as a new element.) - */ - void obliterate(const Key& k) { - typename table_type::iterator i = d_map.find(k); - if(i != d_map.end()) { - Debug("gc") << "key " << k << " obliterated" << std::endl; - // We can't call ->deleteSelf() here, because it calls the - // ContextObj destructor, which calls CDOmap::destroy(), which - // restore()'s, which puts the CDOmap on the trash, which causes - // a double-delete. - (*i).second->~Element(); - // Writing ...->~CDOmap() in the above is legal (?) but breaks - // g++ 4.1, though later versions have no problem. - - typename table_type::iterator j = d_map.find(k); - // This if() succeeds for objects inserted when in the - // zero-scope: they were never save()'d there, so restore() - // never gets a NULL map and so they leak. - if(j != d_map.end()) { - Element* elt = (*j).second; - if(d_first == elt) { - if(elt->d_next == elt) { - Assert(elt->d_prev == elt); - d_first = NULL; - } else { - d_first = elt->d_next; - } - } else { - elt->d_prev->d_next = elt->d_next; - elt->d_next->d_prev = elt->d_prev; - } - d_map.erase(j);//FIXME multithreading - Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl; - // was already destructed, so don't call ->deleteSelf() - if(!elt->d_noTrash) { - ::operator delete(elt); - } - } - } - } - - class iterator { - const Element* d_it; - - public: - - iterator(const Element* p) : d_it(p) {} - iterator(const iterator& i) : d_it(i.d_it) {} - - // Default constructor - iterator() {} - - // (Dis)equality - bool operator==(const iterator& i) const { - return d_it == i.d_it; - } - bool operator!=(const iterator& i) const { - return d_it != i.d_it; - } - - // Dereference operators. - std::pair operator*() const { - return std::pair(d_it->getKey(), d_it->get()); - } - - // Prefix increment - iterator& operator++() { - d_it = d_it->next(); - return *this; - } - - // Postfix increment: requires a Proxy object to hold the - // intermediate value for dereferencing - class Proxy { - const std::pair* d_pair; - - public: - - Proxy(const std::pair& p) : d_pair(&p) {} - - const std::pair& operator*() const { - return *d_pair; - } - };/* class CDMap<>::iterator::Proxy */ - - // Actual postfix increment: returns Proxy with the old value. - // Now, an expression like *i++ will return the current *i, and - // then advance the iterator. However, don't try to use - // Proxy for anything else. - const Proxy operator++(int) { - Proxy e(*(*this)); - ++(*this); - return e; - } - };/* class CDMap<>::iterator */ - - typedef iterator const_iterator; - - iterator begin() const { - return iterator(d_first); - } - - iterator end() const { - return iterator(NULL); - } - - iterator find(const Key& k) const { - typename table_type::const_iterator i = d_map.find(k); - - if(i == d_map.end()) { - return end(); - } else { - return iterator((*i).second); - } - } - - iterator find(const Key& k) { - emptyTrash(); - return const_cast(this)->find(k); - } - -};/* class CDMap<> */ - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDMAP_H */ diff --git a/src/context/cdmap_forward.h b/src/context/cdmap_forward.h deleted file mode 100644 index 331d6a93e..000000000 --- a/src/context/cdmap_forward.h +++ /dev/null @@ -1,42 +0,0 @@ -/********************* */ -/*! \file cdmap_forward.h - ** \verbatim - ** Original author: mdeters - ** 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 a forward declaration header to declare the CDMap<> - ** 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 - ** public header context. - ** - ** For CDMap<> in particular, it's difficult to forward-declare it - ** yourself, becase it has a default template argument. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H -#define __CVC4__CONTEXT__CDMAP_FORWARD_H - -namespace __gnu_cxx { - template struct hash; -}/* __gnu_cxx namespace */ - -namespace CVC4 { - namespace context { - template > - class CDMap; - }/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */ diff --git a/src/context/cdset.h b/src/context/cdset.h deleted file mode 100644 index 8699d9cf4..000000000 --- a/src/context/cdset.h +++ /dev/null @@ -1,151 +0,0 @@ -/********************* */ -/*! \file cdset.h - ** \verbatim - ** Original author: mdeters - ** 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 Context-dependent set class. - ** - ** Context-dependent set class. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CONTEXT__CDSET_H -#define __CVC4__CONTEXT__CDSET_H - -#include "context/context.h" -#include "context/cdset_forward.h" -#include "context/cdmap.h" -#include "util/Assert.h" - -namespace CVC4 { -namespace context { - -template -class CDSet : protected CDMap { - typedef CDMap super; - -public: - - // ensure these are publicly accessible - static void* operator new(size_t size, bool b) { - return ContextObj::operator new(size, b); - } - - static void operator delete(void* pMem, bool b) { - return ContextObj::operator delete(pMem, b); - } - - void deleteSelf() { - this->ContextObj::deleteSelf(); - } - - static void operator delete(void* pMem) { - AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); - } - - CDSet(Context* context) : - super(context) { - } - - size_t size() const { - return super::size(); - } - - size_t count(const V& v) const { - return super::count(v); - } - - bool insert(const V& v) { - return super::insert(v, v); - } - - bool contains(const V& v) { - return find(v) != end(); - } - - // FIXME: no erase(), too much hassle to implement efficiently... - - class iterator { - typename super::iterator d_it; - - public: - - iterator(const typename super::iterator& it) : d_it(it) {} - iterator(const iterator& it) : d_it(it.d_it) {} - - // Default constructor - iterator() {} - - // (Dis)equality - bool operator==(const iterator& i) const { - return d_it == i.d_it; - } - bool operator!=(const iterator& i) const { - return d_it != i.d_it; - } - - // Dereference operators. - V operator*() const { - return (*d_it).first; - } - - // Prefix increment - iterator& operator++() { - ++d_it; - return *this; - } - - // Postfix increment: requires a Proxy object to hold the - // intermediate value for dereferencing - class Proxy { - const V& d_val; - - public: - - Proxy(const V& v) : d_val(v) {} - - V operator*() const { - return d_val; - } - };/* class CDSet<>::iterator::Proxy */ - - // Actual postfix increment: returns Proxy with the old value. - // Now, an expression like *i++ will return the current *i, and - // then advance the orderedIterator. However, don't try to use - // Proxy for anything else. - const Proxy operator++(int) { - Proxy e(*(*this)); - ++(*this); - return e; - } - };/* class CDSet<>::iterator */ - - typedef iterator const_iterator; - - const_iterator begin() const { - return iterator(super::begin()); - } - - const_iterator end() const { - return iterator(super::end()); - } - - const_iterator find(const V& v) const { - return iterator(super::find(v)); - } - -};/* class CDSet */ - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDSET_H */ diff --git a/src/context/cdset_forward.h b/src/context/cdset_forward.h deleted file mode 100644 index 2339552a6..000000000 --- a/src/context/cdset_forward.h +++ /dev/null @@ -1,42 +0,0 @@ -/********************* */ -/*! \file cdset_forward.h - ** \verbatim - ** Original author: mdeters - ** 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 a forward declaration header to declare the CDSet<> - ** template - ** - ** This is a forward declaration header to declare the CDSet<> - ** template. It's useful if you want to forward-declare CDSet<> - ** without including the full cdset.h header, for example, in a - ** public header context. - ** - ** For CDSet<> in particular, it's difficult to forward-declare it - ** yourself, becase it has a default template argument. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__CONTEXT__CDSET_FORWARD_H -#define __CVC4__CONTEXT__CDSET_FORWARD_H - -namespace __gnu_cxx { - template struct hash; -}/* __gnu_cxx namespace */ - -namespace CVC4 { - namespace context { - template > - class CDSet; - }/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDSET_FORWARD_H */ diff --git a/src/context/context.h b/src/context/context.h index 4e0832882..f0dbff72b 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -496,7 +496,7 @@ protected: * class-facing interface. This is a "forced" makeCurrent(), useful * for ContextObjs allocated in CMM that need a special "bottom" * case when they disappear out of existence (kind of a destructor). - * See CDOmap (in cdmap.h) for an example. + * See CDOhash_map (in cdhashmap.h) for an example. */ inline void makeSaveRestorePoint() throw(AssertionException); diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index b359b1666..70535cf1c 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -27,7 +27,7 @@ #include -#include "context/cdmap.h" +#include "context/cdhashmap.h" namespace CVC4 { namespace expr { @@ -365,12 +365,12 @@ public: */ template class CDAttrHash : - public context::CDMap, + public context::CDHashMap, value_type, AttrHashStrategy> { public: CDAttrHash(context::Context* ctxt) : - context::CDMap, + context::CDHashMap, value_type, AttrHashStrategy>(ctxt) { } @@ -382,12 +382,12 @@ public: */ template <> class CDAttrHash : - protected context::CDMap { /** A "super" type, like in Java, for easy reference below. */ - typedef context::CDMap super; + typedef context::CDHashMap super; /** * BitAccessor allows us to return a bit "by reference." Of course, diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 37c709b6a..22187ad06 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -22,8 +22,8 @@ #include "expr/expr.h" #include "expr/type.h" #include "expr/expr_manager_scope.h" -#include "context/cdmap.h" -#include "context/cdset.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "context/context.h" #include @@ -37,9 +37,9 @@ namespace CVC4 { DeclarationScope::DeclarationScope() : d_context(new Context), - d_exprMap(new(true) CDMap(d_context)), - d_typeMap(new(true) CDMap, Type>, StringHashFunction>(d_context)), - d_functions(new(true) CDSet(d_context)) { + d_exprMap(new(true) CDHashMap(d_context)), + d_typeMap(new(true) CDHashMap, Type>, StringHashFunction>(d_context)), + d_functions(new(true) CDHashSet(d_context)) { } DeclarationScope::~DeclarationScope() { @@ -67,7 +67,7 @@ bool DeclarationScope::isBound(const std::string& name) const throw() { } bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() { - CDMap::iterator found = + CDHashMap::iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 4bce5e1be..27533cca8 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -28,8 +28,8 @@ #include "expr/expr.h" #include "util/hash.h" -#include "context/cdset_forward.h" -#include "context/cdmap_forward.h" +#include "context/cdhashset_forward.h" +#include "context/cdhashmap_forward.h" namespace CVC4 { @@ -52,13 +52,13 @@ class CVC4_PUBLIC DeclarationScope { context::Context* d_context; /** A map for expressions. */ - context::CDMap *d_exprMap; + context::CDHashMap *d_exprMap; /** A map for types. */ - context::CDMap, Type>, StringHashFunction> *d_typeMap; + context::CDHashMap, Type>, StringHashFunction> *d_typeMap; /** A set of defined functions. */ - context::CDSet *d_functions; + context::CDHashSet *d_functions; public: /** Create a declaration scope. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3c320b814..8b5a93fa9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -25,7 +25,7 @@ #include #include "context/cdlist.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "context/context.h" #include "expr/command.h" #include "expr/expr.h" @@ -124,7 +124,7 @@ class SmtEnginePrivate { theory::SubstitutionMap d_topLevelSubstitutions; /** - * The last substition that the SAT layer was told about. + * The last substitution that the SAT layer was told about. * In incremental settings, substitutions cannot be performed * "backward," only forward. So SAT needs to be told of all * substitutions that are going to be done. This iterator diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 84d6d1a73..5149ed2e9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -24,8 +24,8 @@ #include #include "context/cdlist_forward.h" -#include "context/cdmap_forward.h" -#include "context/cdset_forward.h" +#include "context/cdhashmap_forward.h" +#include "context/cdhashset_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/proof.h" @@ -89,12 +89,12 @@ namespace smt { class CVC4_PUBLIC SmtEngine { /** The type of our internal map of defined functions */ - typedef context::CDMap + typedef context::CDHashMap DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList AssertionList; /** The type of our internal assignment set */ - typedef context::CDSet AssignmentSet; + typedef context::CDHashSet AssignmentSet; /** Expr manager context */ context::Context* d_context; diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index 6d2e04de1..4b52133da 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -23,7 +23,7 @@ #include "theory/arith/arith_utilities.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" using namespace CVC4; diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index bf7564593..2bac21437 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -29,7 +29,7 @@ #include "theory/arith/delta_rational.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" #include "theory/rewriter.h" #include "util/stats.h" @@ -59,7 +59,7 @@ private: * to its corresponding PropUnit. * This is node is potentially both the consequent or Rewriter::rewrite(consequent). */ - typedef context::CDMap ExplainMap; + typedef context::CDHashMap ExplainMap; ExplainMap d_explanationMap; size_t getIndex(TNode n) const { diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 07387c977..44b55440e 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -26,7 +26,7 @@ #include "expr/node.h" #include "expr/attribute.h" #include "theory/arith/delta_rational.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include #include #include @@ -47,9 +47,9 @@ typedef __gnu_cxx::hash_map ArithVarToNodeMap; //Sets of Nodes typedef __gnu_cxx::hash_set NodeSet; -typedef context::CDSet CDNodeSet; +typedef context::CDHashSet CDNodeSet; -typedef context::CDSet CDArithVarSet; +typedef context::CDHashSet CDArithVarSet; class ArithVarCallBack { public: diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index df82fde91..1dc8ddf38 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -26,7 +26,7 @@ #include "theory/arith/arith_utilities.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" namespace CVC4 { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index fcac6f10e..bea87fdde 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1030,8 +1030,8 @@ Node TheoryArith::roundRobinBranch(){ bool TheoryArith::splitDisequalities(){ bool splitSomething = false; - context::CDSet::iterator it = d_diseq.begin(); - context::CDSet::iterator it_end = d_diseq.end(); + context::CDHashSet::iterator it = d_diseq.begin(); + context::CDHashSet::iterator it_end = d_diseq.end(); for(; it != it_end; ++ it) { TNode eq = (*it)[0]; Assert(eq.getKind() == kind::EQUAL); @@ -1073,8 +1073,8 @@ void TheoryArith::debugPrintAssertions() { Debug("arith::print_assertions") << uConstr << endl; } } - context::CDSet::iterator it = d_diseq.begin(); - context::CDSet::iterator it_end = d_diseq.end(); + context::CDHashSet::iterator it = d_diseq.begin(); + context::CDHashSet::iterator it_end = d_diseq.end(); for(; it != it_end; ++ it) { Debug("arith::print_assertions") << *it << endl; } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index f364885c2..e6bdbfba0 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -23,7 +23,7 @@ #include "theory/theory.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "expr/node.h" #include "theory/arith/arith_utilities.h" @@ -183,7 +183,7 @@ private: /** * List of all of the inequalities asserted in the current context. */ - context::CDSet d_diseq; + context::CDHashSet d_diseq; /** * Manages information about the assignment and upper and lower bounds on diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index fcc45bbd5..d1c435b48 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -41,7 +41,7 @@ #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H #include "util/backtrackable.h" #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "expr/node.h" #include "util/stats.h" #include "util/ntuple.h" diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index d699617e2..fcb6ee382 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -152,8 +152,8 @@ private: typedef context::CDList > CTNodeListAlloc; - typedef context::CDMap CNodeTNodesMap; - typedef context::CDMap*, TNodeHashFunction > EqLists; + typedef context::CDHashMap CNodeTNodesMap; + typedef context::CDHashMap*, TNodeHashFunction > EqLists; typedef __gnu_cxx::hash_map NodeTNodesMap; @@ -174,7 +174,7 @@ private: /** List of disequalities needed to construct explanations for propagated * row lemmas */ - context::CDMap, TNodeHashFunction> d_explanations; + context::CDHashMap, TNodeHashFunction> d_explanations; /** * stores the conflicting disequality (still need to call construct @@ -447,9 +447,9 @@ public: void propagate(Effort e) { - Trace("arrays-prop")<<"Propagating \n"; + // Trace("arrays-prop")<<"Propagating \n"; - context::CDList::const_iterator it = d_prop_queue.begin(); + // context::CDList::const_iterator it = d_prop_queue.begin(); /* for(; it!= d_prop_queue.end(); it++) { TNode eq = *it; diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 2f9a8f928..78221a617 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -28,8 +28,8 @@ #include "context/context.h" #include "util/hash.h" #include "expr/node.h" -#include "context/cdset.h" -#include "context/cdmap.h" +#include "context/cdhashset.h" +#include "context/cdhashmap.h" #include "context/cdo.h" namespace CVC4 { @@ -113,12 +113,12 @@ private: /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far - context::CDSet d_seen; + context::CDHashSet d_seen; /** * Assignment status of each node. */ - typedef context::CDMap AssignmentMap; + typedef context::CDHashMap AssignmentMap; AssignmentMap d_state; /** diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index 6967bff98..dacd6a538 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -79,7 +79,7 @@ void inline rshift(Bits& bits, unsigned amount) { } void inline lshift(Bits& bits, unsigned amount) { - for (int i = bits.size() - 1; i >= amount ; --i) { + for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) { bits[i] = bits[i-amount]; } for(unsigned i = 0; i < amount; ++i) { diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index ee48dbef4..773491fd0 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -30,7 +30,7 @@ #include #include "context/cdo.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "context/cdlist.h" #include "theory_bv_utils.h" diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp index 6107e7f2c..be0bf6805 100644 --- a/src/theory/datatypes/explanation_manager.cpp +++ b/src/theory/datatypes/explanation_manager.cpp @@ -47,7 +47,7 @@ void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm ) } }else{ if( !pm->hasExplained( n ) ){ - context::CDMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n ); + context::CDHashMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n ); Reason r; Node exp; if( it!=d_drv_map.end() ){ diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h index 2232d0048..fa0d3f818 100644 --- a/src/theory/datatypes/explanation_manager.h +++ b/src/theory/datatypes/explanation_manager.h @@ -160,7 +160,7 @@ class ExplanationManager : public Explainer { private: /** map from nodes and the reason for them */ - context::CDMap< Node, Reason, NodeHashFunction > d_drv_map; + context::CDHashMap< Node, Reason, NodeHashFunction > d_drv_map; /** has conflict */ context::CDO< bool > d_hasConflict; /** process the reason for node n */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 4d429bc54..921df028e 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -40,10 +40,10 @@ namespace datatypes { class TheoryDatatypes : public Theory { private: typedef context::CDList > EqList; - typedef context::CDMap EqLists; + typedef context::CDHashMap EqLists; typedef context::CDList > EqListN; - typedef context::CDMap EqListsN; - typedef context::CDMap< Node, bool, NodeHashFunction > BoolMap; + typedef context::CDHashMap EqListsN; + typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** for debugging */ context::CDList d_currAsserts; diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index a5481b807..2efd121a0 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -51,11 +51,11 @@ private: /** Context-dependent size of the d_addedSharedTerms list */ context::CDO d_addedSharedTermsSize; - typedef context::CDMap, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; + typedef context::CDHashMap, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; /** A map from atoms and subterms to the theories that use it */ SharedTermsTheoriesMap d_termsToTheories; - typedef context::CDMap AlreadyNotifiedMap; + typedef context::CDHashMap AlreadyNotifiedMap; /** Map from term to theories that have already been notified about the shared term */ AlreadyNotifiedMap d_alreadyNotifiedMap; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 1ade4815d..27c1a2b69 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "context/context.h" #include "context/cdo.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "util/hash.h" namespace CVC4 { @@ -46,7 +46,7 @@ class SubstitutionMap { public: - typedef context::CDMap NodeMap; + typedef context::CDHashMap NodeMap; typedef NodeMap::iterator iterator; typedef NodeMap::const_iterator const_iterator; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index edb759157..74b756a03 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -36,7 +36,7 @@ class PreRegisterVisitor { /** * Map from nodes to the theories that have already seen them. */ - typedef context::CDMap TNodeVisitedMap; + typedef context::CDHashMap TNodeVisitedMap; TNodeVisitedMap d_visited; /** diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 72244a573..4c9309fb6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "expr/command.h" #include "prop/prop_engine.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "theory/theory.h" #include "theory/substitutions.h" #include "theory/rewriter.h" @@ -121,7 +121,7 @@ class TheoryEngine { * context-dependent set of those theory-propagable literals that * have been propagated. */ - context::CDSet d_hasPropagated; + context::CDHashSet d_hasPropagated; /** * Statistics for a particular theory. @@ -311,7 +311,7 @@ class TheoryEngine { /** * Map from equalities asserted to a theory, to the theory that can explain them. */ - typedef context::CDMap SharedAssertionsMap; + typedef context::CDHashMap SharedAssertionsMap; /** * A map from asserted facts to where they came from (for explanations). diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index ab391e242..cb7674342 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -30,7 +30,7 @@ #include "theory/uf/symmetry_breaker.h" #include "context/cdo.h" -#include "context/cdset.h" +#include "context/cdhashset.h" namespace CVC4 { namespace theory { diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 4e690ec16..ed1cecd7b 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -30,8 +30,8 @@ #include "expr/node.h" #include "context/context_mm.h" #include "context/cdo.h" -#include "context/cdmap.h" -#include "context/cdset.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "context/cdlist_context_memory.h" #include "util/exception.h" #include "context/stacking_map.h" @@ -141,15 +141,15 @@ class CongruenceClosure { // typedef all of these so that iterators are easy to define typedef context::StackingMap RepresentativeMap; typedef context::CDList > ClassList; - typedef context::CDMap ClassLists; + typedef context::CDHashMap ClassLists; typedef context::CDList > UseList; - typedef context::CDMap UseLists; - typedef context::CDMap LookupMap; + typedef context::CDHashMap UseLists; + typedef context::CDHashMap LookupMap; typedef __gnu_cxx::hash_map EqMap; - typedef context::CDMap ProofMap; - typedef context::CDMap ProofLabel; + typedef context::CDHashMap ProofMap; + typedef context::CDHashMap ProofLabel; // Simple, NON-context-dependent pending list, union find and "seen // set" types for constructing explanations and @@ -164,7 +164,7 @@ class CongruenceClosure { LookupMap d_lookup; EqMap d_eqMap; - context::CDSet d_added; + context::CDHashSet d_added; ProofMap d_proof; ProofLabel d_proofLabel; @@ -175,7 +175,7 @@ class CongruenceClosure { * The set of terms we care about (i.e. those that have been given * us with addTerm() and their representatives). */ - typedef context::CDSet CareSet; + typedef context::CDHashSet CareSet; CareSet d_careSet; // === STATISTICS === diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index 5d772b576..ba289080c 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -98,7 +98,7 @@ void TransitiveClosure::debugPrintMatrix() } unsigned TransitiveClosureNode::getId( Node i ){ - context::CDMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i ); + context::CDHashMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i ); if( it==nodeMap.end() ){ unsigned c = d_counter.get(); nodeMap[i] = c; diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h index a551d4a31..3cb3385dd 100644 --- a/src/util/trans_closure.h +++ b/src/util/trans_closure.h @@ -26,7 +26,7 @@ #include #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" namespace CVC4 { @@ -128,7 +128,7 @@ public: */ class TransitiveClosureNode : public TransitiveClosure{ context::CDO< unsigned > d_counter; - context::CDMap< Node, unsigned, NodeHashFunction > nodeMap; + context::CDHashMap< Node, unsigned, NodeHashFunction > nodeMap; //for debugging context::CDList< std::pair< Node, Node > > currEdges; public: diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index eb2caa98f..0358d1edd 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -18,7 +18,7 @@ #include -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdlist.h" using namespace std; @@ -43,7 +43,7 @@ public: } void testSimpleSequence() { - CDMap map(d_context); + CDHashMap map(d_context); TS_ASSERT(map.find(3) == map.end()); TS_ASSERT(map.find(5) == map.end()); @@ -188,7 +188,7 @@ public: // no intervening find() in this one // (under the theory that this could trigger a bug) void testSimpleSequenceFewerFinds() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -226,7 +226,7 @@ public: } void testObliterate() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -357,7 +357,7 @@ public: } void testObliteratePrimordial() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -460,7 +460,7 @@ public: } void testObliterateCurrent() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -566,7 +566,7 @@ public: } void testInsertAtContextLevelZero() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -739,7 +739,7 @@ public: } void testObliterateInsertedAtContextLevelZero() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -933,7 +933,7 @@ public: //Debug.on("gc"); //Debug.on("context"); - CDMap*, int_hasher> map(d_context); + CDHashMap*, int_hasher> map(d_context); CDList *list1, *list2, *list3, *list4; @@ -1026,7 +1026,7 @@ public: d_context->push(); // This re-uses context memory used above. the map.clear() - // triggers an emptyTrash() which fails if the CDOmaps are put + // triggers an emptyTrash() which fails if the CDOhash_maps are put // in the trash. (We use insertDataFromContextMemory() above to // keep them out of the trash.) cout << "allocating\n"; @@ -1059,7 +1059,7 @@ public: void testCmmElementsAtLevel0() { // this was crashing - CDMap map(d_context); + CDHashMap map(d_context); int* a = (int*)d_context->getCMM()->newData(sizeof(int)); map.insertDataFromContextMemory(1, a); } diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index 42f9b8563..db940f3ea 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -18,7 +18,7 @@ #include -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "util/Assert.h" using namespace std; @@ -40,7 +40,7 @@ public: } void testUnreachableSaveAndRestore() { - CDMap map(d_context); + CDHashMap map(d_context); TS_ASSERT_THROWS_NOTHING(map.makeCurrent()); diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h index 187b7dc08..0c14160f7 100644 --- a/test/unit/util/congruence_closure_white.h +++ b/test/unit/util/congruence_closure_white.h @@ -20,8 +20,8 @@ #include #include "context/context.h" -#include "context/cdset.h" -#include "context/cdmap.h" +#include "context/cdhashset.h" +#include "context/cdhashmap.h" #include "expr/node.h" #include "expr/kind.h" #include "expr/node_manager.h" @@ -34,8 +34,8 @@ using namespace std; struct MyOutputChannel { - CDSet d_notifications; - CDMap d_equivalences; + CDHashSet d_notifications; + CDHashMap d_equivalences; NodeManager* d_nm; MyOutputChannel(Context* ctxt, NodeManager* nm) : @@ -50,7 +50,7 @@ struct MyOutputChannel { } TNode find(TNode n) { - CDMap::iterator i = d_equivalences.find(n); + CDHashMap::iterator i = d_equivalences.find(n); if(i == d_equivalences.end()) { return n; } else {