Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Morgan Deters, Andres Noetzli, Dejan Jovanovic
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * A builder interface for Nodes.
14 : : *
15 : : * The idea is to permit a flexible and efficient (in the common
16 : : * case) interface for building Nodes. The general pattern of use is
17 : : * to create a NodeBuilder, set its kind, append children to it, then
18 : : * "extract" the resulting Node. This resulting Node may be one that
19 : : * already exists (the NodeManager keeps a table of all Nodes in the
20 : : * system), or may be entirely new.
21 : : *
22 : : * This implementation gets a bit hairy for a handful of reasons. We
23 : : * want a user-supplied "in-line" buffer (probably on the stack, see
24 : : * below) to hold the children, but then the number of children must
25 : : * be known ahead of time. Therefore, if this buffer is overrun, we
26 : : * need to heap-allocate a new buffer to hold the children.
27 : : *
28 : : * Note that as children are added to a NodeBuilder, they are stored
29 : : * as raw pointers-to-NodeValue. However, their reference counts are
30 : : * carefully maintained.
31 : : *
32 : : * When the "in-line" buffer "d_inlineNv" is superceded by a
33 : : * heap-allocated buffer, we allocate the new buffer (a NodeValue
34 : : * large enough to hold more children), copy the elements to it, and
35 : : * mark d_inlineNv as having zero children. We do this last bit so
36 : : * that we don't have to modify any child reference counts. The new
37 : : * heap-allocated buffer "takes over" the reference counts of the old
38 : : * "in-line" buffer. (If we didn't mark it as having zero children,
39 : : * the destructor may improperly decrement the children's reference
40 : : * counts.)
41 : : *
42 : : * There are then four normal cases at the end of a NodeBuilder's
43 : : * life cycle:
44 : : *
45 : : * 0. We have a VARIABLE-kinded Node. These are special (they have
46 : : * no children and are all distinct by definition). They are
47 : : * really a subcase of 1(b), below.
48 : : * 1. d_nv points to d_inlineNv: it is the backing store supplied
49 : : * by the user (or derived class).
50 : : * (a) The Node under construction already exists in the
51 : : * NodeManager's pool.
52 : : * (b) The Node under construction is NOT already in the
53 : : * NodeManager's pool.
54 : : * 2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer
55 : : * that was heap-allocated by this NodeBuilder.
56 : : * (a) The Node under construction already exists in the
57 : : * NodeManager's pool.
58 : : * (b) The Node under construction is NOT already in the
59 : : * NodeManager's pool.
60 : : *
61 : : * When a Node is extracted, we convert the NodeBuilder to a Node and
62 : : * make sure the reference counts are properly maintained. That
63 : : * means we must ensure there are no reference-counting errors among
64 : : * the node's children, that the children aren't re-decremented on
65 : : * clear() or NodeBuilder destruction, and that the returned Node
66 : : * wraps a NodeValue with a reference count of 1.
67 : : *
68 : : * 0. If a VARIABLE, treat similarly to 1(b), except that we
69 : : * know there are no children (no reference counts to reason
70 : : * about) and we don't keep VARIABLE-kinded Nodes in the
71 : : * NodeManager pool.
72 : : *
73 : : * 1(a). Reference-counts for all children in d_inlineNv must be
74 : : * decremented, and the NodeBuilder must be marked as "used"
75 : : * and the number of children set to zero so that we don't
76 : : * decrement them again on destruction. The existing
77 : : * NodeManager pool entry is returned.
78 : : *
79 : : * 1(b). A new heap-allocated NodeValue must be constructed and all
80 : : * settings and children from d_inlineNv copied into it.
81 : : * This new NodeValue is put into the NodeManager's pool.
82 : : * The NodeBuilder is marked as "used" and the number of
83 : : * children in d_inlineNv set to zero so that we don't
84 : : * decrement child reference counts on destruction (the child
85 : : * reference counts have been "taken over" by the new
86 : : * NodeValue). We return a Node wrapper for this new
87 : : * NodeValue, which increments its reference count.
88 : : *
89 : : * 2(a). Reference counts for all children in d_nv must be
90 : : * decremented. The NodeBuilder is marked as "used" and the
91 : : * heap-allocated d_nv deleted. d_nv is repointed to
92 : : * d_inlineNv so that destruction of the NodeBuilder doesn't
93 : : * cause any problems. The existing NodeManager pool entry
94 : : * is returned.
95 : : *
96 : : * 2(b). The heap-allocated d_nv is "cropped" to the correct size
97 : : * (based on the number of children it _actually_ has). d_nv
98 : : * is repointed to d_inlineNv so that destruction of the
99 : : * NodeBuilder doesn't cause any problems, and the (old)
100 : : * value it had is placed into the NodeManager's pool and
101 : : * returned in a Node wrapper.
102 : : *
103 : : * NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper
104 : : * temporary for the NodeValue in the NodeBuilder::operator Node()
105 : : * member function. If we create a temporary (for example by writing
106 : : * Trace("builder") << Node(nv) << endl), the NodeValue will have its
107 : : * reference count incremented from zero to one, then decremented,
108 : : * which makes it eligible for collection before the builder has even
109 : : * returned it! So this is a no-no.
110 : : *
111 : : * There are also two cases when the NodeBuilder is clear()'ed:
112 : : *
113 : : * 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
114 : : * backing store): all d_inlineNv children have their reference
115 : : * counts decremented, d_inlineNv.d_nchildren is set to zero,
116 : : * and its kind is set to UNDEFINED_KIND.
117 : : *
118 : : * 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
119 : : * d_nv children have their reference counts decremented, d_nv
120 : : * is deallocated, and d_nv is set to &d_inlineNv. d_inlineNv's
121 : : * kind is set to UNDEFINED_KIND.
122 : : *
123 : : * ... destruction is similar:
124 : : *
125 : : * 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
126 : : * backing store): all d_inlineNv children have their reference
127 : : * counts decremented.
128 : : *
129 : : * 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
130 : : * d_nv children have their reference counts decremented, and
131 : : * d_nv is deallocated.
132 : : */
133 : :
134 : : #include "cvc5_private.h"
135 : :
136 : : /* strong dependency; make sure node is included first */
137 : : #include "expr/node.h"
138 : :
139 : : #ifndef CVC5__NODE_BUILDER_H
140 : : #define CVC5__NODE_BUILDER_H
141 : :
142 : : #include <iostream>
143 : : #include <vector>
144 : :
145 : : #include "base/check.h"
146 : : #include "expr/kind.h"
147 : : #include "expr/metakind.h"
148 : : #include "expr/node_value.h"
149 : : #include "expr/type_node.h"
150 : :
151 : : namespace cvc5::internal {
152 : :
153 : : class NodeManager;
154 : :
155 : : /**
156 : : * The NodeBuilder.
157 : : */
158 : : class NodeBuilder {
159 : : friend std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb);
160 : :
161 : : constexpr static size_t default_nchild_thresh = 10;
162 : :
163 : : public:
164 : : NodeBuilder();
165 : : NodeBuilder(Kind k);
166 : : NodeBuilder(NodeManager* nm);
167 : : NodeBuilder(NodeManager* nm, Kind k);
168 : : NodeBuilder(const NodeBuilder& nb);
169 : :
170 : : ~NodeBuilder();
171 : :
172 : : /** Get the kind of this Node-under-construction. */
173 : : Kind getKind() const;
174 : :
175 : : /** Get the kind of this Node-under-construction. */
176 : : kind::MetaKind getMetaKind() const;
177 : :
178 : : /** Get the current number of children of this Node-under-construction. */
179 : : unsigned getNumChildren() const;
180 : :
181 : : /**
182 : : * Access to the operator of this Node-under-construction. Only
183 : : * allowed if this NodeBuilder is unused, and has a defined kind
184 : : * that is of PARAMETERIZED metakind.
185 : : */
186 : : Node getOperator() const;
187 : :
188 : : /**
189 : : * Access to children of this Node-under-construction. Only allowed
190 : : * if this NodeBuilder is unused and has a defined kind.
191 : : */
192 : : Node getChild(int i) const;
193 : :
194 : : /** Access to children of this Node-under-construction. */
195 : : Node operator[](int i) const;
196 : :
197 : : /**
198 : : * "Reset" this node builder (optionally setting a new kind for it),
199 : : * using the same "inline" memory as at construction time. This
200 : : * deallocates NodeBuilder-allocated heap memory, if it was
201 : : * allocated, and decrements the reference counts of any currently
202 : : * children in the NodeBuilder.
203 : : *
204 : : * This should leave the NodeBuilder in the state it was after
205 : : * initial construction, except for Kind, which is set to the
206 : : * argument, if provided, or UNDEFINED_KIND. In particular, the
207 : : * associated NodeManager is not affected by clear().
208 : : */
209 : : void clear(Kind k = Kind::UNDEFINED_KIND);
210 : :
211 : : // "Stream" expression constructor syntax
212 : :
213 : : /** Set the Kind of this Node-under-construction. */
214 : : NodeBuilder& operator<<(const Kind& k);
215 : :
216 : : /**
217 : : * If this Node-under-construction has a Kind set, collapse it and
218 : : * append the given Node as a child. Otherwise, simply append.
219 : : */
220 : : NodeBuilder& operator<<(TNode n);
221 : :
222 : : /**
223 : : * If this Node-under-construction has a Kind set, collapse it and
224 : : * append the given Node as a child. Otherwise, simply append.
225 : : */
226 : : NodeBuilder& operator<<(TypeNode n);
227 : :
228 : : /** Append a sequence of children to this TypeNode-under-construction. */
229 : : NodeBuilder& append(const std::vector<TypeNode>& children);
230 : :
231 : : /** Append a sequence of children to this Node-under-construction. */
232 : : template <bool ref_count>
233 : 119919809 : inline NodeBuilder& append(
234 : : const std::vector<NodeTemplate<ref_count> >& children)
235 : : {
236 [ - + ][ - + ]: 119919809 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
237 : : "attempt to access it after conversion";
238 : 119919809 : return append(children.begin(), children.end());
239 : : }
240 : :
241 : : /** Append a sequence of children to this Node-under-construction. */
242 : : template <class Iterator>
243 : 131010625 : NodeBuilder& append(const Iterator& begin, const Iterator& end)
244 : : {
245 [ - + ][ - + ]: 131010625 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
246 : : "attempt to access it after conversion";
247 [ + + ]: 713353081 : for(Iterator i = begin; i != end; ++i) {
248 : 582342556 : append(*i);
249 : : }
250 : 131010625 : return *this;
251 : : }
252 : :
253 : : /** Append a child to this Node-under-construction. */
254 : : NodeBuilder& append(TNode n);
255 : :
256 : : /** Append a child to this Node-under-construction. */
257 : : NodeBuilder& append(const TypeNode& typeNode);
258 : :
259 : : /** Construct the Node out of the node builder */
260 : : Node constructNode();
261 : :
262 : : /** Construct a Node on the heap out of the node builder */
263 : : Node* constructNodePtr();
264 : :
265 : : /** Construction of the TypeNode out of the node builder */
266 : : TypeNode constructTypeNode();
267 : :
268 : : // two versions, so we can support extraction from (const)
269 : : // NodeBuilders which are temporaries appearing as rvalues
270 : : operator Node();
271 : :
272 : : // similarly for TypeNode
273 : : operator TypeNode();
274 : :
275 : : private:
276 : : void internalCopy(const NodeBuilder& nb);
277 : :
278 : : /**
279 : : * Returns whether or not this NodeBuilder has been "used"---i.e.,
280 : : * whether a Node has been extracted with operator Node().
281 : : * Internally, this state is represented by d_nv pointing to NULL.
282 : : */
283 : : bool isUsed() const;
284 : :
285 : : /**
286 : : * Set this NodeBuilder to the `used' state.
287 : : */
288 : : void setUsed();
289 : :
290 : : /**
291 : : * Set this NodeBuilder to the `unused' state. Should only be done
292 : : * from clear().
293 : : */
294 : : void setUnused();
295 : :
296 : : /**
297 : : * Returns true if d_nv is *not* the "in-line" one (it was
298 : : * heap-allocated by this class).
299 : : */
300 : : bool nvIsAllocated() const;
301 : :
302 : : /**
303 : : * Returns true if adding a child requires (re)allocation of d_nv
304 : : * first.
305 : : */
306 : : bool nvNeedsToBeAllocated() const;
307 : :
308 : : /**
309 : : * (Re)allocate d_nv using a default grow factor. Ensure that child
310 : : * pointers are copied into the new buffer, and if the "inline"
311 : : * NodeValue is evacuated, make sure its children won't be
312 : : * double-decremented later (on destruction/clear).
313 : : */
314 : : void realloc();
315 : :
316 : : /**
317 : : * (Re)allocate d_nv to a specific size. Specify "copy" if the
318 : : * children should be copied; if they are, and if the "inline"
319 : : * NodeValue is evacuated, make sure its children won't be
320 : : * double-decremented later (on destruction/clear).
321 : : */
322 : : void realloc(size_t toSize);
323 : :
324 : : /**
325 : : * If d_nv needs to be (re)allocated to add an additional child, do
326 : : * so using realloc(), which ensures child pointers are copied and
327 : : * that the reference counts of the "inline" NodeValue won't be
328 : : * double-decremented on destruction/clear. Otherwise, do nothing.
329 : : */
330 : : void allocateNvIfNecessaryForAppend();
331 : :
332 : : /**
333 : : * Deallocate a d_nv that was heap-allocated by this class during
334 : : * grow operations. (Marks this NodeValue no longer allocated so
335 : : * that double-deallocations don't occur.)
336 : : *
337 : : * PRECONDITION: only call this when nvIsAllocated() == true.
338 : : * POSTCONDITION: !nvIsAllocated()
339 : : */
340 : : void dealloc();
341 : :
342 : : /**
343 : : * "Purge" the "inline" children. Decrement all their reference
344 : : * counts and set the number of children to zero.
345 : : *
346 : : * PRECONDITION: only call this when nvIsAllocated() == false.
347 : : * POSTCONDITION: d_inlineNv.d_nchildren == 0.
348 : : */
349 : : void decrRefCounts();
350 : :
351 : : /**
352 : : * Trim d_nv down to the size it needs to be for the number of
353 : : * children it has. Used when a Node is extracted from a
354 : : * NodeBuilder and we want the returned memory not to suffer from
355 : : * internal fragmentation. If d_nv was not heap-allocated by this
356 : : * class, or is already the right size, this function does nothing.
357 : : *
358 : : * @throws bad_alloc if the reallocation fails
359 : : */
360 : : void crop();
361 : :
362 : : /** Construct the node value out of the node builder */
363 : : expr::NodeValue* constructNV();
364 : :
365 : : #ifdef CVC5_DEBUG
366 : : // Throws a TypeCheckingExceptionPrivate on a failure.
367 : : void maybeCheckType(const TNode n) const;
368 : : #else /* CVC5_DEBUG */
369 : : // Do nothing if not in debug mode.
370 : : inline void maybeCheckType(const TNode n) const {}
371 : : #endif /* CVC5_DEBUG */
372 : :
373 : : // used by convenience node builders
374 : : NodeBuilder& collapseTo(Kind k);
375 : :
376 : : /**
377 : : * An "in-line" stack-allocated buffer for use by the
378 : : * NodeBuilder.
379 : : */
380 : : expr::NodeValue d_inlineNv;
381 : : /**
382 : : * Space for the children of the node being constructed. This is
383 : : * never accessed directly, but rather through
384 : : * d_inlineNv.d_children[i].
385 : : */
386 : : expr::NodeValue* d_inlineNvChildSpace[default_nchild_thresh];
387 : :
388 : : /**
389 : : * A pointer to the "current" NodeValue buffer; either &d_inlineNv
390 : : * or a heap-allocated one if d_inlineNv wasn't big enough.
391 : : */
392 : : expr::NodeValue* d_nv;
393 : :
394 : : /** The NodeManager at play */
395 : : NodeManager* d_nm;
396 : :
397 : : /**
398 : : * The number of children allocated in d_nv.
399 : : */
400 : : uint32_t d_nvMaxChildren;
401 : : }; /* class NodeBuilder */
402 : :
403 : : // Sometimes it's useful for debugging to output a NodeBuilder that
404 : : // isn't yet a Node..
405 : : std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb);
406 : :
407 : : } // namespace cvc5::internal
408 : :
409 : : #endif /* CVC5__NODE_BUILDER_H */
|
