From 88b52c971b43248e6ceacf1c8140a06427d0418d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 5 Mar 2010 08:26:37 +0000 Subject: * public/private code untangled (smt/smt_engine.h no longer #includes expr/node.h). This removes the warnings we had during compilation, and heads off a number of potential linking errors due to improper inlining of private (library-only) stuff in client (out-of-library) code. * "configure" now takes some options as part of a "bare-option" build type (e.g., "./configure debug-coverage" or "./configure production-muzzle"). * split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h * split cdlist_black unit test from context_black * implement CDMap<>. * give ExprManagers ownership of the context (and have SmtEngine share that one) * fix main driver to properly report file-not-found * fix MemoryMappedInputBuffer class to report reasons for "errno"-returned system errors * src/expr/attribute.h: context-dependent attribute kinds now supported * test/unit/expr/node_white.h: context-dependent attribute tests * src/prop/cnf_conversion.h and associated parts of src/util/options.h and src/main/getopt.cpp: obsolete command-line option, removed. * src/util/Assert.h: assertions are now somewhat more useful (in debug builds, anyway) during stack unwinding. * test/unit/theory/theory_black.h: test context-dependent behavior of registerTerm() attribute for theories * src/expr/node_builder.h: formatting, fixes for arithmetic convenience node builders, check memory allocations * test/unit/expr/node_builder_black.h: add tessts for addition, subtraction, unary minus, and multiplication convenience node builders * src/expr/attribute.h: more comments * (various) code formatting, comment cleanup, added throws specifier to some destructors * contrib/code-checker: prototype perl script to test (some) code policy * contrib/indent-settings: command line for GNU indent to indent using CVC4 style (sort of; this is a work in progress) * COPYING: legal stuff * DESIGN_QUESTIONS: obsolete, removed --- src/context/cdmap.h | 407 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 407 insertions(+) create mode 100644 src/context/cdmap.h (limited to 'src/context/cdmap.h') diff --git a/src/context/cdmap.h b/src/context/cdmap.h new file mode 100644 index 000000000..994ff76b4 --- /dev/null +++ b/src/context/cdmap.h @@ -0,0 +1,407 @@ +/********************* */ +/** cdmap.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. + ** + ** 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. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDMAP_H +#define __CVC4__CONTEXT__CDMAP_H + +#include "context/context.h" +#include "util/Assert.h" + +#include +#include + +namespace CVC4 { +namespace context { + +// Auxiliary class: almost the same as CDO (see cdo.h), but on +// setNull() call it erases itself from the map. + +template > class CDMap; + +template > +class CDOmap : public ContextObj { + Key d_key; + Data d_data; + bool d_inMap; // whether the data must be in the map + CDMap* d_cdmap; + + // 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) { + CDOmap* p((CDOmap*) 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); + } + + 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; + } + } + } + } + +public: + + CDOmap(Context* context, + CDMap* cdmap, + const Key& key, + const Data& data) : + ContextObj(context), + d_key(key), + d_inMap(false), + d_cdmap(cdmap) { + + set(data); + + CDOmap*& first = d_cdmap->d_first; + if(first == NULL) { + first = d_next = d_prev = this; + } else { + d_prev = first->d_prev; + d_next = first; + d_prev->d_next = first->d_prev = this; + } + } + + ~CDOmap() throw(AssertionException) {} + + void set(const Data& data) { + makeCurrent(); + d_data = data; + d_inMap = true; + } + + const Key& getKey() const { + return d_key; + } + + const Data& get() const { + return d_data; + } + + operator Data() { + return get(); + } + + CDOmap& operator=(const Data& data) { + set(data); + return *this; + } + + CDOmap* next() const { + if(d_next == d_cdmap->d_first) { + return NULL; + } else { + return d_next; + } + } +};/* class CDOmap */ + +// Dummy subclass of ContextObj to serve as our data class +class CDMapData : public ContextObj { + // befriend CDMap<> so that it can allocate us + template + friend class CDMap; + + ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDMapData(*this); + } + + void restore(ContextObj* data) {} + +public: + + CDMapData(Context* context) : ContextObj(context) {} + CDMapData(const ContextObj& co) : ContextObj(co) {} +}; + +/** + * 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 { + + friend class CDOmap; + + __gnu_cxx::hash_map*, HashFcn> d_map; + + // The vector of CDOmap objects to be destroyed + std::vector*> d_trash; + CDOmap* d_first; + Context* d_context; + + // 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*>::iterator + i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) { + /* + delete *i; + free(*i); + */ + } + d_trash.clear(); + } + +public: + + CDMap(Context* context) : + ContextObj(context), + d_first(NULL), + d_context(context) { + } + + ~CDMap() throw(AssertionException) { + // Delete all the elements and clear the map + for(typename __gnu_cxx::hash_map*, HashFcn>::iterator + i = d_map.begin(), iend = d_map.end(); i != iend; ++i) { + /* + delete (*i).second; + free((*i).second); + */ + } + d_map.clear(); + emptyTrash(); + } + + // The usual operators of map + + size_t size() const { + return d_map.size(); + } + + size_t count(const Key& k) const { + return d_map.count(k); + } + + typedef CDOmap& ElementReference; + + // If a key is not present, a new object is created and inserted + CDOmap& operator[](const Key& k) { + emptyTrash(); + + typename __gnu_cxx::hash_map*, HashFcn>::iterator + i(d_map.find(k)); + + CDOmap* obj; + if(i == d_map.end()) { // Create new object + obj = new(true) CDOmap(d_context, this, k, Data()); + d_map[k] = obj; + } else { + obj = (*i).second; + } + return *obj; + } + + void insert(const Key& k, const Data& d) { + emptyTrash(); + + typename __gnu_cxx::hash_map*, HashFcn>::iterator + i(d_map.find(k)); + + if(i == d_map.end()) { // Create new object + CDOmap* + obj(new(true) CDOmap(d_context, this, k, d)); + d_map[k] = obj; + } else { + (*i).second->set(d); + } + } + // FIXME: no erase(), too much hassle to implement efficiently... + + // Iterator for CDMap: points to pair&>; + // in most cases, this will be functionally similar to pair. + class iterator : public std::iterator, std::ptrdiff_t> { + + // Private members + typename __gnu_cxx::hash_map*, HashFcn>::const_iterator d_it; + + public: + + // Constructor from __gnu_cxx::hash_map + iterator(const typename __gnu_cxx::hash_map*, HashFcn>::const_iterator& i) : d_it(i) {} + + // Copy constructor + 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 { + const std::pair*>& p(*d_it); + return std::pair(p.first, *p.second); + } + + // Who needs an operator->() for maps anyway?... + // It'd be nice, but not possible by design. + //std::pair* operator->() const { + // return &(operator*()); + //} + + // Prefix and postfix increment + iterator& operator++() { + ++d_it; + 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) {} + std::pair& operator*() { + 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. + Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDMap<>::iterator */ + + typedef iterator const_iterator; + + iterator begin() const { + return iterator(d_map.begin()); + } + + iterator end() const { + return iterator(d_map.end()); + } + + class orderedIterator { + const CDOmap* d_it; + + public: + + orderedIterator(const CDOmap* p) : d_it(p) {} + orderedIterator(const orderedIterator& i) : d_it(i.d_it) {} + + // Default constructor + orderedIterator() {} + + // (Dis)equality + bool operator==(const orderedIterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const orderedIterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + std::pair operator*() const { + return std::pair(d_it->getKey(), d_it->get()); + } + + // Prefix and postfix increment + orderedIterator& 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) {} + + std::pair& operator*() { + return *d_pair; + } + };/* class CDMap<>::orderedIterator::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. + Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDMap<>::orderedIterator */ + + orderedIterator orderedBegin() const { + return orderedIterator(d_first); + } + + orderedIterator orderedEnd() const { + return orderedIterator(NULL); + } + + iterator find(const Key& k) const { + return iterator(d_map.find(k)); + } + +};/* class CDMap<> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDMAP_H */ -- cgit v1.2.3