1 /********************* -*- C++ -*- */
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
7 ** See the file COPYING in the top-level source directory for licensing
10 ** Reference-counted encapsulation of a pointer to an expression.
13 #include "expr/node.h"
14 #include "expr/expr_value.h"
15 #include "expr/node_builder.h"
16 #include "util/Assert.h"
20 using namespace CVC4::expr
;
25 ExprValue
ExprValue::s_null
;
27 Node
Node::s_null(&ExprValue::s_null
);
34 bool Node::isNull() const {
35 return d_ev
== &ExprValue::s_null
;
39 d_ev(&ExprValue::s_null
) {
43 Node::Node(ExprValue
* ev
)
45 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
49 Node::Node(const Node
& e
) {
50 Assert(e
.d_ev
!= NULL
, "Expecting a non-NULL expression value!");
56 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
60 void Node::assignExprValue(ExprValue
* ev
) {
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
) {
75 ExprValue
const* Node::operator->() const {
76 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
80 uint64_t Node::hash() const {
81 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
85 Node
Node::eqExpr(const Node
& right
) const {
86 return NodeManager::currentEM()->mkExpr(EQUAL
, *this, right
);
89 Node
Node::notExpr() const {
90 return NodeManager::currentEM()->mkExpr(NOT
, *this);
93 Node
Node::andExpr(const Node
& right
) const {
94 return NodeManager::currentEM()->mkExpr(AND
, *this, right
);
97 Node
Node::orExpr(const Node
& right
) const {
98 return NodeManager::currentEM()->mkExpr(OR
, *this, right
);
101 Node
Node::iteExpr(const Node
& thenpart
, const Node
& elsepart
) const {
102 return NodeManager::currentEM()->mkExpr(ITE
, *this, thenpart
, elsepart
);
105 Node
Node::iffExpr(const Node
& right
) const {
106 return NodeManager::currentEM()->mkExpr(IFF
, *this, right
);
109 Node
Node::impExpr(const Node
& right
) const {
110 return NodeManager::currentEM()->mkExpr(IMPLIES
, *this, right
);
113 Node
Node::xorExpr(const Node
& right
) const {
114 return NodeManager::currentEM()->mkExpr(XOR
, *this, right
);
117 }/* CVC4 namespace */