Switching to types-as-attributes in parser

[cvc5.git] / src / expr / node.cpp

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index f1b3c5980d29e1250e18aedd8d919605aeda4ebf..080623e21e63c7a04342f9e89e3893ea4c50d6df 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,7 +1,10 @@
-/*********************                                           -*- 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
@@ -34,6 +37,23 @@ 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
@@ -67,7 +87,8 @@ void Node::assignNodeValue(NodeValue* ev) {
 
 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();
@@ -75,46 +96,105 @@ Node& Node::operator=(const Node& e) {
   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 */