Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * A builder interface for Nodes.
11 : : */
12 : :
13 : : #include "expr/node_builder.h"
14 : :
15 : : #include <memory>
16 : :
17 : : namespace cvc5::internal {
18 : :
19 : 64677815 : NodeBuilder::NodeBuilder(NodeManager* nm)
20 : 64677815 : : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh)
21 : : {
22 : 64677815 : d_inlineNv.d_id = 0;
23 : 64677815 : d_inlineNv.d_rc = 0;
24 : 64677815 : d_inlineNv.d_kind = expr::NodeValue::kindToDKind(Kind::UNDEFINED_KIND);
25 : 64677815 : d_inlineNv.d_nm = d_nm;
26 : 64677815 : d_inlineNv.d_nchildren = 0;
27 : 64677815 : }
28 : :
29 : 644303276 : NodeBuilder::NodeBuilder(NodeManager* nm, Kind k)
30 : 644303276 : : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh)
31 : : {
32 [ + - ][ + - ]: 644303276 : Assert(k != Kind::NULL_EXPR && k != Kind::UNDEFINED_KIND)
[ - + ][ - + ]
[ - - ]
33 : 0 : << "illegal Node-building kind";
34 : :
35 : 644303276 : d_inlineNv.d_id = 1; // have a kind already
36 : 644303276 : d_inlineNv.d_rc = 0;
37 : 644303276 : d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
38 : 644303276 : d_inlineNv.d_nm = d_nm;
39 : 644303276 : d_inlineNv.d_nchildren = 0;
40 : 644303276 : }
41 : :
42 : 63444864 : NodeBuilder::NodeBuilder(const NodeBuilder& nb)
43 : 63444864 : : d_nv(&d_inlineNv), d_nm(nb.d_nm), d_nvMaxChildren(default_nchild_thresh)
44 : : {
45 : 63444864 : d_inlineNv.d_id = nb.d_nv->d_id;
46 : 63444864 : d_inlineNv.d_rc = 0;
47 : 63444864 : d_inlineNv.d_kind = nb.d_nv->d_kind;
48 : 63444864 : d_inlineNv.d_nm = d_nm;
49 : 63444864 : d_inlineNv.d_nchildren = 0;
50 : :
51 : 63444864 : internalCopy(nb);
52 : 63444864 : }
53 : :
54 : 772425607 : NodeBuilder::~NodeBuilder()
55 : : {
56 [ + + ]: 772425607 : if (CVC5_PREDICT_FALSE(nvIsAllocated()))
57 : : {
58 : 3 : dealloc();
59 : : }
60 [ + + ]: 772425604 : else if (CVC5_PREDICT_FALSE(!isUsed()))
61 : : {
62 : 114252797 : decrRefCounts();
63 : : }
64 : 772425607 : }
65 : :
66 : 5189175217 : Kind NodeBuilder::getKind() const
67 : : {
68 [ - + ][ - + ]: 5189175217 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
69 : 0 : "attempt to access it after conversion";
70 : 5189175217 : return d_nv->getKind();
71 : : }
72 : :
73 : 1927477421 : kind::MetaKind NodeBuilder::getMetaKind() const
74 : : {
75 [ - + ][ - + ]: 1927477421 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
76 : 0 : "attempt to access it after conversion";
77 [ - + ][ - + ]: 1927477421 : Assert(getKind() != Kind::UNDEFINED_KIND)
[ - - ]
78 : : << "The metakind of a NodeBuilder is undefined "
79 : 0 : "until a Kind is set";
80 : 1927477421 : return d_nv->getMetaKind();
81 : : }
82 : :
83 : 1281757557 : unsigned NodeBuilder::getNumChildren() const
84 : : {
85 [ - + ][ - + ]: 1281757557 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
86 : 0 : "attempt to access it after conversion";
87 [ - + ][ - + ]: 1281757557 : Assert(getKind() != Kind::UNDEFINED_KIND)
[ - - ]
88 : : << "The number of children of a NodeBuilder is undefined "
89 : 0 : "until a Kind is set";
90 : 1281757557 : return d_nv->getNumChildren();
91 : : }
92 : :
93 : 0 : Node NodeBuilder::getOperator() const
94 : : {
95 : 0 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
96 : 0 : "attempt to access it after conversion";
97 : 0 : Assert(getKind() != Kind::UNDEFINED_KIND)
98 : : << "NodeBuilder operator access is not permitted "
99 : 0 : "until a Kind is set";
100 : 0 : Assert(getMetaKind() == kind::metakind::PARAMETERIZED)
101 : : << "NodeBuilder operator access is only permitted "
102 : 0 : "on parameterized kinds, not `"
103 : 0 : << getKind() << "'";
104 : 0 : return Node(d_nv->getOperator());
105 : : }
106 : :
107 : 6618842 : Node NodeBuilder::getChild(int i) const
108 : : {
109 [ - + ][ - + ]: 6618842 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
110 : 0 : "attempt to access it after conversion";
111 [ - + ][ - + ]: 6618842 : Assert(getKind() != Kind::UNDEFINED_KIND)
[ - - ]
112 : : << "NodeBuilder child access is not permitted "
113 : 0 : "until a Kind is set";
114 [ + - ][ + - ]: 6618842 : Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren())
[ - + ][ - + ]
[ - - ]
115 : 0 : << "index out of range for NodeBuilder::getChild()";
116 : 6618842 : return Node(d_nv->getChild(i));
117 : : }
118 : :
119 : 6598018 : Node NodeBuilder::operator[](int i) const { return getChild(i); }
120 : :
121 : 30 : void NodeBuilder::clear(Kind k)
122 : : {
123 [ - + ][ - + ]: 30 : Assert(k != Kind::NULL_EXPR) << "illegal Node-building clear kind";
[ - - ]
124 : :
125 [ + + ]: 30 : if (CVC5_PREDICT_FALSE(nvIsAllocated()))
126 : : {
127 : 3 : dealloc();
128 : : }
129 [ + + ]: 27 : else if (CVC5_PREDICT_FALSE(!isUsed()))
130 : : {
131 : 24 : decrRefCounts();
132 : : }
133 : : else
134 : : {
135 : 3 : setUnused();
136 : : }
137 : :
138 : 30 : d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
139 : 30 : for (expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
140 [ - + ]: 30 : i != d_inlineNv.nv_end();
141 : : ++i)
142 : : {
143 : 0 : (*i)->dec();
144 : : }
145 : 30 : d_inlineNv.d_nm = d_nm;
146 : 30 : d_inlineNv.d_nchildren = 0;
147 : : // keep track of whether or not we hvae a kind already
148 : 30 : d_inlineNv.d_id = (k == Kind::UNDEFINED_KIND) ? 0 : 1;
149 : 30 : }
150 : :
151 : 20511757 : NodeBuilder& NodeBuilder::operator<<(const Kind& k)
152 : : {
153 [ - + ][ - + ]: 20511757 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
154 : 0 : "attempt to access it after conversion";
155 [ - + ][ - - ]: 20511757 : Assert(getKind() == Kind::UNDEFINED_KIND || d_nv->d_id == 0)
[ - + ][ - + ]
[ - - ]
156 : 0 : << "can't redefine the Kind of a NodeBuilder";
157 [ - + ][ - + ]: 20511757 : Assert(d_nv->d_id == 0)
[ - - ]
158 : 0 : << "internal inconsistency with NodeBuilder: d_id != 0";
159 [ + - ][ - + ]: 20511757 : AssertArgument(
[ + - ][ - + ]
[ - + ]
160 : : k != Kind::UNDEFINED_KIND && k != Kind::NULL_EXPR && k < Kind::LAST_KIND,
161 : : k,
162 : : "illegal node-building kind");
163 : : // This test means: we didn't have a Kind at the beginning (on
164 : : // NodeBuilder construction or at the last clear()), but we do
165 : : // now. That means we appended a Kind with operator<<(Kind),
166 : : // which now (lazily) we'll collapse.
167 [ + - ][ - + ]: 20511757 : if (CVC5_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != Kind::UNDEFINED_KIND))
[ - + ]
168 : : {
169 : 0 : Node n2 = operator Node();
170 : 0 : clear();
171 : 0 : append(n2);
172 : 0 : }
173 [ + + ]: 20511757 : else if (d_nv->d_nchildren == 0)
174 : : {
175 : 20511743 : d_nv->d_id = 1; // remember that we had a kind from the start
176 : : }
177 : 20511757 : d_nv->d_kind = expr::NodeValue::kindToDKind(k);
178 : 20511757 : return *this;
179 : : }
180 : :
181 : 897724908 : NodeBuilder& NodeBuilder::operator<<(TNode n)
182 : : {
183 [ - + ][ - + ]: 897724908 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
184 : 0 : "attempt to access it after conversion";
185 : : // This test means: we didn't have a Kind at the beginning (on
186 : : // NodeBuilder construction or at the last clear()), but we do
187 : : // now. That means we appended a Kind with operator<<(Kind),
188 : : // which now (lazily) we'll collapse.
189 [ + + ][ + + ]: 897724908 : if (CVC5_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != Kind::UNDEFINED_KIND))
[ + + ]
190 : : {
191 : 3 : Node n2 = operator Node();
192 : 3 : clear();
193 : 3 : append(n2);
194 : 3 : }
195 : 897724908 : return append(n);
196 : : }
197 : :
198 : 4346656 : NodeBuilder& NodeBuilder::operator<<(TypeNode n)
199 : : {
200 [ - + ][ - + ]: 4346656 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
201 : 0 : "attempt to access it after conversion";
202 : : // This test means: we didn't have a Kind at the beginning (on
203 : : // NodeBuilder construction or at the last clear()), but we do
204 : : // now. That means we appended a Kind with operator<<(Kind),
205 : : // which now (lazily) we'll collapse.
206 [ - + ][ - - ]: 4346656 : if (CVC5_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != Kind::UNDEFINED_KIND))
[ - + ]
207 : : {
208 : 0 : Node n2 = operator Node();
209 : 0 : clear();
210 : 0 : append(n2);
211 : 0 : }
212 : 4346656 : return append(n);
213 : : }
214 : :
215 : 3342970 : NodeBuilder& NodeBuilder::append(const std::vector<TypeNode>& children)
216 : : {
217 [ - + ][ - + ]: 3342970 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
218 : 0 : "attempt to access it after conversion";
219 : 3342970 : return append(children.begin(), children.end());
220 : : }
221 : :
222 : 1413298042 : NodeBuilder& NodeBuilder::append(TNode n)
223 : : {
224 [ - + ][ - + ]: 1413298042 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
225 : 0 : "attempt to access it after conversion";
226 [ - + ][ - + ]: 1413298042 : Assert(!n.isNull()) << "Cannot use NULL Node as a child of a Node";
[ - - ]
227 [ - + ][ - + ]: 1413298042 : Assert(n.getNodeManager() == d_nm);
[ - - ]
228 [ - + ]: 1413298042 : if (n.getKind() == Kind::BUILTIN)
229 : : {
230 : 0 : return *this << NodeManager::operatorToKind(n);
231 : : }
232 : 1413298042 : allocateNvIfNecessaryForAppend();
233 : 1413298042 : expr::NodeValue* nv = n.d_nv;
234 : 1413298042 : nv->inc();
235 : 1413298042 : d_nv->d_children[d_nv->d_nchildren++] = nv;
236 [ - + ][ - + ]: 1413298042 : Assert(d_nv->d_nchildren <= d_nvMaxChildren);
[ - - ]
237 : 1413298042 : return *this;
238 : : }
239 : :
240 : 16144486 : NodeBuilder& NodeBuilder::append(const TypeNode& typeNode)
241 : : {
242 [ - + ][ - + ]: 16144486 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
243 : 0 : "attempt to access it after conversion";
244 [ - + ][ - + ]: 16144486 : Assert(!typeNode.isNull()) << "Cannot use NULL Node as a child of a Node";
[ - - ]
245 [ - + ][ - + ]: 16144486 : Assert(typeNode.getNodeManager() == d_nm);
[ - - ]
246 : 16144486 : allocateNvIfNecessaryForAppend();
247 : 16144486 : expr::NodeValue* nv = typeNode.d_nv;
248 : 16144486 : nv->inc();
249 : 16144486 : d_nv->d_children[d_nv->d_nchildren++] = nv;
250 [ - + ][ - + ]: 16144486 : Assert(d_nv->d_nchildren <= d_nvMaxChildren);
[ - - ]
251 : 16144486 : return *this;
252 : : }
253 : :
254 : 9725939 : void NodeBuilder::realloc(size_t toSize)
255 : : {
256 [ - + ][ - + ]: 9725939 : AlwaysAssert(toSize > d_nvMaxChildren)
[ - - ]
257 : 0 : << "attempt to realloc() a NodeBuilder to a smaller/equal size!";
258 [ - + ][ - + ]: 9725939 : Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN))
[ - - ]
259 : 0 : << "attempt to realloc() a NodeBuilder to size " << toSize
260 : 0 : << " (beyond hard limit of " << expr::NodeValue::MAX_CHILDREN << ")";
261 : :
262 [ + + ]: 9725939 : if (CVC5_PREDICT_FALSE(nvIsAllocated()))
263 : : {
264 : : // Ensure d_nv is not modified on allocation failure
265 : 4330826 : expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc(
266 : 4330826 : d_nv, sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * toSize));
267 [ - + ]: 4330826 : if (newBlock == nullptr)
268 : : {
269 : : // In this case, d_nv was NOT freed. If we throw, the
270 : : // deallocation should occur on destruction of the NodeBuilder.
271 : 0 : throw std::bad_alloc();
272 : : }
273 : 4330826 : d_nvMaxChildren = toSize;
274 [ - + ][ - + ]: 4330826 : Assert(d_nvMaxChildren == toSize); // overflow check
[ - - ]
275 : : // Here, the copy (between two heap-allocated buffers) has already
276 : : // been done for us by the std::realloc().
277 : 4330826 : d_nv = newBlock;
278 : : }
279 : : else
280 : : {
281 : : // Ensure d_nv is not modified on allocation failure
282 : 5395113 : expr::NodeValue* newBlock = (expr::NodeValue*)std::malloc(
283 : 5395113 : sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * toSize));
284 [ - + ]: 5395113 : if (newBlock == nullptr)
285 : : {
286 : 0 : throw std::bad_alloc();
287 : : }
288 : 5395113 : d_nvMaxChildren = toSize;
289 [ - + ][ - + ]: 5395113 : Assert(d_nvMaxChildren == toSize); // overflow check
[ - - ]
290 : :
291 : 5395113 : d_nv = newBlock;
292 : 5395113 : d_nv->d_id = d_inlineNv.d_id;
293 : 5395113 : d_nv->d_rc = 0;
294 : 5395113 : d_nv->d_kind = d_inlineNv.d_kind;
295 : 5395113 : d_nv->d_nm = d_nm;
296 : 5395113 : d_nv->d_nchildren = d_inlineNv.d_nchildren;
297 : :
298 : 5395113 : std::copy(d_inlineNv.d_children,
299 : 5395113 : d_inlineNv.d_children + d_inlineNv.d_nchildren,
300 : 5395113 : d_nv->d_children);
301 : :
302 : : // ensure "inline" children don't get decremented in dtor
303 : 5395113 : d_inlineNv.d_nchildren = 0;
304 : : }
305 : 9725939 : }
306 : :
307 : 2832766 : void NodeBuilder::dealloc()
308 : : {
309 [ - + ][ - + ]: 2832766 : Assert(nvIsAllocated())
[ - - ]
310 : : << "Internal error: NodeBuilder: dealloc() called without a "
311 : 0 : "private NodeBuilder-allocated buffer";
312 : :
313 [ + + ]: 87980944 : for (expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end();
314 : : ++i)
315 : : {
316 : 85148178 : (*i)->dec();
317 : : }
318 : :
319 : 2832766 : free(d_nv);
320 : 2832766 : d_nv = &d_inlineNv;
321 : 2832766 : d_nvMaxChildren = default_nchild_thresh;
322 : 2832766 : }
323 : :
324 : 616667634 : void NodeBuilder::decrRefCounts()
325 : : {
326 [ - + ][ - + ]: 616667634 : Assert(!nvIsAllocated())
[ - - ]
327 : : << "Internal error: NodeBuilder: decrRefCounts() called with a "
328 : 0 : "private NodeBuilder-allocated buffer";
329 : :
330 : 1558891472 : for (expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
331 [ + + ]: 1558891472 : i != d_inlineNv.nv_end();
332 : : ++i)
333 : : {
334 : 942223838 : (*i)->dec();
335 : : }
336 : :
337 : 616667634 : d_inlineNv.d_nchildren = 0;
338 : 616667634 : }
339 : :
340 : 7465522 : TypeNode NodeBuilder::constructTypeNode()
341 : : {
342 : : // NOLINTNEXTLINE(clang-analyzer-unix.Malloc)
343 : 7465522 : return TypeNode(constructNV());
344 : : }
345 : :
346 : 650707288 : Node NodeBuilder::constructNode()
347 : : {
348 : : // NOLINTNEXTLINE(clang-analyzer-unix.Malloc)
349 : 650707288 : Node n(constructNV());
350 : 650707290 : maybeCheckType(n);
351 : 650707286 : return n;
352 : 2 : }
353 : :
354 : 131804344 : NodeBuilder::operator Node() { return constructNode(); }
355 : :
356 : 0 : NodeBuilder::operator TypeNode() { return constructTypeNode(); }
357 : :
358 : 658172810 : expr::NodeValue* NodeBuilder::constructNV()
359 : : {
360 [ - + ][ - + ]: 658172810 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
361 : 0 : "attempt to access it after conversion";
362 [ - + ][ - + ]: 658172810 : Assert(getKind() != Kind::UNDEFINED_KIND)
[ - - ]
363 : 0 : << "Can't make an expression of an undefined kind!";
364 : :
365 : : // NOTE: The comments in this function refer to the cases in the
366 : : // file comments at the top of this file.
367 : :
368 : : // Case 0: If a VARIABLE
369 : 658172810 : if (getMetaKind() == kind::metakind::VARIABLE
370 [ + + ][ + + ]: 658172810 : || getMetaKind() == kind::metakind::NULLARY_OPERATOR)
[ + + ]
371 : : {
372 : : /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
373 : : * there are no children (no reference counts to reason about),
374 : : * and we don't keep VARIABLE-kinded Nodes in the NodeManager
375 : : * pool. */
376 : :
377 [ - + ][ - + ]: 23554826 : Assert(!nvIsAllocated())
[ - - ]
378 : : << "internal NodeBuilder error: "
379 : 0 : "VARIABLE-kinded NodeBuilder is heap-allocated !?";
380 [ - + ][ - + ]: 23554826 : Assert(d_inlineNv.d_nchildren == 0)
[ - - ]
381 : : << "improperly-formed VARIABLE-kinded NodeBuilder: "
382 : 0 : "no children permitted";
383 : :
384 : : // we have to copy the inline NodeValue out
385 : : expr::NodeValue* nv =
386 : 23554826 : (expr::NodeValue*)std::malloc(sizeof(expr::NodeValue));
387 [ - + ]: 23554826 : if (nv == nullptr)
388 : : {
389 : 0 : throw std::bad_alloc();
390 : : }
391 : : // there are no children, so we don't have to worry about
392 : : // reference counts in this case.
393 : 23554826 : nv->d_nchildren = 0;
394 : 23554826 : nv->d_kind = d_nv->d_kind;
395 : 23554826 : nv->d_id = d_nm->d_nextId++;
396 : 23554826 : nv->d_nm = d_nm;
397 : 23554826 : nv->d_rc = 0;
398 : 23554826 : setUsed();
399 [ - + ]: 23554826 : if (TraceIsOn("gc"))
400 : : {
401 [ - - ]: 0 : Trace("gc") << "creating node value " << nv << " [" << nv->d_id << "]: ";
402 [ - - ]: 0 : nv->printAst(Trace("gc"));
403 [ - - ]: 0 : Trace("gc") << std::endl;
404 : : }
405 : 23554826 : return nv;
406 : : }
407 : :
408 : : // check that there are the right # of children for this kind
409 [ - + ][ - + ]: 634617984 : Assert(getMetaKind() != kind::metakind::CONSTANT)
[ - - ]
410 : 0 : << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds";
411 [ - + ][ - + ]: 634617984 : Assert(getNumChildren() >= kind::metakind::getMinArityForKind(getKind()))
[ - - ]
412 : 0 : << "Nodes with kind `" << getKind() << "` must have at least "
413 : 0 : << kind::metakind::getMinArityForKind(getKind())
414 : : << " children (the one under "
415 : 0 : "construction has "
416 : 0 : << getNumChildren() << ")";
417 [ - + ][ - + ]: 634617984 : Assert(getNumChildren() <= kind::metakind::getMaxArityForKind(getKind()))
[ - - ]
418 : 0 : << "Nodes with kind `" << getKind() << "` must have at most "
419 : 0 : << kind::metakind::getMaxArityForKind(getKind())
420 : : << " children (the one under "
421 : 0 : "construction has "
422 : 0 : << getNumChildren() << ")";
423 : :
424 : : // Implementation differs depending on whether the NodeValue was
425 : : // malloc'ed or not and whether or not it's in the already-been-seen
426 : : // NodeManager pool of Nodes. See implementation notes at the top
427 : : // of this file.
428 : :
429 [ + + ]: 634617984 : if (CVC5_PREDICT_TRUE(!nvIsAllocated()))
430 : : {
431 : : /** Case 1. d_nv points to d_inlineNv: it is the backing store
432 : : ** allocated "inline" in this NodeBuilder. **/
433 : :
434 : : // Lookup the expression value in the pool we already have
435 : 629222877 : expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
436 : : // If something else is there, we reuse it
437 [ + + ]: 629222877 : if (poolNv != nullptr)
438 : : {
439 : : /* Subcase (a): The Node under construction already exists in
440 : : * the NodeManager's pool. */
441 : :
442 : : /* 1(a). Reference-counts for all children in d_inlineNv must be
443 : : * decremented, and the NodeBuilder must be marked as "used" and
444 : : * the number of children set to zero so that we don't decrement
445 : : * them again on destruction. The existing NodeManager pool
446 : : * entry is returned.
447 : : */
448 : 502414813 : decrRefCounts();
449 : 502414813 : d_inlineNv.d_nchildren = 0;
450 : 502414813 : setUsed();
451 : 502414813 : return poolNv;
452 : : }
453 : : else
454 : : {
455 : : /* Subcase (b): The Node under construction is NOT already in
456 : : * the NodeManager's pool. */
457 : :
458 : : /* 1(b). A new heap-allocated NodeValue must be constructed and
459 : : * all settings and children from d_inlineNv copied into it.
460 : : * This new NodeValue is put into the NodeManager's pool. The
461 : : * NodeBuilder is marked as "used" and the number of children in
462 : : * d_inlineNv set to zero so that we don't decrement child
463 : : * reference counts on destruction (the child reference counts
464 : : * have been "taken over" by the new NodeValue). We return a
465 : : * Node wrapper for this new NodeValue, which increments its
466 : : * reference count. */
467 : :
468 : : // create the canonical expression value for this node
469 : 126808064 : expr::NodeValue* nv = (expr::NodeValue*)std::malloc(
470 : : sizeof(expr::NodeValue)
471 : 126808064 : + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren));
472 [ - + ]: 126808064 : if (nv == nullptr)
473 : : {
474 : 0 : throw std::bad_alloc();
475 : : }
476 : 126808064 : nv->d_nchildren = d_inlineNv.d_nchildren;
477 : 126808064 : nv->d_kind = d_inlineNv.d_kind;
478 : 126808064 : nv->d_id = d_nm->d_nextId++;
479 : 126808064 : nv->d_nm = d_nm;
480 : 126808064 : nv->d_rc = 0;
481 : :
482 : 126808064 : std::copy(d_inlineNv.d_children,
483 : 126808064 : d_inlineNv.d_children + d_inlineNv.d_nchildren,
484 : 126808064 : nv->d_children);
485 : :
486 : 126808064 : d_inlineNv.d_nchildren = 0;
487 : 126808064 : setUsed();
488 : :
489 : : // poolNv = nv;
490 : 126808064 : d_nm->poolInsert(nv);
491 [ - + ]: 126808064 : if (TraceIsOn("gc"))
492 : : {
493 [ - - ]: 0 : Trace("gc") << "creating node value " << nv << " [" << nv->d_id
494 : 0 : << "]: ";
495 [ - - ]: 0 : nv->printAst(Trace("gc"));
496 [ - - ]: 0 : Trace("gc") << std::endl;
497 : : }
498 : 126808064 : return nv;
499 : : }
500 : : }
501 : : else
502 : : {
503 : : /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
504 : : ** buffer that was heap-allocated by this NodeBuilder. **/
505 : :
506 : : // Lookup the expression value in the pool we already have (with insert)
507 : 5395107 : expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
508 : : // If something else is there, we reuse it
509 [ + + ]: 5395107 : if (poolNv != nullptr)
510 : : {
511 : : /* Subcase (a): The Node under construction already exists in
512 : : * the NodeManager's pool. */
513 : :
514 : : /* 2(a). Reference-counts for all children in d_nv must be
515 : : * decremented. The NodeBuilder is marked as "used" and the
516 : : * heap-allocated d_nv deleted. d_nv is repointed to d_inlineNv
517 : : * so that destruction of the NodeBuilder doesn't cause any
518 : : * problems. The existing NodeManager pool entry is
519 : : * returned. */
520 : :
521 : 2832760 : dealloc();
522 : 2832760 : setUsed();
523 : 2832760 : return poolNv;
524 : : }
525 : : else
526 : : {
527 : : /* Subcase (b) The Node under construction is NOT already in the
528 : : * NodeManager's pool. */
529 : :
530 : : /* 2(b). The heap-allocated d_nv is "cropped" to the correct
531 : : * size (based on the number of children it _actually_ has).
532 : : * d_nv is repointed to d_inlineNv so that destruction of the
533 : : * NodeBuilder doesn't cause any problems, and the (old) value
534 : : * it had is placed into the NodeManager's pool and returned in
535 : : * a Node wrapper. */
536 : :
537 : 2562347 : crop();
538 : 2562347 : expr::NodeValue* nv = d_nv;
539 : 2562347 : nv->d_id = d_nm->d_nextId++;
540 : 2562347 : nv->d_nm = d_nm;
541 : 2562347 : d_nv = &d_inlineNv;
542 : 2562347 : d_nvMaxChildren = default_nchild_thresh;
543 : 2562347 : setUsed();
544 : :
545 : : // poolNv = nv;
546 : 2562347 : d_nm->poolInsert(nv);
547 [ + - ]: 5124694 : Trace("gc") << "creating node value " << nv << " [" << nv->d_id
548 : 2562347 : << "]: " << *nv << "\n";
549 : 2562347 : return nv;
550 : : }
551 : : }
552 : : }
553 : :
554 : 63444864 : void NodeBuilder::internalCopy(const NodeBuilder& nb)
555 : : {
556 [ - + ]: 63444864 : if (nb.isUsed())
557 : : {
558 : 0 : setUsed();
559 : 0 : return;
560 : : }
561 : :
562 : 63444864 : bool realloced CVC5_UNUSED = false;
563 [ - + ]: 63444864 : if (nb.d_nvMaxChildren > d_nvMaxChildren)
564 : : {
565 : 0 : realloced = true;
566 : 0 : realloc(nb.d_nvMaxChildren);
567 : : }
568 : :
569 [ - + ][ - + ]: 63444864 : Assert(nb.d_nvMaxChildren <= d_nvMaxChildren);
[ - - ]
570 [ - + ][ - + ]: 63444864 : Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin());
[ - - ]
571 [ - + ][ - + ]: 63444864 : Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren)
[ - - ]
572 : : << "realloced:" << (realloced ? "true" : "false")
573 [ - - ]: 0 : << ", d_nvMax:" << d_nvMaxChildren
574 : 0 : << ", size:" << nb.d_nv->nv_end() - nb.d_nv->nv_begin()
575 : 0 : << ", nc:" << nb.d_nv->getNumChildren();
576 : 63444864 : std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
577 : :
578 : 63444864 : d_nv->d_nchildren = nb.d_nv->d_nchildren;
579 : :
580 [ - + ]: 63444864 : for (expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end();
581 : : ++i)
582 : : {
583 : 0 : (*i)->inc();
584 : : }
585 : : }
586 : :
587 : : #ifdef CVC5_DEBUG
588 : 650707288 : inline void NodeBuilder::maybeCheckType(const TNode n) const
589 : : {
590 : : /* force an immediate type check, if early type checking is
591 : : enabled and the current node isn't a variable or constant */
592 : 650707288 : kind::MetaKind mk = n.getMetaKind();
593 [ + + ][ + + ]: 650707288 : if (mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR
594 [ + - ]: 627380100 : && mk != kind::metakind::CONSTANT)
595 : : {
596 : 627380100 : d_nm->getType(n, true);
597 : : }
598 : 650707286 : }
599 : : #endif /* CVC5_DEBUG */
600 : :
601 :13190334285 : bool NodeBuilder::isUsed() const { return CVC5_PREDICT_FALSE(d_nv == nullptr); }
602 : :
603 : 658172810 : void NodeBuilder::setUsed()
604 : : {
605 [ - + ][ - + ]: 658172810 : Assert(!isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
[ - - ]
606 [ + - ][ + - ]: 658172810 : Assert(d_inlineNv.d_nchildren == 0
[ - + ][ - + ]
[ - - ]
607 : : && d_nvMaxChildren == default_nchild_thresh)
608 : 0 : << "Internal error: bad `inline' state in NodeBuilder!";
609 : 658172810 : d_nv = nullptr;
610 : 658172810 : }
611 : :
612 : 3 : void NodeBuilder::setUnused()
613 : : {
614 [ - + ][ - + ]: 3 : Assert(isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
[ - - ]
615 [ + - ][ + - ]: 3 : Assert(d_inlineNv.d_nchildren == 0
[ - + ][ - + ]
[ - - ]
616 : : && d_nvMaxChildren == default_nchild_thresh)
617 : 0 : << "Internal error: bad `inline' state in NodeBuilder!";
618 : 3 : d_nv = &d_inlineNv;
619 : 3 : }
620 : :
621 : 2062387133 : bool NodeBuilder::nvIsAllocated() const
622 : : {
623 : 2062387133 : return CVC5_PREDICT_FALSE(d_nv != &d_inlineNv)
624 [ + + ][ + + ]: 2062387133 : && CVC5_PREDICT_TRUE(d_nv != nullptr);
625 : : }
626 : :
627 : 1429442528 : bool NodeBuilder::nvNeedsToBeAllocated() const
628 : : {
629 : 1429442528 : return CVC5_PREDICT_FALSE(d_nv->d_nchildren == d_nvMaxChildren);
630 : : }
631 : :
632 : 9725929 : void NodeBuilder::realloc()
633 : : {
634 : 9725929 : size_t newSize = 2 * size_t(d_nvMaxChildren);
635 : 9725929 : size_t hardLimit = expr::NodeValue::MAX_CHILDREN;
636 [ - + ]: 9725929 : realloc(CVC5_PREDICT_FALSE(newSize > hardLimit) ? hardLimit : newSize);
637 : 9725929 : }
638 : :
639 : 1429442528 : void NodeBuilder::allocateNvIfNecessaryForAppend()
640 : : {
641 [ + + ]: 1429442528 : if (CVC5_PREDICT_FALSE(nvNeedsToBeAllocated()))
642 : : {
643 : 9725929 : realloc();
644 : : }
645 : 1429442528 : }
646 : :
647 : 2562347 : void NodeBuilder::crop()
648 : : {
649 : 2562347 : if (CVC5_PREDICT_FALSE(nvIsAllocated())
650 [ + - ][ + + ]: 2562347 : && CVC5_PREDICT_TRUE(d_nvMaxChildren > d_nv->d_nchildren))
[ + + ]
651 : : {
652 : : // Ensure d_nv is not modified on allocation failure
653 : 2467362 : expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc(
654 : 2467362 : d_nv,
655 : : sizeof(expr::NodeValue)
656 : 2467362 : + (sizeof(expr::NodeValue*) * d_nv->d_nchildren));
657 [ - + ]: 2467362 : if (newBlock == nullptr)
658 : : {
659 : : // In this case, d_nv was NOT freed. If we throw, the
660 : : // deallocation should occur on destruction of the
661 : : // NodeBuilder.
662 : 0 : throw std::bad_alloc();
663 : : }
664 : 2467362 : d_nv = newBlock;
665 : 2467362 : d_nvMaxChildren = d_nv->d_nchildren;
666 : : }
667 : 2562347 : }
668 : :
669 : 0 : NodeBuilder& NodeBuilder::collapseTo(Kind k)
670 : : {
671 [ - - ][ - - ]: 0 : AssertArgument(
[ - - ][ - - ]
[ - - ]
672 : : k != Kind::UNDEFINED_KIND && k != Kind::NULL_EXPR && k < Kind::LAST_KIND,
673 : : k,
674 : : "illegal collapsing kind");
675 : :
676 [ - - ]: 0 : if (getKind() != k)
677 : : {
678 : 0 : Node n = operator Node();
679 : 0 : clear();
680 : 0 : d_nv->d_kind = expr::NodeValue::kindToDKind(k);
681 : 0 : d_nv->d_id = 1; // have a kind already
682 : 0 : return append(n);
683 : 0 : }
684 : 0 : return *this;
685 : : }
686 : :
687 : 0 : std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb)
688 : : {
689 : 0 : return out << *nb.d_nv;
690 : : }
691 : :
692 : : } // namespace cvc5::internal
|
