src/expr/node.cpp

   1 /*********************                                           -*- C++ -*-  */
   2 /** node.cpp
   3  ** This file is part of the CVC4 prototype.
   4  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   5  ** Courant Institute of Mathematical Sciences
   6  ** New York University
   7  ** See the file COPYING in the top-level source directory for licensing
   8  ** information.
   9  **
  10  ** Reference-counted encapsulation of a pointer to an expression.
  11  **/
  12
  13 #include "expr/node.h"
  14 #include "expr/node_value.h"
  15 #include "expr/node_builder.h"
  16 #include "util/Assert.h"
  17
  18 #include <sstream>
  19
  20 using namespace CVC4::expr;
  21 using namespace std;
  22
  23 namespace CVC4 {
  24
  25 NodeValue NodeValue::s_null;
  26
  27 Node Node::s_null(&NodeValue::s_null);
  28
  29 Node Node::null() {
  30   return s_null;
  31 }
  32
  33 bool Node::isNull() const {
  34   return d_ev == &NodeValue::s_null;
  35 }
  36
  37 Node::Node() :
  38   d_ev(&NodeValue::s_null) {
  39   // No refcount needed
  40 }
  41
  42 // FIXME: escape from type system convenient but is there a better
  43 // way?  Nodes conceptually don't change their expr values but of
  44 // course they do modify the refcount.  But it's nice to be able to
  45 // support node_iterators over const NodeValue*.  So.... hm.
  46 Node::Node(const NodeValue* ev)
  47   : d_ev(const_cast<NodeValue*>(ev)) {
  48   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  49   d_ev->inc();
  50 }
  51
  52 Node::Node(const Node& e) {
  53   Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
  54   d_ev = e.d_ev;
  55   d_ev->inc();
  56 }
  57
  58 Node::~Node() {
  59   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  60   d_ev->dec();
  61 }
  62
  63 void Node::assignNodeValue(NodeValue* ev) {
  64   d_ev = ev;
  65   d_ev->inc();
  66 }
  67
  68 Node& Node::operator=(const Node& e) {
  69   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  70   if(this != &e && d_ev != e.d_ev) {
  71     d_ev->dec();
  72     d_ev = e.d_ev;
  73     d_ev->inc();
  74   }
  75   return *this;
  76 }
  77
  78 NodeValue const* Node::operator->() const {
  79   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  80   return d_ev;
  81 }
  82
  83 uint64_t Node::hash() const {
  84   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  85   return d_ev->hash();
  86 }
  87
  88 Node Node::eqExpr(const Node& right) const {
  89   return NodeManager::currentNM()->mkExpr(EQUAL, *this, right);
  90 }
  91
  92 Node Node::notExpr() const {
  93   return NodeManager::currentNM()->mkExpr(NOT, *this);
  94 }
  95
  96 Node Node::andExpr(const Node& right) const {
  97   return NodeManager::currentNM()->mkExpr(AND, *this, right);
  98 }
  99
 100 Node Node::orExpr(const Node& right) const {
 101   return NodeManager::currentNM()->mkExpr(OR, *this, right);
 102 }
 103
 104 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
 105   return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart);
 106 }
 107
 108 Node Node::iffExpr(const Node& right) const {
 109   return NodeManager::currentNM()->mkExpr(IFF, *this, right);
 110 }
 111
 112 Node Node::impExpr(const Node& right) const {
 113   return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right);
 114 }
 115
 116 Node Node::xorExpr(const Node& right) const {
 117   return NodeManager::currentNM()->mkExpr(XOR, *this, right);
 118 }
 119
 120 }/* CVC4 namespace */