summaryrefslogtreecommitdiff
path: root/src/expr/node.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r--src/expr/node.cpp14
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback