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/node_value.h"
15 #include "expr/node_builder.h"
16 #include "util/Assert.h"
20 using namespace CVC4::expr
;
25 NodeValue
NodeValue::s_null
;
27 Node
Node::s_null(&NodeValue::s_null
);
33 bool Node::isNull() const {
34 return d_ev
== &NodeValue::s_null
;
38 d_ev(&NodeValue::s_null
) {
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!");
52 Node::Node(const Node
& e
) {
53 Assert(e
.d_ev
!= NULL
, "Expecting a non-NULL expression value!");
59 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
63 void Node::assignNodeValue(NodeValue
* ev
) {
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
) {
78 NodeValue
const* Node::operator->() const {
79 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
83 uint64_t Node::hash() const {
84 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
88 Node
Node::eqExpr(const Node
& right
) const {
89 return NodeManager::currentNM()->mkExpr(EQUAL
, *this, right
);
92 Node
Node::notExpr() const {
93 return NodeManager::currentNM()->mkExpr(NOT
, *this);
96 Node
Node::andExpr(const Node
& right
) const {
97 return NodeManager::currentNM()->mkExpr(AND
, *this, right
);
100 Node
Node::orExpr(const Node
& right
) const {
101 return NodeManager::currentNM()->mkExpr(OR
, *this, right
);
104 Node
Node::iteExpr(const Node
& thenpart
, const Node
& elsepart
) const {
105 return NodeManager::currentNM()->mkExpr(ITE
, *this, thenpart
, elsepart
);
108 Node
Node::iffExpr(const Node
& right
) const {
109 return NodeManager::currentNM()->mkExpr(IFF
, *this, right
);
112 Node
Node::impExpr(const Node
& right
) const {
113 return NodeManager::currentNM()->mkExpr(IMPLIES
, *this, right
);
116 Node
Node::xorExpr(const Node
& right
) const {
117 return NodeManager::currentNM()->mkExpr(XOR
, *this, right
);
120 }/* CVC4 namespace */