1 /********************* */
3 ** Original author: mdeters
4 ** Major contributors: taking, dejan
5 ** Minor contributors (to current version): none
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** Reference-counted encapsulation of a pointer to an expression.
16 #include "expr/node.h"
17 #include "expr/node_value.h"
18 #include "expr/node_builder.h"
19 #include "util/Assert.h"
23 using namespace CVC4::expr
;
28 NodeValue
NodeValue::s_null
;
30 Node
Node::s_null(&NodeValue::s_null
);
36 bool Node::isNull() const {
37 return d_ev
== &NodeValue::s_null
;
40 ////FIXME: This function is a major hack! Should be changed ASAP
41 ////TODO: Should use positive definition, i.e. what kinds are atomic.
42 bool Node::isAtomic() const {
58 d_ev(&NodeValue::s_null
) {
62 // FIXME: escape from type system convenient but is there a better
63 // way? Nodes conceptually don't change their expr values but of
64 // course they do modify the refcount. But it's nice to be able to
65 // support node_iterators over const NodeValue*. So.... hm.
66 Node::Node(const NodeValue
* ev
)
67 : d_ev(const_cast<NodeValue
*>(ev
)) {
68 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
72 Node::Node(const Node
& e
) {
73 Assert(e
.d_ev
!= NULL
, "Expecting a non-NULL expression value!");
79 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
83 void Node::assignNodeValue(NodeValue
* ev
) {
88 Node
& Node::operator=(const Node
& e
) {
89 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
90 Assert(e
.d_ev
!= NULL
, "Expecting a non-NULL expression value on RHS!");
91 if(EXPECT_TRUE( d_ev
!= e
.d_ev
)) {
99 Node
Node::eqExpr(const Node
& right
) const {
100 return NodeManager::currentNM()->mkNode(EQUAL
, *this, right
);
103 Node
Node::notExpr() const {
104 return NodeManager::currentNM()->mkNode(NOT
, *this);
107 Node
Node::andExpr(const Node
& right
) const {
108 return NodeManager::currentNM()->mkNode(AND
, *this, right
);
111 Node
Node::orExpr(const Node
& right
) const {
112 return NodeManager::currentNM()->mkNode(OR
, *this, right
);
115 Node
Node::iteExpr(const Node
& thenpart
, const Node
& elsepart
) const {
116 return NodeManager::currentNM()->mkNode(ITE
, *this, thenpart
, elsepart
);
119 Node
Node::iffExpr(const Node
& right
) const {
120 return NodeManager::currentNM()->mkNode(IFF
, *this, right
);
123 Node
Node::impExpr(const Node
& right
) const {
124 return NodeManager::currentNM()->mkNode(IMPLIES
, *this, right
);
127 Node
Node::xorExpr(const Node
& right
) const {
128 return NodeManager::currentNM()->mkNode(XOR
, *this, right
);
131 static void indent(ostream
& o
, int indent
){
132 for(int i
=0; i
< indent
; i
++)
136 void Node::printAst(ostream
& o
, int ind
) const {
140 if(getKind() == VARIABLE
){
143 }else if(getNumChildren() >= 1){
144 for(Node::iterator child
= begin(); child
!= end(); ++child
){
146 (*child
).printAst(o
, ind
+ 1);
154 void Node::debugPrint() {
156 printAst(Warning(), 0);
158 #endif /* ! CVC4_MUZZLE */
161 }/* CVC4 namespace */