1 /********************* -*- C++ -*- */
3 ** Original author: mdeters
4 ** Major contributors: dejan
5 ** Minor contributors (to current version): none
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009 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
;
41 d_ev(&NodeValue::s_null
) {
45 // FIXME: escape from type system convenient but is there a better
46 // way? Nodes conceptually don't change their expr values but of
47 // course they do modify the refcount. But it's nice to be able to
48 // support node_iterators over const NodeValue*. So.... hm.
49 Node::Node(const NodeValue
* ev
)
50 : d_ev(const_cast<NodeValue
*>(ev
)) {
51 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
55 Node::Node(const Node
& e
) {
56 Assert(e
.d_ev
!= NULL
, "Expecting a non-NULL expression value!");
62 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
66 void Node::assignNodeValue(NodeValue
* ev
) {
71 Node
& Node::operator=(const Node
& e
) {
72 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
73 Assert(e
.d_ev
!= NULL
, "Expecting a non-NULL expression value on RHS!");
74 if(EXPECT_TRUE( d_ev
!= e
.d_ev
)) {
82 uint64_t Node::hash() const {
83 Assert(d_ev
!= NULL
, "Expecting a non-NULL expression value!");
87 Node
Node::eqExpr(const Node
& right
) const {
88 return NodeManager::currentNM()->mkNode(EQUAL
, *this, right
);
91 Node
Node::notExpr() const {
92 return NodeManager::currentNM()->mkNode(NOT
, *this);
95 Node
Node::andExpr(const Node
& right
) const {
96 return NodeManager::currentNM()->mkNode(AND
, *this, right
);
99 Node
Node::orExpr(const Node
& right
) const {
100 return NodeManager::currentNM()->mkNode(OR
, *this, right
);
103 Node
Node::iteExpr(const Node
& thenpart
, const Node
& elsepart
) const {
104 return NodeManager::currentNM()->mkNode(ITE
, *this, thenpart
, elsepart
);
107 Node
Node::iffExpr(const Node
& right
) const {
108 return NodeManager::currentNM()->mkNode(IFF
, *this, right
);
111 Node
Node::impExpr(const Node
& right
) const {
112 return NodeManager::currentNM()->mkNode(IMPLIES
, *this, right
);
115 Node
Node::xorExpr(const Node
& right
) const {
116 return NodeManager::currentNM()->mkNode(XOR
, *this, right
);
119 static void indent(ostream
& o
, int indent
){
120 for(int i
=0; i
< indent
; i
++)
124 void Node::printAst(ostream
& o
, int ind
) const{
128 if(getKind() == VARIABLE
){
131 }else if(getNumChildren() >= 1){
132 for(Node::iterator child
= begin(); child
!= end(); ++child
){
134 (*child
).printAst(o
, ind
+1);
142 void Node::debugPrint(){
143 printAst(Warning(), 0);
147 }/* CVC4 namespace */