diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 23:01:16 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 23:01:16 +0000 |
commit | 1ca8427a5c79e2e0425a55bc83fe8572055e1660 (patch) | |
tree | c9431983b76c3884a4e34a95c7a94476b95efc51 /src/expr/node_value.h | |
parent | c5872ac197a68ea0686c90f3a8bd1e7cc993532d (diff) |
Merging from branch branches/Liana r241
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r-- | src/expr/node_value.h | 47 |
1 files changed, 22 insertions, 25 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 2d84967c6..73418b06d 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -33,7 +33,7 @@ namespace CVC4 { -class Node; +template <bool ref_count> class NodeTemplate; template <unsigned> class NodeBuilder; class NodeManager; @@ -76,7 +76,7 @@ class NodeValue { // todo add exprMgr ref in debug case - friend class CVC4::Node; + template <bool> friend class CVC4::NodeTemplate; template <unsigned> friend class CVC4::NodeBuilder; friend class CVC4::NodeManager; @@ -103,49 +103,45 @@ class NodeValue { const_ev_iterator ev_begin() const; const_ev_iterator ev_end() const; - class node_iterator { + template <bool ref_count> + class iterator { const_ev_iterator d_i; public: - explicit node_iterator(const_ev_iterator i) : d_i(i) {} + explicit iterator(const_ev_iterator i) : d_i(i) {} - inline Node operator*(); + inline CVC4::NodeTemplate<ref_count> operator*(); - bool operator==(const node_iterator& i) { + bool operator==(const iterator& i) { return d_i == i.d_i; } - bool operator!=(const node_iterator& i) { + bool operator!=(const iterator& i) { return d_i != i.d_i; } - node_iterator operator++() { + iterator operator++() { ++d_i; return *this; } - node_iterator operator++(int) { - return node_iterator(d_i++); + iterator operator++(int) { + return iterator(d_i++); } typedef std::input_iterator_tag iterator_category; - typedef Node value_type; - typedef ptrdiff_t difference_type; - typedef Node* pointer; - typedef Node& reference; }; - typedef node_iterator const_node_iterator; public: - // Iterator support - typedef node_iterator iterator; - typedef node_iterator const_iterator; - - iterator begin(); - iterator end(); + template <bool ref_count> + iterator<ref_count> begin() const { + return iterator<ref_count>(d_children); + } - const_iterator begin() const; - const_iterator end() const; + template <bool ref_count> + iterator<ref_count> end() const { + return iterator<ref_count>(d_children + d_nchildren); + } /** * Hash this expression. @@ -207,8 +203,9 @@ public: namespace CVC4 { namespace expr { -inline Node NodeValue::node_iterator::operator*() { - return Node(*d_i); +template <bool ref_count> +inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*() { + return NodeTemplate<ref_count>(*d_i); } }/* CVC4::expr namespace */ |