diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-12 23:52:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-12 23:52:14 +0000 |
commit | c8e9b1d6422b56476a2efb3fbaf19bce66de4c2b (patch) | |
tree | aa2b6400b7a5663599eff687310c509156ca788d /src/expr | |
parent | 856567b63c56b238db8a5bb84ad0da7990c1f1eb (diff) |
* 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.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 2 | ||||
-rw-r--r-- | src/expr/expr.cpp | 5 | ||||
-rw-r--r-- | src/expr/expr.h | 6 | ||||
-rw-r--r-- | src/expr/node.h | 10 | ||||
-rw-r--r-- | src/expr/node_builder.h | 91 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 36 | ||||
-rw-r--r-- | src/expr/node_manager.h | 5 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_value.h | 34 |
9 files changed, 100 insertions, 91 deletions
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 @@ -92,12 +92,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 @@ -219,14 +219,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<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!) @@ -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 <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; @@ -637,19 +648,31 @@ class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > { 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 @@ -657,20 +680,22 @@ public: // 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); } @@ -1019,8 +1044,8 @@ inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) { 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), @@ -1033,8 +1058,8 @@ inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned 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), 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<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 } } } 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 <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(); @@ -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 <bool ref_count> @@ -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(); } |