src/expr/node_value.h

   1 /*********************                                                        */
   2 /** node_value.h
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): none
   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  ** An expression node.
  14  **
  15  ** Instances of this class are generally referenced through
  16  ** cvc4::Node rather than by pointer; cvc4::Node maintains the
  17  ** reference count on NodeValue instances and
  18  **/
  19
  20 /* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */
  21 /* to resolve a circular dependency */
  22 //#include "expr/node.h"
  23
  24 #ifndef __CVC4__EXPR__NODE_VALUE_H
  25 #define __CVC4__EXPR__NODE_VALUE_H
  26
  27 #include "cvc4_config.h"
  28 #include <stdint.h>
  29 #include "kind.h"
  30
  31 #include <string>
  32 #include <iterator>
  33
  34 namespace CVC4 {
  35
  36 class Node;
  37 template <unsigned> class NodeBuilder;
  38 class NodeManager;
  39
  40 namespace expr {
  41
  42 /**
  43  * This is an NodeValue.
  44  */
  45 class NodeValue {
  46
  47   /** A convenient null-valued expression value */
  48   static NodeValue s_null;
  49
  50   /** Maximum reference count possible.  Used for sticky
  51    *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
  52   static const unsigned MAX_RC = 255;
  53
  54   /** Number of bits assigned to the kind in the NodeValue header */
  55   static const unsigned KINDBITS = 8;
  56
  57   /** A mask for d_kind */
  58   static const unsigned kindMask = (1u << KINDBITS) - 1;
  59
  60   // this header fits into one 64-bit word
  61
  62   /** The ID (0 is reserved for the null value) */
  63   unsigned d_id        : 32;
  64
  65   /** The expression's reference count.  @see cvc4::Node. */
  66   unsigned d_rc        :  8;
  67
  68   /** Kind of the expression */
  69   unsigned d_kind      : KINDBITS;
  70
  71   /** Number of children */
  72   unsigned d_nchildren : 16;
  73
  74   /** Variable number of child nodes */
  75   NodeValue *d_children[0];
  76
  77   // todo add exprMgr ref in debug case
  78
  79   friend class CVC4::Node;
  80   template <unsigned> friend class CVC4::NodeBuilder;
  81   friend class CVC4::NodeManager;
  82
  83   void inc();
  84   void dec();
  85
  86   static size_t next_id;
  87
  88   /** Private default constructor for the null value. */
  89   NodeValue();
  90
  91   /** Private default constructor for the NodeBuilder. */
  92   NodeValue(int);
  93
  94   /** Destructor decrements the ref counts of its children */
  95   ~NodeValue();
  96
  97   typedef NodeValue** ev_iterator;
  98   typedef NodeValue const* const* const_ev_iterator;
  99
 100   ev_iterator ev_begin();
 101   ev_iterator ev_end();
 102
 103   const_ev_iterator ev_begin() const;
 104   const_ev_iterator ev_end() const;
 105
 106   class node_iterator {
 107     const_ev_iterator d_i;
 108   public:
 109     explicit node_iterator(const_ev_iterator i) : d_i(i) {}
 110
 111     inline Node operator*();
 112
 113     bool operator==(const node_iterator& i) {
 114       return d_i == i.d_i;
 115     }
 116
 117     bool operator!=(const node_iterator& i) {
 118       return d_i != i.d_i;
 119     }
 120
 121     node_iterator operator++() {
 122       ++d_i;
 123       return *this;
 124     }
 125
 126     node_iterator operator++(int) {
 127       return node_iterator(d_i++);
 128     }
 129
 130     typedef std::input_iterator_tag iterator_category;
 131     typedef Node value_type;
 132     typedef ptrdiff_t difference_type;
 133     typedef Node* pointer;
 134     typedef Node& reference;
 135   };
 136   typedef node_iterator const_node_iterator;
 137
 138 public:
 139
 140   // Iterator support
 141   typedef node_iterator iterator;
 142   typedef node_iterator const_iterator;
 143
 144   iterator begin();
 145   iterator end();
 146
 147   const_iterator begin() const;
 148   const_iterator end() const;
 149
 150   /**
 151    * Hash this expression.
 152    * @return the hash value of this expression.
 153    */
 154   size_t hash() const {
 155     size_t hash = d_kind;
 156     const_ev_iterator i = ev_begin();
 157     const_ev_iterator i_end = ev_end();
 158     while (i != i_end) {
 159       hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 160       ++ i;
 161     }
 162     return hash;
 163   }
 164
 165   inline bool compareTo(const NodeValue* nv) const {
 166     if(d_kind != nv->d_kind)
 167       return false;
 168     if(d_nchildren != nv->d_nchildren)
 169       return false;
 170     const_ev_iterator i = ev_begin();
 171     const_ev_iterator j = nv->ev_begin();
 172     const_ev_iterator i_end = ev_end();
 173     while(i != i_end) {
 174       if ((*i) != (*j)) return false;
 175       ++i; ++j;
 176     }
 177     return true;
 178   }
 179
 180   // Comparison predicate
 181   struct NodeValueEq {
 182     bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
 183       return nv1->compareTo(nv2);
 184     }
 185   };
 186
 187   unsigned getId() const { return d_id; }
 188   Kind getKind() const { return dKindToKind(d_kind); }
 189   unsigned getNumChildren() const { return d_nchildren; }
 190
 191   std::string toString() const;
 192   void toStream(std::ostream& out) const;
 193
 194   static inline unsigned kindToDKind(Kind k) {
 195     return ((unsigned) k) & kindMask;
 196   }
 197   static inline Kind dKindToKind(unsigned d) {
 198     return (d == kindMask) ? UNDEFINED_KIND : Kind(d);
 199   }
 200 };
 201
 202 }/* CVC4::expr namespace */
 203 }/* CVC4 namespace */
 204
 205 #include "expr/node.h"
 206
 207 namespace CVC4 {
 208 namespace expr {
 209
 210 inline Node NodeValue::node_iterator::operator*() {
 211   return Node(*d_i);
 212 }
 213
 214 }/* CVC4::expr namespace */
 215 }/* CVC4 namespace */
 216
 217 #endif /* __CVC4__EXPR__NODE_VALUE_H */