1 files changed, 115 insertions, 0 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
new file mode 100644
index 000000000..22a905470
--- /dev/null
+++ b/src/expr/node.cpp
@@ -0,0 +1,115 @@
+/*********************                                           -*- C++ -*-  */
+/** expr.cpp
+ ** 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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **/
+
+#include "expr/node.h"
+#include "expr/expr_value.h"
+#include "expr/node_builder.h"
+#include "util/Assert.h"
+
+using namespace CVC4::expr;
+
+namespace CVC4 {
+
+ExprValue ExprValue::s_null;
+
+Node Node::s_null(&ExprValue::s_null);
+
+bool Node::isNull() const {
+  return d_ev == &ExprValue::s_null;
+}
+
+Node::Node() :
+  d_ev(&ExprValue::s_null) {
+  // No refcount needed
+}
+
+Node::Node(ExprValue* ev)
+  : d_ev(ev) {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  d_ev->inc();
+}
+
+Node::Node(const Node& e) {
+  Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
+  d_ev = e.d_ev;
+  d_ev->inc();
+}
+
+Node::~Node() {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  d_ev->dec();
+}
+
+void Node::assignExprValue(ExprValue* ev) {
+  d_ev = ev;
+  d_ev->inc();
+}
+
+Node& Node::operator=(const Node& e) {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  if(this != &e && d_ev != e.d_ev) {
+    d_ev->dec();
+    d_ev = e.d_ev;
+    d_ev->inc();
+  }
+  return *this;
+}
+
+ExprValue const* Node::operator->() const {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  return d_ev;
+}
+
+uint64_t Node::hash() const {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  return d_ev->hash();
+}
+
+Node Node::eqExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(EQUAL, *this, right);
+}
+
+Node Node::notExpr() const {
+  return NodeManager::currentEM()->mkExpr(NOT, *this);
+}
+
+// FIXME: What does this do and why?
+Node Node::negate() const { // avoid double-negatives
+  return NodeBuilder(*this).negate();
+}
+
+
+Node Node::andExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(AND, *this, right);
+}
+
+Node Node::orExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(OR, *this, right);
+}
+
+Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
+  return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
+}
+
+Node Node::iffExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(IFF, *this, right);
+}
+
+Node Node::impExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right);
+}
+
+Node Node::xorExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(XOR, *this, right);
+}
+
+}/* CVC4 namespace */