src/expr/node.cpp

   1 /*********************                                           -*- C++ -*-  */
   2 /** node.cpp
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009 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 Node::Node() :
  41   d_ev(&NodeValue::s_null) {
  42   // No refcount needed
  43 }
  44
  45 // FIXME: escape from type system convenient but is there a better
  46 // way?  Nodes conceptually don't change their expr values but of
  47 // course they do modify the refcount.  But it's nice to be able to
  48 // support node_iterators over const NodeValue*.  So.... hm.
  49 Node::Node(const NodeValue* ev)
  50   : d_ev(const_cast<NodeValue*>(ev)) {
  51   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  52   d_ev->inc();
  53 }
  54
  55 Node::Node(const Node& e) {
  56   Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
  57   d_ev = e.d_ev;
  58   d_ev->inc();
  59 }
  60
  61 Node::~Node() {
  62   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  63   d_ev->dec();
  64 }
  65
  66 void Node::assignNodeValue(NodeValue* ev) {
  67   d_ev = ev;
  68   d_ev->inc();
  69 }
  70
  71 Node& Node::operator=(const Node& e) {
  72   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  73   Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!");
  74   if(EXPECT_TRUE( d_ev != e.d_ev )) {
  75     d_ev->dec();
  76     d_ev = e.d_ev;
  77     d_ev->inc();
  78   }
  79   return *this;
  80 }
  81
  82 uint64_t Node::hash() const {
  83   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  84   return d_ev->hash();
  85 }
  86
  87 Node Node::eqExpr(const Node& right) const {
  88   return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
  89 }
  90
  91 Node Node::notExpr() const {
  92   return NodeManager::currentNM()->mkNode(NOT, *this);
  93 }
  94
  95 Node Node::andExpr(const Node& right) const {
  96   return NodeManager::currentNM()->mkNode(AND, *this, right);
  97 }
  98
  99 Node Node::orExpr(const Node& right) const {
 100   return NodeManager::currentNM()->mkNode(OR, *this, right);
 101 }
 102
 103 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
 104   return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
 105 }
 106
 107 Node Node::iffExpr(const Node& right) const {
 108   return NodeManager::currentNM()->mkNode(IFF, *this, right);
 109 }
 110
 111 Node Node::impExpr(const Node& right) const {
 112   return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
 113 }
 114
 115 Node Node::xorExpr(const Node& right) const {
 116   return NodeManager::currentNM()->mkNode(XOR, *this, right);
 117 }
 118
 119 static void indent(ostream & o, int indent){
 120   for(int i=0; i < indent; i++)
 121     o << ' ';
 122 }
 123
 124 void Node::printAst(ostream & o, int ind) const{
 125   indent(o, ind);
 126   o << '(';
 127   o << getKind();
 128   if(getKind() == VARIABLE){
 129     o << ' ' << getId();
 130
 131   }else if(getNumChildren() >= 1){
 132     for(Node::iterator child = begin(); child != end(); ++child){
 133       o << endl;
 134       (*child).printAst(o, ind+1);
 135     }
 136     o << endl;
 137     indent(o, ind);
 138   }
 139   o << ')';
 140 }
 141
 142 void Node::debugPrint(){
 143   printAst(Warning(), 0);
 144   Warning().flush();
 145 }
 146
 147 }/* CVC4 namespace */