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 : 58700788 : NodeBuilder::NodeBuilder(NodeManager* nm)
20 : 58700788 : : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh)
21 : : {
22 : 58700788 : d_inlineNv.d_id = 0;
23 : 58700788 : d_inlineNv.d_rc = 0;
24 : 58700788 : d_inlineNv.d_kind = expr::NodeValue::kindToDKind(Kind::UNDEFINED_KIND);
25 : 58700788 : d_inlineNv.d_nm = d_nm;
26 : 58700788 : d_inlineNv.d_nchildren = 0;
27 : 58700788 : }
28 : :
29 : 611612610 : NodeBuilder::NodeBuilder(NodeManager* nm, Kind k)
30 : 611612610 : : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh)
31 : : {
32 [ + - ][ + - ]: 611612610 : Assert(k != Kind::NULL_EXPR && k != Kind::UNDEFINED_KIND)
[ - + ][ - + ]
[ - - ]
33 : 0 : << "illegal Node-building kind";
34 : :
35 : 611612610 : d_inlineNv.d_id = 1; // have a kind already
36 : 611612610 : d_inlineNv.d_rc = 0;
37 : 611612610 : d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
38 : 611612610 : d_inlineNv.d_nm = d_nm;
39 : 611612610 : d_inlineNv.d_nchildren = 0;
40 : 611612610 : }
41 : :
42 : 72670172 : NodeBuilder::NodeBuilder(const NodeBuilder& nb)
43 : 72670172 : : d_nv(&d_inlineNv), d_nm(nb.d_nm), d_nvMaxChildren(default_nchild_thresh)
44 : : {
45 : 72670172 : d_inlineNv.d_id = nb.d_nv->d_id;
46 : 72670172 : d_inlineNv.d_rc = 0;
47 : 72670172 : d_inlineNv.d_kind = nb.d_nv->d_kind;
48 : 72670172 : d_inlineNv.d_nm = d_nm;
49 : 72670172 : d_inlineNv.d_nchildren = 0;
50 : :
51 : 72670172 : internalCopy(nb);
52 : 72670172 : }
53 : :
54 : 742983225 : NodeBuilder::~NodeBuilder()
55 : : {
56 [ + + ]: 742983225 : if (CVC5_PREDICT_FALSE(nvIsAllocated()))
57 : : {
58 : 9701 : dealloc();
59 : : }
60 [ + + ]: 742973524 : else if (CVC5_PREDICT_FALSE(!isUsed()))
61 : : {
62 : 118421075 : decrRefCounts();
63 : : }
64 : 742983225 : }
65 : :
66 : 4922479348 : Kind NodeBuilder::getKind() const
67 : : {
68 [ - + ][ - + ]: 4922479348 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
69 : 0 : "attempt to access it after conversion";
70 : 4922479348 : return d_nv->getKind();
71 : : }
72 : :
73 : 1828691063 : kind::MetaKind NodeBuilder::getMetaKind() const
74 : : {
75 [ - + ][ - + ]: 1828691063 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
76 : 0 : "attempt to access it after conversion";
77 [ - + ][ - + ]: 1828691063 : Assert(getKind() != Kind::UNDEFINED_KIND)
[ - - ]
78 : : << "The metakind of a NodeBuilder is undefined "
79 : 0 : "until a Kind is set";
80 : 1828691063 : return d_nv->getMetaKind();
81 : : }
82 : :
83 : 1215538852 : unsigned NodeBuilder::getNumChildren() const
84 : : {
85 [ - + ][ - + ]: 1215538852 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
86 : 0 : "attempt to access it after conversion";
87 [ - + ][ - + ]: 1215538852 : Assert(getKind() != Kind::UNDEFINED_KIND)
[ - - ]
88 : : << "The number of children of a NodeBuilder is undefined "
89 : 0 : "until a Kind is set";
90 : 1215538852 : 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 : 6237243 : Node NodeBuilder::getChild(int i) const
108 : : {
109 [ - + ][ - + ]: 6237243 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
110 : 0 : "attempt to access it after conversion";
111 [ - + ][ - + ]: 6237243 : Assert(getKind() != Kind::UNDEFINED_KIND)
[ - - ]
112 : : << "NodeBuilder child access is not permitted "
113 : 0 : "until a Kind is set";
114 [ + - ][ + - ]: 6237243 : Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren())
[ - + ][ - + ]
[ - - ]
115 : 0 : << "index out of range for NodeBuilder::getChild()";
116 : 6237243 : return Node(d_nv->getChild(i));
117 : : }
118 : :
119 : 6217762 : 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 : 19198128 : NodeBuilder& NodeBuilder::operator<<(const Kind& k)
152 : : {
153 [ - + ][ - + ]: 19198128 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
154 : 0 : "attempt to access it after conversion";
155 [ - + ][ - - ]: 19198128 : Assert(getKind() == Kind::UNDEFINED_KIND || d_nv->d_id == 0)
[ - + ][ - + ]
[ - - ]
156 : 0 : << "can't redefine the Kind of a NodeBuilder";
157 [ - + ][ - + ]: 19198128 : Assert(d_nv->d_id == 0)
[ - - ]
158 : 0 : << "internal inconsistency with NodeBuilder: d_id != 0";
159 [ + - ][ - + ]: 19198128 : 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 [ + - ][ - + ]: 19198128 : 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 [ + + ]: 19198128 : else if (d_nv->d_nchildren == 0)
174 : : {
175 : 19198114 : d_nv->d_id = 1; // remember that we had a kind from the start
176 : : }
177 : 19198128 : d_nv->d_kind = expr::NodeValue::kindToDKind(k);
178 : 19198128 : return *this;
179 : : }
180 : :
181 : 884771471 : NodeBuilder& NodeBuilder::operator<<(TNode n)
182 : : {
183 [ - + ][ - + ]: 884771471 : 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 [ + + ][ + + ]: 884771471 : 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 : 884771471 : return append(n);
196 : : }
197 : :
198 : 3403439 : NodeBuilder& NodeBuilder::operator<<(TypeNode n)
199 : : {
200 [ - + ][ - + ]: 3403439 : 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 [ - + ][ - - ]: 3403439 : 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 : 3403439 : return append(n);
213 : : }
214 : :
215 : 3238609 : NodeBuilder& NodeBuilder::append(const std::vector<TypeNode>& children)
216 : : {
217 [ - + ][ - + ]: 3238609 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
218 : 0 : "attempt to access it after conversion";
219 : 3238609 : return append(children.begin(), children.end());
220 : : }
221 : :
222 : 1339357199 : NodeBuilder& NodeBuilder::append(TNode n)
223 : : {
224 [ - + ][ - + ]: 1339357199 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
225 : 0 : "attempt to access it after conversion";
226 [ - + ][ - + ]: 1339357199 : Assert(!n.isNull()) << "Cannot use NULL Node as a child of a Node";
[ - - ]
227 [ - + ][ - + ]: 1339357199 : Assert(n.getNodeManager() == d_nm);
[ - - ]
228 [ - + ]: 1339357199 : if (n.getKind() == Kind::BUILTIN)
229 : : {
230 : 0 : return *this << NodeManager::operatorToKind(n);
231 : : }
232 : 1339357199 : allocateNvIfNecessaryForAppend();
233 : 1339357199 : expr::NodeValue* nv = n.d_nv;
234 : 1339357199 : nv->inc();
235 : 1339357199 : d_nv->d_children[d_nv->d_nchildren++] = nv;
236 [ - + ][ - + ]: 1339357199 : Assert(d_nv->d_nchildren <= d_nvMaxChildren);
[ - - ]
237 : 1339357199 : return *this;
238 : : }
239 : :
240 : 15136829 : NodeBuilder& NodeBuilder::append(const TypeNode& typeNode)
241 : : {
242 [ - + ][ - + ]: 15136829 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
243 : 0 : "attempt to access it after conversion";
244 [ - + ][ - + ]: 15136829 : Assert(!typeNode.isNull()) << "Cannot use NULL Node as a child of a Node";
[ - - ]
245 [ - + ][ - + ]: 15136829 : Assert(typeNode.getNodeManager() == d_nm);
[ - - ]
246 : 15136829 : allocateNvIfNecessaryForAppend();
247 : 15136829 : expr::NodeValue* nv = typeNode.d_nv;
248 : 15136829 : nv->inc();
249 : 15136829 : d_nv->d_children[d_nv->d_nchildren++] = nv;
250 [ - + ][ - + ]: 15136829 : Assert(d_nv->d_nchildren <= d_nvMaxChildren);
[ - - ]
251 : 15136829 : return *this;
252 : : }
253 : :
254 : 9685538 : void NodeBuilder::realloc(size_t toSize)
255 : : {
256 [ - + ][ - + ]: 9685538 : AlwaysAssert(toSize > d_nvMaxChildren)
[ - - ]
257 : 0 : << "attempt to realloc() a NodeBuilder to a smaller/equal size!";
258 [ - + ][ - + ]: 9685538 : 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 [ + + ]: 9685538 : if (CVC5_PREDICT_FALSE(nvIsAllocated()))
263 : : {
264 : : // Ensure d_nv is not modified on allocation failure
265 : 4248573 : expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc(
266 : 4248573 : d_nv, sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * toSize));
267 [ - + ]: 4248573 : 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 : 4248573 : d_nvMaxChildren = toSize;
274 [ - + ][ - + ]: 4248573 : 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 : 4248573 : d_nv = newBlock;
278 : : }
279 : : else
280 : : {
281 : : // Ensure d_nv is not modified on allocation failure
282 : 5436965 : expr::NodeValue* newBlock = (expr::NodeValue*)std::malloc(
283 : 5436965 : sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * toSize));
284 [ - + ]: 5436965 : if (newBlock == nullptr)
285 : : {
286 : 0 : throw std::bad_alloc();
287 : : }
288 : 5436965 : d_nvMaxChildren = toSize;
289 [ - + ][ - + ]: 5436965 : Assert(d_nvMaxChildren == toSize); // overflow check
[ - - ]
290 : :
291 : 5436965 : d_nv = newBlock;
292 : 5436965 : d_nv->d_id = d_inlineNv.d_id;
293 : 5436965 : d_nv->d_rc = 0;
294 : 5436965 : d_nv->d_kind = d_inlineNv.d_kind;
295 : 5436965 : d_nv->d_nm = d_nm;
296 : 5436965 : d_nv->d_nchildren = d_inlineNv.d_nchildren;
297 : :
298 : 5436965 : std::copy(d_inlineNv.d_children,
299 : 5436965 : d_inlineNv.d_children + d_inlineNv.d_nchildren,
300 : 5436965 : d_nv->d_children);
301 : :
302 : : // ensure "inline" children don't get decremented in dtor
303 : 5436965 : d_inlineNv.d_nchildren = 0;
304 : : }
305 : 9685538 : }
306 : :
307 : 2841937 : void NodeBuilder::dealloc()
308 : : {
309 [ - + ][ - + ]: 2841937 : Assert(nvIsAllocated())
[ - - ]
310 : : << "Internal error: NodeBuilder: dealloc() called without a "
311 : 0 : "private NodeBuilder-allocated buffer";
312 : :
313 [ + + ]: 87356061 : for (expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end();
314 : : ++i)
315 : : {
316 : 84514124 : (*i)->dec();
317 : : }
318 : :
319 : 2841937 : free(d_nv);
320 : 2841937 : d_nv = &d_inlineNv;
321 : 2841937 : d_nvMaxChildren = default_nchild_thresh;
322 : 2841937 : }
323 : :
324 : 602708098 : void NodeBuilder::decrRefCounts()
325 : : {
326 [ - + ][ - + ]: 602708098 : Assert(!nvIsAllocated())
[ - - ]
327 : : << "Internal error: NodeBuilder: decrRefCounts() called with a "
328 : 0 : "private NodeBuilder-allocated buffer";
329 : :
330 : 1511156833 : for (expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
331 [ + + ]: 1511156833 : i != d_inlineNv.nv_end();
332 : : ++i)
333 : : {
334 : 908448735 : (*i)->dec();
335 : : }
336 : :
337 : 602708098 : d_inlineNv.d_nchildren = 0;
338 : 602708098 : }
339 : :
340 : 6476745 : TypeNode NodeBuilder::constructTypeNode() { return TypeNode(constructNV()); }
341 : :
342 : 618075707 : Node NodeBuilder::constructNode()
343 : : {
344 : 618075707 : Node n(constructNV());
345 : 618075708 : maybeCheckType(n);
346 : 618075706 : return n;
347 : 1 : }
348 : :
349 : 0 : Node* NodeBuilder::constructNodePtr()
350 : : {
351 : 0 : std::unique_ptr<Node> np(new Node(constructNV()));
352 : 0 : maybeCheckType(*np.get());
353 : 0 : return np.release();
354 : 0 : }
355 : :
356 : 133635282 : NodeBuilder::operator Node() { return constructNode(); }
357 : :
358 : 0 : NodeBuilder::operator TypeNode() { return constructTypeNode(); }
359 : :
360 : 624552452 : expr::NodeValue* NodeBuilder::constructNV()
361 : : {
362 [ - + ][ - + ]: 624552452 : Assert(!isUsed()) << "NodeBuilder is one-shot only; "
[ - - ]
363 : 0 : "attempt to access it after conversion";
364 [ - + ][ - + ]: 624552452 : Assert(getKind() != Kind::UNDEFINED_KIND)
[ - - ]
365 : 0 : << "Can't make an expression of an undefined kind!";
366 : :
367 : : // NOTE: The comments in this function refer to the cases in the
368 : : // file comments at the top of this file.
369 : :
370 : : // Case 0: If a VARIABLE
371 : 624552452 : if (getMetaKind() == kind::metakind::VARIABLE
372 [ + + ][ + + ]: 624552452 : || getMetaKind() == kind::metakind::NULLARY_OPERATOR)
[ + + ]
373 : : {
374 : : /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
375 : : * there are no children (no reference counts to reason about),
376 : : * and we don't keep VARIABLE-kinded Nodes in the NodeManager
377 : : * pool. */
378 : :
379 [ - + ][ - + ]: 22516717 : Assert(!nvIsAllocated())
[ - - ]
380 : : << "internal NodeBuilder error: "
381 : 0 : "VARIABLE-kinded NodeBuilder is heap-allocated !?";
382 [ - + ][ - + ]: 22516717 : Assert(d_inlineNv.d_nchildren == 0)
[ - - ]
383 : : << "improperly-formed VARIABLE-kinded NodeBuilder: "
384 : 0 : "no children permitted";
385 : :
386 : : // we have to copy the inline NodeValue out
387 : : expr::NodeValue* nv =
388 : 22516717 : (expr::NodeValue*)std::malloc(sizeof(expr::NodeValue));
389 [ - + ]: 22516717 : if (nv == nullptr)
390 : : {
391 : 0 : throw std::bad_alloc();
392 : : }
393 : : // there are no children, so we don't have to worry about
394 : : // reference counts in this case.
395 : 22516717 : nv->d_nchildren = 0;
396 : 22516717 : nv->d_kind = d_nv->d_kind;
397 : 22516717 : nv->d_id = d_nm->d_nextId++;
398 : 22516717 : nv->d_nm = d_nm;
399 : 22516717 : nv->d_rc = 0;
400 : 22516717 : setUsed();
401 [ - + ]: 22516717 : if (TraceIsOn("gc"))
402 : : {
403 [ - - ]: 0 : Trace("gc") << "creating node value " << nv << " [" << nv->d_id << "]: ";
404 [ - - ]: 0 : nv->printAst(Trace("gc"));
405 [ - - ]: 0 : Trace("gc") << std::endl;
406 : : }
407 : 22516717 : return nv;
408 : : }
409 : :
410 : : // check that there are the right # of children for this kind
411 [ - + ][ - + ]: 602035735 : Assert(getMetaKind() != kind::metakind::CONSTANT)
[ - - ]
412 : 0 : << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds";
413 [ - + ][ - + ]: 602035735 : Assert(getNumChildren() >= kind::metakind::getMinArityForKind(getKind()))
[ - - ]
414 : 0 : << "Nodes with kind `" << getKind() << "` must have at least "
415 : 0 : << kind::metakind::getMinArityForKind(getKind())
416 : : << " children (the one under "
417 : 0 : "construction has "
418 : 0 : << getNumChildren() << ")";
419 [ - + ][ - + ]: 602035735 : Assert(getNumChildren() <= kind::metakind::getMaxArityForKind(getKind()))
[ - - ]
420 : 0 : << "Nodes with kind `" << getKind() << "` must have at most "
421 : 0 : << kind::metakind::getMaxArityForKind(getKind())
422 : : << " children (the one under "
423 : 0 : "construction has "
424 : 0 : << getNumChildren() << ")";
425 : :
426 : : // Implementation differs depending on whether the NodeValue was
427 : : // malloc'ed or not and whether or not it's in the already-been-seen
428 : : // NodeManager pool of Nodes. See implementation notes at the top
429 : : // of this file.
430 : :
431 [ + + ]: 602035735 : if (CVC5_PREDICT_TRUE(!nvIsAllocated()))
432 : : {
433 : : /** Case 1. d_nv points to d_inlineNv: it is the backing store
434 : : ** allocated "inline" in this NodeBuilder. **/
435 : :
436 : : // Lookup the expression value in the pool we already have
437 : 596608474 : expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
438 : : // If something else is there, we reuse it
439 [ + + ]: 596608474 : if (poolNv != nullptr)
440 : : {
441 : : /* Subcase (a): The Node under construction already exists in
442 : : * the NodeManager's pool. */
443 : :
444 : : /* 1(a). Reference-counts for all children in d_inlineNv must be
445 : : * decremented, and the NodeBuilder must be marked as "used" and
446 : : * the number of children set to zero so that we don't decrement
447 : : * them again on destruction. The existing NodeManager pool
448 : : * entry is returned.
449 : : */
450 : 484286999 : decrRefCounts();
451 : 484286999 : d_inlineNv.d_nchildren = 0;
452 : 484286999 : setUsed();
453 : 484286999 : return poolNv;
454 : : }
455 : : else
456 : : {
457 : : /* Subcase (b): The Node under construction is NOT already in
458 : : * the NodeManager's pool. */
459 : :
460 : : /* 1(b). A new heap-allocated NodeValue must be constructed and
461 : : * all settings and children from d_inlineNv copied into it.
462 : : * This new NodeValue is put into the NodeManager's pool. The
463 : : * NodeBuilder is marked as "used" and the number of children in
464 : : * d_inlineNv set to zero so that we don't decrement child
465 : : * reference counts on destruction (the child reference counts
466 : : * have been "taken over" by the new NodeValue). We return a
467 : : * Node wrapper for this new NodeValue, which increments its
468 : : * reference count. */
469 : :
470 : : // create the canonical expression value for this node
471 : 112321475 : expr::NodeValue* nv = (expr::NodeValue*)std::malloc(
472 : : sizeof(expr::NodeValue)
473 : 112321475 : + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren));
474 [ - + ]: 112321475 : if (nv == nullptr)
475 : : {
476 : 0 : throw std::bad_alloc();
477 : : }
478 : 112321475 : nv->d_nchildren = d_inlineNv.d_nchildren;
479 : 112321475 : nv->d_kind = d_inlineNv.d_kind;
480 : 112321475 : nv->d_id = d_nm->d_nextId++;
481 : 112321475 : nv->d_nm = d_nm;
482 : 112321475 : nv->d_rc = 0;
483 : :
484 : 112321475 : std::copy(d_inlineNv.d_children,
485 : 112321475 : d_inlineNv.d_children + d_inlineNv.d_nchildren,
486 : 112321475 : nv->d_children);
487 : :
488 : 112321475 : d_inlineNv.d_nchildren = 0;
489 : 112321475 : setUsed();
490 : :
491 : : // poolNv = nv;
492 : 112321475 : d_nm->poolInsert(nv);
493 [ - + ]: 112321475 : if (TraceIsOn("gc"))
494 : : {
495 [ - - ]: 0 : Trace("gc") << "creating node value " << nv << " [" << nv->d_id
496 : 0 : << "]: ";
497 [ - - ]: 0 : nv->printAst(Trace("gc"));
498 [ - - ]: 0 : Trace("gc") << std::endl;
499 : : }
500 : 112321475 : return nv;
501 : : }
502 : : }
503 : : else
504 : : {
505 : : /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
506 : : ** buffer that was heap-allocated by this NodeBuilder. **/
507 : :
508 : : // Lookup the expression value in the pool we already have (with insert)
509 : 5427261 : expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
510 : : // If something else is there, we reuse it
511 [ + + ]: 5427261 : if (poolNv != nullptr)
512 : : {
513 : : /* Subcase (a): The Node under construction already exists in
514 : : * the NodeManager's pool. */
515 : :
516 : : /* 2(a). Reference-counts for all children in d_nv must be
517 : : * decremented. The NodeBuilder is marked as "used" and the
518 : : * heap-allocated d_nv deleted. d_nv is repointed to d_inlineNv
519 : : * so that destruction of the NodeBuilder doesn't cause any
520 : : * problems. The existing NodeManager pool entry is
521 : : * returned. */
522 : :
523 : 2832233 : dealloc();
524 : 2832233 : setUsed();
525 : 2832233 : return poolNv;
526 : : }
527 : : else
528 : : {
529 : : /* Subcase (b) The Node under construction is NOT already in the
530 : : * NodeManager's pool. */
531 : :
532 : : /* 2(b). The heap-allocated d_nv is "cropped" to the correct
533 : : * size (based on the number of children it _actually_ has).
534 : : * d_nv is repointed to d_inlineNv so that destruction of the
535 : : * NodeBuilder doesn't cause any problems, and the (old) value
536 : : * it had is placed into the NodeManager's pool and returned in
537 : : * a Node wrapper. */
538 : :
539 : 2595028 : crop();
540 : 2595028 : expr::NodeValue* nv = d_nv;
541 : 2595028 : nv->d_id = d_nm->d_nextId++;
542 : 2595028 : nv->d_nm = d_nm;
543 : 2595028 : d_nv = &d_inlineNv;
544 : 2595028 : d_nvMaxChildren = default_nchild_thresh;
545 : 2595028 : setUsed();
546 : :
547 : : // poolNv = nv;
548 : 2595028 : d_nm->poolInsert(nv);
549 [ + - ]: 5190056 : Trace("gc") << "creating node value " << nv << " [" << nv->d_id
550 : 2595028 : << "]: " << *nv << "\n";
551 : 2595028 : return nv;
552 : : }
553 : : }
554 : : }
555 : :
556 : 72670172 : void NodeBuilder::internalCopy(const NodeBuilder& nb)
557 : : {
558 [ - + ]: 72670172 : if (nb.isUsed())
559 : : {
560 : 0 : setUsed();
561 : 0 : return;
562 : : }
563 : :
564 : 72670172 : bool realloced CVC5_UNUSED = false;
565 [ + + ]: 72670172 : if (nb.d_nvMaxChildren > d_nvMaxChildren)
566 : : {
567 : 9698 : realloced = true;
568 : 9698 : realloc(nb.d_nvMaxChildren);
569 : : }
570 : :
571 [ - + ][ - + ]: 72670172 : Assert(nb.d_nvMaxChildren <= d_nvMaxChildren);
[ - - ]
572 [ - + ][ - + ]: 72670172 : Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin());
[ - - ]
573 [ - + ][ - + ]: 72670172 : Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren)
[ - - ]
574 : : << "realloced:" << (realloced ? "true" : "false")
575 [ - - ]: 0 : << ", d_nvMax:" << d_nvMaxChildren
576 : 0 : << ", size:" << nb.d_nv->nv_end() - nb.d_nv->nv_begin()
577 : 0 : << ", nc:" << nb.d_nv->getNumChildren();
578 : 72670172 : std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
579 : :
580 : 72670172 : d_nv->d_nchildren = nb.d_nv->d_nchildren;
581 : :
582 [ + + ]: 76135726 : for (expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end();
583 : : ++i)
584 : : {
585 : 3465554 : (*i)->inc();
586 : : }
587 : : }
588 : :
589 : : #ifdef CVC5_DEBUG
590 : 618075707 : inline void NodeBuilder::maybeCheckType(const TNode n) const
591 : : {
592 : : /* force an immediate type check, if early type checking is
593 : : enabled and the current node isn't a variable or constant */
594 : 618075707 : kind::MetaKind mk = n.getMetaKind();
595 [ + + ][ + + ]: 618075707 : if (mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR
596 [ + - ]: 595783146 : && mk != kind::metakind::CONSTANT)
597 : : {
598 : 595783146 : d_nm->getType(n, true);
599 : : }
600 : 618075706 : }
601 : : #endif /* CVC5_DEBUG */
602 : :
603 :12540576127 : bool NodeBuilder::isUsed() const { return CVC5_PREDICT_FALSE(d_nv == nullptr); }
604 : :
605 : 624552452 : void NodeBuilder::setUsed()
606 : : {
607 [ - + ][ - + ]: 624552452 : Assert(!isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
[ - - ]
608 [ + - ][ + - ]: 624552452 : Assert(d_inlineNv.d_nchildren == 0
[ - + ][ - + ]
[ - - ]
609 : : && d_nvMaxChildren == default_nchild_thresh)
610 : 0 : << "Internal error: bad `inline' state in NodeBuilder!";
611 : 624552452 : d_nv = nullptr;
612 : 624552452 : }
613 : :
614 : 3 : void NodeBuilder::setUnused()
615 : : {
616 [ - + ][ - + ]: 3 : Assert(isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
[ - - ]
617 [ + - ][ + - ]: 3 : Assert(d_inlineNv.d_nchildren == 0
[ - + ][ - + ]
[ - - ]
618 : : && d_nvMaxChildren == default_nchild_thresh)
619 : 0 : << "Internal error: bad `inline' state in NodeBuilder!";
620 : 3 : d_nv = &d_inlineNv;
621 : 3 : }
622 : :
623 : 1985366308 : bool NodeBuilder::nvIsAllocated() const
624 : : {
625 : 1985366308 : return CVC5_PREDICT_FALSE(d_nv != &d_inlineNv)
626 [ + + ][ + + ]: 1985366308 : && CVC5_PREDICT_TRUE(d_nv != nullptr);
627 : : }
628 : :
629 : 1354494028 : bool NodeBuilder::nvNeedsToBeAllocated() const
630 : : {
631 : 1354494028 : return CVC5_PREDICT_FALSE(d_nv->d_nchildren == d_nvMaxChildren);
632 : : }
633 : :
634 : 9675830 : void NodeBuilder::realloc()
635 : : {
636 : 9675830 : size_t newSize = 2 * size_t(d_nvMaxChildren);
637 : 9675830 : size_t hardLimit = expr::NodeValue::MAX_CHILDREN;
638 [ - + ]: 9675830 : realloc(CVC5_PREDICT_FALSE(newSize > hardLimit) ? hardLimit : newSize);
639 : 9675830 : }
640 : :
641 : 1354494028 : void NodeBuilder::allocateNvIfNecessaryForAppend()
642 : : {
643 [ + + ]: 1354494028 : if (CVC5_PREDICT_FALSE(nvNeedsToBeAllocated()))
644 : : {
645 : 9675830 : realloc();
646 : : }
647 : 1354494028 : }
648 : :
649 : 2595028 : void NodeBuilder::crop()
650 : : {
651 : 2595028 : if (CVC5_PREDICT_FALSE(nvIsAllocated())
652 [ + - ][ + + ]: 2595028 : && CVC5_PREDICT_TRUE(d_nvMaxChildren > d_nv->d_nchildren))
[ + + ]
653 : : {
654 : : // Ensure d_nv is not modified on allocation failure
655 : 2500672 : expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc(
656 : 2500672 : d_nv,
657 : : sizeof(expr::NodeValue)
658 : 2500672 : + (sizeof(expr::NodeValue*) * d_nv->d_nchildren));
659 [ - + ]: 2500672 : if (newBlock == nullptr)
660 : : {
661 : : // In this case, d_nv was NOT freed. If we throw, the
662 : : // deallocation should occur on destruction of the
663 : : // NodeBuilder.
664 : 0 : throw std::bad_alloc();
665 : : }
666 : 2500672 : d_nv = newBlock;
667 : 2500672 : d_nvMaxChildren = d_nv->d_nchildren;
668 : : }
669 : 2595028 : }
670 : :
671 : 0 : NodeBuilder& NodeBuilder::collapseTo(Kind k)
672 : : {
673 [ - - ][ - - ]: 0 : AssertArgument(
[ - - ][ - - ]
[ - - ]
674 : : k != Kind::UNDEFINED_KIND && k != Kind::NULL_EXPR && k < Kind::LAST_KIND,
675 : : k,
676 : : "illegal collapsing kind");
677 : :
678 [ - - ]: 0 : if (getKind() != k)
679 : : {
680 : 0 : Node n = operator Node();
681 : 0 : clear();
682 : 0 : d_nv->d_kind = expr::NodeValue::kindToDKind(k);
683 : 0 : d_nv->d_id = 1; // have a kind already
684 : 0 : return append(n);
685 : 0 : }
686 : 0 : return *this;
687 : : }
688 : :
689 : 0 : std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb)
690 : : {
691 : 0 : return out << *nb.d_nv;
692 : : }
693 : :
694 : : } // namespace cvc5::internal
|
