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   Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!");
  71   if(EXPECT_TRUE( d_ev != e.d_ev )) {
  72     d_ev->dec();
  73     d_ev = e.d_ev;
  74     d_ev->inc();
  75   }
  76   return *this;
  77 }
  78
  79 NodeValue const* Node::operator->() const {
  80   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  81   return d_ev;
  82 }
  83
  84 uint64_t Node::hash() const {
  85   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  86   return d_ev->hash();
  87 }
  88
  89 Node Node::eqExpr(const Node& right) const {
  90   return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
  91 }
  92
  93 Node Node::notExpr() const {
  94   return NodeManager::currentNM()->mkNode(NOT, *this);
  95 }
  96
  97 Node Node::andExpr(const Node& right) const {
  98   return NodeManager::currentNM()->mkNode(AND, *this, right);
  99 }
 100
 101 Node Node::orExpr(const Node& right) const {
 102   return NodeManager::currentNM()->mkNode(OR, *this, right);
 103 }
 104
 105 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
 106   return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
 107 }
 108
 109 Node Node::iffExpr(const Node& right) const {
 110   return NodeManager::currentNM()->mkNode(IFF, *this, right);
 111 }
 112
 113 Node Node::impExpr(const Node& right) const {
 114   return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
 115 }
 116
 117 Node Node::xorExpr(const Node& right) const {
 118   return NodeManager::currentNM()->mkNode(XOR, *this, right);
 119 }
 120
 121 }/* CVC4 namespace */