1 files changed, 71 insertions, 0 deletions
diff --git a/src/include/expr_value.h b/src/include/expr_value.h
new file mode 100644
index 000000000..ca12b8e03
--- /dev/null
+++ b/src/include/expr_value.h
@@ -0,0 +1,71 @@
+/*********************
+/** expr_value.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** An expression node.
+ **
+ ** Instances of this class are generally referenced through
+ ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
+ ** reference count on ExprValue instances and
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_EXPR_VALUE_H
+#define __CVC4_EXPR_VALUE_H
+
+#include "expr.h"
+
+namespace CVC4 {
+
+/**
+ * This is an ExprValue.
+ */
+class ExprValue {
+  // this header fits into one 64-bit word
+
+  /** The ID */
+  unsigned d_id        : 32;
+
+  /** The expression's reference count.  @see cvc4::Expr. */
+  unsigned d_rc        :  8;
+
+  /** Kind of the expression */
+  unsigned d_kind      :  8;
+
+  /** Number of children */
+  unsigned d_nchildren : 16;
+
+  /** Variable number of child nodes */
+  Expr     d_children[0];
+
+public:
+  /** Hash this expression.
+   *  @return the hash value of this expression. */
+  unsigned hash() const;
+
+  /** Convert to (wrap in) an Expr.
+   *  @return an Expr pointing to this expression. */
+  operator Expr();
+
+  // Iterator support
+
+  typedef Expr* iterator;
+  typedef Expr const* 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;
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_VALUE_H */