Extracted the public Expr and ExprManager interface to encapsulate the optimized expressions and the internal expression manager.

1 files changed, 8 insertions, 6 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 22a905470..be9ac995c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -15,7 +15,10 @@
 #include "expr/node_builder.h"
 #include "util/Assert.h"
 
+#include <sstream>
+
 using namespace CVC4::expr;
+using namespace std;
 
 namespace CVC4 {
 
@@ -23,6 +26,11 @@ ExprValue ExprValue::s_null;
 
 Node Node::s_null(&ExprValue::s_null);
 
+Node Node::null() {
+  return s_null;
+}
+
+
 bool Node::isNull() const {
   return d_ev == &ExprValue::s_null;
 }
@@ -82,12 +90,6 @@ 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);
 }