src/expr/node.h

   1 /*********************                                                        */
   2 /** node.h
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): taking
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Reference-counted encapsulation of a pointer to node information.
  14  **/
  15
  16 #include "expr/node_value.h"
  17
  18 #ifndef __CVC4__NODE_H
  19 #define __CVC4__NODE_H
  20
  21 #include <vector>
  22 #include <string>
  23 #include <iostream>
  24 #include <stdint.h>
  25
  26 #include "cvc4_config.h"
  27 #include "expr/kind.h"
  28 #include "expr/type.h"
  29 #include "util/Assert.h"
  30
  31 namespace CVC4 {
  32
  33 class Node;
  34
  35 inline std::ostream& operator<<(std::ostream&, const Node&);
  36
  37 class NodeManager;
  38 class Type;
  39
  40 namespace expr {
  41   class NodeValue;
  42 }/* CVC4::expr namespace */
  43
  44 using CVC4::expr::NodeValue;
  45
  46 /**
  47  * Encapsulation of an NodeValue pointer.  The reference count is
  48  * maintained in the NodeValue.
  49  */
  50 class Node {
  51
  52   friend class NodeValue;
  53
  54   /** A convenient null-valued encapsulated pointer */
  55   static Node s_null;
  56
  57   /** The referenced NodeValue */
  58   NodeValue* d_ev;
  59
  60   /** This constructor is reserved for use by the Node package; one
  61    *  must construct an Node using one of the build mechanisms of the
  62    *  Node package.
  63    *
  64    *  Increments the reference count.
  65    *
  66    *  FIXME: there's a type-system escape here to cast away the const,
  67    *  since the refcount needs to be updated.  But conceptually Nodes
  68    *  don't change their arguments, and it's nice to have
  69    *  const_iterators over them.  See notes in .cpp file for
  70    *  details. */
  71   // this really does needs to be explicit to avoid hard to track
  72   // errors with Nodes implicitly wrapping NodeValues
  73   explicit Node(const NodeValue*);
  74
  75   template <unsigned> friend class NodeBuilder;
  76   friend class NodeManager;
  77
  78   /**
  79    * Assigns the expression value and does reference counting. No assumptions
  80    * are made on the expression, and should only be used if we know what we are
  81    * doing.
  82    *
  83    * @param ev the expression value to assign
  84    */
  85   void assignNodeValue(NodeValue* ev);
  86
  87   typedef NodeValue::ev_iterator ev_iterator;
  88   typedef NodeValue::const_ev_iterator const_ev_iterator;
  89
  90   inline ev_iterator ev_begin();
  91   inline ev_iterator ev_end();
  92   inline const_ev_iterator ev_begin() const;
  93   inline const_ev_iterator ev_end() const;
  94
  95 public:
  96
  97   /** Default constructor, makes a null expression. */
  98   Node();
  99
 100   Node(const Node&);
 101
 102   /** Destructor.  Decrements the reference count and, if zero,
 103    *  collects the NodeValue. */
 104   ~Node();
 105
 106   bool operator==(const Node& e) const { return d_ev == e.d_ev; }
 107   bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
 108
 109   Node operator[](int i) const {
 110     Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
 111     return Node(d_ev->d_children[i]);
 112   }
 113
 114   /**
 115    * We compare by expression ids so, keeping things deterministic and having
 116    * that subexpressions have to be smaller than the enclosing expressions.
 117    */
 118   inline bool operator<(const Node& e) const;
 119
 120   Node& operator=(const Node&);
 121
 122   size_t hash() const { return d_ev->getId(); }
 123   uint64_t getId() const { return d_ev->getId(); }
 124
 125   Node eqExpr(const Node& right) const;
 126   Node notExpr() const;
 127   Node andExpr(const Node& right) const;
 128   Node orExpr(const Node& right) const;
 129   Node iteExpr(const Node& thenpart, const Node& elsepart) const;
 130   Node iffExpr(const Node& right) const;
 131   Node impExpr(const Node& right) const;
 132   Node xorExpr(const Node& right) const;
 133
 134   /*
 135   Node plusExpr(const Node& right) const;
 136   Node uMinusExpr() const;
 137   Node multExpr(const Node& right) const;
 138   */
 139
 140   inline Kind getKind() const;
 141
 142   inline size_t getNumChildren() const;
 143   const Type* getType() const;
 144
 145   static Node null();
 146
 147   typedef NodeValue::node_iterator iterator;
 148   typedef NodeValue::node_iterator const_iterator;
 149
 150   inline iterator begin();
 151   inline iterator end();
 152   inline const_iterator begin() const;
 153   inline const_iterator end() const;
 154
 155   inline std::string toString() const;
 156   inline void toStream(std::ostream&) const;
 157
 158   bool isNull() const;
 159   bool isAtomic() const;
 160
 161   template <class AttrKind>
 162   inline typename AttrKind::value_type getAttribute(const AttrKind&) const;
 163
 164   template <class AttrKind>
 165   inline bool hasAttribute(const AttrKind&,
 166                            typename AttrKind::value_type* = NULL) const;
 167
 168   template <class AttrKind>
 169   inline void setAttribute(const AttrKind&,
 170                            const typename AttrKind::value_type& value);
 171
 172   /**
 173    * Very basic pretty printer for Node.
 174    * @param o output stream to print to.
 175    * @param indent number of spaces to indent the formula by.
 176    */
 177   void printAst(std::ostream & o, int indent = 0) const;
 178
 179 private:
 180
 181   /**
 182    * Pretty printer for use within gdb
 183    * This is not intended to be used outside of gdb.
 184    * This writes to the ostream Warning() and immediately flushes
 185    * the ostream.
 186    */
 187   void debugPrint();
 188
 189 };/* class Node */
 190
 191 }/* CVC4 namespace */
 192
 193 #include <ext/hash_map>
 194
 195 // for hashtables
 196 namespace __gnu_cxx {
 197   template <>
 198   struct hash<CVC4::Node> {
 199     size_t operator()(const CVC4::Node& node) const {
 200       return (size_t)node.hash();
 201     }
 202   };
 203 }/* __gnu_cxx namespace */
 204
 205 #include "expr/attribute.h"
 206 #include "expr/node_manager.h"
 207
 208 namespace CVC4 {
 209
 210 inline bool Node::operator<(const Node& e) const {
 211   return d_ev->d_id < e.d_ev->d_id;
 212 }
 213
 214 inline std::ostream& operator<<(std::ostream& out, const Node& e) {
 215   e.toStream(out);
 216   return out;
 217 }
 218
 219 inline Kind Node::getKind() const {
 220   return Kind(d_ev->d_kind);
 221 }
 222
 223 inline std::string Node::toString() const {
 224   return d_ev->toString();
 225 }
 226
 227 inline void Node::toStream(std::ostream& out) const {
 228   d_ev->toStream(out);
 229 }
 230
 231 inline Node::ev_iterator Node::ev_begin() {
 232   return d_ev->ev_begin();
 233 }
 234
 235 inline Node::ev_iterator Node::ev_end() {
 236   return d_ev->ev_end();
 237 }
 238
 239 inline Node::const_ev_iterator Node::ev_begin() const {
 240   return d_ev->ev_begin();
 241 }
 242
 243 inline Node::const_ev_iterator Node::ev_end() const {
 244   return d_ev->ev_end();
 245 }
 246
 247 inline Node::iterator Node::begin() {
 248   return d_ev->begin();
 249 }
 250
 251 inline Node::iterator Node::end() {
 252   return d_ev->end();
 253 }
 254
 255 inline Node::const_iterator Node::begin() const {
 256   return d_ev->begin();
 257 }
 258
 259 inline Node::const_iterator Node::end() const {
 260   return d_ev->end();
 261 }
 262
 263 inline size_t Node::getNumChildren() const {
 264   return d_ev->d_nchildren;
 265 }
 266
 267 template <class AttrKind>
 268 inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) const {
 269   Assert( NodeManager::currentNM() != NULL,
 270           "There is no current CVC4::NodeManager associated to this thread.\n"
 271           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 272
 273   return NodeManager::currentNM()->getAttribute(*this, AttrKind());
 274 }
 275
 276 template <class AttrKind>
 277 inline bool Node::hasAttribute(const AttrKind&,
 278                                typename AttrKind::value_type* ret) const {
 279   Assert( NodeManager::currentNM() != NULL,
 280           "There is no current CVC4::NodeManager associated to this thread.\n"
 281           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 282
 283   return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
 284 }
 285
 286 template <class AttrKind>
 287 inline void Node::setAttribute(const AttrKind&,
 288                                const typename AttrKind::value_type& value) {
 289   Assert( NodeManager::currentNM() != NULL,
 290           "There is no current CVC4::NodeManager associated to this thread.\n"
 291           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 292
 293   NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
 294 }
 295
 296 }/* CVC4 namespace */
 297
 298 #endif /* __CVC4__NODE_H */