src/expr/type_node.h

   1 /*********************                                                        */
   2 /*! \file type_node.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): taking
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Reference-counted encapsulation of a pointer to node information.
  15  **
  16  ** Reference-counted encapsulation of a pointer to node information.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 // circular dependency
  22 #include "expr/node_value.h"
  23
  24 #ifndef __CVC4__TYPE_NODE_H
  25 #define __CVC4__TYPE_NODE_H
  26
  27 #include <vector>
  28 #include <string>
  29 #include <iostream>
  30 #include <stdint.h>
  31
  32 #include "expr/kind.h"
  33 #include "expr/metakind.h"
  34 #include "util/Assert.h"
  35 #include "util/output.h"
  36
  37 namespace CVC4 {
  38
  39 class NodeManager;
  40
  41 namespace expr {
  42 class NodeValue;
  43 }/* CVC4::expr namespace */
  44
  45 /**
  46  * Encapsulation of an NodeValue pointer for Types. The reference count is
  47  * maintained in the NodeValue.
  48  */
  49 class TypeNode {
  50
  51   /**
  52    * The NodeValue has access to the private constructors, so that the
  53    * iterators can can create new types.
  54    */
  55   friend class expr::NodeValue;
  56
  57   /** A convenient null-valued encapsulated pointer */
  58   static TypeNode s_null;
  59
  60   /** The referenced NodeValue */
  61   expr::NodeValue* d_nv;
  62
  63   /**
  64    * This constructor is reserved for use by the TypeNode package.
  65    */
  66   explicit TypeNode(const expr::NodeValue*);
  67
  68   friend class NodeManager;
  69
  70   template <unsigned nchild_thresh>
  71   friend class NodeBuilder;
  72
  73   /**
  74    * Assigns the expression value and does reference counting. No assumptions
  75    * are made on the expression, and should only be used if we know what we
  76    * are doing.
  77    *
  78    * @param ev the expression value to assign
  79    */
  80   void assignNodeValue(expr::NodeValue* ev);
  81
  82 public:
  83
  84   /** Default constructor, makes a null expression. */
  85   TypeNode() : d_nv(&expr::NodeValue::s_null) { }
  86
  87   /** Copy constructor */
  88   TypeNode(const TypeNode& node);
  89
  90   /**
  91    * Assignment operator for nodes, copies the relevant information from node
  92    * to this node.
  93    * @param node the node to copy
  94    * @return reference to this node
  95    */
  96   TypeNode& operator=(const TypeNode& typeNode);
  97
  98   /**
  99    * Destructor. If ref_count is true it will decrement the reference count
 100    * and, if zero, collect the NodeValue.
 101    */
 102   ~TypeNode() throw(AssertionException);
 103
 104   /**
 105    * Return the null node.
 106    * @return the null node
 107    */
 108   static TypeNode null() {
 109     return s_null;
 110   }
 111
 112   /**
 113    * Structural comparison operator for expressions.
 114    * @param typeNode the type node to compare to
 115    * @return true if expressions are equal, false otherwise
 116    */
 117   bool operator==(const TypeNode& typeNode) const {
 118     return d_nv == typeNode.d_nv || (typeNode.isReal() && this->isReal());
 119   }
 120
 121   /**
 122    * Structural comparison operator for expressions.
 123    * @param typeNode the type node to compare to
 124    * @return true if expressions are equal, false otherwise
 125    */
 126   bool operator!=(const TypeNode& typeNode) const {
 127     return !(*this == typeNode);
 128   }
 129
 130   /**
 131    * We compare by expression ids so, keeping things deterministic and having
 132    * that subexpressions have to be smaller than the enclosing expressions.
 133    * @param node the node to compare to
 134    * @return true if this expression is smaller
 135    */
 136   inline bool operator<(const TypeNode& typeNode) const {
 137     return d_nv->d_id < typeNode.d_nv->d_id;
 138   }
 139
 140   /**
 141    * Returns the i-th child of this node.
 142    * @param i the index of the child
 143    * @return the node representing the i-th child
 144    */
 145   TypeNode operator[](int i) const {
 146     return TypeNode(d_nv->getChild(i));
 147   }
 148
 149   /**
 150    * Returns the unique id of this node
 151    * @return the id
 152    */
 153   unsigned getId() const {
 154     return d_nv->getId();
 155   }
 156
 157   /**
 158    * Returns the kind of this type node.
 159    * @return the kind
 160    */
 161   inline Kind getKind() const {
 162     return Kind(d_nv->d_kind);
 163   }
 164
 165   /**
 166    * Returns the metakind of this type node.
 167    * @return the metakind
 168    */
 169   inline kind::MetaKind getMetaKind() const {
 170     return kind::metaKindOf(getKind());
 171   }
 172
 173   /**
 174    * Returns the number of children this node has.
 175    * @return the number of children
 176    */
 177   inline size_t getNumChildren() const;
 178
 179   /**
 180    * If this is a CONST_* TypeNode, extract the constant from it.
 181    */
 182   template <class T>
 183   inline const T& getConst() const;
 184
 185   /**
 186    * Returns the value of the given attribute that this has been attached.
 187    * @param attKind the kind of the attribute
 188    * @return the value of the attribute
 189    */
 190   template <class AttrKind>
 191   inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
 192
 193   // Note that there are two, distinct hasAttribute() declarations for
 194   // a reason (rather than using a pointer-valued argument with a
 195   // default value): they permit more optimized code in the underlying
 196   // hasAttribute() implementations.
 197
 198   /**
 199    * Returns true if this node has been associated an attribute of given kind.
 200    * Additionaly, if a pointer to the value_kind is give, and the attribute
 201    * value has been set for this node, it will be returned.
 202    * @param attKind the kind of the attribute
 203    * @return true if this node has the requested attribute
 204    */
 205   template <class AttrKind>
 206   inline bool hasAttribute(const AttrKind& attKind) const;
 207
 208   /**
 209    * Returns true if this node has been associated an attribute of given kind.
 210    * Additionaly, if a pointer to the value_kind is give, and the attribute
 211    * value has been set for this node, it will be returned.
 212    * @param attKind the kind of the attribute
 213    * @param value where to store the value if it exists
 214    * @return true if this node has the requested attribute
 215    */
 216   template <class AttrKind>
 217   inline bool getAttribute(const AttrKind& attKind,
 218                            typename AttrKind::value_type& value) const;
 219
 220   /**
 221    * Sets the given attribute of this node to the given value.
 222    * @param attKind the kind of the atribute
 223    * @param value the value to set the attribute to
 224    */
 225   template <class AttrKind>
 226   inline void setAttribute(const AttrKind& attKind,
 227                            const typename AttrKind::value_type& value);
 228
 229   /** Iterator allowing for scanning through the children. */
 230   typedef expr::NodeValue::iterator<TypeNode> iterator;
 231   /** Constant iterator allowing for scanning through the children. */
 232   typedef expr::NodeValue::iterator<TypeNode> const_iterator;
 233
 234   /**
 235    * Returns the iterator pointing to the first child.
 236    * @return the iterator
 237    */
 238   inline iterator begin() {
 239     return d_nv->begin<TypeNode>();
 240   }
 241
 242   /**
 243    * Returns the iterator pointing to the end of the children (one beyond the
 244    * last one.
 245    * @return the end of the children iterator.
 246    */
 247   inline iterator end() {
 248     return d_nv->end<TypeNode>();
 249   }
 250
 251   /**
 252    * Returns the const_iterator pointing to the first child.
 253    * @return the const_iterator
 254    */
 255   inline const_iterator begin() const {
 256     return d_nv->begin<TypeNode>();
 257   }
 258
 259   /**
 260    * Returns the const_iterator pointing to the end of the children (one
 261    * beyond the last one.
 262    * @return the end of the children const_iterator.
 263    */
 264   inline const_iterator end() const {
 265     return d_nv->end<TypeNode>();
 266   }
 267
 268   /**
 269    * Converts this node into a string representation.
 270    * @return the string representation of this node.
 271    */
 272   inline std::string toString() const {
 273     return d_nv->toString();
 274   }
 275
 276   /**
 277    * Converst this node into a string representation and sends it to the
 278    * given stream
 279    * @param out the sream to serialise this node to
 280    */
 281   inline void toStream(std::ostream& out, int toDepth = -1) const {
 282     d_nv->toStream(out, toDepth);
 283   }
 284
 285   /**
 286    * Very basic pretty printer for Node.
 287    * @param o output stream to print to.
 288    * @param indent number of spaces to indent the formula by.
 289    */
 290   void printAst(std::ostream & o, int indent = 0) const;
 291
 292   /**
 293    * Returns true if this type is a null type.
 294    * @return true if null
 295    */
 296   bool isNull() const {
 297     return d_nv == &expr::NodeValue::s_null;
 298   }
 299
 300   /** Is this the Boolean type? */
 301   bool isBoolean() const;
 302
 303   /** Is this the Integer type? */
 304   bool isInteger() const;
 305
 306   /** Is this the Real type? */
 307   bool isReal() const;
 308
 309   /** Is this a function type? */
 310   bool isFunction() const;
 311
 312   /** Get the argument types */
 313   std::vector<TypeNode> getArgTypes() const;
 314
 315   /** Get the range type (i.e., the type of the result). */
 316   TypeNode getRangeType() const;
 317
 318   /** Is this a predicate type? NOTE: all predicate types are also
 319       function types. */
 320   bool isPredicate() const;
 321
 322   /** Is this a bit-vector type */
 323   bool isBitVector() const;
 324
 325   /** Is this a bit-vector type of size <code>size</code> */
 326   bool isBitVector(unsigned size) const;
 327
 328   /** Get the size of this bit-vector type */
 329   unsigned getBitVectorSize() const;
 330
 331   /** Is this a sort kind */
 332   bool isSort() const;
 333
 334   /** Is this a kind type (i.e., the type of a type)? */
 335   bool isKind() const;
 336
 337 private:
 338
 339   /**
 340    * Indents the given stream a given amount of spaces.
 341    * @param out the stream to indent
 342    * @param indent the numer of spaces
 343    */
 344   static void indent(std::ostream& out, int indent) {
 345     for(int i = 0; i < indent; i++) {
 346       out << ' ';
 347     }
 348   }
 349
 350 };/* class TypeNode */
 351
 352 /**
 353  * Serializes a given node to the given stream.
 354  * @param out the output stream to use
 355  * @param node the node to output to the stream
 356  * @return the changed stream.
 357  */
 358 inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
 359   n.toStream(out, Node::setdepth::getDepth(out));
 360   return out;
 361 }
 362
 363 }/* CVC4 namespace */
 364
 365 #include <ext/hash_map>
 366
 367 #include "expr/node_manager.h"
 368
 369 namespace CVC4 {
 370
 371 // for hash_maps, hash_sets..
 372 struct TypeNodeHashFunction {
 373   size_t operator()(const CVC4::TypeNode& node) const {
 374     return (size_t) node.getId();
 375   }
 376 };
 377
 378 inline size_t TypeNode::getNumChildren() const {
 379   return d_nv->getNumChildren();
 380 }
 381
 382 template <class T>
 383 inline const T& TypeNode::getConst() const {
 384   return d_nv->getConst<T>();
 385 }
 386
 387 inline TypeNode::TypeNode(const expr::NodeValue* ev) :
 388   d_nv(const_cast<expr::NodeValue*> (ev)) {
 389   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
 390   d_nv->inc();
 391 }
 392
 393 inline TypeNode::TypeNode(const TypeNode& typeNode) {
 394   Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value!");
 395   d_nv = typeNode.d_nv;
 396   d_nv->inc();
 397 }
 398
 399 inline TypeNode::~TypeNode() throw(AssertionException) {
 400   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
 401   d_nv->dec();
 402 }
 403
 404 inline void TypeNode::assignNodeValue(expr::NodeValue* ev) {
 405   d_nv = ev;
 406   d_nv->inc();
 407 }
 408
 409 inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
 410   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
 411   Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
 412   if(EXPECT_TRUE( d_nv != typeNode.d_nv )) {
 413     d_nv->dec();
 414     d_nv = typeNode.d_nv;
 415     d_nv->inc();
 416   }
 417   return *this;
 418 }
 419
 420 template <class AttrKind>
 421 inline typename AttrKind::value_type TypeNode::
 422 getAttribute(const AttrKind&) const {
 423   Assert( NodeManager::currentNM() != NULL,
 424           "There is no current CVC4::NodeManager associated to this thread.\n"
 425           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 426   return NodeManager::currentNM()->getAttribute(d_nv, AttrKind());
 427 }
 428
 429 template <class AttrKind>
 430 inline bool TypeNode::
 431 hasAttribute(const AttrKind&) const {
 432   Assert( NodeManager::currentNM() != NULL,
 433           "There is no current CVC4::NodeManager associated to this thread.\n"
 434           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 435   return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind());
 436 }
 437
 438 template <class AttrKind>
 439 inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
 440   Assert( NodeManager::currentNM() != NULL,
 441           "There is no current CVC4::NodeManager associated to this thread.\n"
 442           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 443   return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret);
 444 }
 445
 446 template <class AttrKind>
 447 inline void TypeNode::
 448 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
 449   Assert( NodeManager::currentNM() != NULL,
 450           "There is no current CVC4::NodeManager associated to this thread.\n"
 451           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 452   NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
 453 }
 454
 455 }/* CVC4 namespace */
 456
 457 #endif /* __CVC4__NODE_H */