src/expr/node.cpp

   1 /*********************                                                        */
   2 /** node.cpp
   3  ** Original author: mdeters
   4  ** Major contributors: taking, dejan
   5  ** Minor contributors (to current version): none
   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   return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
 101 }
 102
 103 Node Node::notExpr() const {
 104   return NodeManager::currentNM()->mkNode(NOT, *this);
 105 }
 106
 107 Node Node::andExpr(const Node& right) const {
 108   return NodeManager::currentNM()->mkNode(AND, *this, right);
 109 }
 110
 111 Node Node::orExpr(const Node& right) const {
 112   return NodeManager::currentNM()->mkNode(OR, *this, right);
 113 }
 114
 115 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
 116   return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
 117 }
 118
 119 Node Node::iffExpr(const Node& right) const {
 120   return NodeManager::currentNM()->mkNode(IFF, *this, right);
 121 }
 122
 123 Node Node::impExpr(const Node& right) const {
 124   return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
 125 }
 126
 127 Node Node::xorExpr(const Node& right) const {
 128   return NodeManager::currentNM()->mkNode(XOR, *this, right);
 129 }
 130
 131 static void indent(ostream & o, int indent){
 132   for(int i=0; i < indent; i++)
 133     o << ' ';
 134 }
 135
 136 void Node::printAst(ostream & o, int ind) const {
 137   indent(o, ind);
 138   o << '(';
 139   o << getKind();
 140   if(getKind() == VARIABLE){
 141     o << ' ' << getId();
 142
 143   }else if(getNumChildren() >= 1){
 144     for(Node::iterator child = begin(); child != end(); ++child){
 145       o << endl;
 146       (*child).printAst(o, ind + 1);
 147     }
 148     o << endl;
 149     indent(o, ind);
 150   }
 151   o << ')';
 152 }
 153
 154 void Node::debugPrint() {
 155 #ifndef CVC4_MUZZLE
 156   printAst(Warning(), 0);
 157   Warning().flush();
 158 #endif /* ! CVC4_MUZZLE */
 159 }
 160
 161 }/* CVC4 namespace */