1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
|
/********************* -*- C++ -*- */
/** node.cpp
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
** Reference-counted encapsulation of a pointer to an expression.
**/
#include "expr/node.h"
#include "expr/node_value.h"
#include "expr/node_builder.h"
#include "util/Assert.h"
#include <sstream>
using namespace CVC4::expr;
using namespace std;
namespace CVC4 {
NodeValue NodeValue::s_null;
Node Node::s_null(&NodeValue::s_null);
Node Node::null() {
return s_null;
}
bool Node::isNull() const {
return d_ev == &NodeValue::s_null;
}
Node::Node() :
d_ev(&NodeValue::s_null) {
// No refcount needed
}
// FIXME: escape from type system convenient but is there a better
// way? Nodes conceptually don't change their expr values but of
// course they do modify the refcount. But it's nice to be able to
// support node_iterators over const NodeValue*. So.... hm.
Node::Node(const NodeValue* ev)
: d_ev(const_cast<NodeValue*>(ev)) {
Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
d_ev->inc();
}
Node::Node(const Node& e) {
Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
d_ev = e.d_ev;
d_ev->inc();
}
Node::~Node() {
Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
d_ev->dec();
}
void Node::assignNodeValue(NodeValue* ev) {
d_ev = ev;
d_ev->inc();
}
Node& Node::operator=(const Node& e) {
Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!");
if(EXPECT_TRUE( d_ev != e.d_ev )) {
d_ev->dec();
d_ev = e.d_ev;
d_ev->inc();
}
return *this;
}
uint64_t Node::hash() const {
Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
return d_ev->hash();
}
Node Node::eqExpr(const Node& right) const {
return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
}
Node Node::notExpr() const {
return NodeManager::currentNM()->mkNode(NOT, *this);
}
Node Node::andExpr(const Node& right) const {
return NodeManager::currentNM()->mkNode(AND, *this, right);
}
Node Node::orExpr(const Node& right) const {
return NodeManager::currentNM()->mkNode(OR, *this, right);
}
Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
}
Node Node::iffExpr(const Node& right) const {
return NodeManager::currentNM()->mkNode(IFF, *this, right);
}
Node Node::impExpr(const Node& right) const {
return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
}
Node Node::xorExpr(const Node& right) const {
return NodeManager::currentNM()->mkNode(XOR, *this, right);
}
static void indent(ostream & o, int indent){
for(int i=0; i < indent; i++)
o << ' ';
}
void Node::printAst(ostream & o, int ind) const{
indent(o, ind);
o << '(';
o << getKind();
if(getKind() == VARIABLE){
o << ' ' << getId();
}else if(getNumChildren() >= 1){
for(Node::iterator child = begin(); child != end(); ++child){
o << endl;
(*child).printAst(o, ind+1);
}
o << endl;
indent(o, ind);
}
o << ')';
}
void Node::debugPrint(){
printAst(Warning(), 0);
Warning().flush();
}
}/* CVC4 namespace */
|
