1 files changed, 189 insertions, 0 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
new file mode 100644
index 000000000..9bdbb7f8c
--- /dev/null
+++ b/src/expr/node_value.h
@@ -0,0 +1,189 @@
+/*********************                                           -*- C++ -*-  */
+/** node_value.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** An expression node.
+ **
+ ** Instances of this class are generally referenced through
+ ** cvc4::Node rather than by pointer; cvc4::Node maintains the
+ ** reference count on NodeValue instances and
+ **/
+
+/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */
+/* to resolve a circular dependency */
+//#include "expr/node.h"
+
+#ifndef __CVC4__EXPR__NODE_VALUE_H
+#define __CVC4__EXPR__NODE_VALUE_H
+
+#include "cvc4_config.h"
+#include <stdint.h>
+#include "kind.h"
+
+#include <string>
+
+namespace CVC4 {
+
+class Node;
+template <unsigned> class NodeBuilder;
+class NodeManager;
+
+namespace expr {
+
+/**
+ * This is an NodeValue.
+ */
+class NodeValue {
+
+  /** A convenient null-valued expression value */
+  static NodeValue s_null;
+
+  /** Maximum reference count possible.  Used for sticky
+   *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
+  static const unsigned MAX_RC = 255;
+
+  // this header fits into one 64-bit word
+
+  /** The ID (0 is reserved for the null value) */
+  unsigned d_id        : 32;
+
+  /** The expression's reference count.  @see cvc4::Node. */
+  unsigned d_rc        :  8;
+
+  /** Kind of the expression */
+  unsigned d_kind      :  8;
+
+  /** Number of children */
+  unsigned d_nchildren : 16;
+
+  /** Variable number of child nodes */
+  NodeValue *d_children[0];
+
+  // todo add exprMgr ref in debug case
+
+  friend class CVC4::Node;
+  template <unsigned> friend class CVC4::NodeBuilder;
+  friend class CVC4::NodeManager;
+
+  NodeValue* inc();
+  NodeValue* dec();
+
+  static size_t next_id;
+
+  /** Private default constructor for the null value. */
+  NodeValue();
+
+  /** Private default constructor for the NodeBuilder. */
+  NodeValue(int);
+
+  /** Destructor decrements the ref counts of its children */
+  ~NodeValue();
+
+  /**
+   * Computes the hash over the given iterator span of children, and the
+   * root hash. The iterator should be either over a range of Node or pointers
+   * to NodeValue.
+   * @param hash the initial value for the hash
+   * @param begin the begining of the range
+   * @param end the end of the range
+   * @return the hash value
+   */
+  template<typename const_iterator_type>
+  static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) {
+    for(const_iterator_type i = begin; i != end; ++i) {
+      hash = computeHash(hash, *i);
+    }
+    return hash;
+  }
+
+  static uint64_t computeHash(uint64_t hash, const NodeValue* ev) {
+    return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId();
+  }
+
+  typedef NodeValue** ev_iterator;
+  typedef NodeValue const* const* const_ev_iterator;
+
+  ev_iterator ev_begin();
+  ev_iterator ev_end();
+  ev_iterator ev_rbegin();
+  ev_iterator ev_rend();
+
+  const_ev_iterator ev_begin() const;
+  const_ev_iterator ev_end() const;
+  const_ev_iterator ev_rbegin() const;
+  const_ev_iterator ev_rend() const;
+
+  class node_iterator {
+    const_ev_iterator d_i;
+  public:
+    node_iterator(const_ev_iterator i) : d_i(i) {}
+
+    inline Node operator*();
+
+    bool operator==(const node_iterator& i) {
+      return d_i == i.d_i;
+    }
+
+    bool operator!=(const node_iterator& i) {
+      return d_i != i.d_i;
+    }
+
+    node_iterator& operator++() {
+      ++d_i;
+      return *this;
+    }
+
+    node_iterator operator++(int) {
+      return node_iterator(d_i++);
+    }
+  };
+  typedef node_iterator const_node_iterator;
+
+public:
+  /** Hash this expression.
+   *  @return the hash value of this expression. */
+  uint64_t hash() const;
+
+  // Iterator support
+
+  typedef node_iterator iterator;
+  typedef node_iterator const_iterator;
+
+  iterator begin();
+  iterator end();
+  iterator rbegin();
+  iterator rend();
+
+  const_iterator begin() const;
+  const_iterator end() const;
+  const_iterator rbegin() const;
+  const_iterator rend() const;
+
+  unsigned getId() const { return d_id; }
+  Kind getKind() const { return (Kind) d_kind; }
+  unsigned numChildren() const { return d_nchildren; }
+  std::string toString() const;
+  void toStream(std::ostream& out) const;
+};
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+inline Node NodeValue::node_iterator::operator*() {
+  return Node(*d_i);
+}
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__NODE_VALUE_H */