From c8e9b1d6422b56476a2efb3fbaf19bce66de4c2b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 12 Mar 2010 23:52:14 +0000 Subject: [PATCH] * src/context/cdmap.h: rename orderedIterator to iterator, do away with old iterator (closes bug #47). * src/context/cdset.h: implemented. * src/expr/node_builder.h: fixed all the strict-aliasing warnings. * Remove Node::hash() and Expr::hash() (they had been aliases for getId()). There's now a NodeValue::internalHash(), for internal expr package purposes only, that doesn't depend on the ID. That's the only hashing of Nodes or Exprs. * Automake-quiet generation of kind.h, theoryof_table.h, and CVC and SMT parsers. * various minor code cleanups. --- configure.ac | 32 ++++--- src/context/cdlist.h | 102 +++++++++++++++++----- src/context/cdmap.h | 126 +++++++--------------------- src/context/cdo.h | 2 +- src/context/cdset.h | 96 ++++++++++++++++++++- src/context/context.h | 52 ++++++------ src/expr/Makefile.am | 2 +- src/expr/expr.cpp | 5 -- src/expr/expr.h | 6 -- src/expr/node.h | 10 +-- src/expr/node_builder.h | 91 ++++++++++++-------- src/expr/node_manager.cpp | 36 ++++---- src/expr/node_manager.h | 5 -- src/expr/node_value.cpp | 2 +- src/expr/node_value.h | 34 +++++--- src/main/getopt.cpp | 2 +- src/main/main.cpp | 6 +- src/parser/cvc/Makefile.am | 8 +- src/parser/smt/Makefile.am | 8 +- src/theory/Makefile.am | 2 +- test/unit/expr/node_black.h | 10 --- test/unit/expr/node_builder_black.h | 21 +++++ 22 files changed, 385 insertions(+), 273 deletions(-) diff --git a/configure.ac b/configure.ac index 3da3671a9..8cabfe98b 100644 --- a/configure.ac +++ b/configure.ac @@ -164,33 +164,41 @@ case "$with_build" in CVC4CPPFLAGS= CVC4CXXFLAGS=-O3 CVC4LDFLAGS= - if test -z "${enable_assertions+set}"; then enable_assertions=no ; fi - if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi - if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi + if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi + if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi + if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi + if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi ;; debug) # unoptimized, debug symbols, assertions, tracing CVC4CPPFLAGS=-DCVC4_DEBUG CVC4CXXFLAGS='-O0 -fno-inline -ggdb3' CVC4LDFLAGS= - if test -z "${enable_assertions+set}"; then enable_assertions=yes ; fi - if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi - if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi + if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi + if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi + if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi + if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi ;; default) # moderately optimized, assertions, tracing CVC4CPPFLAGS= CVC4CXXFLAGS=-O2 CVC4LDFLAGS= - if test -z "${enable_assertions+set}"; then enable_assertions=yes ; fi - if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi - if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi + if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi + if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi + if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi + if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi ;; competition) # maximally optimized, no assertions, no tracing, muzzled CVC4CPPFLAGS= CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs' CVC4LDFLAGS= - if test -z "${enable_assertions+set}"; then enable_assertions=no ; fi - if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi - if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi + if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi + if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi + if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi + if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi + if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi ;; *) AC_MSG_FAILURE([unknown build profile: $with_build]) diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 5b4ba639a..fd50d4149 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -56,6 +56,8 @@ class CDList : public ContextObj { */ unsigned d_sizeAlloc; +protected: + /** * Implementation of mandatory ContextObj method save: simply copies the * current size to a copy using the copy constructor (the pointer and the @@ -83,8 +85,10 @@ class CDList : public ContextObj { } } +private: + /** - * Privae copy constructor used only by save above. d_list and d_sizeAlloc + * Private 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. */ @@ -122,14 +126,18 @@ 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) { } + 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() { + ~CDList() throw(AssertionException) { if(d_list != NULL) { if(d_callDestructor) { while(d_size != 0) { @@ -144,26 +152,33 @@ public: /** * Return the current size of (i.e. valid number of objects in) the list */ - unsigned size() const { return d_size; } - + unsigned size() const { + return d_size; + } /** * Return true iff there are no valid objects in the list. */ - bool empty() const { return d_size == 0; } + 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(); + + if(d_size == d_sizeAlloc) { + grow(); + } + ::new((void*)(d_list + d_size)) T(data); - ++ d_size; + ++d_size; } /** - * operator[]: return the ith item in the list + * Access to the ith item in the list. */ const T& operator[](unsigned i) const { Assert(i < d_size, "index out of bounds in CDList::operator[]"); @@ -171,11 +186,11 @@ public: } /** - * return the most recent item added to the list + * Returns 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]; + return d_list[d_size - 1]; } /** @@ -186,19 +201,66 @@ public: * uninitialized list, as begin() and end() will have the same value (NULL). */ class const_iterator { - friend class CDList; T* d_it; - const_iterator(T* it) : d_it(it) {}; + + const_iterator(T* it) : d_it(it) {} + + friend class CDList; + 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; } + + inline bool operator==(const const_iterator& i) const { + return d_it == i.d_it; + } + + inline bool operator!=(const const_iterator& i) const { + return d_it != i.d_it; + } + + inline const T& operator*() const { + return *d_it; + } + /** Prefix increment */ - const_iterator& operator++() { ++d_it; return *this; } + const_iterator& operator++() { + ++d_it; + return *this; + } + /** Prefix decrement */ const_iterator& operator--() { --d_it; return *this; } - }; /* class const_iterator */ + + // Postfix operations on iterators: requires a Proxy object to + // hold the intermediate value for dereferencing + class Proxy { + const T* d_t; + + public: + + Proxy(const T& p): d_t(&p) {} + + T& operator*() { + return *d_t; + } + };/* class CDList<>::const_iterator::Proxy */ + + /** Postfix increment: returns Proxy with the old value. */ + Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + + /** Postfix decrement: returns Proxy with the old value. */ + Proxy operator--(int) { + Proxy e(*(*this)); + --(*this); + return e; + } + + };/* class CDList<>::const_iterator */ /** * Returns an iterator pointing to the first item in the list. diff --git a/src/context/cdmap.h b/src/context/cdmap.h index dc3448e52..b1bb47c4c 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -163,7 +163,8 @@ class CDMap : public ContextObj { friend class CDOmap; - __gnu_cxx::hash_map*, HashFcn> d_map; + typedef __gnu_cxx::hash_map*, HashFcn> table_type; + table_type d_map; // The vector of CDOmap objects to be destroyed std::vector*> d_trash; @@ -200,7 +201,7 @@ public: ~CDMap() throw(AssertionException) { // Delete all the elements and clear the map - for(typename __gnu_cxx::hash_map*, HashFcn>::iterator + for(typename table_type::iterator i = d_map.begin(), iend = d_map.end(); i != iend; ++i) { /* delete (*i).second; @@ -227,11 +228,10 @@ public: CDOmap& operator[](const Key& k) { emptyTrash(); - typename __gnu_cxx::hash_map*, HashFcn>::iterator - i(d_map.find(k)); + typename table_type::iterator i = d_map.find(k); CDOmap* obj; - if(i == d_map.end()) { // Create new object + if(i == d_map.end()) {// create new object obj = new(true) CDOmap(d_context, this, k, Data()); d_map[k] = obj; } else { @@ -243,8 +243,7 @@ public: void insert(const Key& k, const Data& d) { emptyTrash(); - typename __gnu_cxx::hash_map*, HashFcn>::iterator - i = d_map.find(k); + typename table_type::iterator i = d_map.find(k); if(i == d_map.end()) {// create new object CDOmap* @@ -257,19 +256,12 @@ public: // 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; + class iterator { + const CDOmap* 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 CDOmap* p) : d_it(p) {} iterator(const iterator& i) : d_it(i.d_it) {} // Default constructor @@ -283,82 +275,13 @@ public: 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++() { + // Prefix increment + iterator& operator++() { d_it = d_it->next(); return *this; } @@ -370,34 +293,41 @@ public: public: - Proxy(const std::pair& p): d_pair(&p) {} + Proxy(const std::pair& p) : d_pair(&p) {} - std::pair& operator*() { + const std::pair& operator*() const { return *d_pair; } - };/* class CDMap<>::orderedIterator::Proxy */ + };/* 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 orderedIterator. However, don't try to use // Proxy for anything else. - Proxy operator++(int) { + const Proxy operator++(int) { Proxy e(*(*this)); ++(*this); return e; } - };/* class CDMap<>::orderedIterator */ + };/* class CDMap<>::iterator */ + + typedef iterator const_iterator; - orderedIterator orderedBegin() const { - return orderedIterator(d_first); + iterator begin() const { + return iterator(d_first); } - orderedIterator orderedEnd() const { - return orderedIterator(NULL); + iterator end() const { + return iterator(NULL); } iterator find(const Key& k) const { - return iterator(d_map.find(k)); + typename table_type::const_iterator i = d_map.find(k); + if(i == d_map.end()) { + return end(); + } else { + return iterator((*i).second); + } } };/* class CDMap<> */ diff --git a/src/context/cdo.h b/src/context/cdo.h index 6c30a70f4..aca48d264 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -63,7 +63,7 @@ class CDO : public ContextObj { /** * operator= for CDO is private to ensure CDO object is not copied. */ - CDO& operator=(const CDO& cdo) {} + CDO& operator=(const CDO& cdo); public: /** diff --git a/src/context/cdset.h b/src/context/cdset.h index 48ad12daa..f51e689d5 100644 --- a/src/context/cdset.h +++ b/src/context/cdset.h @@ -24,8 +24,100 @@ namespace CVC4 { namespace context { -template -class CDSet; +template +class CDSet : protected CDMap { + typedef CDMap super; + +public: + + CDSet(Context* context) : + super(context) { + } + + size_t size() const { + return super::size(); + } + + size_t count(const V& v) const { + return super::count(v); + } + + void insert(const V& v) { + super::insert(v, v); + } + + // 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 */ diff --git a/src/context/context.h b/src/context/context.h index 4e10347d7..69e8fe776 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -134,23 +134,23 @@ public: */ void addNotifyObjPost(ContextNotifyObj* pCNO); -}; /* class Context */ - - /** - * Conceptually, a Scope encapsulates that portion of the context that - * changes after a call to push() and must be undone on a subsequent call to - * pop(). In particular, each call to push() creates a new Scope object . - * This new Scope object becomes the top scope and it points (via the - * d_pScopePrev member) to the previous top Scope. Each call to pop() - * deletes the current top scope and restores the previous one. The main - * purpose of a Scope is to maintain a linked list of ContexObj objects which - * change while the Scope is the top scope and which must be restored when - * the Scope is deleted. - * - * A Scope is also associated with a ContextMemoryManager. All memory - * allocated by the Scope is allocated in a single region using the - * ContextMemoryManager and released all at once when the Scope is popped. - */ +};/* class Context */ + +/** + * Conceptually, a Scope encapsulates that portion of the context that + * changes after a call to push() and must be undone on a subsequent call to + * pop(). In particular, each call to push() creates a new Scope object . + * This new Scope object becomes the top scope and it points (via the + * d_pScopePrev member) to the previous top Scope. Each call to pop() + * deletes the current top scope and restores the previous one. The main + * purpose of a Scope is to maintain a linked list of ContexObj objects which + * change while the Scope is the top scope and which must be restored when + * the Scope is deleted. + * + * A Scope is also associated with a ContextMemoryManager. All memory + * allocated by the Scope is allocated in a single region using the + * ContextMemoryManager and released all at once when the Scope is popped. + */ class Scope { /** @@ -432,14 +432,14 @@ public: };/* class ContextObj */ - /** - * For more flexible context-dependent behavior than that provided - * by ContextObj, objects may implement the ContextNotifyObj - * interface and simply get a notification when a pop has occurred. - * See Context class for how to register a ContextNotifyObj with the - * Context (you can choose to have notification come before or after - * the ContextObj objects have been restored). - */ +/** + * For more flexible context-dependent behavior than that provided by + * ContextObj, objects may implement the ContextNotifyObj interface + * and simply get a notification when a pop has occurred. See + * Context class for how to register a ContextNotifyObj with the + * Context (you can choose to have notification come before or after + * the ContextObj objects have been restored). + */ class ContextNotifyObj { /** * Context is our friend so that when the Context is deleted, any @@ -490,7 +490,7 @@ public: * implemented by the subclass. */ virtual void notify() = 0; -}; /* class ContextNotifyObj */ +};/* class ContextNotifyObj */ // Inline functions whose definitions had to be delayed: diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 3deed9a52..6d041814f 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -34,7 +34,7 @@ EXTRA_DIST = \ @srcdir@/kind.h: mkkind kind_prologue.h kind_middle.h kind_epilogue.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds chmod +x @srcdir@/mkkind - (@srcdir@/mkkind \ + $(AM_V_GEN)(@srcdir@/mkkind \ @srcdir@/kind_prologue.h \ @srcdir@/kind_middle.h \ @srcdir@/kind_epilogue.h \ diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index b6348394c..2f84f018b 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -81,11 +81,6 @@ bool Expr::operator<(const Expr& e) const { return *d_node < *e.d_node; } -size_t Expr::hash() const { - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - return (d_node->hash()); -} - Kind Expr::getKind() const { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); return d_node->getKind(); diff --git a/src/expr/expr.h b/src/expr/expr.h index 6c615d391..b297be6fb 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -91,12 +91,6 @@ public: */ operator bool() const; - /** - * Returns the hash value of the expression. Equal expression will have the - * same hash value. - */ - size_t hash() const; - /** * Returns the kind of the expression (AND, PLUS ...). * @return the kind of the expression diff --git a/src/expr/node.h b/src/expr/node.h index c1df399a1..d1bb8f3b3 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -218,14 +218,6 @@ public: */ bool isAtomic() const; - /** - * Returns the hash value of this node. - * @return the hash value - */ - size_t hash() const { - return d_nv->getId(); - } - /** * Returns the unique id of this node * @return the ud @@ -420,7 +412,7 @@ namespace CVC4 { // for hash_maps, hash_sets.. struct NodeHashFcn { size_t operator()(const CVC4::Node& node) const { - return (size_t) node.hash(); + return (size_t) node.getId(); } }; diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index a92c3a872..76307a525 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -421,9 +421,9 @@ protected: protected: - inline NodeBuilderBase(char* buf, unsigned maxChildren, + inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, Kind k = kind::UNDEFINED_KIND); - inline NodeBuilderBase(char* buf, unsigned maxChildren, + inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k = kind::UNDEFINED_KIND); private: @@ -575,24 +575,24 @@ public: */ class BackedNodeBuilder : public NodeBuilderBase { public: - inline BackedNodeBuilder(char* buf, unsigned maxChildren) : + inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren) : NodeBuilderBase(buf, maxChildren) { } - inline BackedNodeBuilder(char* buf, unsigned maxChildren, Kind k) : + inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, Kind k) : NodeBuilderBase(buf, maxChildren) { } - inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm) : + inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm) : NodeBuilderBase(buf, maxChildren) { } - inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) : + inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k) : NodeBuilderBase(buf, maxChildren) { } // we don't want a vtable, so do not declare a dtor! - //inline ~NodeBuilder(); + //inline ~BackedNodeBuilder(); private: // disallow copy or assignment (there would be no backing store!) @@ -610,13 +610,15 @@ private: * declarations are permitted. */ #define makeStackNodeBuilder(__v, __n) \ - size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n); \ - char __cvc4_backednodebuilder_buf__ ## __v \ - [ sizeof(NodeValue) + \ - sizeof(NodeValue*) * __cvc4_backednodebuilder_nchildren__ ## __v ] \ - __attribute__((aligned(__WORDSIZE / 8))); \ - BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \ - __cvc4_backednodebuilder_nchildren__ ## __v) + const size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n); \ + ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v[1 + (((sizeof(::CVC4::expr::NodeValue) + sizeof(::CVC4::expr::NodeValue*) + 1) / sizeof(::CVC4::expr::NodeValue*)) * __cvc4_backednodebuilder_nchildren__ ## __v)]; \ + ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \ + __cvc4_backednodebuilder_nchildren__ ## __v) +// IF THE ABOVE ASSERTION FAILS, write another compiler-specific +// version of makeStackNodeBuilder() that works for your compiler +// (even if it's suboptimal, ignoring its __n argument, and just +// creates a NodeBuilder<10>). + /** * Simple NodeBuilder interface. This is a template that requires @@ -626,9 +628,18 @@ private: */ template class NodeBuilder : public NodeBuilderBase > { - char d_backingStore[ sizeof(expr::NodeValue) - + (sizeof(expr::NodeValue*) * nchild_thresh) ] - __attribute__((aligned(__WORDSIZE / 8))); + // This is messy: + // 1. This (anonymous) struct here must be a POD to avoid the + // compiler laying out things in a different way. + // 2. The layout is engineered carefully. We can't just + // stack-allocate enough bytes as a char[] because we break + // strict-aliasing rules. The first thing in the struct is a + // "NodeValue" so a pointer to this struct should be safely + // castable to a pointer to a NodeValue (same alignment). + struct BackingStore { + expr::NodeValue n; + expr::NodeValue* c[nchild_thresh]; + } d_backingStore; typedef NodeBuilderBase > super; @@ -637,19 +648,31 @@ class NodeBuilder : public NodeBuilderBase > { public: inline NodeBuilder() : - NodeBuilderBase >(d_backingStore, nchild_thresh) { + NodeBuilderBase > + (reinterpret_cast(&d_backingStore), + nchild_thresh) { } inline NodeBuilder(Kind k) : - NodeBuilderBase >(d_backingStore, nchild_thresh, k) { + NodeBuilderBase > + (reinterpret_cast(&d_backingStore), + nchild_thresh, + k) { } inline NodeBuilder(NodeManager* nm) : - NodeBuilderBase >(d_backingStore, nchild_thresh, nm) { + NodeBuilderBase > + (reinterpret_cast(&d_backingStore), + nchild_thresh, + nm) { } inline NodeBuilder(NodeManager* nm, Kind k) : - NodeBuilderBase >(d_backingStore, nchild_thresh, nm, k) { + NodeBuilderBase > + (reinterpret_cast(&d_backingStore), + nchild_thresh, + nm, + k) { } // These implementations are identical, but we need to have both of @@ -657,20 +680,22 @@ public: // generalization of a copy constructor (and a default copy // constructor will be generated [?]) inline NodeBuilder(const NodeBuilder& nb) : - NodeBuilderBase >(d_backingStore, - nchild_thresh, - nb.d_nm, - nb.getKind()) { + NodeBuilderBase > + (reinterpret_cast(&d_backingStore), + nchild_thresh, + nb.d_nm, + nb.getKind()) { internalCopy(nb); } // technically this is a conversion, not a copy template inline NodeBuilder(const NodeBuilder& nb) : - NodeBuilderBase >(d_backingStore, - nchild_thresh, - nb.d_nm, - nb.getKind()) { + NodeBuilderBase > + (reinterpret_cast(&d_backingStore), + nchild_thresh, + nb.d_nm, + nb.getKind()) { internalCopy(nb); } @@ -1019,8 +1044,8 @@ inline NodeTemplate operator-(const NodeTemplate& a) { namespace CVC4 { template -inline NodeBuilderBase::NodeBuilderBase(char* buf, unsigned maxChildren, Kind k) : - d_inlineNv(*reinterpret_cast(buf)), +inline NodeBuilderBase::NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, Kind k) : + d_inlineNv(*buf), d_nv(&d_inlineNv), d_nm(NodeManager::currentNM()), d_inlineNvMaxChildren(maxChildren), @@ -1033,8 +1058,8 @@ inline NodeBuilderBase::NodeBuilderBase(char* buf, unsigned maxChildren } template -inline NodeBuilderBase::NodeBuilderBase(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) : - d_inlineNv(*reinterpret_cast(buf)), +inline NodeBuilderBase::NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k) : + d_inlineNv(*buf), d_nv(&d_inlineNv), d_nm(nm), d_inlineNvMaxChildren(maxChildren), diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 98171cb2e..7be593575 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -52,24 +52,6 @@ struct Reclaim { } }; -/** - * Reclaim a particular zombie. - */ -void NodeManager::reclaimZombie(expr::NodeValue* nv) { - Debug("gc") << "deleting node value " << nv - << " [" << nv->d_id << "]: " << nv->toString() << "\n"; - - if(nv->getKind() != kind::VARIABLE) { - poolRemove(nv); - } - - d_attrManager.deleteAllAttributes(nv); - - // dtor decr's ref counts of children - // FIXME: NOT ACTUALLY GARBAGE COLLECTING YET (DUE TO ISSUES WITH - // CDMAPs (?) ) delete nv; -} - void NodeManager::reclaimZombies() { // FIXME multithreading @@ -102,9 +84,25 @@ void NodeManager::reclaimZombies() { for(vector::iterator i = zombies.begin(); i != zombies.end(); ++i) { + NodeValue* nv = *i; + // collect ONLY IF still zero if((*i)->d_rc == 0) { - reclaimZombie(*i); + Debug("gc") << "deleting node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + + // remove from the pool + if(nv->getKind() != kind::VARIABLE) { + poolRemove(nv); + } + + // remove attributes + d_attrManager.deleteAllAttributes(nv); + + // decr ref counts of children + nv->decrRefCounts(); + //free(nv); +#warning NOT FREEING NODEVALUES } } } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 32c1cd210..b40ec2978 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -100,11 +100,6 @@ class NodeManager { */ void reclaimZombies(); - /** - * Reclaim a particular zombie. - */ - void reclaimZombie(expr::NodeValue* nv); - public: NodeManager(context::Context* ctxt) : diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 5dbfac169..7a4263d8a 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -28,7 +28,7 @@ namespace expr { size_t NodeValue::next_id = 1; -NodeValue NodeValue::s_null; +NodeValue NodeValue::s_null(0); string NodeValue::toString() const { stringstream ss; diff --git a/src/expr/node_value.h b/src/expr/node_value.h index a5f68babf..cbe4e718a 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -75,17 +75,13 @@ class NodeValue { unsigned d_nchildren : 16; /** Variable number of child nodes */ - NodeValue *d_children[0]; + NodeValue* d_children[0]; // todo add exprMgr ref in debug case template friend class CVC4::NodeTemplate; template friend class CVC4::NodeBuilderBase; - template friend class CVC4::NodeBuilder; - friend class CVC4::AndNodeBuilder; - friend class CVC4::OrNodeBuilder; - friend class CVC4::PlusNodeBuilder; - friend class CVC4::MultNodeBuilder; + template friend class CVC4::NodeBuilder; friend class CVC4::NodeManager; void inc(); @@ -93,11 +89,17 @@ class NodeValue { static size_t next_id; - /** Private default constructor for the null value. */ - NodeValue(); +public: + /** + * Uninitializing constructor for NodeBuilder's use. This is + * somewhat dangerous, but must also be public for the + * makeStackNodeBuilder() macro to work. + */ + NodeValue() { /* do not initialize! */ } - /** Destructor decrements the ref counts of its children */ - ~NodeValue(); +private: + /** Private constructor for the null value. */ + NodeValue(int); typedef NodeValue** nv_iterator; typedef NodeValue const* const* const_nv_iterator; @@ -136,6 +138,9 @@ class NodeValue { typedef std::input_iterator_tag iterator_category; }; + /** Decrement ref counts of children */ + inline void decrRefCounts(); + public: template @@ -211,6 +216,11 @@ public: static inline Kind dKindToKind(unsigned d) { return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } + + static inline const NodeValue& null() { + return s_null; + } + };/* class NodeValue */ /** @@ -242,14 +252,14 @@ struct NodeValueIDHashFcn { namespace CVC4 { namespace expr { -inline NodeValue::NodeValue() : +inline NodeValue::NodeValue(int) : d_id(0), d_rc(MAX_RC), d_kind(kind::NULL_EXPR), d_nchildren(0) { } -inline NodeValue::~NodeValue() { +inline void NodeValue::decrRefCounts() { for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { (*i)->dec(); } diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index b319b7293..df94ef9ab 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -107,7 +107,7 @@ const char *progPath; const char *progName; /** Parse argc/argv and put the result into a CVC4::Options struct. */ -int parseOptions(int argc, char** argv, CVC4::Options* opts) +int parseOptions(int argc, char* argv[], CVC4::Options* opts) throw(OptionException) { progPath = progName = argv[0]; int c; diff --git a/src/main/main.cpp b/src/main/main.cpp index 1da56b9f9..f5e53f34a 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -39,7 +39,7 @@ using namespace CVC4::main; static Result lastResult; static struct Options options; -int runCvc4(int argc, char *argv[]); +int runCvc4(int argc, char* argv[]); void doCommand(SmtEngine&, Command*); /** @@ -49,7 +49,7 @@ void doCommand(SmtEngine&, Command*); * problems. That's why main() wraps runCvc4() in the first place. * Put everything in runCvc4(). */ -int main(int argc, char *argv[]) { +int main(int argc, char* argv[]) { try { return runCvc4(argc, argv); } catch(OptionException& e) { @@ -80,7 +80,7 @@ int main(int argc, char *argv[]) { } } -int runCvc4(int argc, char *argv[]) { +int runCvc4(int argc, char* argv[]) { // Initialize the signal handlers cvc4_init(); diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index ad0eb70d8..c1b5f752e 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -38,14 +38,14 @@ maintainer-clean-local: touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated - -rm -f $(ANTLR_LEXER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g" + $(AM_V_at)-rm -f $(ANTLR_LEXER_STUFF) + $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g" @srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp # doesn't actually depend on the lexer, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules # from running in parallel (since the token files will be deleted & # recreated) @srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated - -rm -f $(ANTLR_PARSER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g" + $(AM_V_at)-rm -f $(ANTLR_PARSER_STUFF) + $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g" @srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 96ad9c27f..7fe235002 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -38,14 +38,14 @@ maintainer-clean-local: touch @srcdir@/stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/AntlrSmtLexer.hpp: smt_lexer.g @srcdir@/stamp-generated - -rm -f $(ANTLR_LEXER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g" + $(AM_V_at)-rm -f $(ANTLR_LEXER_STUFF) + $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g" @srcdir@/generated/AntlrSmtLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrSmtLexer.hpp # doesn't actually depend on the lexer, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules # from running in parallel (since the token files will be deleted & # recreated) @srcdir@/generated/AntlrSmtParser.hpp: smt_parser.g smt_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated - -rm -f $(ANTLR_PARSER_STUFF) - $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g" + $(AM_V_at)-rm -f $(ANTLR_PARSER_STUFF) + $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g" @srcdir@/generated/AntlrSmtParser.cpp: @srcdir@/generated/AntlrSmtParser.hpp diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index d71ae842f..43ed0574a 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -27,7 +27,7 @@ EXTRA_DIST = \ @srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_prologue.h theoryof_table_middle.h theoryof_table_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds chmod +x @srcdir@/mktheoryof - (@srcdir@/mktheoryof \ + $(AM_V_GEN)(@srcdir@/mktheoryof \ @srcdir@/theoryof_table_prologue.h \ @srcdir@/theoryof_table_middle.h \ @srcdir@/theoryof_table_epilogue.h \ diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 96f02c489..c1ece1145 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -258,16 +258,6 @@ public: } - void testHash() { - /* Not sure how to test this except survial... */ - Node a = d_nodeManager->mkNode(ITE); - Node b = d_nodeManager->mkNode(ITE); - - TS_ASSERT(b.hash() == a.hash()); - } - - - void testEqNode() { /*Node eqNode(const Node& right) const;*/ diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index ab3c1c842..46e524f59 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -647,4 +647,25 @@ public: TS_ASSERT_EQUALS(Node(- a + b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), b)); TS_ASSERT_EQUALS(Node(- a * b), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, a), b)); } + + /** + * This tests the "stack builder" + */ + void testStackBuilder() { + try { + for(unsigned i = 0; i < 100; ++i) { + size_t n = 1 + (rand() % 50); + + // make a builder "b" with a backing store for n children + makeStackNodeBuilder(b, n); + + // build one-past-the-end + for(size_t j = 0; j <= n; ++j) { + b << Node::null(); + } + } + } catch(Exception e) { + std::cout << e; + } + } }; -- 2.30.2