diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
commit | 88b52c971b43248e6ceacf1c8140a06427d0418d (patch) | |
tree | 4ee443c898a858fcdd658f3f043e4180eddd8784 /src/context/cdlist.h | |
parent | 29cc307cdf2c42bebf4f5615874a864783f47fd0 (diff) |
* 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
Diffstat (limited to 'src/context/cdlist.h')
-rw-r--r-- | src/context/cdlist.h | 222 |
1 files changed, 222 insertions, 0 deletions
diff --git a/src/context/cdlist.h b/src/context/cdlist.h new file mode 100644 index 000000000..5b4ba639a --- /dev/null +++ b/src/context/cdlist.h @@ -0,0 +1,222 @@ +/********************* */ +/** cdlist.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 list class. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDLIST_H +#define __CVC4__CONTEXT__CDLIST_H + +#include "context/context.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +/** + * Generic context-dependent dynamic array. Note that for efficiency, this + * implementation makes the following assumptions: + * 1. Over time, objects are only added to the list. Objects are only + * removed when a pop restores the list to a previous state. + * 2. T objects can safely be copied using their copy constructor, + * operator=, and memcpy. + */ +template <class T> +class CDList : public ContextObj { + /** + * d_list is a dynamic array of objects of type T. + */ + T* d_list; + + /** + * Whether to call the destructor when items are popped from the + * list. True by default, but can be set to false by setting the + * second argument in the constructor to false. + */ + bool d_callDestructor; + + /** + * Number of objects in d_list + */ + unsigned d_size; + + /** + * Allocated size of d_list. + */ + unsigned d_sizeAlloc; + + /** + * Implementation of mandatory ContextObj method save: simply copies the + * current size to a copy using the copy constructor (the pointer and the + * allocated size are *not* copied as they are not restored on a pop). + * The saved information is allocated using the ContextMemoryManager. + */ + ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDList<T>(*this); + } + + /** + * Implementation of mandatory ContextObj method restore: simply restores the + * previous size. Note that the list pointer and the allocated size are not + * changed. + */ + void restore(ContextObj* data) { + if(d_callDestructor) { + unsigned size = ((CDList<T>*)data)->d_size; + while(d_size != size) { + --d_size; + d_list[d_size].~T(); + } + } else { + d_size = ((CDList<T>*)data)->d_size; + } + } + + /** + * Privae copy constructor used only by save above. d_list and d_sizeAlloc + * are not copied: only the base class information and d_size are needed in + * restore. + */ + CDList(const CDList<T>& l) : + ContextObj(l), + d_list(NULL), + d_size(l.d_size), + d_sizeAlloc(0) { + } + + /** + * Reallocate the array with more space. + * Throws bad_alloc if memory allocation fails. + */ + void grow() { + if(d_list == NULL) { + // Allocate an initial list if one does not yet exist + d_sizeAlloc = 10; + d_list = (T*) malloc(sizeof(T) * d_sizeAlloc); + if(d_list == NULL) { + throw std::bad_alloc(); + } + } else { + // Allocate a new array with double the size + d_sizeAlloc *= 2; + T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc); + if(tmpList == NULL) { + throw std::bad_alloc(); + } + d_list = tmpList; + } + } + +public: + /** + * Main constructor: d_list starts as NULL, size is 0 + */ + CDList(Context* context, bool callDestructor = true) + : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor), + d_size(0), d_sizeAlloc(0) { } + + /** + * Destructor: delete the list + */ + ~CDList() throw() { + if(d_list != NULL) { + if(d_callDestructor) { + while(d_size != 0) { + --d_size; + d_list[d_size].~T(); + } + } + free(d_list); + } + } + + /** + * Return the current size of (i.e. valid number of objects in) the list + */ + unsigned size() const { return d_size; } + + + /** + * Return true iff there are no valid objects in the list. + */ + bool empty() const { return d_size == 0; } + + /** + * Add an item to the end of the list. + */ + void push_back(const T& data) { + makeCurrent(); + if(d_size == d_sizeAlloc) grow(); + ::new((void*)(d_list + d_size)) T(data); + ++ d_size; + } + + /** + * operator[]: return the ith item in the list + */ + const T& operator[](unsigned i) const { + Assert(i < d_size, "index out of bounds in CDList::operator[]"); + return d_list[i]; + } + + /** + * return the most recent item added to the list + */ + const T& back() const { + Assert(d_size > 0, "CDList::back() called on empty list"); + return d_list[d_size-1]; + } + + /** + * Iterator for CDList class. It has to be const because we don't allow + * items in the list to be changed. It's a straightforward wrapper around a + * pointer. Note that for efficiency, we implement only prefix increment and + * decrement. Also note that it's OK to create an iterator from an empty, + * uninitialized list, as begin() and end() will have the same value (NULL). + */ + class const_iterator { + friend class CDList<T>; + T* d_it; + const_iterator(T* it) : d_it(it) {}; + public: + const_iterator() : d_it(NULL) {} + bool operator==(const const_iterator& i) const { return d_it == i.d_it; } + bool operator!=(const const_iterator& i) const { return d_it != i.d_it; } + const T& operator*() const { return *d_it; } + /** Prefix increment */ + const_iterator& operator++() { ++d_it; return *this; } + /** Prefix decrement */ + const_iterator& operator--() { --d_it; return *this; } + }; /* class const_iterator */ + + /** + * Returns an iterator pointing to the first item in the list. + */ + const_iterator begin() const { + return const_iterator(d_list); + } + + /** + * Returns an iterator pointing one past the last item in the list. + */ + const_iterator end() const { + return const_iterator(d_list + d_size); + } + +};/* class CDList */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDLIST_H */ |