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