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