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.
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])
*/
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
}
}
+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.
*/
/**
* 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) {
/**
* 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[]");
}
/**
- * 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];
}
/**
* 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) {};
+
+ const_iterator(T* it) : d_it(it) {}
+
+ friend class CDList<T>;
+
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.
friend class CDOmap<Key, Data, HashFcn>;
- __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> d_map;
+ 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;
~CDMap() throw(AssertionException) {
// Delete all the elements and clear the map
- for(typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
+ for(typename table_type::iterator
i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
/*
delete (*i).second;
CDOmap<Key, Data, HashFcn>& operator[](const Key& k) {
emptyTrash();
- typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
- i(d_map.find(k));
+ typename table_type::iterator i = d_map.find(k);
CDOmap<Key, Data, HashFcn>* obj;
- if(i == d_map.end()) { // Create new object
+ if(i == d_map.end()) {// create new object
obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data());
d_map[k] = obj;
} else {
void insert(const Key& k, const Data& d) {
emptyTrash();
- typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, 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<Key, Data, HashFcn>*
// FIXME: no erase(), too much hassle to implement efficiently...
- // Iterator for CDMap: points to pair<const Key, CDOMap<Key, Data, HashFcn>&>;
- // in most cases, this will be functionally similar to pair<const Key, Data>.
- class iterator : public std::iterator<std::input_iterator_tag, std::pair<const Key, Data>, std::ptrdiff_t> {
-
- // Private members
- typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator d_it;
+ class iterator {
+ const CDOmap<Key, Data, HashFcn>* d_it;
public:
- // Constructor from __gnu_cxx::hash_map
- iterator(const typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator& i) : d_it(i) {}
-
- // Copy constructor
+ iterator(const CDOmap<Key, Data, HashFcn>* p) : d_it(p) {}
iterator(const iterator& i) : d_it(i.d_it) {}
// Default constructor
return d_it != i.d_it;
}
- // Dereference operators.
- std::pair<const Key, Data> operator*() const {
- const std::pair<const Key, CDOmap<Key, Data, HashFcn>*>& p(*d_it);
- return std::pair<const Key, Data>(p.first, *p.second);
- }
-
- // Who needs an operator->() for maps anyway?...
- // It'd be nice, but not possible by design.
- //std::pair<const Key, Data>* 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<const Key, Data>* d_pair;
- public:
- Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {}
- std::pair<const Key, Data>& 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<Key, Data, HashFcn>* d_it;
-
- public:
-
- orderedIterator(const CDOmap<Key, Data, HashFcn>* 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<const Key, Data> operator*() const {
return std::pair<const Key, Data>(d_it->getKey(), d_it->get());
}
- // Prefix and postfix increment
- orderedIterator& operator++() {
+ // Prefix increment
+ iterator& operator++() {
d_it = d_it->next();
return *this;
}
public:
- Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {}
+ Proxy(const std::pair<const Key, Data>& p) : d_pair(&p) {}
- std::pair<const Key, Data>& operator*() {
+ const std::pair<const Key, Data>& 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<> */
/**
* operator= for CDO is private to ensure CDO object is not copied.
*/
- CDO<T>& operator=(const CDO<T>& cdo) {}
+ CDO<T>& operator=(const CDO<T>& cdo);
public:
/**
namespace CVC4 {
namespace context {
-template <class K, class HashFcn>
-class CDSet;
+template <class V, class HashFcn>
+class CDSet : protected CDMap<V, V, HashFcn> {
+ typedef CDMap<V, V, HashFcn> 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 */
*/
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 {
/**
};/* 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
* implemented by the subclass.
*/
virtual void notify() = 0;
-}; /* class ContextNotifyObj */
+};/* class ContextNotifyObj */
// Inline functions whose definitions had to be delayed:
@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 \
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();
*/
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
*/
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
// 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();
}
};
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:
*/
class BackedNodeBuilder : public NodeBuilderBase<BackedNodeBuilder> {
public:
- inline BackedNodeBuilder(char* buf, unsigned maxChildren) :
+ inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren) :
NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
}
- inline BackedNodeBuilder(char* buf, unsigned maxChildren, Kind k) :
+ inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, Kind k) :
NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
}
- inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm) :
+ inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm) :
NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
}
- inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+ inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
NodeBuilderBase<BackedNodeBuilder>(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!)
* 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
*/
template <unsigned nchild_thresh = default_nchild_thresh>
class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > {
- 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<NodeBuilder<nchild_thresh> > super;
public:
inline NodeBuilder() :
- NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh) {
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >
+ (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+ nchild_thresh) {
}
inline NodeBuilder(Kind k) :
- NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, k) {
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >
+ (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+ nchild_thresh,
+ k) {
}
inline NodeBuilder(NodeManager* nm) :
- NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, nm) {
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >
+ (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+ nchild_thresh,
+ nm) {
}
inline NodeBuilder(NodeManager* nm, Kind k) :
- NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, nm, k) {
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >
+ (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+ nchild_thresh,
+ nm,
+ k) {
}
// These implementations are identical, but we need to have both of
// generalization of a copy constructor (and a default copy
// constructor will be generated [?])
inline NodeBuilder(const NodeBuilder& nb) :
- NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore,
- nchild_thresh,
- nb.d_nm,
- nb.getKind()) {
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >
+ (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+ nchild_thresh,
+ nb.d_nm,
+ nb.getKind()) {
internalCopy(nb);
}
// technically this is a conversion, not a copy
template <unsigned N>
inline NodeBuilder(const NodeBuilder<N>& nb) :
- NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore,
- nchild_thresh,
- nb.d_nm,
- nb.getKind()) {
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >
+ (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
+ nchild_thresh,
+ nb.d_nm,
+ nb.getKind()) {
internalCopy(nb);
}
namespace CVC4 {
template <class Builder>
-inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren, Kind k) :
- d_inlineNv(*reinterpret_cast<expr::NodeValue*>(buf)),
+inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, Kind k) :
+ d_inlineNv(*buf),
d_nv(&d_inlineNv),
d_nm(NodeManager::currentNM()),
d_inlineNvMaxChildren(maxChildren),
}
template <class Builder>
-inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
- d_inlineNv(*reinterpret_cast<expr::NodeValue*>(buf)),
+inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+ d_inlineNv(*buf),
d_nv(&d_inlineNv),
d_nm(nm),
d_inlineNvMaxChildren(maxChildren),
}
};
-/**
- * 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
for(vector<NodeValue*>::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
}
}
}
*/
void reclaimZombies();
- /**
- * Reclaim a particular zombie.
- */
- void reclaimZombie(expr::NodeValue* nv);
-
public:
NodeManager(context::Context* ctxt) :
size_t NodeValue::next_id = 1;
-NodeValue NodeValue::s_null;
+NodeValue NodeValue::s_null(0);
string NodeValue::toString() const {
stringstream ss;
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 <bool> friend class CVC4::NodeTemplate;
template <class Builder> friend class CVC4::NodeBuilderBase;
- template <unsigned N> friend class CVC4::NodeBuilder;
- friend class CVC4::AndNodeBuilder;
- friend class CVC4::OrNodeBuilder;
- friend class CVC4::PlusNodeBuilder;
- friend class CVC4::MultNodeBuilder;
+ template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
friend class CVC4::NodeManager;
void inc();
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;
typedef std::input_iterator_tag iterator_category;
};
+ /** Decrement ref counts of children */
+ inline void decrRefCounts();
+
public:
template <bool ref_count>
static inline Kind dKindToKind(unsigned d) {
return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
}
+
+ static inline const NodeValue& null() {
+ return s_null;
+ }
+
};/* class NodeValue */
/**
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();
}
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;
static Result lastResult;
static struct Options options;
-int runCvc4(int argc, char *argv[]);
+int runCvc4(int argc, char* argv[]);
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) {
}
}
-int runCvc4(int argc, char *argv[]) {
+int runCvc4(int argc, char* argv[]) {
// Initialize the signal handlers
cvc4_init();
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
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
@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 \
}
- 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;*/
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;
+ }
+ }
};
projects / cvc5.git / commitdiff