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