From: Morgan Deters Date: Mon, 8 Mar 2010 23:49:47 +0000 (+0000) Subject: This fixes regressions at levels >= 1 which were failing X-Git-Tag: cvc5-1.0.0~9197 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf4d347cbbbb4c1a1e1db99337cfd2b22b84b756;p=cvc5.git This fixes regressions at levels >= 1 which were failing * implement zombification and garbage collection of NodeValues (but GC not turned on yet) * implement removal of key nodes from all attribute tables * audit NodeBuilder and fix memory leaks and improper reference-count management. This is in many places a re-write. Clearly documented invariants on NodeBuilder state. (Closes Bug 38) * created a "BackedNodeBuilder" that can be used to construct NodeBuilders with a stack-based backing store for a size that's not a compile-time constant. * NodeValues no longer depend on Node for toStream()'ing * make unit test-building "silent" with --enable-silent-rules * (Makefile.am, Makefile.builds.in) fix top-level build system so that "make regressN" works with unbuilt/out-of-date source trees in the expected way. * (various) code cleanup, documentation, formatting --- diff --git a/Makefile.am b/Makefile.am index 6f077bb47..5aec4e904 100644 --- a/Makefile.am +++ b/Makefile.am @@ -8,6 +8,6 @@ ACLOCAL_AMFLAGS = -I config SUBDIRS = src test contrib .PHONY: regress0 regress1 regress2 regress3 -regress0 regress1 regress2 regress3: +regress0 regress1 regress2 regress3: all (cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 diff --git a/Makefile.builds.in b/Makefile.builds.in index f26111c4f..1cf9c1a52 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -85,6 +85,9 @@ endif test -e lib || ln -sfv ".$(libdir)" lib test -e bin || ln -sfv ".$(bindir)" bin +regress0 regress1 regress2 regress3: all + (cd $(CURRENT_BUILD) && $(MAKE) $@) + # any other target than the default doesn't do the extra stuff above %: (cd $(CURRENT_BUILD) && $(MAKE) $@) diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 994ff76b4..dc3448e52 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -244,16 +244,17 @@ public: emptyTrash(); typename __gnu_cxx::hash_map*, HashFcn>::iterator - i(d_map.find(k)); + i = d_map.find(k); - if(i == d_map.end()) { // Create new object + if(i == d_map.end()) {// create new object CDOmap* - obj(new(true) CDOmap(d_context, this, k, d)); + obj = new(true) CDOmap(d_context, this, k, d); d_map[k] = obj; } else { (*i).second->set(d); } } + // FIXME: no erase(), too much hassle to implement efficiently... // Iterator for CDMap: points to pair&>; diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index bd02cf452..3deed9a52 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -15,6 +15,7 @@ libexpr_la_SOURCES = \ node_manager.h \ expr_manager.h \ attribute.h \ + attribute.cpp \ @srcdir@/kind.h \ node_builder.cpp \ node_manager.cpp \ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp new file mode 100644 index 000000000..e8e93f6ff --- /dev/null +++ b/src/expr/attribute.cpp @@ -0,0 +1,61 @@ +/********************* */ +/** attribute.cpp + ** 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. + ** + ** AttributeManager implementation. + **/ + +#include "expr/attribute.h" +#include "expr/node_value.h" +#include "util/output.h" + +namespace CVC4 { +namespace expr { +namespace attr { + +void AttributeManager::deleteAllAttributes(NodeValue* nv) { + d_bools.erase(nv); + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_ints.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_exprs.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_strings.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_ptrs.erase(std::make_pair(id, nv)); + } + + // FIXME CD-bools in optimized table + /* + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_cdbools.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_cdints.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_cdexprs.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_cdstrings.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { + d_cdptrs.erase(std::make_pair(id, nv)); + } + */ +} + +}/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 285c7ce87..4dc050648 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -342,6 +342,14 @@ public: uint64_t& word = super::operator[](k.second); return BitAccessor(word, k.first); } + + /** + * Delete all flags from the given node. + */ + void erase(NodeValue* nv) { + super::erase(nv); + } + };/* class AttrHash */ /** @@ -363,6 +371,17 @@ public: } }; +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME +/// FIXME ------ need optimized (packed) specialization of CDAttrHash ------- FIXME + }/* CVC4::expr::attr namespace */ // ATTRIBUTE CLEANUP FUNCTIONS ================================================= @@ -562,6 +581,9 @@ namespace attr { */ class AttributeManager { + // IF YOU ADD ANY TABLES, don't forget to add them also to the + // implementation of deleteAllAttributes(). + /** Underlying hash table for boolean-valued attributes */ AttrHash d_bools; /** Underlying hash table for integral-valued attributes */ @@ -573,6 +595,9 @@ class AttributeManager { /** Underlying hash table for pointer-valued attributes */ AttrHash d_ptrs; + // IF YOU ADD ANY TABLES, don't forget to add them also to the + // implementation of deleteAllAttributes(). + /** Underlying hash table for context-dependent boolean-valued attributes */ CDAttrHash d_cdbools; /** Underlying hash table for context-dependent integral-valued attributes */ @@ -605,7 +630,7 @@ public: /** * Get a particular attribute on a particular node. * - * @param n the node about which to inquire + * @param nv the node about which to inquire * * @param const AttrKind& the attribute kind to get * @@ -613,7 +638,7 @@ public: * AttrKind::value_type if not. */ template - typename AttrKind::value_type getAttribute(TNode n, + typename AttrKind::value_type getAttribute(NodeValue* nv, const AttrKind&) const; // Note that there are two, distinct hasAttribute() declarations for @@ -624,21 +649,21 @@ public: /** * Determine if a particular attribute exists for a particular node. * - * @param n the node about which to inquire + * @param nv the node about which to inquire * * @param const AttrKind& the attribute kind to inquire about * * @return true if the given node has the given attribute */ template - bool hasAttribute(TNode n, + bool hasAttribute(NodeValue* nv, const AttrKind&) const; /** * Determine if a particular attribute exists for a particular node, * and get it if it does. * - * @param n the node about which to inquire + * @param nv the node about which to inquire * * @param const AttrKind& the attribute kind to inquire about * @@ -648,14 +673,14 @@ public: * @return true if the given node has the given attribute */ template - bool hasAttribute(TNode n, + bool hasAttribute(NodeValue* nv, const AttrKind&, typename AttrKind::value_type& ret) const; /** * Set a particular attribute on a particular node. * - * @param n the node for which to set the attribute + * @param nv the node for which to set the attribute * * @param const AttrKind& the attribute kind to set * @@ -665,9 +690,16 @@ public: * @return true if the given node has the given attribute */ template - void setAttribute(TNode n, + void setAttribute(NodeValue* nv, const AttrKind&, const typename AttrKind::value_type& value); + + /** + * Remove all attributes associated to the given node. + * + * @param nv the node from which to delete attributes + */ + void deleteAllAttributes(NodeValue* nv); }; }/* CVC4::expr::attr namespace */ @@ -835,7 +867,7 @@ namespace attr { // implementation for AttributeManager::getAttribute() template -typename AttrKind::value_type AttributeManager::getAttribute(TNode n, +typename AttrKind::value_type AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const { typedef typename AttrKind::value_type value_type; @@ -843,7 +875,7 @@ typename AttrKind::value_type AttributeManager::getAttribute(TNode n, typedef typename getTable::table_type table_type; const table_type& ah = getTable::get(*this); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n.d_nv)); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { return typename AttrKind::value_type(); @@ -937,20 +969,20 @@ struct HasAttribute { }; template -bool AttributeManager::hasAttribute(TNode n, +bool AttributeManager::hasAttribute(NodeValue* nv, const AttrKind&) const { - return HasAttribute::hasAttribute(this, n.d_nv); + return HasAttribute::hasAttribute(this, nv); } template -bool AttributeManager::hasAttribute(TNode n, +bool AttributeManager::hasAttribute(NodeValue* nv, const AttrKind&, typename AttrKind::value_type& ret) const { - return HasAttribute::hasAttribute(this, n.d_nv, ret); + return HasAttribute::hasAttribute(this, nv, ret); } template -inline void AttributeManager::setAttribute(TNode n, +inline void AttributeManager::setAttribute(NodeValue* nv, const AttrKind&, const typename AttrKind::value_type& value) { @@ -959,7 +991,7 @@ inline void AttributeManager::setAttribute(TNode n, typedef typename getTable::table_type table_type; table_type& ah = getTable::get(*this); - ah[std::make_pair(AttrKind::getId(), n.d_nv)] = mapping::convert(value); + ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } }/* CVC4::expr::attr namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index f9bbcb5a5..c1df399a1 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -99,8 +99,8 @@ class NodeTemplate { friend class NodeTemplate; friend class NodeManager; - template - friend class NodeBuilder; + template + friend class NodeBuilderBase; friend class ::CVC4::expr::attr::AttributeManager; diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 5c01a3b0f..a92c3a872 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -10,7 +10,195 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** A builder interface for nodes. + ** A builder interface for Nodes. + ** + ** The idea is to permit a flexible and efficient (in the common + ** case) interface for building Nodes. The general pattern of use is + ** to create a NodeBuilder, set its kind, append children to it, then + ** "extract" the resulting Node. This resulting Node may be one that + ** already exists (the NodeManager keeps a table of all Nodes in the + ** system), or may be entirely new. + ** + ** This implementation gets a bit hairy for a handful of reasons. We + ** want a user-supplied "in-line" buffer (probably on the stack, see + ** below) to hold the children, but then the number of children must + ** be known ahead of time. Therefore, if this buffer is overrun, we + ** need to heap-allocate a new buffer to hold the children. + ** + ** Note that as children are added to a NodeBuilder, they are stored + ** as raw pointers-to-NodeValue. However, their reference counts are + ** carefully maintained. + ** + ** When the "in-line" buffer "d_inlineNv" is superceded by a + ** heap-allocated buffer, we allocate the new buffer (a NodeValue + ** large enough to hold more children), copy the elements to it, and + ** mark d_inlineNv as having zero children. We do this last bit so + ** that we don't have to modify any child reference counts. The new + ** heap-allocated buffer "takes over" the reference counts of the old + ** "in-line" buffer. (If we didn't mark it as having zero children, + ** the destructor may improperly decrement the children's reference + ** counts.) + ** + ** There are then four normal cases at the end of a NodeBuilder's + ** life cycle: + ** + ** 0. We have a VARIABLE-kinded Node. These are special (they have + ** no children and are all distinct by definition). They are + ** really a subcase of 1(b), below. + ** 1. d_nv points to d_inlineNv: it is the backing store supplied + ** by the user (or derived class). + ** (a) The Node under construction already exists in the + ** NodeManager's pool. + ** (b) The Node under construction is NOT already in the + ** NodeManager's pool. + ** 2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer + ** that was heap-allocated by this NodeBuilder. + ** (a) The Node under construction already exists in the + ** NodeManager's pool. + ** (b) The Node under construction is NOT already in the + ** NodeManager's pool. + ** + ** When a Node is extracted (see the non-const version of + ** NodeBuilderBase<>::operator Node()), we convert the NodeBuilder to + ** a Node and make sure the reference counts are properly maintained. + ** That means we must ensure there are no reference-counting errors + ** among the node's children, that the children aren't re-decremented + ** on clear() or NodeBuilder destruction, and that the returned Node + ** wraps a NodeValue with a reference count of 1. + ** + ** 0. If a VARIABLE, treat similarly to 1(b), except that we + ** know there are no children (no reference counts to reason + ** about) and we don't keep VARIABLE-kinded Nodes in the + ** NodeManager pool. + ** + ** 1(a). Reference-counts for all children in d_inlineNv must be + ** decremented, and the NodeBuilder must be marked as "used" + ** and the number of children set to zero so that we don't + ** decrement them again on destruction. The existing + ** NodeManager pool entry is returned. + ** + ** 1(b). A new heap-allocated NodeValue must be constructed and all + ** settings and children from d_inlineNv copied into it. + ** This new NodeValue is put into the NodeManager's pool. + ** The NodeBuilder is marked as "used" and the number of + ** children in d_inlineNv set to zero so that we don't + ** decrement child reference counts on destruction (the child + ** reference counts have been "taken over" by the new + ** NodeValue). We return a Node wrapper for this new + ** NodeValue, which increments its reference count. + ** + ** 2(a). Reference counts for all children in d_nv must be + ** decremented. The NodeBuilder is marked as "used" and the + ** heap-allocated d_nv deleted. d_nv is repointed to + ** d_inlineNv so that destruction of the NodeBuilder doesn't + ** cause any problems. The existing NodeManager pool entry + ** is returned. + ** + ** 2(b). The heap-allocated d_nv is "cropped" to the correct size + ** (based on the number of children it _actually_ has). d_nv + ** is repointed to d_inlineNv so that destruction of the + ** NodeBuilder doesn't cause any problems, and the (old) + ** value it had is placed into the NodeManager's pool and + ** returned in a Node wrapper. + ** + ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper + ** temporary for the NodeValue in the NodeBuilderBase<>::operator + ** Node() member function. If we create a temporary (for example by + ** writing Debug("builder") << Node(nv) << endl), the NodeValue will + ** have its reference count incremented from zero to one, then + ** decremented, which makes it eligible for collection before the + ** builder has even returned it! So this is a no-no. + ** + ** For the _const_ version of NodeBuilderBase<>::operator Node(), no + ** reference-count modifications or anything else can take place! + ** Therefore, we have a slightly more expensive version: + ** + ** 0. If a VARIABLE, treat similarly to 1(b), except that we + ** know there are no children, and we don't keep + ** VARIABLE-kinded Nodes in the NodeManager pool. + ** + ** 1(a). The existing NodeManager pool entry is returned; we leave + ** child reference counts alone and get them at NodeBuilder + ** destruction time. + ** + ** 1(b). A new heap-allocated NodeValue must be constructed and all + ** settings and children from d_inlineNv copied into it. + ** This new NodeValue is put into the NodeManager's pool. + ** The NodeBuilder cannot be marked as "used", so we + ** increment all child reference counts (which will be + ** decremented to match on destruction of the NodeBuilder). + ** We return a Node wrapper for this new NodeValue, which + ** increments its reference count. + ** + ** 2(a). The existing NodeManager pool entry is returned; we leave + ** child reference counts alone and get them at NodeBuilder + ** destruction time. + ** + ** 2(b). The heap-allocated d_nv cannot be "cropped" to the correct + ** size; we create a copy, increment child reference counts, + ** place this copy into the NodeManager pool, and return a + ** Node wrapper around it. The child reference counts will + ** be decremented to match at NodeBuilder destruction time. + ** + ** There are also two cases when the NodeBuilder is clear()'ed: + ** + ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied + ** backing store): all d_inlineNv children have their reference + ** counts decremented, d_inlineNv.d_nchildren is set to zero, + ** and its kind is set to UNDEFINED_KIND. + ** + ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all + ** d_nv children have their reference counts decremented, d_nv + ** is deallocated, and d_nv is set to &d_inlineNv. d_inlineNv's + ** kind is set to UNDEFINED_KIND. + ** + ** ... destruction is similar: + ** + ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied + ** backing store): all d_inlineNv children have their reference + ** counts decremented. + ** + ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all + ** d_nv children have their reference counts decremented, and + ** d_nv is deallocated. + ** + ** Regarding the backing store (typically on the stack): the file + ** below provides three classes (two of them are templates): + ** + ** template class NodeBuilderBase; + ** + ** This is the base class for node builders. It can not be used + ** directly. It contains a shared implementation but is intended + ** to be subclassed. Derived classes supply its "in-line" buffer. + ** + ** class BackedNodeBuilder; + ** + ** This is the usable form for a user-supplied-backing-store node + ** builder. A user can allocate a buffer large enough for a + ** NodeValue with N children (say, on the stack), then pass a + ** pointer to this buffer, and the parameter N, to a + ** BackedNodeBuilder. It will use this buffer to build its + ** NodeValue until the number of children exceeds N; then it will + ** allocate d_nv on the heap. + ** + ** To ensure that the buffer is properly-sized, it is recommended + ** to use the makeStackNodeBuilder(b, N) macro to make a + ** BackedNodeBuilder "b" with a stack-allocated buffer large + ** enough to hold N children. + ** + ** template class NodeBuilder; + ** + ** This is the conceptually easiest form of NodeBuilder to use. + ** The default: + ** + ** NodeBuilder<> b; + ** + ** gives you a backing buffer with capacity for 10 children in + ** the same place as the NodeBuilder<> itself is allocated. You + ** can specify another size as a template parameter, but it must + ** be a compile-time constant (which is why the BackedNodeBuilder + ** creator-macro "makeStackNodeBuilder(b, N)" is sometimes + ** preferred). **/ #include "cvc4_private.h" @@ -28,8 +216,8 @@ namespace CVC4 { static const unsigned default_nchild_thresh = 10; - template - class NodeBuilder; + template + class NodeBuilderBase; class NodeManager; }/* CVC4 namespace */ @@ -41,196 +229,459 @@ namespace CVC4 { namespace CVC4 { -template -inline std::ostream& operator<<(std::ostream&, const NodeBuilder&); +template +inline std::ostream& operator<<(std::ostream&, const NodeBuilderBase&); class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; class MultNodeBuilder; -template -class NodeBuilder { +/** + * A base class for NodeBuilders. When extending this class, use: + * + * class MyExtendedNodeBuilder : public NodeBuilderBase { ... }; + * + * This ensures that certain member functions return the right + * (derived) class type. + * + * There are no virtual functions here, and that should remain the + * case! This class is just used for sharing of implementation. Two + * types derive from it: BackedNodeBuilder (which allows for an + * external buffer), and the NodeBuilder<> template, which requires + * that you give it a compile-time constant backing-store size. + */ +template +class NodeBuilderBase { +protected: - unsigned d_size; + /** + * A reference to an "in-line" stack-allocated buffer for use by the + * NodeBuilder. + */ + expr::NodeValue& d_inlineNv; - uint64_t d_hash; + /** + * A pointer to the "current" NodeValue buffer; either &d_inlineNv + * or a heap-allocated one if d_inlineNv wasn't big enough. + */ + expr::NodeValue* d_nv; + /** The NodeManager at play */ NodeManager* d_nm; - // initially false, when you extract the Node this is set and you can't - // extract another - bool d_used; + /** + * The maximum number of children that can be held in this "in-line" + * buffer. + */ + const uint16_t d_inlineNvMaxChildren; - expr::NodeValue* d_nv; - expr::NodeValue d_inlineNv; - expr::NodeValue *d_childrenStorage[nchild_thresh]; + /** + * The number of children allocated in d_nv. + */ + uint16_t d_nvMaxChildren; - bool nvIsAllocated() const { - return d_nv->d_nchildren > nchild_thresh; + /** + * Returns whether or not this NodeBuilder has been "used"---i.e., + * whether a Node has been extracted with [the non-const version of] + * operator Node(). Internally, this state is represented by d_nv + * pointing to NULL. + */ + inline bool isUsed() const { + return EXPECT_FALSE( d_nv == NULL ); } - template - bool nvIsAllocated(const NodeBuilder& nb) const { - return nb.d_nv->d_nchildren > N; + /** + * Set this NodeBuilder to the `used' state. + */ + inline void setUsed() { + Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!"); + Assert(d_inlineNv.d_nchildren == 0 && + d_nvMaxChildren == d_inlineNvMaxChildren, + "Internal error: bad `inline' state in NodeBuilder!"); + d_nv = NULL; } - bool evNeedsToBeAllocated() const { - return d_nv->d_nchildren == d_size; + /** + * Set this NodeBuilder to the `unused' state. Should only be done + * from clear(). + */ + inline void setUnused() { + Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!"); + Assert(d_inlineNv.d_nchildren == 0 && + d_nvMaxChildren == d_inlineNvMaxChildren, + "Internal error: bad `inline' state in NodeBuilder!"); + d_nv = &d_inlineNv; } - // realloc in the default way - void realloc(); + /** + * Returns true if d_nv is *not* the "in-line" one (it was + * heap-allocated by this class). + */ + inline bool nvIsAllocated() const { + return EXPECT_FALSE( d_nv != &d_inlineNv ) && EXPECT_TRUE( d_nv != NULL ); + } - // realloc to a specific size - void realloc(size_t toSize, bool copy = true); + /** + * Returns true if adding a child requires (re)allocation of d_nv + * first. + */ + inline bool nvNeedsToBeAllocated() const { + return EXPECT_FALSE( d_nv->d_nchildren == d_nvMaxChildren ); + } - void allocateEvIfNecessaryForAppend() { - if(EXPECT_FALSE( evNeedsToBeAllocated() )) { + /** + * (Re)allocate d_nv using a default grow factor. Ensure that child + * pointers are copied into the new buffer, and if the "inline" + * NodeValue is evacuated, make sure its children won't be + * double-decremented later (on destruction/clear). + */ + inline void realloc() { + realloc(d_nvMaxChildren * 2); + } + + /** + * (Re)allocate d_nv to a specific size. Specify "copy" if the + * children should be copied; if they are, and if the "inline" + * NodeValue is evacuated, make sure its children won't be + * double-decremented later (on destruction/clear). + */ + void realloc(size_t toSize); + + /** + * If d_nv needs to be (re)allocated to add an additional child, do + * so using realloc(), which ensures child pointers are copied and + * that the reference counts of the "inline" NodeValue won't be + * double-decremented on destruction/clear. Otherwise, do nothing. + */ + inline void allocateNvIfNecessaryForAppend() { + if(EXPECT_FALSE( nvNeedsToBeAllocated() )) { realloc(); } } - // dealloc: only call this with d_used == false and nvIsAllocated() - inline void dealloc(); + /** + * Deallocate a d_nv that was heap-allocated by this class during + * grow operations. (Marks this NodeValue no longer allocated so + * that double-deallocations don't occur.) + * + * PRECONDITION: only call this when nvIsAllocated() == true. + * POSTCONDITION: !nvIsAllocated() + */ + void dealloc(); + + /** + * "Purge" the "inline" children. Decrement all their reference + * counts and set the number of children to zero. + * + * PRECONDITION: only call this when nvIsAllocated() == false. + * POSTCONDITION: d_inlineNv.d_nchildren == 0. + */ + void decrRefCounts(); + /** + * Trim d_nv down to the size it needs to be for the number of + * children it has. Used when a Node is extracted from a + * NodeBuilder and we want the returned memory not to suffer from + * internal fragmentation. If d_nv was not heap-allocated by this + * class, or is already the right size, this function does nothing. + * + * @throws bad_alloc if the reallocation fails + */ void crop() { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); - if(EXPECT_FALSE( nvIsAllocated() ) && EXPECT_TRUE( d_size > d_nv->d_nchildren )) { - d_nv = (expr::NodeValue*) - std::realloc(d_nv, sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * (d_size = d_nv->d_nchildren) )); - if(d_nv == NULL) { + if(EXPECT_FALSE( nvIsAllocated() ) && + EXPECT_TRUE( d_nvMaxChildren > d_nv->d_nchildren )) { + // Ensure d_nv is not modified on allocation failure + expr::NodeValue* newBlock = (expr::NodeValue*) + std::realloc(d_nv, + sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = d_nv->d_nchildren) )); + if(newBlock == NULL) { + // In this case, d_nv was NOT freed. If we throw, the + // deallocation should occur on destruction of the + // NodeBuilder. throw std::bad_alloc(); } + d_nv = newBlock; } } - NodeBuilder& collapseTo(Kind k) { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + Builder& collapseTo(Kind k) { AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k, "illegal collapsing kind"); if(getKind() != k) { - Node n = *this; + Node n = operator Node(); clear(); - d_nv->d_kind = k; - append(n); + d_nv->d_kind = expr::NodeValue::kindToDKind(k); + return append(n); } - return *this; + return static_cast(*this); } +protected: + + inline NodeBuilderBase(char* buf, unsigned maxChildren, + Kind k = kind::UNDEFINED_KIND); + inline NodeBuilderBase(char* buf, unsigned maxChildren, + NodeManager* nm, Kind k = kind::UNDEFINED_KIND); + +private: + // disallow copy or assignment of these base classes directly (there + // would be no backing store!) + NodeBuilderBase(const NodeBuilderBase& nb); + NodeBuilderBase& operator=(const NodeBuilderBase& nb); + public: - inline NodeBuilder(); - inline NodeBuilder(Kind k); - inline NodeBuilder(const NodeBuilder& nb); - template inline NodeBuilder(const NodeBuilder& nb); - inline NodeBuilder(NodeManager* nm); - inline NodeBuilder(NodeManager* nm, Kind k); - inline ~NodeBuilder(); + // Intentionally not virtual; we don't want a vtable. Don't + // override this in a derived class. + inline ~NodeBuilderBase(); typedef expr::NodeValue::iterator iterator; typedef expr::NodeValue::iterator const_iterator; - const_iterator begin() const { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + /** Get the begin-const-iterator of this Node-under-construction. */ + inline const_iterator begin() const { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); return d_nv->begin(); } - const_iterator end() const { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + /** Get the end-const-iterator of this Node-under-construction. */ + inline const_iterator end() const { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); return d_nv->end(); } - Kind getKind() const { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + /** Get the kind of this Node-under-construction. */ + inline Kind getKind() const { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); return d_nv->getKind(); } - unsigned getNumChildren() const { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + /** Get the current number of children of this Node-under-construction. */ + inline unsigned getNumChildren() const { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); return d_nv->getNumChildren(); } - Node operator[](int i) const { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); - Assert(i >= 0 && i < d_nv->getNumChildren()); + /** Access to children of this Node-under-construction. */ + inline Node operator[](int i) const { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(i >= 0 && i < d_nv->getNumChildren(), "index out of range for NodeBuilder[]"); return Node(d_nv->d_children[i]); } /** * "Reset" this node builder (optionally setting a new kind for it), - * using the same memory as before. This should leave the - * NodeBuilder<> in the state it was after initial construction. + * using the same "inline" memory as at construction time. This + * deallocates NodeBuilder-allocated heap memory, if it was + * allocated, and decrements the reference counts of any currently + * children in the NodeBuilder. + * + * This should leave the BackedNodeBuilder in the state it was after + * initial construction, except for Kind, which is set to the + * argument (if provided), or UNDEFINED_KIND. In particular, the + * associated NodeManager is not affected by clear(). */ void clear(Kind k = kind::UNDEFINED_KIND); // "Stream" expression constructor syntax - NodeBuilder& operator<<(const Kind& k) { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); - Assert(d_nv->getKind() == kind::UNDEFINED_KIND); - d_nv->d_kind = k; - return *this; + /** Set the Kind of this Node-under-construction. */ + inline Builder& operator<<(const Kind& k) { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(getKind() == kind::UNDEFINED_KIND, + "can't redefine the Kind of a NodeBuilder"); + Assert(k != kind::UNDEFINED_KIND, + "can't define the Kind of a NodeBuilder to be UNDEFINED_KIND"); + d_nv->d_kind = expr::NodeValue::kindToDKind(k); + return static_cast(*this); } - NodeBuilder& operator<<(TNode n) { - // FIXME: collapse if ! UNDEFINED_KIND - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + /** + * If this Node-under-construction has a Kind set, collapse it and + * append the given Node as a child. Otherwise, simply append. + * FIXME: do we really want that collapse behavior? We had agreed + * on it but then never wrote code like that. + */ + Builder& operator<<(TNode n) { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + /* FIXME: disable this "collapsing" for now.. + if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) { + Node n2 = operator Node(); + clear(); + append(n2); + }*/ return append(n); } - // For pushing sequences of children - NodeBuilder& append(const std::vector& children) { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + /** Append a sequence of children to this Node-under-construction. */ + inline Builder& append(const std::vector& children) { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); return append(children.begin(), children.end()); } - NodeBuilder& append(TNode n) { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); - Debug("node") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl; - allocateEvIfNecessaryForAppend(); - expr::NodeValue* ev = n.d_nv; - ev->inc(); - d_nv->d_children[d_nv->d_nchildren++] = ev; - return *this; - } - + /** Append a sequence of children to this Node-under-construction. */ template - NodeBuilder& append(const Iterator& begin, const Iterator& end) { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + Builder& append(const Iterator& begin, const Iterator& end) { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); for(Iterator i = begin; i != end; ++i) { append(*i); } - return *this; + return static_cast(*this); + } + + /** Append a child to this Node-under-construction. */ + Builder& append(TNode n) { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + allocateNvIfNecessaryForAppend(); + expr::NodeValue* nv = n.d_nv; + nv->inc(); + d_nv->d_children[d_nv->d_nchildren++] = nv; + return static_cast(*this); } + // two versions, so we can support extraction from (const) + // NodeBuilders which are temporaries appearing as rvalues operator Node(); operator Node() const; inline void toStream(std::ostream& out) const { - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); d_nv->toStream(out); } - NodeBuilder& operator&=(TNode); - NodeBuilder& operator|=(TNode); - NodeBuilder& operator+=(TNode); - NodeBuilder& operator-=(TNode); - NodeBuilder& operator*=(TNode); + Builder& operator&=(TNode); + Builder& operator|=(TNode); + Builder& operator+=(TNode); + Builder& operator-=(TNode); + Builder& operator*=(TNode); friend class AndNodeBuilder; friend class OrNodeBuilder; friend class PlusNodeBuilder; friend class MultNodeBuilder; - // Yet 1 more example of how terrifying C++ is as a language +};/* class NodeBuilderBase */ + +/** + * Backing-store interface version for NodeBuilders. To construct one + * of these, you need to create a backing store (preferably on the + * stack) for it to hold its "inline" NodeValue. There's a + * convenience macro defined below, makeStackNodeBuilder(b, N), + * defined below to define a stack-allocated BackedNodeBuilder "b" + * with room for N children on the stack. + */ +class BackedNodeBuilder : public NodeBuilderBase { +public: + inline BackedNodeBuilder(char* buf, unsigned maxChildren) : + NodeBuilderBase(buf, maxChildren) { + } + + inline BackedNodeBuilder(char* buf, unsigned maxChildren, Kind k) : + NodeBuilderBase(buf, maxChildren) { + } + + inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm) : + NodeBuilderBase(buf, maxChildren) { + } + + inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) : + NodeBuilderBase(buf, maxChildren) { + } + + // we don't want a vtable, so do not declare a dtor! + //inline ~NodeBuilder(); + +private: + // disallow copy or assignment (there would be no backing store!) + BackedNodeBuilder(const BackedNodeBuilder& nb); + BackedNodeBuilder& operator=(const BackedNodeBuilder& nb); + +};/* class BackedNodeBuilder */ + +/** + * Stack-allocate a BackedNodeBuilder with a stack-allocated backing + * store of size __n. The BackedNodeBuilder will be named __v. + * + * __v must be a simple name. __n must be convertible to size_t, and + * will be evaluated only once. This macro may only be used where + * 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) + +/** + * Simple NodeBuilder interface. This is a template that requires + * that the number of children of the "inline"-allocated NodeValue be + * specified as a template parameter (which means it must be a + * compile-time constant). + */ +template +class NodeBuilder : public NodeBuilderBase > { + char d_backingStore[ sizeof(expr::NodeValue) + + (sizeof(expr::NodeValue*) * nchild_thresh) ] + __attribute__((aligned(__WORDSIZE / 8))); + + typedef NodeBuilderBase > super; + + template + void internalCopy(const NodeBuilder& nb); + +public: + inline NodeBuilder() : + NodeBuilderBase >(d_backingStore, nchild_thresh) { + } + + inline NodeBuilder(Kind k) : + NodeBuilderBase >(d_backingStore, nchild_thresh, k) { + } + + inline NodeBuilder(NodeManager* nm) : + NodeBuilderBase >(d_backingStore, nchild_thresh, nm) { + } + + inline NodeBuilder(NodeManager* nm, Kind k) : + NodeBuilderBase >(d_backingStore, nchild_thresh, nm, k) { + } + + // These implementations are identical, but we need to have both of + // these because the templatized version isn't recognized as a + // 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()) { + 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()) { + internalCopy(nb); + } + + // we don't want a vtable, so do not declare a dtor! + //inline ~NodeBuilder(); + // This is needed for copy constructors of different sizes to access private fields template friend class NodeBuilder; -};/* class NodeBuilder */ +};/* class NodeBuilder<> */ // TODO: add templatized NodeTemplate to all above and // below inlines for 'const [T]Node&' arguments? Technically a lot of @@ -336,28 +787,28 @@ public: };/* class MultNodeBuilder */ -template -inline NodeBuilder& NodeBuilder::operator&=(TNode e) { +template +inline Builder& NodeBuilderBase::operator&=(TNode e) { return collapseTo(kind::AND).append(e); } -template -inline NodeBuilder& NodeBuilder::operator|=(TNode e) { +template +inline Builder& NodeBuilderBase::operator|=(TNode e) { return collapseTo(kind::OR).append(e); } -template -inline NodeBuilder& NodeBuilder::operator+=(TNode e) { +template +inline Builder& NodeBuilderBase::operator+=(TNode e) { return collapseTo(kind::PLUS).append(e); } -template -inline NodeBuilder& NodeBuilder::operator-=(TNode e) { +template +inline Builder& NodeBuilderBase::operator-=(TNode e) { return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); } -template -inline NodeBuilder& NodeBuilder::operator*=(TNode e) { +template +inline Builder& NodeBuilderBase::operator*=(TNode e) { return collapseTo(kind::MULT).append(e); } @@ -565,391 +1016,481 @@ inline NodeTemplate operator-(const NodeTemplate& a) { #include "expr/node.h" #include "expr/node_manager.h" -// template implementations - namespace CVC4 { -template -inline NodeBuilder::NodeBuilder() : - d_size(nchild_thresh), - d_hash(0), - d_nm(NodeManager::currentNM()), - d_used(false), +template +inline NodeBuilderBase::NodeBuilderBase(char* buf, unsigned maxChildren, Kind k) : + d_inlineNv(*reinterpret_cast(buf)), d_nv(&d_inlineNv), - d_inlineNv(0), - d_childrenStorage() {} - -template -inline NodeBuilder::NodeBuilder(Kind k) : - d_size(nchild_thresh), - d_hash(0), d_nm(NodeManager::currentNM()), - d_used(false), - d_nv(&d_inlineNv), - d_inlineNv(0), - d_childrenStorage() { + d_inlineNvMaxChildren(maxChildren), + d_nvMaxChildren(maxChildren) { - d_inlineNv.d_kind = k; + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + d_inlineNv.d_nchildren = 0; } -template -inline NodeBuilder::NodeBuilder(const NodeBuilder& nb) : - d_size(nchild_thresh), - d_hash(0), - d_nm(nb.d_nm), - d_used(nb.d_used), - d_nv(&d_inlineNv), - d_inlineNv(0), - d_childrenStorage() { - - if(nvIsAllocated(nb)) { - realloc(nb.d_size, false); - std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin()); - } else { - std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_inlineNv.nv_begin()); - } - d_nv->d_kind = nb.d_nv->d_kind; - d_nv->d_nchildren = nb.d_nv->d_nchildren; - for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); - i != d_nv->nv_end(); - ++i) { - (*i)->inc(); - } -} - -template -template -inline NodeBuilder::NodeBuilder(const NodeBuilder& nb) : - d_size(nchild_thresh), - d_hash(0), - d_nm(NodeManager::currentNM()), - d_used(nb.d_used), +template +inline NodeBuilderBase::NodeBuilderBase(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) : + d_inlineNv(*reinterpret_cast(buf)), d_nv(&d_inlineNv), - d_inlineNv(0), - d_childrenStorage() { - - if(nb.d_nv->d_nchildren > nchild_thresh) { - realloc(nb.d_size, false); - std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin()); - } else { - std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_inlineNv.nv_begin()); - } - d_nv->d_kind = nb.d_nv->d_kind; - d_nv->d_nchildren = nb.d_nv->d_nchildren; - for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); - i != d_nv->nv_end(); - ++i) { - (*i)->inc(); - } -} - -template -inline NodeBuilder::NodeBuilder(NodeManager* nm) : - d_size(nchild_thresh), - d_hash(0), d_nm(nm), - d_used(false), - d_nv(&d_inlineNv), - d_inlineNv(0), - d_childrenStorage() { - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); -} + d_inlineNvMaxChildren(maxChildren), + d_nvMaxChildren(maxChildren) { -template -inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : - d_size(nchild_thresh), - d_hash(0), - d_nm(nm), - d_used(false), - d_nv(&d_inlineNv), - d_inlineNv(0), - d_childrenStorage() { - - d_inlineNv.d_kind = k; + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + d_inlineNv.d_nchildren = 0; } -template -inline NodeBuilder::~NodeBuilder() { - if(!d_used) { - // Warning("NodeBuilder unused at destruction\n"); - // Commented above, as it happens a lot, for example with exceptions +template +inline NodeBuilderBase::~NodeBuilderBase() { + if(EXPECT_FALSE( nvIsAllocated() )) { dealloc(); + } else if(EXPECT_FALSE( !isUsed() )) { + decrRefCounts(); } } -template -void NodeBuilder::clear(Kind k) { - if(!d_used) { - Warning("NodeBuilder unused at clear\n"); - +template +void NodeBuilderBase::clear(Kind k) { + if(EXPECT_FALSE( nvIsAllocated() )) { dealloc(); + } else if(EXPECT_FALSE( !isUsed() )) { + decrRefCounts(); + } else { + setUnused(); } - d_size = nchild_thresh; - d_hash = 0; - d_nm = NodeManager::currentNM(); - d_used = false; - d_nv = &d_inlineNv; - d_inlineNv.d_kind = k; - d_inlineNv.d_nchildren = 0;//FIXME leak -} - -template -void NodeBuilder::realloc() { - if(EXPECT_FALSE( nvIsAllocated() )) { - d_nv = (expr::NodeValue*) - std::realloc(d_nv, - sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) )); - if(d_nv == NULL) { - throw std::bad_alloc(); - } - } else { - d_nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) )); - if(d_nv == NULL) { - throw std::bad_alloc(); - } - d_nv->d_id = 0; - d_nv->d_rc = 0; - d_nv->d_kind = d_inlineNv.d_kind; - d_nv->d_nchildren = nchild_thresh; - std::copy(d_inlineNv.d_children, - d_inlineNv.d_children + nchild_thresh, - d_nv->d_children); + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin(); + i != d_inlineNv.nv_end(); + ++i) { + (*i)->dec(); } + d_inlineNv.d_nchildren = 0; } -template -void NodeBuilder::realloc(size_t toSize, bool copy) { - Assert( d_size < toSize ); +template +void NodeBuilderBase::realloc(size_t toSize) { + Assert( toSize > d_nvMaxChildren, + "attempt to realloc() a NodeBuilder to a smaller/equal size!" ); if(EXPECT_FALSE( nvIsAllocated() )) { - d_nv = (expr::NodeValue*) + // Ensure d_nv is not modified on allocation failure + expr::NodeValue* newBlock = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * (d_size = toSize) )); - if(d_nv == NULL) { + ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) )); + if(newBlock == NULL) { + // In this case, d_nv was NOT freed. If we throw, the + // deallocation should occur on destruction of the NodeBuilder. throw std::bad_alloc(); } + // Here, the copy (between two heap-allocated buffers) has already + // been done for us by the std::realloc(). + d_nv = newBlock; } else { - d_nv = (expr::NodeValue*) + // Ensure d_nv is not modified on allocation failure + expr::NodeValue* newBlock = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * (d_size = toSize) )); - if(d_nv == NULL) { + ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) )); + if(newBlock == NULL) { throw std::bad_alloc(); } + + d_nv = newBlock; d_nv->d_id = 0; d_nv->d_rc = 0; d_nv->d_kind = d_inlineNv.d_kind; - d_nv->d_nchildren = nchild_thresh; - if(copy) { - std::copy(d_inlineNv.d_children, - d_inlineNv.d_children + nchild_thresh, - d_nv->d_children); - // inhibit decr'ing refcounts of children in dtor - d_inlineNv.d_nchildren = 0; - } + d_nv->d_nchildren = d_inlineNv.d_nchildren; + + std::copy(d_inlineNv.d_children, + d_inlineNv.d_children + d_inlineNv.d_nchildren, + d_nv->d_children); + + // ensure "inline" children don't get decremented in dtor + d_inlineNv.d_nchildren = 0; } } -template -inline void NodeBuilder::dealloc() { - /* Prefer asserts to if() because usually these conditions have been - * checked already, so we don't want to do a double-check in - * production; these are just sanity checks for debug builds */ - Assert(!d_used, "Internal error: NodeBuilder: dealloc() called with d_used"); +template +void NodeBuilderBase::dealloc() { + Assert( nvIsAllocated(), + "Internal error: NodeBuilder: dealloc() called without a " + "private NodeBuilder-allocated buffer" ); for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end(); ++i) { (*i)->dec(); } - if(nvIsAllocated()) { - free(d_nv); + + free(d_nv); + d_nv = &d_inlineNv; + d_nvMaxChildren = d_inlineNvMaxChildren; +} + +template +void NodeBuilderBase::decrRefCounts() { + Assert( !nvIsAllocated(), + "Internal error: NodeBuilder: decrRefCounts() called with a " + "private NodeBuilder-allocated buffer" ); + + for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin(); + i != d_inlineNv.nv_end(); + ++i) { + (*i)->dec(); } + + d_inlineNv.d_nchildren = 0; } -template -NodeBuilder::operator Node() const {// const version - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); - Assert(d_nv->getKind() != kind::UNDEFINED_KIND, +// NON-CONST VERSION OF NODE EXTRACTOR +template +NodeBuilderBase::operator Node() { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(getKind() != kind::UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); - if(d_nv->d_kind == kind::VARIABLE) { - Assert(d_nv->d_nchildren == 0); + // NOTE: The comments in this function refer to the cases in the + // file comments at the top of this file. + + // Case 0: If a VARIABLE + if(getKind() == kind::VARIABLE) { + /* 0. If a VARIABLE, treat similarly to 1(b), except that we know + * there are no children (no reference counts to reason about) + * and we don't keep VARIABLE-kinded Nodes in the NodeManager + * pool. */ + + Assert( ! nvIsAllocated(), + "internal NodeBuilder error: " + "VARIABLE-kinded NodeBuilder is heap-allocated !?" ); + Assert( d_inlineNv.d_nchildren == 0, + "improperly-formed VARIABLE-kinded NodeBuilder: " + "no children permitted" ); + + // we have to copy the inline NodeValue out expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? + std::malloc(sizeof(expr::NodeValue)); if(nv == NULL) { throw std::bad_alloc(); } + // there are no children, so we don't have to worry about + // reference counts in this case. nv->d_nchildren = 0; - nv->d_kind = kind::VARIABLE; + nv->d_kind = expr::NodeValue::kindToDKind(kind::VARIABLE); nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading nv->d_rc = 0; - //d_used = true; // const version - //d_nv = NULL; // const version + setUsed(); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; return Node(nv); } - // implementation differs depending on whether the expression value - // was malloc'ed or not + // Implementation differs depending on whether the NodeValue was + // malloc'ed or not and whether or not it's in the already-been-seen + // NodeManager pool of Nodes. See implementation notes at the top + // of this file. + + if(EXPECT_TRUE( ! nvIsAllocated() )) { + /** Case 1. d_nv points to d_inlineNv: it is the backing store + ** supplied by the user (or derived class) **/ + + // Lookup the expression value in the pool we already have + expr::NodeValue* nv = d_nm->poolLookup(&d_inlineNv); + if(nv != NULL) { + /* Subcase (a): The Node under construction already exists in + * the NodeManager's pool. */ + + /* 1(a). Reference-counts for all children in d_inlineNv must be + * decremented, and the NodeBuilder must be marked as "used" and + * the number of children set to zero so that we don't decrement + * them again on destruction. The existing NodeManager pool + * entry is returned. + */ + decrRefCounts(); + d_inlineNv.d_nchildren = 0; + setUsed(); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + return Node(nv); + } else { + /* Subcase (b): The Node under construction is NOT already in + * the NodeManager's pool. */ + + /* 1(b). A new heap-allocated NodeValue must be constructed and + * all settings and children from d_inlineNv copied into it. + * This new NodeValue is put into the NodeManager's pool. The + * NodeBuilder is marked as "used" and the number of children in + * d_inlineNv set to zero so that we don't decrement child + * reference counts on destruction (the child reference counts + * have been "taken over" by the new NodeValue). We return a + * Node wrapper for this new NodeValue, which increments its + * reference count. */ + + // create the canonical expression value for this node + nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); + if(nv == NULL) { + throw std::bad_alloc(); + } + nv->d_nchildren = d_inlineNv.d_nchildren; + nv->d_kind = d_inlineNv.d_kind; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_rc = 0; + + std::copy(d_inlineNv.d_children, + d_inlineNv.d_children + d_inlineNv.d_nchildren, + nv->d_children); + + d_inlineNv.d_nchildren = 0; + setUsed(); + + d_nm->poolInsert(nv); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + return Node(nv); + } + } else { + /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger + ** buffer that was heap-allocated by this NodeBuilder. **/ - if(EXPECT_FALSE( nvIsAllocated() )) { // Lookup the expression value in the pool we already have (with insert) expr::NodeValue* nv = d_nm->poolLookup(d_nv); // If something else is there, we reuse it if(nv != NULL) { - // expression already exists in node manager - //dealloc(); // const version - //d_used = true; // const version + /* Subcase (a) The Node under construction already exists in the + * NodeManager's pool. */ + + /* 2(a). Reference counts for all children in d_nv must be + * decremented. The NodeBuilder is marked as "used" and the + * heap-allocated d_nv deleted. d_nv is repointed to d_inlineNv + * so that destruction of the NodeBuilder doesn't cause any + * problems. The existing NodeManager pool entry is + * returned. */ + + dealloc(); + setUsed(); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + return Node(nv); + } else { + /* Subcase (b) The Node under construction is NOT already in the + * NodeManager's pool. */ + + /* 2(b). The heap-allocated d_nv is "cropped" to the correct + * size (based on the number of children it _actually_ has). + * d_nv is repointed to d_inlineNv so that destruction of the + * NodeBuilder doesn't cause any problems, and the (old) value + * it had is placed into the NodeManager's pool and returned in + * a Node wrapper. */ + + crop(); + nv = d_nv; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + d_nv = &d_inlineNv; + d_nvMaxChildren = d_inlineNvMaxChildren; + setUsed(); + d_nm->poolInsert(nv); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; return Node(nv); } - // Otherwise copy children out - nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); - if(nv == NULL) { - throw std::bad_alloc(); - } - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading - nv->d_rc = 0; - nv->d_kind = d_nv->d_kind; - nv->d_nchildren = d_nv->d_nchildren; - std::copy(d_nv->d_children, - d_nv->d_children + d_nv->d_nchildren, - nv->d_children); - // inc child refcounts - for(expr::NodeValue::nv_iterator i = nv->nv_begin(); - i != nv->nv_end(); - ++i) { - (*i)->inc(); - } - d_nm->poolInsert(nv); - return Node(nv); } - - // Lookup the expression value in the pool we already have - expr::NodeValue* ev = d_nm->poolLookup(d_nv); - //DANGER d_nv should be ptr-to-const in the above line b/c it points to d_inlineNv - if(ev != NULL) { - // expression already exists in node manager - //d_used = true; // const version - Debug("node") << "result: " << Node(ev) << std::endl; - return Node(ev); - } - - // otherwise create the canonical expression value for this node - ev = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); - if(ev == NULL) { - throw std::bad_alloc(); - } - ev->d_nchildren = d_inlineNv.d_nchildren; - ev->d_kind = d_inlineNv.d_kind; - ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading - ev->d_rc = 0; - std::copy(d_inlineNv.d_children, - d_inlineNv.d_children + d_inlineNv.d_nchildren, - ev->d_children); - //d_used = true; - //d_nv = NULL; - //d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor - // inc child refcounts - for(expr::NodeValue::nv_iterator i = ev->nv_begin(); - i != ev->nv_end(); - ++i) { - (*i)->inc(); - } - - // Make the new expression - d_nm->poolInsert(ev); - return Node(ev); } -template -NodeBuilder::operator Node() {// not const - Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); - Assert(d_nv->getKind() != kind::UNDEFINED_KIND, +// CONST VERSION OF NODE EXTRACTOR +template +NodeBuilderBase::operator Node() const { + Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(getKind() != kind::UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); - if(d_nv->d_kind == kind::VARIABLE) { - Assert(d_nv->d_nchildren == 0); + // NOTE: The comments in this function refer to the cases in the + // file comments at the top of this file. + + // Case 0: If a VARIABLE + if(getKind() == kind::VARIABLE) { + /* 0. If a VARIABLE, treat similarly to 1(b), except that we know + * there are no children, and we don't keep VARIABLE-kinded Nodes + * in the NodeManager pool. */ + + Assert( ! nvIsAllocated(), + "internal NodeBuilder error: " + "VARIABLE-kinded NodeBuilder is heap-allocated !?" ); + Assert( d_inlineNv.d_nchildren == 0, + "improperly-formed VARIABLE-kinded NodeBuilder: " + "no children permitted" ); + + // we have to copy the inline NodeValue out expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? + std::malloc(sizeof(expr::NodeValue)); if(nv == NULL) { throw std::bad_alloc(); } + // there are no children, so we don't have to worry about + // reference counts in this case. nv->d_nchildren = 0; - nv->d_kind = kind::VARIABLE; + nv->d_kind = expr::NodeValue::kindToDKind(kind::VARIABLE); nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading nv->d_rc = 0; - d_used = true; - d_nv = NULL; - Debug("node") << "result: " << Node(nv) << std::endl; + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; return Node(nv); } - // implementation differs depending on whether the expression value - // was malloc'ed or not + // Implementation differs depending on whether the NodeValue was + // malloc'ed or not and whether or not it's in the already-been-seen + // NodeManager pool of Nodes. See implementation notes at the top + // of this file. + + if(EXPECT_TRUE( ! nvIsAllocated() )) { + /** Case 1. d_nv points to d_inlineNv: it is the backing store + ** supplied by the user (or derived class) **/ + + // Lookup the expression value in the pool we already have + expr::NodeValue* nv = d_nm->poolLookup(&d_inlineNv); + if(nv != NULL) { + /* Subcase (a): The Node under construction already exists in + * the NodeManager's pool. */ + + /* 1(a). The existing NodeManager pool entry is returned; we + * leave child reference counts alone and get them at + * NodeBuilder destruction time. */ + + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + return Node(nv); + } else { + /* Subcase (b): The Node under construction is NOT already in + * the NodeManager's pool. */ + + /* 1(b). A new heap-allocated NodeValue must be constructed and + * all settings and children from d_inlineNv copied into it. + * This new NodeValue is put into the NodeManager's pool. The + * NodeBuilder cannot be marked as "used", so we increment all + * child reference counts (which will be decremented to match on + * destruction of the NodeBuilder). We return a Node wrapper + * for this new NodeValue, which increments its reference + * count. */ + + // create the canonical expression value for this node + nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); + if(nv == NULL) { + throw std::bad_alloc(); + } + nv->d_nchildren = d_inlineNv.d_nchildren; + nv->d_kind = d_inlineNv.d_kind; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_rc = 0; + + std::copy(d_inlineNv.d_children, + d_inlineNv.d_children + d_inlineNv.d_nchildren, + nv->d_children); + + for(expr::NodeValue::nv_iterator i = nv->nv_begin(); + i != nv->nv_end(); + ++i) { + (*i)->inc(); + } + + d_nm->poolInsert(nv); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + return Node(nv); + } + } else { + /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger + ** buffer that was heap-allocated by this NodeBuilder. **/ - if(EXPECT_FALSE( nvIsAllocated() )) { // Lookup the expression value in the pool we already have (with insert) expr::NodeValue* nv = d_nm->poolLookup(d_nv); // If something else is there, we reuse it if(nv != NULL) { - // expression already exists in node manager - dealloc(); - d_used = true; - Debug("node") << "result: " << Node(nv) << std::endl; + /* Subcase (a) The Node under construction already exists in the + * NodeManager's pool. */ + + /* 2(a). The existing NodeManager pool entry is returned; we + * leave child reference counts alone and get them at + * NodeBuilder destruction time. */ + + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + return Node(nv); + } else { + /* Subcase (b) The Node under construction is NOT already in the + * NodeManager's pool. */ + + /* 2(b). The heap-allocated d_nv cannot be "cropped" to the + * correct size; we create a copy, increment child reference + * counts, place this copy into the NodeManager pool, and return + * a Node wrapper around it. The child reference counts will be + * decremented to match at NodeBuilder destruction time. */ + + // create the canonical expression value for this node + nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); + if(nv == NULL) { + throw std::bad_alloc(); + } + nv->d_nchildren = d_nv->d_nchildren; + nv->d_kind = d_nv->d_kind; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_rc = 0; + + std::copy(d_nv->d_children, + d_nv->d_children + d_nv->d_nchildren, + nv->d_children); + + for(expr::NodeValue::nv_iterator i = nv->nv_begin(); + i != nv->nv_end(); + ++i) { + (*i)->inc(); + } + + d_nm->poolInsert(nv); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; return Node(nv); } - // Otherwise crop and set the expression value to the allocated one - crop(); - nv = d_nv; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading - d_nv = NULL; - d_used = true; - d_nm->poolInsert(nv); - return Node(nv); } +} - // Lookup the expression value in the pool we already have - expr::NodeValue* ev = d_nm->poolLookup(&d_inlineNv); - if(ev != NULL) { - // expression already exists in node manager - d_used = true; - Debug("node") << "result: " << Node(ev) << std::endl; - return Node(ev); +template +template +void NodeBuilder::internalCopy(const NodeBuilder& nb) { + if(nb.isUsed()) { + super::setUsed(); + return; } - // otherwise create the canonical expression value for this node - ev = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); - if(ev == NULL) { - throw std::bad_alloc(); + if(nb.d_nvMaxChildren > super::d_nvMaxChildren) { + super::realloc(nb.d_nvMaxChildren); } - ev->d_nchildren = d_inlineNv.d_nchildren; - ev->d_kind = d_inlineNv.d_kind; - ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading - ev->d_rc = 0; - std::copy(d_inlineNv.d_children, - d_inlineNv.d_children + d_inlineNv.d_nchildren, - ev->d_children); - d_used = true; - d_nv = NULL; - d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor - // Make the new expression - d_nm->poolInsert(ev); - return Node(ev); + std::copy(nb.d_nv->nv_begin(), + nb.d_nv->nv_end(), + super::d_nv->nv_begin()); + + super::d_nv->d_nchildren = nb.d_nv->d_nchildren; + + for(expr::NodeValue::nv_iterator i = super::d_nv->nv_begin(); + i != super::d_nv->nv_end(); + ++i) { + (*i)->inc(); + } } -template +template inline std::ostream& operator<<(std::ostream& out, - const NodeBuilder& b) { + const NodeBuilderBase& b) { b.toStream(out); return out; } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5b5dfafa9..98171cb2e 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -15,8 +15,11 @@ #include "node_manager.h" +#include + using namespace std; using namespace CVC4::expr; +using __gnu_cxx::hash_set; namespace CVC4 { @@ -30,4 +33,80 @@ NodeValue* NodeManager::poolLookup(NodeValue* nv) const { return *find; } } + +/** + * This class ensure that NodeManager::d_reclaiming gets set to false + * even on exceptional exit from NodeManager::reclaimZombies(). + */ +struct Reclaim { + bool& d_reclaimField; + Reclaim(bool& reclaim) : + d_reclaimField(reclaim) { + + Debug("gc") << ">> setting RECLAIM field\n"; + d_reclaimField = true; + } + ~Reclaim() { + Debug("gc") << "<< clearing RECLAIM field\n"; + d_reclaimField = false; + } +}; + +/** + * 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 + + Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n"; + + // during reclamation, reclaimZombies() is never supposed to be called + Assert(! d_reclaiming, "NodeManager::reclaimZombies() not re-entrant!"); + Reclaim r(d_reclaiming); + + // We copy the set away and clear the NodeManager's set of zombies. + // This is because reclaimZombie() decrements the RC of the + // NodeValue's children, which may (recursively) reclaim them. + // + // Let's say we're reclaiming zombie NodeValue "A" and its child "B" + // then becomes a zombie (NodeManager::gc(B) is called). + // + // One way to handle B's zombification is simply to put it into + // d_zombies. This is what we do. However, if we're currently + // processing d_zombies in the loop below, such addition may be + // invisible to us (B is leaked) or even invalidate our iterator, + // causing a crash. + + vector zombies; + zombies.reserve(d_zombies.size()); + std::copy(d_zombies.begin(), + d_zombies.end(), + std::back_inserter(zombies)); + d_zombies.clear(); + + for(vector::iterator i = zombies.begin(); + i != zombies.end(); + ++i) { + // collect ONLY IF still zero + if((*i)->d_rc == 0) { + reclaimZombie(*i); + } + } +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c4f54727a..32c1cd210 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -28,6 +28,7 @@ #include "expr/kind.h" #include "expr/expr.h" +#include "expr/node_value.h" #include "context/context.h" namespace CVC4 { @@ -50,31 +51,65 @@ typedef Attribute TypeAttr; class NodeManager { static __thread NodeManager* s_current; - template friend class CVC4::NodeBuilder; + template friend class CVC4::NodeBuilderBase; typedef __gnu_cxx::hash_set NodeValueSet; + typedef __gnu_cxx::hash_set ZombieSet; + NodeValueSet d_nodeValueSet; expr::attr::AttributeManager d_attrManager; expr::NodeValue* poolLookup(expr::NodeValue* nv) const; void poolInsert(expr::NodeValue* nv); + void poolRemove(expr::NodeValue* nv); friend class NodeManagerScope; friend class expr::NodeValue; - std::vector d_zombieList; + bool d_reclaiming; + ZombieSet d_zombies; + /** + * Register a NodeValue as a zombie. + */ inline void gc(expr::NodeValue* nv) { Assert(nv->d_rc == 0); - d_zombieList.push_back(nv); + if(d_reclaiming) {// FIXME multithreading + // currently reclaiming zombies; just push onto the list + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() + << " [CURRENTLY-RECLAIMING]\n"; + d_zombies.insert(nv);// FIXME multithreading + } else { + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + d_zombies.insert(nv);// FIXME multithreading + + // for now, collect eagerly. can add heuristic here later.. + reclaimZombies(); + } } + /** + * Reclaim all zombies. + */ + void reclaimZombies(); + + /** + * Reclaim a particular zombie. + */ + void reclaimZombie(expr::NodeValue* nv); + public: - NodeManager(context::Context* ctxt) : d_attrManager(ctxt) { + NodeManager(context::Context* ctxt) : + d_attrManager(ctxt), + d_reclaiming(false) { poolInsert( &expr::NodeValue::s_null ); } @@ -95,6 +130,29 @@ public: Node mkVar(const Type* type); Node mkVar(); + template + inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv, + const AttrKind&) const; + + // Note that there are two, distinct hasAttribute() declarations for + // a reason (rather than using a pointer-valued argument with a + // default value): they permit more optimized code in the underlying + // hasAttribute() implementations. + + template + inline bool hasAttribute(expr::NodeValue* nv, + const AttrKind&) const; + + template + inline bool hasAttribute(expr::NodeValue* nv, + const AttrKind&, + typename AttrKind::value_type&) const; + + template + inline void setAttribute(expr::NodeValue* nv, + const AttrKind&, + const typename AttrKind::value_type& value); + template inline typename AttrKind::value_type getAttribute(TNode n, const AttrKind&) const; @@ -118,7 +176,6 @@ public: const AttrKind&, const typename AttrKind::value_type& value); - /** Get the type for booleans. */ inline const BooleanType* booleanType() const { return BooleanType::getInstance(); @@ -131,16 +188,16 @@ public: /** Make a function type from domain to range. */ inline const FunctionType* - mkFunctionType(const Type* domain, const Type* range); + mkFunctionType(const Type* domain, const Type* range) const; /** Make a function type with input types from argTypes. */ inline const FunctionType* - mkFunctionType(const std::vector& argTypes, const Type* range); + mkFunctionType(const std::vector& argTypes, const Type* range) const; /** Make a new sort with the given name. */ - inline const Type* mkSort(const std::string& name); + inline const Type* mkSort(const std::string& name) const; - inline const Type* getType(TNode n); + inline const Type* getType(TNode n) const; }; /** @@ -202,37 +259,63 @@ public: } }; +template +inline typename AttrKind::value_type NodeManager::getAttribute(expr::NodeValue* nv, + const AttrKind&) const { + return d_attrManager.getAttribute(nv, AttrKind()); +} + +template +inline bool NodeManager::hasAttribute(expr::NodeValue* nv, + const AttrKind&) const { + return d_attrManager.hasAttribute(nv, AttrKind()); +} + +template +inline bool NodeManager::hasAttribute(expr::NodeValue* nv, + const AttrKind&, + typename AttrKind::value_type& ret) const { + return d_attrManager.hasAttribute(nv, AttrKind(), ret); +} + +template +inline void NodeManager::setAttribute(expr::NodeValue* nv, + const AttrKind&, + const typename AttrKind::value_type& value) { + d_attrManager.setAttribute(nv, AttrKind(), value); +} + template inline typename AttrKind::value_type NodeManager::getAttribute(TNode n, const AttrKind&) const { - return d_attrManager.getAttribute(n, AttrKind()); + return d_attrManager.getAttribute(n.d_nv, AttrKind()); } template inline bool NodeManager::hasAttribute(TNode n, const AttrKind&) const { - return d_attrManager.hasAttribute(n, AttrKind()); + return d_attrManager.hasAttribute(n.d_nv, AttrKind()); } template inline bool NodeManager::hasAttribute(TNode n, const AttrKind&, typename AttrKind::value_type& ret) const { - return d_attrManager.hasAttribute(n, AttrKind(), ret); + return d_attrManager.hasAttribute(n.d_nv, AttrKind(), ret); } template inline void NodeManager::setAttribute(TNode n, const AttrKind&, const typename AttrKind::value_type& value) { - d_attrManager.setAttribute(n, AttrKind(), value); + d_attrManager.setAttribute(n.d_nv, AttrKind(), value); } /** Make a function type from domain to range. - * TODO: Function types should be unique for this manager. */ + * TODO: Function types should be unique for this manager. */ const FunctionType* NodeManager::mkFunctionType(const Type* domain, - const Type* range) { + const Type* range) const { std::vector argTypes; argTypes.push_back(domain); return new FunctionType(argTypes, range); @@ -242,23 +325,29 @@ NodeManager::mkFunctionType(const Type* domain, * TODO: Function types should be unique for this manager. */ const FunctionType* NodeManager::mkFunctionType(const std::vector& argTypes, - const Type* range) { + const Type* range) const { Assert( argTypes.size() > 0 ); return new FunctionType(argTypes, range); } const Type* -NodeManager::mkSort(const std::string& name) { +NodeManager::mkSort(const std::string& name) const { return new SortType(name); } -inline const Type* NodeManager::getType(TNode n) { +inline const Type* NodeManager::getType(TNode n) const { return getAttribute(n, CVC4::expr::TypeAttr()); } inline void NodeManager::poolInsert(expr::NodeValue* nv) { Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in the pool!"); - d_nodeValueSet.insert(nv); + d_nodeValueSet.insert(nv);// FIXME multithreading +} + +inline void NodeManager::poolRemove(expr::NodeValue* nv) { + Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(), + "NodeValue is not in the pool!"); + d_nodeValueSet.erase(nv);// FIXME multithreading } }/* CVC4 namespace */ @@ -305,12 +394,13 @@ inline Node NodeManager::mkVar(const Type* type, const std::string& name) { } inline Node NodeManager::mkVar(const Type* type) { - Node n = NodeBuilder<>(this, kind::VARIABLE); + Node n = mkVar(); n.setAttribute(expr::TypeAttr(), type); return n; } inline Node NodeManager::mkVar() { + // TODO: rewrite to not use NodeBuilder return NodeBuilder<>(this, kind::VARIABLE); } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 5c5765011..5dbfac169 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -38,9 +38,11 @@ string NodeValue::toString() const { void NodeValue::toStream(std::ostream& out) const { if(d_kind == kind::VARIABLE) { - Node n(this); string s; - if(n.hasAttribute(VarNameAttr(), s)) { + // conceptually "this" is const, and hasAttribute() doesn't change + // its argument, but it requires a non-const key arg (for now) + if(NodeManager::currentNM()->hasAttribute(const_cast(this), + VarNameAttr(), s)) { out << s; } else { out << "var_" << d_id; @@ -51,7 +53,7 @@ void NodeValue::toStream(std::ostream& out) const { if(i != nv_end()) { out << " "; } - Node(*i).toStream(out); + (*i)->toStream(out); } out << ")"; } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index bd74fd4d4..a5f68babf 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -32,7 +32,8 @@ namespace CVC4 { template class NodeTemplate; -template class NodeBuilder; +template class NodeBuilderBase; +template class NodeBuilder; class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; @@ -79,7 +80,8 @@ class NodeValue { // todo add exprMgr ref in debug case template friend class CVC4::NodeTemplate; - template friend class CVC4::NodeBuilder; + template friend class CVC4::NodeBuilderBase; + template friend class CVC4::NodeBuilder; friend class CVC4::AndNodeBuilder; friend class CVC4::OrNodeBuilder; friend class CVC4::PlusNodeBuilder; @@ -94,9 +96,6 @@ class NodeValue { /** Private default constructor for the null value. */ NodeValue(); - /** Private default constructor for the NodeBuilder. */ - NodeValue(int); - /** Destructor decrements the ref counts of its children */ ~NodeValue(); @@ -226,6 +225,15 @@ struct NodeValueInternalHashFcn { } };/* struct NodeValueHashFcn */ +/** + * For hash_maps, hash_sets, etc. + */ +struct NodeValueIDHashFcn { + inline size_t operator()(const NodeValue* nv) const { + return (size_t) nv->getId(); + } +};/* struct NodeValueHashFcn */ + }/* CVC4::expr namespace */ }/* CVC4 namespace */ @@ -241,13 +249,6 @@ inline NodeValue::NodeValue() : d_nchildren(0) { } -inline NodeValue::NodeValue(int) : - d_id(0), - d_rc(0), - d_kind(kindToDKind(kind::UNDEFINED_KIND)), - d_nchildren(0) { -} - inline NodeValue::~NodeValue() { for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { (*i)->dec(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8def3e279..6e3a1b801 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -10,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The main entry point into the CVC4 library's SMT interface. **/ #include "smt/smt_engine.h" @@ -67,6 +68,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : d_exprManager(em), d_nodeManager(em->getNodeManager()), d_options(opts) { + NodeManagerScope nms(d_nodeManager); d_decisionEngine = new DecisionEngine; d_theoryEngine = new TheoryEngine(this, d_ctxt); diff --git a/src/util/Assert.h b/src/util/Assert.h index 8c230218c..ad3f4b1d3 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -212,6 +212,7 @@ extern __thread CVC4_PUBLIC const char* s_debugAssertionFailure; Warning() << "The propagating exception is:" << std::endl \ << s_debugAssertionFailure << std::endl \ << "===========================================" << std::endl; \ + s_debugAssertionFailure = NULL; \ } \ } else { \ throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 15f781333..59a37a4db 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -22,6 +22,17 @@ TEST_DEPS = \ EXTRA_DIST = \ $(TEST_DEPS_DIST) +if STATIC_BINARY +system_LINK = $(CXXLINK) -all-static +else +system_LINK = $(CXXLINK) +endif + +# WHEN SYSTEM TESTS ARE ADDED, BUILD LIKE THIS: +# system_test: system_test.cpp +# $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@.lo $< +# $(AM_V_CXXLD)$(system_LINK) $(AM_LDFLAGS) $@.lo + # rebuild tests if a library changes $(TESTS):: $(TEST_DEPS) diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 967d6a8c8..9d1a2995b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -64,18 +64,24 @@ MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp) # that file for comment) # TESTS = +if STATIC_BINARY +unit_LINK = $(CXXLINK) -all-static +else +unit_LINK = $(CXXLINK) +endif + $(UNIT_TESTS:%=%.cpp): %.cpp: %.h - mkdir -p `dirname "$@"` - $(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<" + $(AM_V_at)mkdir -p `dirname "$@"` + $(AM_V_GEN)$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<" $(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS) - $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $< - $(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo + $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $< + $(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_WHITE) $@.lo $(BLACK_TESTS): %_black: %_black.cpp $(TEST_DEPS) - $(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $< - $(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo + $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $< + $(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_BLACK) $@.lo $(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS) - $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $< - $(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo + $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $< + $(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_PUBLIC) $@.lo else