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 78c4f9186fdc2c958db607f15d1e12318c646ddc..080623e21e63c7a04342f9e89e3893ea4c50d6df 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,10 +1,10 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** node.cpp
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** 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
@@ -37,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
@@ -79,67 +96,105 @@ Node& Node::operator=(const Node& e) {
   return *this;
 }
 
-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 {
+  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);
 }
 
-void indent(ostream & o, int indent){
-  for(int i=0; i < indent; i++)
+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{
+void Node::printAst(ostream & o, int ind) const {
   indent(o, ind);
   o << '(';
   o << getKind();
-  if(getKind() == VARIABLE){
+  if(getKind() == VARIABLE) {
     o << ' ' << getId();
-
-  }else if(getNumChildren() >= 1){
-    for(Node::iterator child = begin(); child != end(); ++child){
-      (*child).printAst(o, ind+1);
+  } 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(){
+
+void Node::debugPrint() {
+#ifndef CVC4_MUZZLE
   printAst(Warning(), 0);
   Warning().flush();
+#endif /* ! CVC4_MUZZLE */
 }
 
 }/* CVC4 namespace */