src/expr/node.cpp

   1 /*********************                                           -*- C++ -*-  */
   2 /** expr.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/expr_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 ExprValue ExprValue::s_null;
  26
  27 Node Node::s_null(&ExprValue::s_null);
  28
  29 Node Node::null() {
  30   return s_null;
  31 }
  32
  33
  34 bool Node::isNull() const {
  35   return d_ev == &ExprValue::s_null;
  36 }
  37
  38 Node::Node() :
  39   d_ev(&ExprValue::s_null) {
  40   // No refcount needed
  41 }
  42
  43 Node::Node(ExprValue* ev)
  44   : d_ev(ev) {
  45   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  46   d_ev->inc();
  47 }
  48
  49 Node::Node(const Node& e) {
  50   Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
  51   d_ev = e.d_ev;
  52   d_ev->inc();
  53 }
  54
  55 Node::~Node() {
  56   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  57   d_ev->dec();
  58 }
  59
  60 void Node::assignExprValue(ExprValue* ev) {
  61   d_ev = ev;
  62   d_ev->inc();
  63 }
  64
  65 Node& Node::operator=(const Node& e) {
  66   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  67   if(this != &e && d_ev != e.d_ev) {
  68     d_ev->dec();
  69     d_ev = e.d_ev;
  70     d_ev->inc();
  71   }
  72   return *this;
  73 }
  74
  75 ExprValue const* Node::operator->() const {
  76   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  77   return d_ev;
  78 }
  79
  80 uint64_t Node::hash() const {
  81   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
  82   return d_ev->hash();
  83 }
  84
  85 Node Node::eqExpr(const Node& right) const {
  86   return NodeManager::currentEM()->mkExpr(EQUAL, *this, right);
  87 }
  88
  89 Node Node::notExpr() const {
  90   return NodeManager::currentEM()->mkExpr(NOT, *this);
  91 }
  92
  93 Node Node::andExpr(const Node& right) const {
  94   return NodeManager::currentEM()->mkExpr(AND, *this, right);
  95 }
  96
  97 Node Node::orExpr(const Node& right) const {
  98   return NodeManager::currentEM()->mkExpr(OR, *this, right);
  99 }
 100
 101 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
 102   return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
 103 }
 104
 105 Node Node::iffExpr(const Node& right) const {
 106   return NodeManager::currentEM()->mkExpr(IFF, *this, right);
 107 }
 108
 109 Node Node::impExpr(const Node& right) const {
 110   return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right);
 111 }
 112
 113 Node Node::xorExpr(const Node& right) const {
 114   return NodeManager::currentEM()->mkExpr(XOR, *this, right);
 115 }
 116
 117 }/* CVC4 namespace */