diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-02 20:33:26 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-02 20:33:26 +0000 |
commit | 2b87789ee57a738cccd89dd9d2d81b065875dc29 (patch) | |
tree | f5376c532490088e5dcc7a37ed318127a0dc8c40 /src/expr/node_value.h | |
parent | 7f5036bb37e13dbc7e176d4fa82ee0736d11e913 (diff) |
* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"
(etc.) now work for Nodes a, b, c, d, e. Also refcounting fixes for
NodeBuilder in certain cases
* (various places) don't overload __gnu_cxx::hash<>, instead provide
an explicit hash function to hash_maps and hash_sets.
* add a new kind of assert, DtorAssert(), which doesn't throw
exceptions (right now it operates like a usual C assert()). For use
in destructors.
* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).
* fix some Make rule dependencies
* reformat node.h as per code formatting policy
* added Theory and NodeBuilder unit tests
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r-- | src/expr/node_value.h | 29 |
1 files changed, 23 insertions, 6 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 0ad7ba559..523c5387b 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -98,7 +98,7 @@ class NodeValue { NodeValue(int); /** Destructor decrements the ref counts of its children */ - ~NodeValue(); + ~NodeValue() throw(); typedef NodeValue** nv_iterator; typedef NodeValue const* const* const_nv_iterator; @@ -165,17 +165,26 @@ public: } inline bool compareTo(const NodeValue* nv) const { - if(d_kind != nv->d_kind) + if(d_kind != nv->d_kind) { return false; - if(d_nchildren != nv->d_nchildren) + } + + if(d_nchildren != nv->d_nchildren) { return false; + } + const_nv_iterator i = nv_begin(); const_nv_iterator j = nv->nv_begin(); const_nv_iterator i_end = nv_end(); + while(i != i_end) { - if ((*i) != (*j)) return false; - ++i; ++j; + if((*i) != (*j)) { + return false; + } + ++i; + ++j; } + return true; } @@ -196,6 +205,7 @@ public: static inline unsigned kindToDKind(Kind k) { return ((unsigned) k) & kindMask; } + static inline Kind dKindToKind(unsigned d) { return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } @@ -215,7 +225,7 @@ inline NodeValue::NodeValue(int) : d_nchildren(0) { } -inline NodeValue::~NodeValue() { +inline NodeValue::~NodeValue() throw() { for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { (*i)->dec(); } @@ -254,6 +264,13 @@ 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 */ |