1 /********************* */
3 ** Original author: dejan
4 ** This file is part of the CVC4 prototype.
5 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
6 ** Courant Institute of Mathematical Sciences
8 ** See the file COPYING in the top-level source directory for licensing
11 ** Reference-counted encapsulation of a pointer to node information.
14 #include "cvc4_private.h"
16 // circular dependency
17 #include "expr/node_value.h"
19 #ifndef __CVC4__TYPE_NODE_H
20 #define __CVC4__TYPE_NODE_H
27 #include "expr/kind.h"
28 #include "expr/metakind.h"
29 #include "util/Assert.h"
30 #include "util/output.h"
38 }/* CVC4::expr namespace */
41 * Encapsulation of an NodeValue pointer. The reference count is
42 * maintained in the NodeValue if ref_count is true.
47 * The NodeValue has access to the private constructors, so that the
48 * iterators can can create new nodes.
50 friend class expr::NodeValue
;
52 /** A convenient null-valued encapsulated pointer */
53 static TypeNode s_null
;
55 /** The referenced NodeValue */
56 expr::NodeValue
* d_nv
;
59 * This constructor is reserved for use by the TypeNode package.
61 explicit TypeNode(const expr::NodeValue
*);
63 friend class NodeManager
;
65 template <class Builder
>
66 friend class NodeBuilderBase
;
69 * Assigns the expression value and does reference counting. No assumptions
70 * are made on the expression, and should only be used if we know what we
73 * @param ev the expression value to assign
75 void assignNodeValue(expr::NodeValue
* ev
);
79 /** Default constructor, makes a null expression. */
80 TypeNode() : d_nv(&expr::NodeValue::s_null
) { }
82 /** Copy constructor */
83 TypeNode(const TypeNode
& node
);
86 * Assignment operator for nodes, copies the relevant information from node
88 * @param node the node to copy
89 * @return reference to this node
91 TypeNode
& operator=(const TypeNode
& typeNode
);
94 * Destructor. If ref_count is true it will decrement the reference count
95 * and, if zero, collect the NodeValue.
97 ~TypeNode() throw(AssertionException
);
100 * Return the null node.
101 * @return the null node
103 static TypeNode
null() {
108 * Returns true if this type is a null type.
109 * @return true if null
111 bool isNull() const {
112 return d_nv
== &expr::NodeValue::s_null
;
116 * Structural comparison operator for expressions.
117 * @param typeNode the type node to compare to
118 * @return true if expressions are equal, false otherwise
120 bool operator==(const TypeNode
& typeNode
) const {
121 return d_nv
== typeNode
.d_nv
;
125 * Structural comparison operator for expressions.
126 * @param typeNode the type node to compare to
127 * @return true if expressions are equal, false otherwise
129 bool operator!=(const TypeNode
& typeNode
) const {
130 return d_nv
!= typeNode
.d_nv
;
134 * We compare by expression ids so, keeping things deterministic and having
135 * that subexpressions have to be smaller than the enclosing expressions.
136 * @param node the node to compare to
137 * @return true if this expression is smaller
139 inline bool operator<(const TypeNode
& typeNode
) const {
140 return d_nv
->d_id
< typeNode
.d_nv
->d_id
;
144 * Returns the i-th child of this node.
145 * @param i the index of the child
146 * @return the node representing the i-th child
148 TypeNode
operator[](int i
) const {
149 return TypeNode(d_nv
->getChild(i
));
153 * Returns the unique id of this node
156 unsigned getId() const {
157 return d_nv
->getId();
161 * Returns the kind of this type node.
164 inline Kind
getKind() const {
165 return Kind(d_nv
->d_kind
);
169 * Returns the metakind of this type node.
170 * @return the metakind
172 inline kind::MetaKind
getMetaKind() const {
173 return kind::metaKindOf(getKind());
177 * Returns the number of children this node has.
178 * @return the number of children
180 inline size_t getNumChildren() const;
183 * If this is a CONST_* TypeNode, extract the constant from it.
186 inline const T
& getConst() const;
189 * Returns the value of the given attribute that this has been attached.
190 * @param attKind the kind of the attribute
191 * @return the value of the attribute
193 template <class AttrKind
>
194 inline typename
AttrKind::value_type
getAttribute(const AttrKind
& attKind
) const;
196 // Note that there are two, distinct hasAttribute() declarations for
197 // a reason (rather than using a pointer-valued argument with a
198 // default value): they permit more optimized code in the underlying
199 // hasAttribute() implementations.
202 * Returns true if this node has been associated an attribute of given kind.
203 * Additionaly, if a pointer to the value_kind is give, and the attribute
204 * value has been set for this node, it will be returned.
205 * @param attKind the kind of the attribute
206 * @return true if this node has the requested attribute
208 template <class AttrKind
>
209 inline bool hasAttribute(const AttrKind
& attKind
) const;
212 * Returns true if this node has been associated an attribute of given kind.
213 * Additionaly, if a pointer to the value_kind is give, and the attribute
214 * value has been set for this node, it will be returned.
215 * @param attKind the kind of the attribute
216 * @param value where to store the value if it exists
217 * @return true if this node has the requested attribute
219 template <class AttrKind
>
220 inline bool getAttribute(const AttrKind
& attKind
,
221 typename
AttrKind::value_type
& value
) const;
224 * Sets the given attribute of this node to the given value.
225 * @param attKind the kind of the atribute
226 * @param value the value to set the attribute to
228 template <class AttrKind
>
229 inline void setAttribute(const AttrKind
& attKind
,
230 const typename
AttrKind::value_type
& value
);
232 /** Iterator allowing for scanning through the children. */
233 typedef expr::NodeValue::iterator
<TypeNode
> iterator
;
234 /** Constant iterator allowing for scanning through the children. */
235 typedef expr::NodeValue::iterator
<TypeNode
> const_iterator
;
238 * Returns the iterator pointing to the first child.
239 * @return the iterator
241 inline iterator
begin() {
242 return d_nv
->begin
<TypeNode
>();
246 * Returns the iterator pointing to the end of the children (one beyond the
248 * @return the end of the children iterator.
250 inline iterator
end() {
251 return d_nv
->end
<TypeNode
>();
255 * Returns the const_iterator pointing to the first child.
256 * @return the const_iterator
258 inline const_iterator
begin() const {
259 return d_nv
->begin
<TypeNode
>();
263 * Returns the const_iterator pointing to the end of the children (one
264 * beyond the last one.
265 * @return the end of the children const_iterator.
267 inline const_iterator
end() const {
268 return d_nv
->end
<TypeNode
>();
272 * Converts this node into a string representation.
273 * @return the string representation of this node.
275 inline std::string
toString() const {
276 return d_nv
->toString();
280 * Converst this node into a string representation and sends it to the
282 * @param out the sream to serialise this node to
284 inline void toStream(std::ostream
& out
, int toDepth
= -1) const {
285 d_nv
->toStream(out
, toDepth
);
289 * Very basic pretty printer for Node.
290 * @param o output stream to print to.
291 * @param indent number of spaces to indent the formula by.
293 void printAst(std::ostream
& o
, int indent
= 0) const;
295 /** Is this the Boolean type? */
296 bool isBoolean() const;
298 /** Is this a function type? */
299 bool isFunction() const;
301 /** Get the argument types */
302 std::vector
<TypeNode
> getArgTypes() const;
304 /** Get the range type (i.e., the type of the result). */
305 TypeNode
getRangeType() const;
307 /** Is this a predicate type? NOTE: all predicate types are also
309 bool isPredicate() const;
311 /** Is this a sort kind */
314 /** Is this a kind type (i.e., the type of a type)? */
320 * Indents the given stream a given amount of spaces.
321 * @param out the stream to indent
322 * @param indent the numer of spaces
324 static void indent(std::ostream
& out
, int indent
) {
325 for(int i
= 0; i
< indent
; i
++) {
330 };/* class TypeNode */
333 * Serializes a given node to the given stream.
334 * @param out the output stream to use
335 * @param node the node to output to the stream
336 * @return the changed stream.
338 inline std::ostream
& operator<<(std::ostream
& out
, const TypeNode
& n
) {
339 n
.toStream(out
, Node::setdepth::getDepth(out
));
343 }/* CVC4 namespace */
345 #include <ext/hash_map>
347 #include "expr/node_manager.h"
351 // for hash_maps, hash_sets..
352 struct TypeNodeHashFunction
{
353 size_t operator()(const CVC4::TypeNode
& node
) const {
354 return (size_t) node
.getId();
358 inline size_t TypeNode::getNumChildren() const {
359 return d_nv
->getNumChildren();
363 inline const T
& TypeNode::getConst() const {
364 return d_nv
->getConst
<T
>();
367 inline TypeNode::TypeNode(const expr::NodeValue
* ev
) :
368 d_nv(const_cast<expr::NodeValue
*> (ev
)) {
369 Assert(d_nv
!= NULL
, "Expecting a non-NULL expression value!");
373 inline TypeNode::TypeNode(const TypeNode
& typeNode
) {
374 Assert(typeNode
.d_nv
!= NULL
, "Expecting a non-NULL expression value!");
375 d_nv
= typeNode
.d_nv
;
379 inline TypeNode::~TypeNode() throw(AssertionException
) {
380 Assert(d_nv
!= NULL
, "Expecting a non-NULL expression value!");
384 inline void TypeNode::assignNodeValue(expr::NodeValue
* ev
) {
389 inline TypeNode
& TypeNode::operator=(const TypeNode
& typeNode
) {
390 Assert(d_nv
!= NULL
, "Expecting a non-NULL expression value!");
391 Assert(typeNode
.d_nv
!= NULL
, "Expecting a non-NULL expression value on RHS!");
392 if(EXPECT_TRUE( d_nv
!= typeNode
.d_nv
)) {
394 d_nv
= typeNode
.d_nv
;
400 template <class AttrKind
>
401 inline typename
AttrKind::value_type
TypeNode::
402 getAttribute(const AttrKind
&) const {
403 Assert( NodeManager::currentNM() != NULL
,
404 "There is no current CVC4::NodeManager associated to this thread.\n"
405 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
406 return NodeManager::currentNM()->getAttribute(d_nv
, AttrKind());
409 template <class AttrKind
>
410 inline bool TypeNode::
411 hasAttribute(const AttrKind
&) const {
412 Assert( NodeManager::currentNM() != NULL
,
413 "There is no current CVC4::NodeManager associated to this thread.\n"
414 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
415 return NodeManager::currentNM()->hasAttribute(d_nv
, AttrKind());
418 template <class AttrKind
>
419 inline bool TypeNode::getAttribute(const AttrKind
&, typename
AttrKind::value_type
& ret
) const {
420 Assert( NodeManager::currentNM() != NULL
,
421 "There is no current CVC4::NodeManager associated to this thread.\n"
422 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
423 return NodeManager::currentNM()->getAttribute(d_nv
, AttrKind(), ret
);
426 template <class AttrKind
>
427 inline void TypeNode::
428 setAttribute(const AttrKind
&, const typename
AttrKind::value_type
& value
) {
429 Assert( NodeManager::currentNM() != NULL
,
430 "There is no current CVC4::NodeManager associated to this thread.\n"
431 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
432 NodeManager::currentNM()->setAttribute(d_nv
, AttrKind(), value
);
435 }/* CVC4 namespace */
437 #endif /* __CVC4__NODE_H */