diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-11 04:00:14 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-11 04:00:14 +0000 |
commit | d26cd7a159bb56f492e21b7536f68abf821ca02a (patch) | |
tree | 3f601cae6490a8bfb4dc7dcdcc5c9b4dd1a75711 /src/expr/node.cpp | |
parent | 82faddb718aaae5f52001e09d0754a3d254e2285 (diff) |
Extracted the public Expr and ExprManager interface to encapsulate the optimized expressions and the internal expression manager.
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r-- | src/expr/node.cpp | 14 |
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); } |