blob: aec50000ecb4a8f41183b7eac587832f6f8ed028 (
plain)
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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
/********************* -*- C++ -*- */
/** cvc4_expr.h
** 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.
**/
#ifndef __CVC4__EXPR_H
#define __CVC4__EXPR_H
#include <vector>
#include <iostream>
#include <stdint.h>
#include "cvc4_config.h"
#include "expr/kind.h"
namespace CVC4 {
class Node;
}/* CVC4 namespace */
namespace CVC4 {
inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC;
class NodeManager;
namespace expr {
class ExprValue;
}/* CVC4::expr namespace */
using CVC4::expr::ExprValue;
/**
* Encapsulation of an ExprValue pointer. The reference count is
* maintained in the ExprValue.
*/
class CVC4_PUBLIC Node {
friend class ExprValue;
/** A convenient null-valued encapsulated pointer */
static Node s_null;
/** The referenced ExprValue */
ExprValue* d_ev;
/** This constructor is reserved for use by the Node package; one
* must construct an Node using one of the build mechanisms of the
* Node package.
*
* Increments the reference count. */
explicit Node(ExprValue*);
friend class NodeBuilder;
friend class NodeManager;
/** Access to the encapsulated expression.
* @return the encapsulated expression. */
ExprValue const* operator->() const;
/**
* Assigns the expression value and does reference counting. No assumptions are
* made on the expression, and should only be used if we know what we are
* doing.
*
* @param ev the expression value to assign
*/
void assignExprValue(ExprValue* ev);
public:
/** Default constructor, makes a null expression. */
Node();
Node(const Node&);
/** Destructor. Decrements the reference count and, if zero,
* collects the ExprValue. */
~Node();
bool operator==(const Node& e) const { return d_ev == e.d_ev; }
bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
/**
* We compare by expression ids so, keeping things deterministic and having
* that subexpressions have to be smaller than the enclosing expressions.
*/
inline bool operator<(const Node& e) const;
Node& operator=(const Node&);
uint64_t hash() const;
Node eqExpr(const Node& right) const;
Node notExpr() const;
Node negate() const; // avoid double-negatives
Node andExpr(const Node& right) const;
Node orExpr(const Node& right) const;
Node iteExpr(const Node& thenpart, const Node& elsepart) const;
Node iffExpr(const Node& right) const;
Node impExpr(const Node& right) const;
Node xorExpr(const Node& right) const;
Node plusExpr(const Node& right) const;
Node uMinusExpr() const;
Node multExpr(const Node& right) const;
inline Kind getKind() const;
inline size_t numChildren() const;
static Node null() { return s_null; }
typedef Node* iterator;
typedef Node const* const_iterator;
inline iterator begin();
inline iterator end();
inline const_iterator begin() const;
inline const_iterator end() const;
void toString(std::ostream&) const;
bool isNull() const;
};/* class Node */
}/* CVC4 namespace */
#include "expr/expr_value.h"
namespace CVC4 {
inline bool Node::operator<(const Node& e) const {
return d_ev->d_id < e.d_ev->d_id;
}
inline std::ostream& operator<<(std::ostream& out, const Node& e) {
e.toString(out);
return out;
}
inline Kind Node::getKind() const {
return Kind(d_ev->d_kind);
}
inline void Node::toString(std::ostream& out) const {
if(d_ev)
d_ev->toString(out);
else out << "null";
}
inline Node::iterator Node::begin() {
return d_ev->begin();
}
inline Node::iterator Node::end() {
return d_ev->end();
}
inline Node::const_iterator Node::begin() const {
return d_ev->begin();
}
inline Node::const_iterator Node::end() const {
return d_ev->end();
}
inline size_t Node::numChildren() const {
return d_ev->d_nchildren;
}
}/* CVC4 namespace */
#endif /* __CVC4__EXPR_H */
|
