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-2025 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(NodeManager* nm);
165 : : NodeBuilder(NodeManager* nm, Kind k);
166 : : NodeBuilder(const NodeBuilder& nb);
167 : :
168 : : ~NodeBuilder();
169 : :
170 : : /** Get the kind of this Node-under-construction. */
171 : : Kind getKind() const;
172 : :
173 : : /** Get the kind of this Node-under-construction. */
174 : : kind::MetaKind getMetaKind() const;
175 : :
176 : : /** Get the current number of children of this Node-under-construction. */
177 : : unsigned getNumChildren() const;
178 : :
179 : : /**
180 : : * Access to the operator of this Node-under-construction. Only
181 : : * allowed if this NodeBuilder is unused, and has a defined kind
182 : : * that is of PARAMETERIZED metakind.
183 : : */
184 : : Node getOperator() const;
185 : :
186 : : /**
187 : : * Access to children of this Node-under-construction. Only allowed
188 : : * if this NodeBuilder is unused and has a defined kind.
189 : : */
190 : : Node getChild(int i) const;
191 : :
192 : : /** Access to children of this Node-under-construction. */
193 : : Node operator[](int i) const;
194 : :
195 : : /**
196 : : * "Reset" this node builder (optionally setting a new kind for it),
197 : : * using the same "inline" memory as at construction time. This
198 : : * deallocates NodeBuilder-allocated heap memory, if it was
199 : : * allocated, and decrements the reference counts of any currently
200 : : * children in the NodeBuilder.
201 : : *
202 : : * This should leave the NodeBuilder in the state it was after
203 : : * initial construction, except for Kind, which is set to the
204 : : * argument, if provided, or UNDEFINED_KIND. In particular, the
205 : : * associated NodeManager is not affected by clear().
206 : : */
207 : : void clear(Kind k = Kind::UNDEFINED_KIND);
208 : :
209 : : // "Stream" expression constructor syntax
210 : :
211 : : /** Set the Kind of this Node-under-construction. */
212 : : NodeBuilder& operator<<(const Kind& k);
213 : :
214 : : /**
215 : : * If this Node-under-construction has a Kind set, collapse it and
216 : : * append the given Node as a child. Otherwise, simply append.
217 : : */
218 : : NodeBuilder& operator<<(TNode n);
219 : :
220 : : /**
221 : : * If this Node-under-construction has a Kind set, collapse it and
222 : : * append the given Node as a child. Otherwise, simply append.
223 : : */
224 : : NodeBuilder& operator<<(TypeNode n);
225 : :
226 : : /** Append a sequence of children to this TypeNode-under-construction. */
227 : : NodeBuilder& append(const std::vector<TypeNode>& children);
228 : :
229 : : /** Append a sequence of children to this Node-under-construction. */
230 : : template <bool ref_count>
231 : 106582237 : inline NodeBuilder& append(
232 : : const std::vector<NodeTemplate<ref_count> >& children)
233 : : {
234 [ - + ][ - + ]: 106582237 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
235 : : "attempt to access it after conversion";
236 : 106582237 : return append(children.begin(), children.end());
237 : : }
238 : :
239 : : /** Append a sequence of children to this Node-under-construction. */
240 : : template <class Iterator>
241 : 126696696 : NodeBuilder& append(const Iterator& begin, const Iterator& end)
242 : : {
243 [ - + ][ - + ]: 126696696 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
244 : : "attempt to access it after conversion";
245 [ + + ]: 563105439 : for(Iterator i = begin; i != end; ++i) {
246 : 436408773 : append(*i);
247 : : }
248 : 126696696 : return *this;
249 : : }
250 : :
251 : : /** Append a child to this Node-under-construction. */
252 : : NodeBuilder& append(TNode n);
253 : :
254 : : /** Append a child to this Node-under-construction. */
255 : : NodeBuilder& append(const TypeNode& typeNode);
256 : :
257 : : /** Construct the Node out of the node builder */
258 : : Node constructNode();
259 : :
260 : : /** Construct a Node on the heap out of the node builder */
261 : : Node* constructNodePtr();
262 : :
263 : : /** Construction of the TypeNode out of the node builder */
264 : : TypeNode constructTypeNode();
265 : :
266 : : // two versions, so we can support extraction from (const)
267 : : // NodeBuilders which are temporaries appearing as rvalues
268 : : operator Node();
269 : :
270 : : // similarly for TypeNode
271 : : operator TypeNode();
272 : :
273 : : private:
274 : : void internalCopy(const NodeBuilder& nb);
275 : :
276 : : /**
277 : : * Returns whether or not this NodeBuilder has been "used"---i.e.,
278 : : * whether a Node has been extracted with operator Node().
279 : : * Internally, this state is represented by d_nv pointing to NULL.
280 : : */
281 : : bool isUsed() const;
282 : :
283 : : /**
284 : : * Set this NodeBuilder to the `used' state.
285 : : */
286 : : void setUsed();
287 : :
288 : : /**
289 : : * Set this NodeBuilder to the `unused' state. Should only be done
290 : : * from clear().
291 : : */
292 : : void setUnused();
293 : :
294 : : /**
295 : : * Returns true if d_nv is *not* the "in-line" one (it was
296 : : * heap-allocated by this class).
297 : : */
298 : : bool nvIsAllocated() const;
299 : :
300 : : /**
301 : : * Returns true if adding a child requires (re)allocation of d_nv
302 : : * first.
303 : : */
304 : : bool nvNeedsToBeAllocated() const;
305 : :
306 : : /**
307 : : * (Re)allocate d_nv using a default grow factor. Ensure that child
308 : : * pointers are copied into the new buffer, and if the "inline"
309 : : * NodeValue is evacuated, make sure its children won't be
310 : : * double-decremented later (on destruction/clear).
311 : : */
312 : : void realloc();
313 : :
314 : : /**
315 : : * (Re)allocate d_nv to a specific size. Specify "copy" if the
316 : : * children should be copied; if they are, and if the "inline"
317 : : * NodeValue is evacuated, make sure its children won't be
318 : : * double-decremented later (on destruction/clear).
319 : : */
320 : : void realloc(size_t toSize);
321 : :
322 : : /**
323 : : * If d_nv needs to be (re)allocated to add an additional child, do
324 : : * so using realloc(), which ensures child pointers are copied and
325 : : * that the reference counts of the "inline" NodeValue won't be
326 : : * double-decremented on destruction/clear. Otherwise, do nothing.
327 : : */
328 : : void allocateNvIfNecessaryForAppend();
329 : :
330 : : /**
331 : : * Deallocate a d_nv that was heap-allocated by this class during
332 : : * grow operations. (Marks this NodeValue no longer allocated so
333 : : * that double-deallocations don't occur.)
334 : : *
335 : : * PRECONDITION: only call this when nvIsAllocated() == true.
336 : : * POSTCONDITION: !nvIsAllocated()
337 : : */
338 : : void dealloc();
339 : :
340 : : /**
341 : : * "Purge" the "inline" children. Decrement all their reference
342 : : * counts and set the number of children to zero.
343 : : *
344 : : * PRECONDITION: only call this when nvIsAllocated() == false.
345 : : * POSTCONDITION: d_inlineNv.d_nchildren == 0.
346 : : */
347 : : void decrRefCounts();
348 : :
349 : : /**
350 : : * Trim d_nv down to the size it needs to be for the number of
351 : : * children it has. Used when a Node is extracted from a
352 : : * NodeBuilder and we want the returned memory not to suffer from
353 : : * internal fragmentation. If d_nv was not heap-allocated by this
354 : : * class, or is already the right size, this function does nothing.
355 : : *
356 : : * @throws bad_alloc if the reallocation fails
357 : : */
358 : : void crop();
359 : :
360 : : /** Construct the node value out of the node builder */
361 : : expr::NodeValue* constructNV();
362 : :
363 : : #ifdef CVC5_DEBUG
364 : : // Throws a TypeCheckingExceptionPrivate on a failure.
365 : : void maybeCheckType(const TNode n) const;
366 : : #else /* CVC5_DEBUG */
367 : : // Do nothing if not in debug mode.
368 : : inline void maybeCheckType(const TNode n) const {}
369 : : #endif /* CVC5_DEBUG */
370 : :
371 : : // used by convenience node builders
372 : : NodeBuilder& collapseTo(Kind k);
373 : :
374 : : /**
375 : : * An "in-line" stack-allocated buffer for use by the
376 : : * NodeBuilder.
377 : : */
378 : : expr::NodeValue d_inlineNv;
379 : : /**
380 : : * Space for the children of the node being constructed. This is
381 : : * never accessed directly, but rather through
382 : : * d_inlineNv.d_children[i].
383 : : */
384 : : CVC5_UNUSED_FIELD expr::NodeValue* d_inlineNvChildSpace[default_nchild_thresh];
385 : :
386 : : /**
387 : : * A pointer to the "current" NodeValue buffer; either &d_inlineNv
388 : : * or a heap-allocated one if d_inlineNv wasn't big enough.
389 : : */
390 : : expr::NodeValue* d_nv;
391 : :
392 : : /** The NodeManager at play */
393 : : NodeManager* d_nm;
394 : :
395 : : /**
396 : : * The number of children allocated in d_nv.
397 : : */
398 : : uint32_t d_nvMaxChildren;
399 : : }; /* class NodeBuilder */
400 : :
401 : : // Sometimes it's useful for debugging to output a NodeBuilder that
402 : : // isn't yet a Node..
403 : : std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb);
404 : :
405 : : } // namespace cvc5::internal
406 : :
407 : : #endif /* CVC5__NODE_BUILDER_H */
|
