diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-08 23:49:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-08 23:49:47 +0000 |
commit | cf4d347cbbbb4c1a1e1db99337cfd2b22b84b756 (patch) | |
tree | ceea43e3d37525038bed10b115c73a8aa08ce68d /src/expr/node_value.h | |
parent | de0160112edbed8ce9b62bf87172ae2f0e99a013 (diff) |
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
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r-- | src/expr/node_value.h | 25 |
1 files changed, 13 insertions, 12 deletions
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 <bool ref_count> class NodeTemplate; -template <unsigned> class NodeBuilder; +template <class Builder> class NodeBuilderBase; +template <unsigned N> class NodeBuilder; class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; @@ -79,7 +80,8 @@ class NodeValue { // todo add exprMgr ref in debug case template <bool> friend class CVC4::NodeTemplate; - template <unsigned> friend class CVC4::NodeBuilder; + 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; @@ -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(); |