src/expr/node.cpp

   1 /*********************                                                        */
   2 /** node.cpp
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): taking
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Reference-counted encapsulation of a pointer to an expression.
  14  **/
  15
  16 #include "expr/node.h"
  17 #include "expr/node_value.h"
  18 #include "expr/node_builder.h"
  19 #include "util/Assert.h"
  20
  21 #include <sstream>
  22
  23 using namespace CVC4::expr;
  24 using namespace std;
  25
  26 namespace CVC4 {
  27
  28 NodeValue NodeValue::s_null;
  29
  30 Node Node::s_null(&NodeValue::s_null);
  31
  32 Node Node::null() {
  33   return s_null;
  34 }
  35
  36 bool Node::isNull() const {
  37   return d_ev == &NodeValue::s_null;
  38 }
  39
  40 ////FIXME: This function is a major hack! Should be changed ASAP
  41 ////TODO: Should use positive definition, i.e. what kinds are atomic.
  42 bool Node::isAtomic() const {
  43   switch(getKind()) {
  44   case NOT:
  45   case XOR:
  46   case ITE:
  47   case IFF:
  48   case IMPLIES:
  49   case OR:
  50   case AND:
  51     return false;
  52   default:
  53     return true;
  54   }
  55 }
  56
  57 Node::Node() :
  58   d_ev(&NodeValue::s_null) {
  59   // No refcount needed
  60 }
  61
  62 // FIXME: escape from type system convenient but is there a better
  63 // way?  Nodes conceptually don't change their expr values but of
  64 // course they do modify the refcount.  But it's nice to be able to
  65 // support node_iterators over const NodeValue*.  So.... hm.
  66 Node::Node(const NodeValue* ev)
  67   : d_ev(const_cast<NodeValue*>(ev)) {
  68   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  69   d_ev->inc();
  70 }
  71
  72 Node::Node(const Node& e) {
  73   Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
  74   d_ev = e.d_ev;
  75   d_ev->inc();
  76 }
  77
  78 Node::~Node() {
  79   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  80   d_ev->dec();
  81 }
  82
  83 void Node::assignNodeValue(NodeValue* ev) {
  84   d_ev = ev;
  85   d_ev->inc();
  86 }
  87
  88 Node& Node::operator=(const Node& e) {
  89   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  90   Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!");
  91   if(EXPECT_TRUE( d_ev != e.d_ev )) {
  92     d_ev->dec();
  93     d_ev = e.d_ev;
  94     d_ev->inc();
  95   }
  96   return *this;
  97 }
  98
  99 Node Node::eqExpr(const Node& right) const {
 100   Assert( NodeManager::currentNM() != NULL,
 101           "There is no current CVC4::NodeManager associated to this thread.\n"
 102           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 103
 104   return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
 105 }
 106
 107 Node Node::notExpr() const {
 108   Assert( NodeManager::currentNM() != NULL,
 109           "There is no current CVC4::NodeManager associated to this thread.\n"
 110           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 111
 112   return NodeManager::currentNM()->mkNode(NOT, *this);
 113 }
 114
 115 Node Node::andExpr(const Node& right) const {
 116   Assert( NodeManager::currentNM() != NULL,
 117           "There is no current CVC4::NodeManager associated to this thread.\n"
 118           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 119
 120   return NodeManager::currentNM()->mkNode(AND, *this, right);
 121 }
 122
 123 Node Node::orExpr(const Node& right) const {
 124   Assert( NodeManager::currentNM() != NULL,
 125           "There is no current CVC4::NodeManager associated to this thread.\n"
 126           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 127
 128   return NodeManager::currentNM()->mkNode(OR, *this, right);
 129 }
 130
 131 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
 132   Assert( NodeManager::currentNM() != NULL,
 133           "There is no current CVC4::NodeManager associated to this thread.\n"
 134           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 135
 136   return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
 137 }
 138
 139 Node Node::iffExpr(const Node& right) const {
 140   Assert( NodeManager::currentNM() != NULL,
 141           "There is no current CVC4::NodeManager associated to this thread.\n"
 142           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 143
 144   return NodeManager::currentNM()->mkNode(IFF, *this, right);
 145 }
 146
 147 Node Node::impExpr(const Node& right) const {
 148   Assert( NodeManager::currentNM() != NULL,
 149           "There is no current CVC4::NodeManager associated to this thread.\n"
 150           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 151
 152   return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
 153 }
 154
 155 Node Node::xorExpr(const Node& right) const {
 156   Assert( NodeManager::currentNM() != NULL,
 157           "There is no current CVC4::NodeManager associated to this thread.\n"
 158           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 159
 160   return NodeManager::currentNM()->mkNode(XOR, *this, right);
 161 }
 162
 163 const Type* Node::getType() const {
 164   Assert( NodeManager::currentNM() != NULL,
 165           "There is no current CVC4::NodeManager associated to this thread.\n"
 166           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 167   return NodeManager::currentNM()->getType(*this);
 168 }
 169
 170 static void indent(ostream & o, int indent) {
 171   for(int i=0; i < indent; i++) {
 172     o << ' ';
 173   }
 174 }
 175
 176 void Node::printAst(ostream & o, int ind) const {
 177   indent(o, ind);
 178   o << '(';
 179   o << getKind();
 180   if(getKind() == VARIABLE) {
 181     o << ' ' << getId();
 182   } else if(getNumChildren() >= 1) {
 183     for(Node::iterator child = begin(); child != end(); ++child) {
 184       o << endl;
 185       (*child).printAst(o, ind + 1);
 186     }
 187     o << endl;
 188     indent(o, ind);
 189   }
 190   o << ')';
 191 }
 192
 193 void Node::debugPrint() {
 194 #ifndef CVC4_MUZZLE
 195   printAst(Warning(), 0);
 196   Warning().flush();
 197 #endif /* ! CVC4_MUZZLE */
 198 }
 199
 200 }/* CVC4 namespace */