src/expr/type_node.h

   1 /*********************                                                        */
   2 /** type_node.h
   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
   7  ** New York University
   8  ** See the file COPYING in the top-level source directory for licensing
   9  ** information.
  10  **
  11  ** Reference-counted encapsulation of a pointer to node information.
  12  **/
  13
  14 #include "cvc4_private.h"
  15
  16 // circular dependency
  17 #include "expr/node_value.h"
  18
  19 #ifndef __CVC4__TYPE_NODE_H
  20 #define __CVC4__TYPE_NODE_H
  21
  22 #include <vector>
  23 #include <string>
  24 #include <iostream>
  25 #include <stdint.h>
  26
  27 #include "expr/kind.h"
  28 #include "expr/metakind.h"
  29 #include "util/Assert.h"
  30 #include "util/output.h"
  31
  32 namespace CVC4 {
  33
  34 class NodeManager;
  35
  36 namespace expr {
  37 class NodeValue;
  38 }/* CVC4::expr namespace */
  39
  40 /**
  41  * Encapsulation of an NodeValue pointer.  The reference count is
  42  * maintained in the NodeValue if ref_count is true.
  43  */
  44 class TypeNode {
  45
  46   /**
  47    * The NodeValue has access to the private constructors, so that the
  48    * iterators can can create new nodes.
  49    */
  50   friend class expr::NodeValue;
  51
  52   /** A convenient null-valued encapsulated pointer */
  53   static TypeNode s_null;
  54
  55   /** The referenced NodeValue */
  56   expr::NodeValue* d_nv;
  57
  58   /**
  59    * This constructor is reserved for use by the TypeNode package.
  60    */
  61   explicit TypeNode(const expr::NodeValue*);
  62
  63   friend class NodeManager;
  64
  65   template <class Builder>
  66   friend class NodeBuilderBase;
  67
  68   /**
  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
  71    * are doing.
  72    *
  73    * @param ev the expression value to assign
  74    */
  75   void assignNodeValue(expr::NodeValue* ev);
  76
  77 public:
  78
  79   /** Default constructor, makes a null expression. */
  80   TypeNode() : d_nv(&expr::NodeValue::s_null) { }
  81
  82   /** Copy constructor */
  83   TypeNode(const TypeNode& node);
  84
  85   /**
  86    * Assignment operator for nodes, copies the relevant information from node
  87    * to this node.
  88    * @param node the node to copy
  89    * @return reference to this node
  90    */
  91   TypeNode& operator=(const TypeNode& typeNode);
  92
  93   /**
  94    * Destructor. If ref_count is true it will decrement the reference count
  95    * and, if zero, collect the NodeValue.
  96    */
  97   ~TypeNode() throw(AssertionException);
  98
  99   /**
 100    * Return the null node.
 101    * @return the null node
 102    */
 103   static TypeNode null() {
 104     return s_null;
 105   }
 106
 107   /**
 108    * Returns true if this type is a null type.
 109    * @return true if null
 110    */
 111   bool isNull() const {
 112     return d_nv == &expr::NodeValue::s_null;
 113   }
 114
 115   /**
 116    * Structural comparison operator for expressions.
 117    * @param typeNode the type node to compare to
 118    * @return true if expressions are equal, false otherwise
 119    */
 120   bool operator==(const TypeNode& typeNode) const {
 121     return d_nv == typeNode.d_nv;
 122   }
 123
 124   /**
 125    * Structural comparison operator for expressions.
 126    * @param typeNode the type node to compare to
 127    * @return true if expressions are equal, false otherwise
 128    */
 129   bool operator!=(const TypeNode& typeNode) const {
 130     return d_nv != typeNode.d_nv;
 131   }
 132
 133   /**
 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
 138    */
 139   inline bool operator<(const TypeNode& typeNode) const {
 140     return d_nv->d_id < typeNode.d_nv->d_id;
 141   }
 142
 143   /**
 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
 147    */
 148   TypeNode operator[](int i) const {
 149     return TypeNode(d_nv->getChild(i));
 150   }
 151
 152   /**
 153    * Returns the unique id of this node
 154    * @return the id
 155    */
 156   unsigned getId() const {
 157     return d_nv->getId();
 158   }
 159
 160   /**
 161    * Returns the kind of this type node.
 162    * @return the kind
 163    */
 164   inline Kind getKind() const {
 165     return Kind(d_nv->d_kind);
 166   }
 167
 168   /**
 169    * Returns the metakind of this type node.
 170    * @return the metakind
 171    */
 172   inline kind::MetaKind getMetaKind() const {
 173     return kind::metaKindOf(getKind());
 174   }
 175
 176   /**
 177    * Returns the number of children this node has.
 178    * @return the number of children
 179    */
 180   inline size_t getNumChildren() const;
 181
 182   /**
 183    * If this is a CONST_* TypeNode, extract the constant from it.
 184    */
 185   template <class T>
 186   inline const T& getConst() const;
 187
 188   /**
 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
 192    */
 193   template <class AttrKind>
 194   inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
 195
 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.
 200
 201   /**
 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
 207    */
 208   template <class AttrKind>
 209   inline bool hasAttribute(const AttrKind& attKind) const;
 210
 211   /**
 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
 218    */
 219   template <class AttrKind>
 220   inline bool getAttribute(const AttrKind& attKind,
 221                            typename AttrKind::value_type& value) const;
 222
 223   /**
 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
 227    */
 228   template <class AttrKind>
 229   inline void setAttribute(const AttrKind& attKind,
 230                            const typename AttrKind::value_type& value);
 231
 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;
 236
 237   /**
 238    * Returns the iterator pointing to the first child.
 239    * @return the iterator
 240    */
 241   inline iterator begin() {
 242     return d_nv->begin<TypeNode>();
 243   }
 244
 245   /**
 246    * Returns the iterator pointing to the end of the children (one beyond the
 247    * last one.
 248    * @return the end of the children iterator.
 249    */
 250   inline iterator end() {
 251     return d_nv->end<TypeNode>();
 252   }
 253
 254   /**
 255    * Returns the const_iterator pointing to the first child.
 256    * @return the const_iterator
 257    */
 258   inline const_iterator begin() const {
 259     return d_nv->begin<TypeNode>();
 260   }
 261
 262   /**
 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.
 266    */
 267   inline const_iterator end() const {
 268     return d_nv->end<TypeNode>();
 269   }
 270
 271   /**
 272    * Converts this node into a string representation.
 273    * @return the string representation of this node.
 274    */
 275   inline std::string toString() const {
 276     return d_nv->toString();
 277   }
 278
 279   /**
 280    * Converst this node into a string representation and sends it to the
 281    * given stream
 282    * @param out the sream to serialise this node to
 283    */
 284   inline void toStream(std::ostream& out, int toDepth = -1) const {
 285     d_nv->toStream(out, toDepth);
 286   }
 287
 288   /**
 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.
 292    */
 293   void printAst(std::ostream & o, int indent = 0) const;
 294
 295   /** Is this the Boolean type? */
 296   bool isBoolean() const;
 297
 298   /** Is this a function type? */
 299   bool isFunction() const;
 300
 301   /** Get the argument types */
 302   std::vector<TypeNode> getArgTypes() const;
 303
 304   /** Get the range type (i.e., the type of the result). */
 305   TypeNode getRangeType() const;
 306
 307   /** Is this a predicate type? NOTE: all predicate types are also
 308       function types. */
 309   bool isPredicate() const;
 310
 311   /** Is this a sort kind */
 312   bool isSort() const;
 313
 314   /** Is this a kind type (i.e., the type of a type)? */
 315   bool isKind() const;
 316
 317 private:
 318
 319   /**
 320    * Indents the given stream a given amount of spaces.
 321    * @param out the stream to indent
 322    * @param indent the numer of spaces
 323    */
 324   static void indent(std::ostream& out, int indent) {
 325     for(int i = 0; i < indent; i++) {
 326       out << ' ';
 327     }
 328   }
 329
 330 };/* class TypeNode */
 331
 332 /**
 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.
 337  */
 338 inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
 339   n.toStream(out, Node::setdepth::getDepth(out));
 340   return out;
 341 }
 342
 343 }/* CVC4 namespace */
 344
 345 #include <ext/hash_map>
 346
 347 #include "expr/node_manager.h"
 348
 349 namespace CVC4 {
 350
 351 // for hash_maps, hash_sets..
 352 struct TypeNodeHashFunction {
 353   size_t operator()(const CVC4::TypeNode& node) const {
 354     return (size_t) node.getId();
 355   }
 356 };
 357
 358 inline size_t TypeNode::getNumChildren() const {
 359   return d_nv->getNumChildren();
 360 }
 361
 362 template <class T>
 363 inline const T& TypeNode::getConst() const {
 364   return d_nv->getConst<T>();
 365 }
 366
 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!");
 370   d_nv->inc();
 371 }
 372
 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;
 376   d_nv->inc();
 377 }
 378
 379 inline TypeNode::~TypeNode() throw(AssertionException) {
 380   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
 381   d_nv->dec();
 382 }
 383
 384 inline void TypeNode::assignNodeValue(expr::NodeValue* ev) {
 385   d_nv = ev;
 386   d_nv->inc();
 387 }
 388
 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 )) {
 393     d_nv->dec();
 394     d_nv = typeNode.d_nv;
 395     d_nv->inc();
 396   }
 397   return *this;
 398 }
 399
 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());
 407 }
 408
 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());
 416 }
 417
 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);
 424 }
 425
 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);
 433 }
 434
 435 }/* CVC4 namespace */
 436
 437 #endif /* __CVC4__NODE_H */