blob: 75c694ec9e5a1c60767a1ea7536becc1de060a4b (
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++ -*- */
/** node_value.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.
**
** An expression node.
**
** Instances of this class are generally referenced through
** cvc4::Node rather than by pointer; cvc4::Node maintains the
** reference count on NodeValue instances and
**/
/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */
/* to resolve a circular dependency */
//#include "expr/node.h"
#ifndef __CVC4__EXPR__NODE_VALUE_H
#define __CVC4__EXPR__NODE_VALUE_H
#include "cvc4_config.h"
#include <stdint.h>
#include "kind.h"
#include <string>
namespace CVC4 {
class Node;
template <unsigned> class NodeBuilder;
class NodeManager;
namespace expr {
/**
* This is an NodeValue.
*/
class NodeValue {
/** A convenient null-valued expression value */
static NodeValue s_null;
/** Maximum reference count possible. Used for sticky
* reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
static const unsigned MAX_RC = 255;
// this header fits into one 64-bit word
/** The ID (0 is reserved for the null value) */
unsigned d_id : 32;
/** The expression's reference count. @see cvc4::Node. */
unsigned d_rc : 8;
/** Kind of the expression */
unsigned d_kind : 8;
/** Number of children */
unsigned d_nchildren : 16;
/** Variable number of child nodes */
NodeValue *d_children[0];
// todo add exprMgr ref in debug case
friend class CVC4::Node;
template <unsigned> friend class CVC4::NodeBuilder;
friend class CVC4::NodeManager;
void inc();
void dec();
static size_t next_id;
/** Private default constructor for the null value. */
NodeValue();
/** Private default constructor for the NodeBuilder. */
NodeValue(int);
/** Destructor decrements the ref counts of its children */
~NodeValue();
/**
* Computes the hash over the given iterator span of children, and the
* root hash. The iterator should be either over a range of Node or pointers
* to NodeValue.
* @param hash the initial value for the hash
* @param begin the begining of the range
* @param end the end of the range
* @return the hash value
*/
template<typename const_iterator_type>
static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) {
for(const_iterator_type i = begin; i != end; ++i) {
hash = computeHash(hash, *i);
}
return hash;
}
static uint64_t computeHash(uint64_t hash, const NodeValue* ev) {
return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId();
}
typedef NodeValue** ev_iterator;
typedef NodeValue const* const* const_ev_iterator;
ev_iterator ev_begin();
ev_iterator ev_end();
const_ev_iterator ev_begin() const;
const_ev_iterator ev_end() const;
class node_iterator {
const_ev_iterator d_i;
public:
node_iterator(const_ev_iterator i) : d_i(i) {}
inline Node operator*();
bool operator==(const node_iterator& i) {
return d_i == i.d_i;
}
bool operator!=(const node_iterator& i) {
return d_i != i.d_i;
}
node_iterator& operator++() {
++d_i;
return *this;
}
node_iterator operator++(int) {
return node_iterator(d_i++);
}
};
typedef node_iterator const_node_iterator;
public:
/** Hash this expression.
* @return the hash value of this expression. */
uint64_t hash() const;
// Iterator support
typedef node_iterator iterator;
typedef node_iterator const_iterator;
iterator begin();
iterator end();
const_iterator begin() const;
const_iterator end() const;
unsigned getId() const { return d_id; }
Kind getKind() const { return (Kind) d_kind; }
unsigned numChildren() const { return d_nchildren; }
std::string toString() const;
void toStream(std::ostream& out) const;
};
}/* CVC4::expr namespace */
}/* CVC4 namespace */
#include "expr/node.h"
namespace CVC4 {
namespace expr {
inline Node NodeValue::node_iterator::operator*() {
return Node(*d_i);
}
}/* CVC4::expr namespace */
}/* CVC4 namespace */
#endif /* __CVC4__EXPR__NODE_VALUE_H */
|
