-/********************* -*- C++ -*- */
+/********************* */
/** 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 The Analysis of Computer Systems Group (ACSys)
+ ** 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
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
Node& Node::operator=(const Node& e) {
Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
- if((this != &e) && (d_ev != e.d_ev)) {
+ 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;
}
-NodeValue 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::currentNM()->mkExpr(EQUAL, *this, right);
+ 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 {
- return NodeManager::currentNM()->mkExpr(NOT, *this);
+ 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 {
- return NodeManager::currentNM()->mkExpr(AND, *this, right);
+ 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 {
- return NodeManager::currentNM()->mkExpr(OR, *this, right);
+ 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 {
- return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart);
+ 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 {
- return NodeManager::currentNM()->mkExpr(IFF, *this, right);
+ 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 {
- return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right);
+ 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 {
- return NodeManager::currentNM()->mkExpr(XOR, *this, right);
+ 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 */