diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
commit | 88b52c971b43248e6ceacf1c8140a06427d0418d (patch) | |
tree | 4ee443c898a858fcdd658f3f043e4180eddd8784 /src/expr/node_value.h | |
parent | 29cc307cdf2c42bebf4f5615874a864783f47fd0 (diff) |
* public/private code untangled (smt/smt_engine.h no longer #includes
expr/node.h). This removes the warnings we had during compilation,
and heads off a number of potential linking errors due to improper
inlining of private (library-only) stuff in client (out-of-library)
code.
* "configure" now takes some options as part of a "bare-option" build
type (e.g., "./configure debug-coverage" or "./configure production-muzzle").
* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h
* split cdlist_black unit test from context_black
* implement CDMap<>.
* give ExprManagers ownership of the context (and have SmtEngine share
that one)
* fix main driver to properly report file-not-found
* fix MemoryMappedInputBuffer class to report reasons for
"errno"-returned system errors
* src/expr/attribute.h: context-dependent attribute kinds now
supported
* test/unit/expr/node_white.h: context-dependent attribute tests
* src/prop/cnf_conversion.h and associated parts of src/util/options.h
and src/main/getopt.cpp: obsolete command-line option, removed.
* src/util/Assert.h: assertions are now somewhat more useful (in debug
builds, anyway) during stack unwinding.
* test/unit/theory/theory_black.h: test context-dependent behavior of
registerTerm() attribute for theories
* src/expr/node_builder.h: formatting, fixes for arithmetic
convenience node builders, check memory allocations
* test/unit/expr/node_builder_black.h: add tessts for addition,
subtraction, unary minus, and multiplication convenience node
builders
* src/expr/attribute.h: more comments
* (various) code formatting, comment cleanup, added throws specifier
to some destructors
* contrib/code-checker: prototype perl script to test (some) code policy
* contrib/indent-settings: command line for GNU indent to indent using
CVC4 style (sort of; this is a work in progress)
* COPYING: legal stuff
* DESIGN_QUESTIONS: obsolete, removed
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r-- | src/expr/node_value.h | 51 |
1 files changed, 35 insertions, 16 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 523c5387b..bd74fd4d4 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -24,7 +24,7 @@ #include "cvc4_config.h" #include <stdint.h> -#include "kind.h" +#include "expr/kind.h" #include <string> #include <iterator> @@ -98,7 +98,7 @@ class NodeValue { NodeValue(int); /** Destructor decrements the ref counts of its children */ - ~NodeValue() throw(); + ~NodeValue(); typedef NodeValue** nv_iterator; typedef NodeValue const* const* const_nv_iterator; @@ -150,16 +150,19 @@ public: } /** - * Hash this expression. + * Hash this NodeValue. For hash_maps, hash_sets, etc.. but this is + * for expr package internal use only at present! This is likely to + * be POORLY PERFORMING for other uses! For example, this gives + * collisions for all VARIABLEs. * @return the hash value of this expression. */ - size_t hash() const { + size_t internalHash() const { size_t hash = d_kind; const_nv_iterator i = nv_begin(); const_nv_iterator i_end = nv_end(); - while (i != i_end) { + while(i != i_end) { hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2); - ++ i; + ++i; } return hash; } @@ -209,7 +212,27 @@ public: static inline Kind dKindToKind(unsigned d) { return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } -}; +};/* class NodeValue */ + +/** + * For hash_maps, hash_sets, etc.. but this is for expr package + * internal use only at present! This is likely to be POORLY + * PERFORMING for other uses! NodeValue::internalHash() will lead to + * collisions for all VARIABLEs. + */ +struct NodeValueInternalHashFcn { + inline size_t operator()(const NodeValue* nv) const { + return (size_t) nv->internalHash(); + } +};/* struct NodeValueHashFcn */ + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#include "node_manager.h" + +namespace CVC4 { +namespace expr { inline NodeValue::NodeValue() : d_id(0), @@ -225,7 +248,7 @@ inline NodeValue::NodeValue(int) : d_nchildren(0) { } -inline NodeValue::~NodeValue() throw() { +inline NodeValue::~NodeValue() { for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { (*i)->dec(); } @@ -243,7 +266,10 @@ inline void NodeValue::dec() { if(EXPECT_TRUE( d_rc < MAX_RC )) { --d_rc; if(EXPECT_FALSE( d_rc == 0 )) { - // FIXME gc + Assert(NodeManager::currentNM() != NULL, + "No current NodeManager on destruction of NodeValue: " + "maybe a public CVC4 interface function is missing a NodeManagerScope ?"); + NodeManager::currentNM()->gc(this); } } } @@ -264,13 +290,6 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const { return d_children + d_nchildren; } -// for hash_maps, hash_sets, ... -struct NodeValueHashFcn { - size_t operator()(const CVC4::expr::NodeValue* nv) const { - return (size_t)nv->hash(); - } -};/* struct NodeValueHashFcn */ - }/* CVC4::expr namespace */ }/* CVC4 namespace */ |