diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-26 21:37:34 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-26 21:37:34 +0000 |
commit | 3ee48833fd8cffe897a05a986c08a30d9de57213 (patch) | |
tree | db56dd28b96b12414a763ee9104adc8389225ca5 /src/expr/node.h | |
parent | 96733823eadf9ff566a177cf74e19d1712c48e4b (diff) |
Adding the intermediary TypeNode to represent (and separate) the Types at the Node level.
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 27756da5b..f8d9117c7 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -33,7 +33,7 @@ namespace CVC4 { -class Type; +class TypeNode; class NodeManager; template <bool ref_count> @@ -229,7 +229,7 @@ public: * Returns the unique id of this node * @return the ud */ - uint64_t getId() const { + unsigned getId() const { return d_nv->getId(); } @@ -247,7 +247,7 @@ public: * Returns the type of this node. * @return the type */ - Type getType() const; + TypeNode getType() const; /** * Returns the kind of this node. @@ -322,16 +322,16 @@ public: const typename AttrKind::value_type& value); /** Iterator allowing for scanning through the children. */ - typedef typename expr::NodeValue::iterator<ref_count> iterator; + typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > iterator; /** Constant iterator allowing for scanning through the children. */ - typedef typename expr::NodeValue::iterator<ref_count> const_iterator; + typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > const_iterator; /** * Returns the iterator pointing to the first child. * @return the iterator */ inline iterator begin() { - return d_nv->begin<ref_count>(); + return d_nv->begin< NodeTemplate<ref_count> >(); } /** @@ -340,7 +340,7 @@ public: * @return the end of the children iterator. */ inline iterator end() { - return d_nv->end<ref_count>(); + return d_nv->end< NodeTemplate<ref_count> >(); } /** @@ -348,7 +348,7 @@ public: * @return the const_iterator */ inline const_iterator begin() const { - return d_nv->begin<ref_count>(); + return d_nv->begin< NodeTemplate<ref_count> >(); } /** @@ -357,7 +357,7 @@ public: * @return the end of the children const_iterator. */ inline const_iterator end() const { - return d_nv->end<ref_count>(); + return d_nv->end< NodeTemplate<ref_count> >(); } /** @@ -814,7 +814,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { } template <bool ref_count> -Type NodeTemplate<ref_count>::getType() const { +TypeNode NodeTemplate<ref_count>::getType() const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); |