diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 23:15:48 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 23:15:48 +0000 |
commit | ad223d3d5e5d19b04790dd48e586774e64735e3b (patch) | |
tree | b9a0feb7fc981cd2e46e93e268ca388b1a3727a9 /src/expr/node.cpp | |
parent | 1ca8427a5c79e2e0425a55bc83fe8572055e1660 (diff) |
finally works
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r-- | src/expr/node.cpp | 203 |
1 files changed, 0 insertions, 203 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp deleted file mode 100644 index b9d3d13bb..000000000 --- a/src/expr/node.cpp +++ /dev/null @@ -1,203 +0,0 @@ -<<<<<<< .working -/********************* */ -/** node.cpp - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 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/node_value.h" -#include "expr/node_builder.h" -#include "util/Assert.h" - -#include <sstream> - -using namespace CVC4::expr; -using namespace std; - -namespace CVC4 { - -NodeValue NodeValue::s_null; - -Node Node::s_null(&NodeValue::s_null); - -Node Node::null() { - return s_null; -} - -bool Node::isNull() const { - return d_ev == &NodeValue::s_null; -} - -////FIXME: This function is a major hack! Should be changed ASAP -////TODO: Should use positive definition, i.e. what kinds are atomic. -bool Node::isAtomic() const { - switch(getKind()) { - case NOT: - case XOR: - case ITE: - case IFF: - case IMPLIES: - case OR: - case AND: - return false; - default: - return true; - } -} - -Node::Node() : - d_ev(&NodeValue::s_null) { - // No refcount needed -} - -// FIXME: escape from type system convenient but is there a better -// way? Nodes conceptually don't change their expr values but of -// course they do modify the refcount. But it's nice to be able to -// support node_iterators over const NodeValue*. So.... hm. -Node::Node(const NodeValue* ev) - : d_ev(const_cast<NodeValue*>(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::assignNodeValue(NodeValue* ev) { - d_ev = ev; - d_ev->inc(); -} - -Node& Node::operator=(const Node& e) { - Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); - Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!"); - if(EXPECT_TRUE( d_ev != e.d_ev )) { - d_ev->dec(); - d_ev = e.d_ev; - d_ev->inc(); - } - return *this; -} - -Node Node::eqExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - - return NodeManager::currentNM()->mkNode(EQUAL, *this, right); -} - -Node Node::notExpr() const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - - return NodeManager::currentNM()->mkNode(NOT, *this); -} - -Node Node::andExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - - return NodeManager::currentNM()->mkNode(AND, *this, right); -} - -Node Node::orExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - - return NodeManager::currentNM()->mkNode(OR, *this, right); -} - -Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - - return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); -} - -Node Node::iffExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - - return NodeManager::currentNM()->mkNode(IFF, *this, right); -} - -Node Node::impExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - - return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); -} - -Node Node::xorExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - - return NodeManager::currentNM()->mkNode(XOR, *this, right); -} - -const Type* Node::getType() const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->getType(*this); -} - -static void indent(ostream & o, int indent) { - for(int i=0; i < indent; i++) { - o << ' '; - } -} - -void Node::printAst(ostream & o, int ind) const { - indent(o, ind); - o << '('; - o << getKind(); - if(getKind() == VARIABLE) { - o << ' ' << getId(); - } else if(getNumChildren() >= 1) { - for(Node::iterator child = begin(); child != end(); ++child) { - o << endl; - (*child).printAst(o, ind + 1); - } - o << endl; - indent(o, ind); - } - o << ')'; -} - -void Node::debugPrint() { -#ifndef CVC4_MUZZLE - printAst(Warning(), 0); - Warning().flush(); -#endif /* ! CVC4_MUZZLE */ -} - -}/* CVC4 namespace */ -======= ->>>>>>> .merge-right.r241 |