#include "context/context.h"
#include "util/Assert.h"
+#include <vector>
#include <iterator>
#include <ext/hash_map>
namespace CVC4 {
namespace context {
-// Auxiliary class: almost the same as CDO (see cdo.h), but on
-// setNull() call it erases itself from the map.
+// Auxiliary class: almost the same as CDO (see cdo.h)
template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
+template <class T, class U>
+inline std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
+ return out << "[" << p.first << "," << p.second << "]";
+}
+
template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
class CDOmap : public ContextObj {
Key d_key;
Data d_data;
- bool d_inMap; // whether the data must be in the map
- CDMap<Key, Data, HashFcn>* d_cdmap;
+ CDMap<Key, Data, HashFcn>* d_map;
// Doubly-linked list for keeping track of elements in order of insertion
- CDOmap<Key, Data, HashFcn>* d_prev;
- CDOmap<Key, Data, HashFcn>* d_next;
+ CDOmap* d_prev;
+ CDOmap* d_next;
virtual ContextObj* save(ContextMemoryManager* pCMM) {
- return new(pCMM) CDOmap<Key, Data, HashFcn>(*this);
+ return new(pCMM) CDOmap(*this);
}
virtual void restore(ContextObj* data) {
- CDOmap<Key, Data, HashFcn>* p((CDOmap<Key, Data, HashFcn>*) data);
- if(p->d_inMap) {
- d_data = p->d_data;
- d_inMap = true;
- } else {
- // Erase itself from the map and put itself into trash. We cannot
- // "delete this" here, because it will break context operations in
- // a non-trivial way.
- if(d_cdmap->d_map.count(d_key) > 0) {
- d_cdmap->d_map.erase(d_key);
- d_cdmap->d_trash.push_back(this);
+ CDOmap* p = static_cast<CDOmap*>(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) {
+ d_map->d_first = d_next;
}
-
- d_prev->d_next = d_next;
d_next->d_prev = d_prev;
-
- if(d_cdmap->d_first == this) {
- d_cdmap->d_first = d_next;
-
- if(d_next == this) {
- d_cdmap->d_first = NULL;
- }
- }
+ d_prev->d_next = d_next;
+ d_map->d_trash.push_back(this);
+ } else {
+ d_data = p->d_data;
}
}
public:
CDOmap(Context* context,
- CDMap<Key, Data, HashFcn>* cdmap,
+ CDMap<Key, Data, HashFcn>* map,
const Key& key,
const Data& data) :
ContextObj(context),
d_key(key),
- d_inMap(false),
- d_cdmap(cdmap) {
+ d_map(NULL) {
+ // makeCurrent(), then set the data and then 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.
set(data);
+ d_map = map;
- CDOmap<Key, Data, HashFcn>*& first = d_cdmap->d_first;
+ CDOmap*& first = d_map->d_first;
if(first == NULL) {
first = d_next = d_prev = this;
} else {
}
}
- ~CDOmap() throw(AssertionException) { destroy(); }
+ ~CDOmap() throw(AssertionException) {
+ destroy();
+ }
void set(const Data& data) {
makeCurrent();
d_data = data;
- d_inMap = true;
}
const Key& getKey() const {
return get();
}
- CDOmap<Key, Data, HashFcn>& operator=(const Data& data) {
+ CDOmap& operator=(const Data& data) {
set(data);
return *this;
}
- CDOmap<Key, Data, HashFcn>* next() const {
- if(d_next == d_cdmap->d_first) {
+ CDOmap* next() const {
+ if(d_next == d_map->d_first) {
return NULL;
} else {
return d_next;
}
}
-};/* class CDOmap */
+};/* class CDOmap<> */
// Dummy subclass of ContextObj to serve as our data class
class CDMapData : public ContextObj {
CDMapData(Context* context) : ContextObj(context) {}
CDMapData(const ContextObj& co) : ContextObj(co) {}
+ ~CDMapData() { destroy(); }
};
/**
template <class Key, class Data, class HashFcn>
class CDMap : public ContextObj {
+ typedef CDOmap<Key, Data, HashFcn> Element;
+ typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+
friend class CDOmap<Key, Data, HashFcn>;
- typedef __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> table_type;
table_type d_map;
- // The vector of CDOmap objects to be destroyed
- std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
- CDOmap<Key, Data, HashFcn>* d_first;
+ Element* d_first;
Context* d_context;
+ std::vector<Element*> d_trash;
+
// Nothing to save; the elements take care of themselves
virtual ContextObj* save(ContextMemoryManager* pCMM) {
return new(pCMM) CDMapData(*this);
// Similarly, nothing to restore
virtual void restore(ContextObj* data) {}
- // Destroy stale CDOmap objects from trash
void emptyTrash() {
- for(typename std::vector<CDOmap<Key, Data, HashFcn>*>::iterator
- i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) {
- /*
- delete *i;
- free(*i);
- */
+ //FIXME multithreading
+ for(typename std::vector<Element*>::iterator i = d_trash.begin();
+ i != d_trash.end();
+ ++i) {
+ (*i)->deleteSelf();
}
d_trash.clear();
}
CDMap(Context* context) :
ContextObj(context),
d_first(NULL),
- d_context(context) {
+ d_context(context),
+ d_trash() {
}
~CDMap() throw(AssertionException) {
- // Delete all the elements and clear the map
- /*for(typename table_type::iterator
- i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
-
- delete (*i).second;
- free((*i).second);
-
- }*/
- d_map.clear();
+ destroy();
+ for(typename table_type::iterator i = d_map.begin();
+ i != d_map.end();
+ ++i) {
+ (*i).second->deleteSelf();
+ }
+ //d_map.clear();
+ Debug("gc") << "cdmap gone, emptying trash" << std::endl;
emptyTrash();
}
return d_map.count(k);
}
- typedef CDOmap<Key, Data, HashFcn>& ElementReference;
-
// If a key is not present, a new object is created and inserted
- CDOmap<Key, Data, HashFcn>& operator[](const Key& k) {
+ Element& operator[](const Key& k) {
emptyTrash();
typename table_type::iterator i = d_map.find(k);
- CDOmap<Key, Data, HashFcn>* obj;
+ Element* obj;
if(i == d_map.end()) {// create new object
- obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data());
+ obj = new(true) Element(d_context, this, k, Data());
d_map[k] = obj;
} else {
obj = (*i).second;
typename table_type::iterator i = d_map.find(k);
if(i == d_map.end()) {// create new object
- CDOmap<Key, Data, HashFcn>*
- obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d);
+ Element* obj = new(true) Element(d_context, this, k, d);
d_map[k] = obj;
} else {
(*i).second->set(d);
// 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->~CDOmap();
+
+ 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;
+ d_map.erase(j);//FIXME multithreading
+ // was already destructed, so don't call ->deleteSelf()
+ ::operator delete(elt);
+ }
+ }
+ }
+
class iterator {
- const CDOmap<Key, Data, HashFcn>* d_it;
+ const Element* d_it;
public:
- iterator(const CDOmap<Key, Data, HashFcn>* p) : d_it(p) {}
+ iterator(const Element* p) : d_it(p) {}
iterator(const iterator& i) : d_it(i.d_it) {}
// Default constructor
// 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
+ // then advance the iterator. However, don't try to use
// Proxy for anything else.
const Proxy operator++(int) {
Proxy e(*(*this));
iterator find(const Key& k) const {
typename table_type::const_iterator i = d_map.find(k);
+
if(i == d_map.end()) {
return end();
} else {
}
}
+ iterator find(const Key& k) {
+ emptyTrash();
+ return const_cast<const CDMap*>(this)->find(k);
+ }
+
};/* class CDMap<> */
}/* CVC4::context namespace */
void ContextObj::destroy() throw(AssertionException) {
for(;;) {
+ // If valgrind reports invalid writes on the next few lines,
+ // here's a hint: make sure all classes derived from ContextObj in
+ // the system properly call destroy() in their destructors.
+ // That's needed to maintain this linked list properly.
if(next() != NULL) {
next()->prev() = prev();
}
deleteFromTable(d_ptrs, nv);
// FIXME CD-bools in optimized table
- /*
for(unsigned id = 0; id < attr::LastAttributeId<bool, true>::s_id; ++id) {
- d_cdbools.erase(std::make_pair(id, nv));
+ Debug("gc") << "looking for " << id << " x " << nv << ":" << *nv << std::endl;
+ d_cdbools.obliterate(std::make_pair(id, nv));
}
for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, true>::s_id; ++id) {
- d_cdints.erase(std::make_pair(id, nv));
+ d_cdints.obliterate(std::make_pair(id, nv));
}
for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) {
- d_cdexprs.erase(std::make_pair(id, nv));
+ d_cdexprs.obliterate(std::make_pair(id, nv));
}
for(unsigned id = 0; id < attr::LastAttributeId<std::string, true>::s_id; ++id) {
- d_cdstrings.erase(std::make_pair(id, nv));
+ d_cdstrings.obliterate(std::make_pair(id, nv));
}
for(unsigned id = 0; id < attr::LastAttributeId<void*, true>::s_id; ++id) {
- d_cdptrs.erase(std::make_pair(id, nv));
+ d_cdptrs.obliterate(std::make_pair(id, nv));
}
- */
}
}/* CVC4::expr::attr namespace */
/** Make a function type from domain to range.
* TODO: Function types should be unique for this manager. */
-FunctionType* NodeManager::mkFunctionType(Type* domain,
- Type* range) const {
+inline FunctionType* NodeManager::mkFunctionType(Type* domain,
+ Type* range) const {
std::vector<Type*> argTypes;
argTypes.push_back(domain);
return new FunctionType(argTypes, range);
/** Make a function type with input types from argTypes.
* TODO: Function types should be unique for this manager. */
-FunctionType* NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
- Type* range) const {
+inline FunctionType*
+NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
+ Type* range) const {
Assert( argTypes.size() > 0 );
return new FunctionType(argTypes, range);
}
-Type* NodeManager::mkSort(const std::string& name) const {
+inline Type* NodeManager::mkSort(const std::string& name) const {
return new SortType(name);
}
}
Type::Type(std::string name) :
- d_name(name) {
+ d_name(name),
+ d_rc(0) {
}
std::string Type::getName() const {
*/
ECData(context::Context* context, TNode n);
- ~ECData() { Debug("ufgc") << "Calling ECData destructor" << std::endl;}
+ ~ECData() {
+ Debug("ufgc") << "Calling ECData destructor" << std::endl;
+ destroy();
+ }
/**
* An ECData takes over the watch list of another ECData.
parser/parser_black \
context/context_black \
context/context_mm_black \
+ context/cdo_black \
context/cdlist_black \
+ context/cdmap_black \
theory/theory_black \
theory/theory_uf_white \
util/assert_white \
util/configuration_white \
- util/output_white \
- util/integer_black \
- util/integer_white \
- util/rational_white
+ util/output_white
+# util/integer_black \
+# util/integer_white \
+# util/rational_white
# Things that aren't tests but that tests rely on and need to
# go into the distribution
--- /dev/null
+/********************* */
+/** cdmap_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Black box testing of CVC4::context::CDMap<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/cdmap.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDMapBlack : public CxxTest::TestSuite {
+
+ Context* d_context;
+
+public:
+
+ void setUp() {
+ d_context = new Context;
+ //Debug.on("cdmap");
+ }
+
+ void tearDown() {
+ delete d_context;
+ }
+
+ void testSimpleSequence() {
+ CDMap<int, int> map(d_context);
+
+ map.insert(3, 4);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ map.insert(1, 2);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ map.insert(1, 45);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+ }
+
+ // no intervening find() in this one
+ // (under the theory that this could trigger a bug)
+ void testSimpleSequenceFewerFinds() {
+ CDMap<int, int> map(d_context);
+
+ map.insert(3, 4);
+
+ {
+ d_context->push();
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+
+ {
+ d_context->push();
+
+ map.insert(1, 2);
+
+ TS_ASSERT(map.find(1) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(7) == map.end());
+
+ {
+ d_context->push();
+
+ d_context->pop();
+ }
+
+ d_context->pop();
+ }
+
+ d_context->pop();
+ }
+ }
+
+ void testObliterate() {
+ CDMap<int, int> map(d_context);
+
+ map.insert(3, 4);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ map.insert(1, 2);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ map.obliterate(5);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+ }
+
+ void testObliteratePrimordial() {
+ CDMap<int, int> map(d_context);
+
+ map.insert(3, 4);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ map.insert(1, 2);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ map.obliterate(3);
+
+ TS_ASSERT(map.find(3) == map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) == map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) == map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) == map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) == map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+ }
+
+ void testObliterateCurrent() {
+ CDMap<int, int> map(d_context);
+
+ map.insert(3, 4);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ map.insert(1, 2);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) != map.end());
+
+ map.obliterate(1);
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ {
+ d_context->push();
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) != map.end());
+ TS_ASSERT(map.find(9) != map.end());
+ TS_ASSERT(map.find(1) == map.end());
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(map.find(3) != map.end());
+ TS_ASSERT(map.find(5) == map.end());
+ TS_ASSERT(map.find(9) == map.end());
+ TS_ASSERT(map.find(1) == map.end());
+ }
+};
--- /dev/null
+/********************* */
+/** cdo_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Black box testing of CVC4::context::CDO<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <vector>
+#include <iostream>
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDOBlack : public CxxTest::TestSuite {
+private:
+
+ Context* d_context;
+
+public:
+
+ void setUp() {
+ d_context = new Context;
+ }
+
+ void tearDown() {
+ delete d_context;
+ }
+
+ void testIntCDO() {
+ // Test that push/pop maintains the original value
+ CDO<int> a1(d_context);
+ a1 = 5;
+ TS_ASSERT(d_context->getLevel() == 0);
+ d_context->push();
+ a1 = 10;
+ TS_ASSERT(d_context->getLevel() == 1);
+ TS_ASSERT(a1 == 10);
+ d_context->pop();
+ TS_ASSERT(d_context->getLevel() == 0);
+ TS_ASSERT(a1 == 5);
+ }
+};
delete d_context;
}
- void testIntCDO() {
- // Test that push/pop maintains the original value
- CDO<int> a1(d_context);
- a1 = 5;
- TS_ASSERT(d_context->getLevel() == 0);
- d_context->push();
- a1 = 10;
- TS_ASSERT(d_context->getLevel() == 1);
- TS_ASSERT(a1 == 10);
- d_context->pop();
- TS_ASSERT(d_context->getLevel() == 0);
- TS_ASSERT(a1 == 5);
- }
-
void testContextPushPop() {
// Test what happens when the context is popped below 0
// the interface doesn't declare any exceptions
projects / cvc5.git / commitdiff