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 : : * Reference-counted encapsulation of a pointer to node information.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__NODE_H
16 : : #define CVC5__NODE_H
17 : :
18 : : #include <cvc5/cvc5_skolem_id.h>
19 : :
20 : : #include <iostream>
21 : : #include <map>
22 : : #include <sstream>
23 : : #include <string>
24 : : #include <unordered_map>
25 : : #include <unordered_set>
26 : : #include <utility>
27 : : #include <vector>
28 : :
29 : : #include "base/check.h"
30 : : #include "base/exception.h"
31 : : #include "base/output.h"
32 : : #include "expr/internal_skolem_id.h"
33 : : #include "expr/kind.h"
34 : : #include "expr/metakind.h"
35 : : #include "expr/node_value.h"
36 : : #include "options/io_utils.h"
37 : : #include "options/language.h"
38 : : #include "util/hash.h"
39 : : #include "util/utility.h"
40 : :
41 : : namespace cvc5::internal {
42 : :
43 : : class TypeNode;
44 : : class NodeManager;
45 : :
46 : : template <bool ref_count>
47 : : class NodeTemplate;
48 : :
49 : : /**
50 : : * Exception thrown during the type-checking phase, it can be
51 : : * thrown by node.getType().
52 : : */
53 : : class TypeCheckingExceptionPrivate : public Exception
54 : : {
55 : : private:
56 : : /** The node responsible for the failure */
57 : : NodeTemplate<true>* d_node;
58 : :
59 : : public:
60 : : /**
61 : : * Construct the exception with the problematic node and the message
62 : : * @param node the problematic node
63 : : * @param message the message explaining the failure
64 : : */
65 : : TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message);
66 : :
67 : : /** Destructor */
68 : : ~TypeCheckingExceptionPrivate() override;
69 : :
70 : : /**
71 : : * Get the Node that caused the type-checking to fail.
72 : : * @return the node
73 : : */
74 : : NodeTemplate<true> getNode() const;
75 : :
76 : : /**
77 : : * Returns the message corresponding to the type-checking failure.
78 : : * We prefer toStream() to toString() because that keeps the expr-depth
79 : : * and expr-language settings present in the stream.
80 : : */
81 : : void toStream(std::ostream& out) const override;
82 : :
83 : : }; /* class TypeCheckingExceptionPrivate */
84 : :
85 : : class UnknownTypeException : public TypeCheckingExceptionPrivate
86 : : {
87 : : public:
88 : : UnknownTypeException(NodeTemplate<false> node);
89 : : }; /* class UnknownTypeException */
90 : :
91 : : /**
92 : : * \typedef NodeTemplate<true> Node;
93 : : *
94 : : * The Node class encapsulates the NodeValue with reference counting.
95 : : *
96 : : * One should use generally use Nodes to manipulate expressions, to be safe.
97 : : * Every outstanding Node that references a NodeValue is counted in that
98 : : * NodeValue's reference count. Reference counts are maintained correctly
99 : : * on assignment of the Node object (to point to another NodeValue), and,
100 : : * upon destruction of the Node object, the NodeValue's reference count is
101 : : * decremented and, if zero, it becomes eligible for reclamation by the
102 : : * system.
103 : : */
104 : : typedef NodeTemplate<true> Node;
105 : :
106 : : /**
107 : : * \typedef NodeTemplate<false> TNode;
108 : : *
109 : : * The TNode class encapsulates the NodeValue but doesn't count references.
110 : : *
111 : : * TNodes are just like Nodes, but they don't update the reference count.
112 : : * Therefore, there is less overhead (copying a TNode is just the cost of
113 : : * the underlying pointer copy). Generally speaking, this is unsafe!
114 : : * However, there are certain situations where a TNode can be used safely.
115 : : *
116 : : * The largest class of uses for TNodes are when you need to use them in a
117 : : * "temporary," scoped fashion (hence the "T" in "TNode"). In general,
118 : : * it is safe to use TNode as a function parameter type, since the calling
119 : : * function (or some other function on the call stack) presumably has a Node
120 : : * reference to the expression data. It is generally _not_ safe, however,
121 : : * to return a TNode _from_ a function. (Functions that return Nodes often
122 : : * create the expression they return; such new expressions may not be
123 : : * referenced on the call stack, and have a reference count of 1 on
124 : : * creation. If this is returned as a TNode rather than a Node, the
125 : : * count drops to zero, marking the expression as eligible for reclamation.)
126 : : *
127 : : * More guidelines on when to use TNodes is available in the cvc5
128 : : * Developer's Guide:
129 : : * https://github.com/cvc5/cvc5/wiki/Developer-Guide#dealing-with-expressions-nodes-and-tnodes
130 : : */
131 : : typedef NodeTemplate<false> TNode;
132 : :
133 : : } // namespace cvc5::internal
134 : :
135 : : namespace std {
136 : :
137 : : template <>
138 : : struct hash<cvc5::internal::Node>
139 : : {
140 : : size_t operator()(const cvc5::internal::Node& node) const;
141 : : };
142 : :
143 : : template <>
144 : : struct hash<cvc5::internal::TNode>
145 : : {
146 : : size_t operator()(const cvc5::internal::TNode& node) const;
147 : : };
148 : :
149 : : } // namespace std
150 : :
151 : : namespace cvc5::internal {
152 : : namespace expr {
153 : :
154 : : class NodeValue;
155 : :
156 : : namespace attr {
157 : : class AttributeManager;
158 : : struct SmtAttributes;
159 : : } // namespace attr
160 : :
161 : : class ExprSetDepth;
162 : : } // namespace expr
163 : :
164 : : /**
165 : : * Encapsulation of an NodeValue pointer. The reference count is
166 : : * maintained in the NodeValue if ref_count is true.
167 : : * @param ref_count if true reference are counted in the NodeValue
168 : : */
169 : : template <bool ref_count>
170 : : class NodeTemplate
171 : : {
172 : : /**
173 : : * The NodeValue has access to the private constructors, so that the
174 : : * iterators can can create new nodes.
175 : : */
176 : : friend class expr::NodeValue;
177 : :
178 : : /** A convenient null-valued encapsulated pointer */
179 : : static NodeTemplate s_null;
180 : :
181 : : /** The referenced NodeValue */
182 : : expr::NodeValue* d_nv;
183 : :
184 : : /**
185 : : * This constructor is reserved for use by the NodeTemplate package; one
186 : : * must construct an NodeTemplate using one of the build mechanisms of the
187 : : * NodeTemplate package.
188 : : *
189 : : * FIXME: there's a type-system escape here to cast away the const,
190 : : * since the refcount needs to be updated. But conceptually Nodes
191 : : * don't change their arguments, and it's nice to have
192 : : * const_iterators over them.
193 : : *
194 : : * This really does needs to be explicit to avoid hard to track errors with
195 : : * Nodes implicitly wrapping NodeValues
196 : : */
197 : : explicit NodeTemplate(const expr::NodeValue*);
198 : :
199 : : friend class NodeTemplate<true>;
200 : : friend class NodeTemplate<false>;
201 : : friend class TypeNode;
202 : : friend class NodeManager;
203 : :
204 : : friend class NodeBuilder;
205 : :
206 : : friend class ::cvc5::internal::expr::attr::AttributeManager;
207 : : friend struct ::cvc5::internal::expr::attr::SmtAttributes;
208 : :
209 : : /**
210 : : * Assigns the expression value and does reference counting. No assumptions
211 : : * are made on the expression, and should only be used if we know what we
212 : : * are doing.
213 : : *
214 : : * @param ev the expression value to assign
215 : : */
216 : : void assignNodeValue(expr::NodeValue* ev);
217 : :
218 : : // May throw an AssertionException if the Node is not live, i.e. the ref count
219 : : // is not positive.
220 :81344462524 : inline void assertTNodeNotExpired() const
221 : : {
222 : : if (!ref_count)
223 : : {
224 [ - + ][ - + ]:42153403184 : Assert(d_nv->d_rc > 0) << "TNode pointing to an expired NodeValue";
[ - - ]
225 : : }
226 :81344462524 : }
227 : :
228 : : public:
229 : : /**
230 : : * Cache-aware, recursive version of substitute() used by the public
231 : : * member function with a similar signature.
232 : : */
233 : : Node substitute(TNode node,
234 : : TNode replacement,
235 : : std::unordered_map<TNode, TNode>& cache) const;
236 : :
237 : : /**
238 : : * Cache-aware, recursive version of substitute() used by the public
239 : : * member function with a similar signature.
240 : : */
241 : : template <class Iterator1, class Iterator2>
242 : : Node substitute(Iterator1 nodesBegin,
243 : : Iterator1 nodesEnd,
244 : : Iterator2 replacementsBegin,
245 : : Iterator2 replacementsEnd,
246 : : std::unordered_map<TNode, TNode>& cache) const;
247 : :
248 : : /**
249 : : * Cache-aware, recursive version of substitute() used by the public
250 : : * member function with a similar signature.
251 : : */
252 : : template <class Iterator>
253 : : Node substitute(Iterator substitutionsBegin,
254 : : Iterator substitutionsEnd,
255 : : std::unordered_map<TNode, TNode>& cache) const;
256 : :
257 : : /** Default constructor, makes a null expression.
258 : : *
259 : : * This constructor is `explicit` to avoid accidentially creating a null node
260 : : * from an empty braced-init-list.
261 : : */
262 : 2868937744 : explicit NodeTemplate() : d_nv(&expr::NodeValue::null()) {}
263 : :
264 : : /**
265 : : * Conversion between nodes that are reference-counted and those that are
266 : : * not.
267 : : * @param node the node to make copy of
268 : : */
269 : : NodeTemplate(const NodeTemplate<!ref_count>& node);
270 : :
271 : : /**
272 : : * Copy constructor. Note that GCC does NOT recognize an instantiation of
273 : : * the above template as a copy constructor and problems ensue. So we
274 : : * provide an explicit one here.
275 : : * @param node the node to make copy of
276 : : */
277 : : NodeTemplate(const NodeTemplate& node);
278 : :
279 : : /**
280 : : * Assignment operator for nodes, copies the relevant information from node
281 : : * to this node.
282 : : * @param node the node to copy
283 : : * @return reference to this node
284 : : */
285 : : NodeTemplate& operator=(const NodeTemplate& node);
286 : :
287 : : /**
288 : : * Assignment operator for nodes, copies the relevant information from node
289 : : * to this node.
290 : : * @param node the node to copy
291 : : * @return reference to this node
292 : : */
293 : : NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
294 : :
295 : : /**
296 : : * Destructor. If ref_count is true it will decrement the reference count
297 : : * and, if zero, collect the NodeValue.
298 : : */
299 : : ~NodeTemplate();
300 : :
301 : : /**
302 : : * Return the null node.
303 : : * @return the null node
304 : : */
305 : 1157691574 : static NodeTemplate null() { return s_null; }
306 : :
307 : : /**
308 : : * Returns true if this expression is a null expression.
309 : : * @return true if null
310 : : */
311 : 8107235372 : bool isNull() const
312 : : {
313 : 8107235372 : assertTNodeNotExpired();
314 : 8107235372 : return d_nv == &expr::NodeValue::null();
315 : : }
316 : :
317 : : /**
318 : : * Structural comparison operator for expressions.
319 : : * @param node the node to compare to
320 : : * @return true if expressions are equal, false otherwise
321 : : */
322 : : template <bool ref_count_1>
323 : 9818917118 : bool operator==(const NodeTemplate<ref_count_1>& node) const
324 : : {
325 : 9818917118 : assertTNodeNotExpired();
326 : 9818917118 : node.assertTNodeNotExpired();
327 : 9818917118 : return d_nv == node.d_nv;
328 : : }
329 : :
330 : : /**
331 : : * Structural comparison operator for expressions.
332 : : * @param node the node to compare to
333 : : * @return false if expressions are equal, true otherwise
334 : : */
335 : : template <bool ref_count_1>
336 : 508366456 : bool operator!=(const NodeTemplate<ref_count_1>& node) const
337 : : {
338 : 508366456 : assertTNodeNotExpired();
339 : 508366456 : node.assertTNodeNotExpired();
340 : 508366456 : return d_nv != node.d_nv;
341 : : }
342 : :
343 : : /**
344 : : * We compare by expression ids so, keeping things deterministic and having
345 : : * that subexpressions have to be smaller than the enclosing expressions.
346 : : * @param node the node to compare to
347 : : * @return true if this expression is smaller
348 : : */
349 : : template <bool ref_count_1>
350 : 6648701941 : inline bool operator<(const NodeTemplate<ref_count_1>& node) const
351 : : {
352 : 6648701941 : assertTNodeNotExpired();
353 : 6648701941 : node.assertTNodeNotExpired();
354 : 6648701941 : return d_nv->d_id < node.d_nv->d_id;
355 : : }
356 : :
357 : : /**
358 : : * We compare by expression ids so, keeping things deterministic and having
359 : : * that subexpressions have to be smaller than the enclosing expressions.
360 : : * @param node the node to compare to
361 : : * @return true if this expression is greater
362 : : */
363 : : template <bool ref_count_1>
364 : 16843239 : inline bool operator>(const NodeTemplate<ref_count_1>& node) const
365 : : {
366 : 16843239 : assertTNodeNotExpired();
367 : 16843239 : node.assertTNodeNotExpired();
368 : 16843239 : return d_nv->d_id > node.d_nv->d_id;
369 : : }
370 : :
371 : : /**
372 : : * We compare by expression ids so, keeping things deterministic and having
373 : : * that subexpressions have to be smaller than the enclosing expressions.
374 : : * @param node the node to compare to
375 : : * @return true if this expression is smaller than or equal to
376 : : */
377 : : template <bool ref_count_1>
378 : 14373 : inline bool operator<=(const NodeTemplate<ref_count_1>& node) const
379 : : {
380 : 14373 : assertTNodeNotExpired();
381 : 14373 : node.assertTNodeNotExpired();
382 : 14373 : return d_nv->d_id <= node.d_nv->d_id;
383 : : }
384 : :
385 : : /**
386 : : * We compare by expression ids so, keeping things deterministic and having
387 : : * that subexpressions have to be smaller than the enclosing expressions.
388 : : * @param node the node to compare to
389 : : * @return true if this expression is greater than or equal to
390 : : */
391 : : template <bool ref_count_1>
392 : 8070240 : inline bool operator>=(const NodeTemplate<ref_count_1>& node) const
393 : : {
394 : 8070240 : assertTNodeNotExpired();
395 : 8070240 : node.assertTNodeNotExpired();
396 : 8070240 : return d_nv->d_id >= node.d_nv->d_id;
397 : : }
398 : :
399 : : /**
400 : : * Returns the i-th child of this node.
401 : : * @param i the index of the child
402 : : * @return the node representing the i-th child
403 : : */
404 : 2817525285 : NodeTemplate operator[](int i) const
405 : : {
406 : 2817525285 : assertTNodeNotExpired();
407 : 2817525285 : return NodeTemplate(d_nv->getChild(i));
408 : : }
409 : :
410 : : /**
411 : : * Returns true if this node represents a constant
412 : : * @return true if const
413 : : */
414 : : bool isConst() const;
415 : :
416 : : /**
417 : : * Returns true if this node represents a variable
418 : : * @return true if variable
419 : : */
420 : 681570318 : inline bool isVar() const
421 : : {
422 : 681570318 : assertTNodeNotExpired();
423 : 681570318 : return getMetaKind() == kind::metakind::VARIABLE;
424 : : }
425 : :
426 : : /**
427 : : * Returns true if this node represents a nullary operator
428 : : */
429 : : inline bool isNullaryOp() const
430 : : {
431 : : assertTNodeNotExpired();
432 : : return getMetaKind() == kind::metakind::NULLARY_OPERATOR;
433 : : }
434 : :
435 : : /**
436 : : * Returns true if this node represents a closure, that is an expression
437 : : * that binds variables.
438 : : */
439 : 192497938 : inline bool isClosure() const
440 : : {
441 : 192497938 : assertTNodeNotExpired();
442 : 192497938 : return isClosureKind(getKind());
443 : : }
444 : :
445 : : /**
446 : : * Returns the unique id of this node
447 : : * @return the ud
448 : : */
449 : 7872927307 : uint64_t getId() const
450 : : {
451 : 7872927307 : assertTNodeNotExpired();
452 : 7872927307 : return d_nv->getId();
453 : : }
454 : :
455 : : /**
456 : : * Returns the associated node manager
457 : : */
458 : 4338854328 : NodeManager* getNodeManager() const
459 : : {
460 : 4338854328 : assertTNodeNotExpired();
461 : 4338854328 : return d_nv->getNodeManager();
462 : : }
463 : :
464 : : /**
465 : : * Returns a node representing the operator of this expression.
466 : : * If this is an APPLY_UF, then the operator will be a functional term.
467 : : * Otherwise, it will be a node with kind BUILTIN.
468 : : */
469 : : NodeTemplate<true> getOperator() const;
470 : :
471 : : /**
472 : : * Returns true if the node has an operator (i.e., it's not a
473 : : * variable or a constant).
474 : : */
475 : : inline bool hasOperator() const;
476 : :
477 : : /**
478 : : * Get the type for the node and optionally do type checking.
479 : : *
480 : : * Initial type computation will be near-constant time if
481 : : * type checking is not requested. Results are memoized, so that
482 : : * subsequent calls to getType() without type checking will be
483 : : * constant time.
484 : : *
485 : : * Initial type checking is linear in the size of the expression.
486 : : * Again, the results are memoized, so that subsequent calls to
487 : : * getType(), with or without type checking, will be constant
488 : : * time.
489 : : *
490 : : * NOTE: A TypeCheckingException can be thrown even when type
491 : : * checking is not requested. getType() will always return a
492 : : * valid and correct type and, thus, an exception will be thrown
493 : : * when no valid or correct type can be computed (e.g., if the
494 : : * arguments to a bit-vector operation aren't bit-vectors). When
495 : : * type checking is not requested, getType() will do the minimum
496 : : * amount of checking required to return a valid result.
497 : : *
498 : : * @param check whether we should check the type as we compute it
499 : : * (default: false)
500 : : */
501 : : TypeNode getType(bool check = false) const;
502 : : /**
503 : : * Same as getType, but does not throw a type exception if this term is
504 : : * not well-typed. Instead, this method will return the null type.
505 : : */
506 : : TypeNode getTypeOrNull(bool check = false) const;
507 : :
508 : : /**
509 : : * Has name? Return true if this node has an associated variable
510 : : * name (via the attribute expr::VarNameAttr). This is true typically for
511 : : * user-created variables.
512 : : */
513 : : bool hasName() const;
514 : : /**
515 : : * Get the name. Returns the string value of the expr::VarNameAttr attribute
516 : : * for this node.
517 : : */
518 : : std::string getName() const;
519 : :
520 : : /**
521 : : * Substitution of Nodes.
522 : : */
523 : : Node substitute(TNode node, TNode replacement) const;
524 : :
525 : : /**
526 : : * Simultaneous substitution of Nodes. Elements in the Iterator1
527 : : * range will be replaced by their corresponding element in the
528 : : * Iterator2 range. Both ranges should have the same size.
529 : : */
530 : : template <class Iterator1, class Iterator2>
531 : : Node substitute(Iterator1 nodesBegin,
532 : : Iterator1 nodesEnd,
533 : : Iterator2 replacementsBegin,
534 : : Iterator2 replacementsEnd) const;
535 : :
536 : : /**
537 : : * Simultaneous substitution of Nodes. Iterators should be over
538 : : * pairs (x,y) for the rewrites [x->y].
539 : : */
540 : : template <class Iterator>
541 : : Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd) const;
542 : :
543 : : /**
544 : : * Simultaneous substitution of Nodes in cache.
545 : : */
546 : : Node substitute(std::unordered_map<TNode, TNode>& cache) const;
547 : :
548 : : /**
549 : : * Returns the kind of this node.
550 : : * @return the kind
551 : : */
552 :11179890327 : inline Kind getKind() const
553 : : {
554 :11179890327 : assertTNodeNotExpired();
555 :11179890327 : return Kind(d_nv->d_kind);
556 : : }
557 : :
558 : : /**
559 : : * Returns the metakind of this node.
560 : : * @return the metakind
561 : : */
562 : 2629073819 : inline kind::MetaKind getMetaKind() const
563 : : {
564 : 2629073819 : assertTNodeNotExpired();
565 : 2629073819 : return kind::metaKindOf(getKind());
566 : : }
567 : :
568 : : /**
569 : : * Returns the number of children this node has.
570 : : * @return the number of children
571 : : */
572 : : inline size_t getNumChildren() const;
573 : :
574 : : /**
575 : : * If this is a CONST_* Node, extract the constant from it.
576 : : */
577 : : template <class T>
578 : : CVC5_NO_DANGLING inline const T& getConst() const;
579 : :
580 : : /**
581 : : * @return true if this is a skolem function.
582 : : */
583 : : bool isSkolem() const;
584 : :
585 : : /**
586 : : * @return the skolem identifier of this node.
587 : : */
588 : : SkolemId getSkolemId() const;
589 : :
590 : : /**
591 : : * @return the skolem indices of this node.
592 : : */
593 : : std::vector<Node> getSkolemIndices() const;
594 : :
595 : : /**
596 : : * @return the internal skolem function id, for skolems whose id is
597 : : * SkolemId::INTERNAL.
598 : : */
599 : : InternalSkolemId getInternalSkolemId() const;
600 : :
601 : : /**
602 : : * Returns the reference count of this node.
603 : : * @return the refcount
604 : : */
605 : : unsigned getRefCount() const { return d_nv->getRefCount(); }
606 : :
607 : : /**
608 : : * Returns the value of the given attribute that this has been attached.
609 : : * @param attKind the kind of the attribute
610 : : * @return the value of the attribute
611 : : */
612 : : template <class AttrKind>
613 : : inline typename AttrKind::value_type getAttribute(
614 : : const AttrKind& attKind) const;
615 : :
616 : : // Note that there are two, distinct hasAttribute() declarations for
617 : : // a reason (rather than using a pointer-valued argument with a
618 : : // default value): they permit more optimized code in the underlying
619 : : // hasAttribute() implementations.
620 : :
621 : : /**
622 : : * Returns true if this node has been associated an attribute of given kind.
623 : : * Additionaly, if a pointer to the value_kind is give, and the attribute
624 : : * value has been set for this node, it will be returned.
625 : : * @param attKind the kind of the attribute
626 : : * @return true if this node has the requested attribute
627 : : */
628 : : template <class AttrKind>
629 : : inline bool hasAttribute(const AttrKind& attKind) const;
630 : :
631 : : /**
632 : : * Returns true if this node has been associated an attribute of given kind.
633 : : * Additionaly, if a pointer to the value_kind is give, and the attribute
634 : : * value has been set for this node, it will be returned.
635 : : * @param attKind the kind of the attribute
636 : : * @param value where to store the value if it exists
637 : : * @return true if this node has the requested attribute
638 : : */
639 : : template <class AttrKind>
640 : : inline bool getAttribute(const AttrKind& attKind,
641 : : typename AttrKind::value_type& value) const;
642 : :
643 : : /**
644 : : * Sets the given attribute of this node to the given value.
645 : : * @param attKind the kind of the atribute
646 : : * @param value the value to set the attribute to
647 : : */
648 : : template <class AttrKind>
649 : : inline void setAttribute(const AttrKind& attKind,
650 : : const typename AttrKind::value_type& value);
651 : :
652 : : /** Iterator allowing for scanning through the children. */
653 : : typedef typename expr::NodeValue::iterator<NodeTemplate<ref_count>> iterator;
654 : : /** Constant iterator allowing for scanning through the children. */
655 : : using const_iterator =
656 : : typename expr::NodeValue::iterator<NodeTemplate<ref_count>>;
657 : : /**
658 : : * Reverse constant iterator allowing for scanning through the children in
659 : : * reverse order.
660 : : */
661 : : using const_reverse_iterator = std::reverse_iterator<
662 : : typename expr::NodeValue::iterator<NodeTemplate<ref_count>>>;
663 : :
664 : : class kinded_iterator
665 : : {
666 : : friend class NodeTemplate<ref_count>;
667 : :
668 : : NodeTemplate<ref_count> d_node;
669 : : ssize_t d_child;
670 : :
671 : 4 : kinded_iterator(TNode node, ssize_t child) : d_node(node), d_child(child) {}
672 : :
673 : : // These are factories to serve as clients to Node::begin<K>() and
674 : : // Node::end<K>().
675 : 2 : static kinded_iterator begin(TNode n, Kind k)
676 : : {
677 [ + + ]: 2 : return kinded_iterator(n, n.getKind() == k ? 0 : -2);
678 : : }
679 : 2 : static kinded_iterator end(TNode n, Kind k)
680 : : {
681 [ + + ]: 2 : return kinded_iterator(n, n.getKind() == k ? n.getNumChildren() : -1);
682 : : }
683 : :
684 : : public:
685 : : typedef NodeTemplate<ref_count> value_type;
686 : : typedef std::ptrdiff_t difference_type;
687 : : typedef NodeTemplate<ref_count>* pointer;
688 : : typedef NodeTemplate<ref_count>& reference;
689 : :
690 : : kinded_iterator() : d_node(NodeTemplate<ref_count>::null()), d_child(-2) {}
691 : :
692 : 4 : NodeTemplate<ref_count> operator*()
693 : : {
694 [ + + ]: 4 : return d_child < 0 ? d_node : d_node[d_child];
695 : : }
696 : :
697 : 2 : bool operator==(const kinded_iterator& i)
698 : : {
699 [ + - ][ + - ]: 2 : return d_node == i.d_node && d_child == i.d_child;
700 : : }
701 : :
702 : 0 : bool operator!=(const kinded_iterator& i) { return !(*this == i); }
703 : :
704 : 4 : kinded_iterator& operator++()
705 : : {
706 [ + - ]: 4 : if (d_child != -1)
707 : : {
708 : 4 : ++d_child;
709 : : }
710 : 4 : return *this;
711 : : }
712 : :
713 : 4 : kinded_iterator operator++(int)
714 : : {
715 : 4 : kinded_iterator i = *this;
716 : 4 : ++*this;
717 : 4 : return i;
718 : : }
719 : : }; /* class NodeTemplate<ref_count>::kinded_iterator */
720 : :
721 : : typedef kinded_iterator const_kinded_iterator;
722 : :
723 : : /**
724 : : * Returns the iterator pointing to the first child.
725 : : * @return the iterator
726 : : */
727 : 845686292 : inline iterator begin()
728 : : {
729 : 845686292 : assertTNodeNotExpired();
730 : 845686292 : return d_nv->begin<NodeTemplate<ref_count>>();
731 : : }
732 : :
733 : : /**
734 : : * Returns the iterator pointing to the end of the children (one beyond the
735 : : * last one).
736 : : * @return the end of the children iterator.
737 : : */
738 : 1446496222 : inline iterator end()
739 : : {
740 : 1446496222 : assertTNodeNotExpired();
741 : 1446496222 : return d_nv->end<NodeTemplate<ref_count>>();
742 : : }
743 : :
744 : : /**
745 : : * Returns the iterator pointing to the first child, if the node's
746 : : * kind is the same as the parameter, otherwise returns the iterator
747 : : * pointing to the node itself. This is useful if you want to
748 : : * pretend to iterate over a "unary" ADD, for instance, since unary
749 : : * PLUSes don't exist---begin(ADD) will give an iterator over the
750 : : * children if the node's an ADD node, otherwise give an iterator
751 : : * over the node itself, as if it were a unary ADD.
752 : : * @param kind the kind to match
753 : : * @return the kinded_iterator iterating over this Node (if its kind
754 : : * is not the passed kind) or its children
755 : : */
756 : 2 : inline kinded_iterator begin(Kind kind)
757 : : {
758 : 2 : assertTNodeNotExpired();
759 : 2 : return kinded_iterator::begin(*this, kind);
760 : : }
761 : :
762 : : /**
763 : : * Returns the iterator pointing to the end of the children (one
764 : : * beyond the last one), if the node's kind is the same as the
765 : : * parameter, otherwise returns the iterator pointing to the
766 : : * one-of-the-node-itself. This is useful if you want to pretend to
767 : : * iterate over a "unary" ADD, for instance, since unary PLUSes
768 : : * don't exist---begin(ADD) will give an iterator over the children
769 : : * if the node's an ADD node, otherwise give an iterator over the
770 : : * node itself, as if it were a unary ADD.
771 : : * @param kind the kind to match
772 : : * @return the kinded_iterator pointing off-the-end of this Node (if
773 : : * its kind is not the passed kind) or off-the-end of its children
774 : : */
775 : 2 : inline kinded_iterator end(Kind kind)
776 : : {
777 : 2 : assertTNodeNotExpired();
778 : 2 : return kinded_iterator::end(*this, kind);
779 : : }
780 : :
781 : : /**
782 : : * Returns the const_iterator pointing to the first child.
783 : : * @return the const_iterator
784 : : */
785 : 127068426 : const_iterator begin() const
786 : : {
787 : 127068426 : assertTNodeNotExpired();
788 : 127068426 : return d_nv->begin<NodeTemplate<ref_count>>();
789 : : }
790 : :
791 : : /**
792 : : * Returns the const_iterator pointing to the end of the children (one
793 : : * beyond the last one.
794 : : * @return the end of the children const_iterator.
795 : : */
796 : 117494993 : const_iterator end() const
797 : : {
798 : 117494993 : assertTNodeNotExpired();
799 : 117494993 : return d_nv->end<NodeTemplate<ref_count>>();
800 : : }
801 : :
802 : : /**
803 : : * Returns the const_reverse_iterator pointing to the last child.
804 : : * @return the const_reverse_iterator
805 : : */
806 : 11395268 : const_reverse_iterator rbegin() const
807 : : {
808 : 11395268 : assertTNodeNotExpired();
809 : 11395268 : return std::make_reverse_iterator(d_nv->end<NodeTemplate<ref_count>>());
810 : : }
811 : :
812 : : /**
813 : : * Returns the const_reverse_iterator pointing to one before the first child.
814 : : * @return the end of the const_reverse_iterator.
815 : : */
816 : 11395268 : const_reverse_iterator rend() const
817 : : {
818 : 11395268 : assertTNodeNotExpired();
819 : 11395268 : return std::make_reverse_iterator(d_nv->begin<NodeTemplate<ref_count>>());
820 : : }
821 : :
822 : : /**
823 : : * Returns the iterator pointing to the first child, if the node's
824 : : * kind is the same as the parameter, otherwise returns the iterator
825 : : * pointing to the node itself. This is useful if you want to
826 : : * pretend to iterate over a "unary" ADD, for instance, since unary
827 : : * PLUSes don't exist---begin(ADD) will give an iterator over the
828 : : * children if the node's an ADD node, otherwise give an iterator
829 : : * over the node itself, as if it were a unary ADD.
830 : : * @param kind the kind to match
831 : : * @return the kinded_iterator iterating over this Node (if its kind
832 : : * is not the passed kind) or its children
833 : : */
834 : : inline const_kinded_iterator begin(Kind kind) const
835 : : {
836 : : assertTNodeNotExpired();
837 : : return const_kinded_iterator::begin(*this, kind);
838 : : }
839 : :
840 : : /**
841 : : * Returns the iterator pointing to the end of the children (one
842 : : * beyond the last one), if the node's kind is the same as the
843 : : * parameter, otherwise returns the iterator pointing to the
844 : : * one-of-the-node-itself. This is useful if you want to pretend to
845 : : * iterate over a "unary" ADD, for instance, since unary PLUSes
846 : : * don't exist---begin(ADD) will give an iterator over the children
847 : : * if the node's an ADD node, otherwise give an iterator over the
848 : : * node itself, as if it were a unary ADD.
849 : : * @param kind the kind to match
850 : : * @return the kinded_iterator pointing off-the-end of this Node (if
851 : : * its kind is not the passed kind) or off-the-end of its children
852 : : */
853 : : inline const_kinded_iterator end(Kind kind) const
854 : : {
855 : : assertTNodeNotExpired();
856 : : return const_kinded_iterator::end(*this, kind);
857 : : }
858 : :
859 : : /**
860 : : * Converts this node into a string representation.
861 : : * @return the string representation of this node.
862 : : */
863 : 68057 : inline std::string toString() const
864 : : {
865 : 68057 : assertTNodeNotExpired();
866 : 68057 : return d_nv->toString();
867 : : }
868 : :
869 : : /**
870 : : * Converts this node into a string representation and sends it to the
871 : : * given stream
872 : : *
873 : : * @param out the stream to serialize this node to
874 : : */
875 : 8379954 : inline void toStream(std::ostream& out) const
876 : : {
877 : 8379954 : assertTNodeNotExpired();
878 : 8379954 : d_nv->toStream(out);
879 : 8379954 : }
880 : :
881 : 542 : void constToStream(std::ostream& out) const
882 : : {
883 : 542 : kind::metakind::nodeValueConstantToStream(out, d_nv);
884 : 542 : }
885 : :
886 : : /**
887 : : * Very basic pretty printer for Node.
888 : : * @param out output stream to print to.
889 : : * @param indent number of spaces to indent the formula by.
890 : : */
891 : : inline void printAst(std::ostream& out, int indent = 0) const;
892 : :
893 : : template <bool ref_count2>
894 : : NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const;
895 : :
896 : : NodeTemplate<true> notNode() const;
897 : : NodeTemplate<true> negate() const;
898 : : template <bool ref_count2>
899 : : NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const;
900 : : template <bool ref_count2>
901 : : NodeTemplate<true> orNode(const NodeTemplate<ref_count2>& right) const;
902 : : template <bool ref_count2, bool ref_count3>
903 : : NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
904 : : const NodeTemplate<ref_count3>& elsepart) const;
905 : : NodeTemplate<true> iteNode(const TNode (&args)[2]) const;
906 : : template <bool ref_count2>
907 : : NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
908 : : template <bool ref_count2>
909 : : NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
910 : :
911 : : }; /* class NodeTemplate<ref_count> */
912 : :
913 : : /**
914 : : * Serializes a given node to the given stream.
915 : : *
916 : : * @param out the output stream to use
917 : : * @param n the node to output to the stream
918 : : * @return the stream
919 : : */
920 : 3141653 : inline std::ostream& operator<<(std::ostream& out, TNode n)
921 : : {
922 : 3141653 : n.toStream(out);
923 : 3141653 : return out;
924 : : }
925 : :
926 : : /**
927 : : * Serialize a vector of nodes to given stream.
928 : : *
929 : : * @param out the output stream to use
930 : : * @param container the vector of nodes to output to the stream
931 : : * @return the stream
932 : : */
933 : : template <bool RC>
934 : 0 : std::ostream& operator<<(std::ostream& out,
935 : : const std::vector<NodeTemplate<RC>>& container)
936 : : {
937 : 0 : container_to_stream(out, container);
938 : 0 : return out;
939 : : }
940 : :
941 : : /**
942 : : * Serialize a set of nodes to the given stream.
943 : : *
944 : : * @param out the output stream to use
945 : : * @param container the set of nodes to output to the stream
946 : : * @return the stream
947 : : */
948 : : template <bool RC>
949 : 0 : std::ostream& operator<<(std::ostream& out,
950 : : const std::set<NodeTemplate<RC>>& container)
951 : : {
952 : 0 : container_to_stream(out, container);
953 : 0 : return out;
954 : : }
955 : :
956 : : /**
957 : : * Serialize an unordered_set of nodes to the given stream.
958 : : *
959 : : * @param out the output stream to use
960 : : * @param container the unordered_set of nodes to output to the stream
961 : : * @return the stream
962 : : */
963 : : template <bool RC, typename hash_function>
964 : 0 : std::ostream& operator<<(
965 : : std::ostream& out,
966 : : const std::unordered_set<NodeTemplate<RC>, hash_function>& container)
967 : : {
968 : 0 : container_to_stream(out, container);
969 : 0 : return out;
970 : : }
971 : :
972 : : /**
973 : : * Serialize a map of nodes to the given stream.
974 : : *
975 : : * @param out the output stream to use
976 : : * @param container the map of nodes to output to the stream
977 : : * @return the stream
978 : : */
979 : : template <bool RC, typename V>
980 : 0 : std::ostream& operator<<(std::ostream& out,
981 : : const std::map<NodeTemplate<RC>, V>& container)
982 : : {
983 : 0 : container_to_stream(out, container);
984 : 0 : return out;
985 : : }
986 : :
987 : : /**
988 : : * Serialize an unordered_map of nodes to the given stream.
989 : : *
990 : : * @param out the output stream to use
991 : : * @param container the unordered_map of nodes to output to the stream
992 : : * @return the stream
993 : : */
994 : : template <bool RC, typename V, typename HF>
995 : : std::ostream& operator<<(
996 : : std::ostream& out,
997 : : const std::unordered_map<NodeTemplate<RC>, V, HF>& container)
998 : : {
999 : : container_to_stream(out, container);
1000 : : return out;
1001 : : }
1002 : :
1003 : : } // namespace cvc5::internal
1004 : :
1005 : : // #include "expr/attribute.h"
1006 : : #include "expr/node_manager.h"
1007 : :
1008 : : namespace cvc5::internal {
1009 : :
1010 : : using TNodePairHashFunction =
1011 : : PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>;
1012 : :
1013 : : template <bool ref_count>
1014 : 1473805739 : inline size_t NodeTemplate<ref_count>::getNumChildren() const
1015 : : {
1016 : 1473805739 : assertTNodeNotExpired();
1017 : 1473805739 : return d_nv->getNumChildren();
1018 : : }
1019 : :
1020 : : template <bool ref_count>
1021 : : template <class T>
1022 : 789366493 : inline const T& NodeTemplate<ref_count>::getConst() const
1023 : : {
1024 : 789366493 : assertTNodeNotExpired();
1025 : 789366493 : return d_nv->getConst<T>();
1026 : : }
1027 : :
1028 : : template <bool ref_count>
1029 : : template <class AttrKind>
1030 : 1187555355 : inline typename AttrKind::value_type NodeTemplate<ref_count>::getAttribute(
1031 : : const AttrKind&) const
1032 : : {
1033 : 1187555355 : assertTNodeNotExpired();
1034 : :
1035 : 1187555355 : return d_nv->getNodeManager()->getAttribute(*this, AttrKind());
1036 : : }
1037 : :
1038 : : template <bool ref_count>
1039 : : template <class AttrKind>
1040 : 372444877 : inline bool NodeTemplate<ref_count>::hasAttribute(const AttrKind&) const
1041 : : {
1042 : 372444877 : assertTNodeNotExpired();
1043 : :
1044 : 372444877 : return d_nv->getNodeManager()->hasAttribute(*this, AttrKind());
1045 : : }
1046 : :
1047 : : template <bool ref_count>
1048 : : template <class AttrKind>
1049 : 159825424 : inline bool NodeTemplate<ref_count>::getAttribute(
1050 : : const AttrKind&, typename AttrKind::value_type& ret) const
1051 : : {
1052 : 159825424 : assertTNodeNotExpired();
1053 : :
1054 : 159825424 : return d_nv->getNodeManager()->getAttribute(*this, AttrKind(), ret);
1055 : : }
1056 : :
1057 : : template <bool ref_count>
1058 : : template <class AttrKind>
1059 : 238987587 : inline void NodeTemplate<ref_count>::setAttribute(
1060 : : const AttrKind&, const typename AttrKind::value_type& value)
1061 : : {
1062 : 238987587 : assertTNodeNotExpired();
1063 : :
1064 : 238987587 : d_nv->getNodeManager()->setAttribute(*this, AttrKind(), value);
1065 : 238987587 : }
1066 : :
1067 : : template <bool ref_count>
1068 : : NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(
1069 : : &expr::NodeValue::null());
1070 : :
1071 : : // FIXME: escape from type system convenient but is there a better
1072 : : // way? Nodes conceptually don't change their expr values but of
1073 : : // course they do modify the refcount. But it's nice to be able to
1074 : : // support node_iterators over const NodeValue*. So.... hm.
1075 : : template <bool ref_count>
1076 : 6348174269 : NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev)
1077 : 6348174269 : : d_nv(const_cast<expr::NodeValue*>(ev))
1078 : : {
1079 [ - + ][ - + ]: 6348174269 : Assert(d_nv != nullptr) << "Expecting a non-NULL expression value!";
[ - - ]
1080 : : if (ref_count)
1081 : : {
1082 : 2900719808 : d_nv->inc();
1083 : : }
1084 : : else
1085 : : {
1086 [ - + ][ - - ]: 3447454461 : Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null())
[ - + ][ - + ]
[ - - ]
1087 : 0 : << "TNode constructed from NodeValue with rc == 0";
1088 : : }
1089 : 6348174269 : }
1090 : :
1091 : : // the code for these two following constructors ("conversion/copy
1092 : : // constructors") is identical, but we need both. see comment in the
1093 : : // class.
1094 : :
1095 : : template <bool ref_count>
1096 :12215859433 : NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e)
1097 : : {
1098 [ - + ][ - + ]:12215859433 : Assert(e.d_nv != nullptr) << "Expecting a non-NULL expression value!";
[ - - ]
1099 :12215859433 : d_nv = e.d_nv;
1100 : : if (ref_count)
1101 : : {
1102 [ - + ][ - + ]: 4439145779 : Assert(d_nv->d_rc > 0) << "Node constructed from TNode with rc == 0";
[ - - ]
1103 : 4439145779 : d_nv->inc();
1104 : : }
1105 : : else
1106 : : {
1107 : : // shouldn't ever fail
1108 [ - + ][ - + ]: 7776713654 : Assert(d_nv->d_rc > 0) << "TNode constructed from Node with rc == 0";
[ - - ]
1109 : : }
1110 :12215859433 : }
1111 : :
1112 : : template <bool ref_count>
1113 :41792199104 : NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e)
1114 : : {
1115 [ - + ][ - + ]:41792199104 : Assert(e.d_nv != nullptr) << "Expecting a non-NULL expression value!";
[ - - ]
1116 :41792199104 : d_nv = e.d_nv;
1117 : : if (ref_count)
1118 : : {
1119 : : // shouldn't ever fail
1120 [ - + ][ - + ]:18949774963 : Assert(d_nv->d_rc > 0) << "Node constructed from Node with rc == 0";
[ - - ]
1121 :18949774963 : d_nv->inc();
1122 : : }
1123 : : else
1124 : : {
1125 [ - + ][ - + ]:22842424141 : Assert(d_nv->d_rc > 0) << "TNode constructed from TNode with rc == 0";
[ - - ]
1126 : : }
1127 :41792199104 : }
1128 : :
1129 : : template <bool ref_count>
1130 :63222667244 : NodeTemplate<ref_count>::~NodeTemplate()
1131 : : {
1132 [ - + ][ - + ]:63222667244 : Assert(d_nv != nullptr) << "Expecting a non-NULL expression value!";
1133 : : if (ref_count)
1134 : : {
1135 : : // shouldn't ever fail
1136 [ - + ][ - + ]:28321340330 : Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
1137 :28321340330 : d_nv->dec();
1138 : : }
1139 :63222667244 : }
1140 : :
1141 : : template <bool ref_count>
1142 : : void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev)
1143 : : {
1144 : : d_nv = ev;
1145 : : if (ref_count)
1146 : : {
1147 : : d_nv->inc();
1148 : : }
1149 : : else
1150 : : {
1151 : : Assert(d_nv->d_rc > 0) << "TNode assigned to NodeValue with rc == 0";
1152 : : }
1153 : : }
1154 : :
1155 : : template <bool ref_count>
1156 : 5142195594 : NodeTemplate<ref_count>& NodeTemplate<ref_count>::operator=(
1157 : : const NodeTemplate& e)
1158 : : {
1159 [ - + ][ - + ]: 5142195594 : Assert(d_nv != nullptr) << "Expecting a non-NULL expression value!";
[ - - ]
1160 [ - + ][ - + ]: 5142195594 : Assert(e.d_nv != nullptr) << "Expecting a non-NULL expression value on RHS!";
[ - - ]
1161 [ + + ]: 5142195594 : if (__builtin_expect((d_nv != e.d_nv), true))
1162 : : {
1163 : : if (ref_count)
1164 : : {
1165 : : // shouldn't ever fail
1166 [ - + ][ - + ]: 2027598672 : Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
[ - - ]
1167 : 2027598672 : d_nv->dec();
1168 : : }
1169 : 4005797246 : d_nv = e.d_nv;
1170 : : if (ref_count)
1171 : : {
1172 : : // shouldn't ever fail
1173 [ - + ][ - + ]: 2027598672 : Assert(d_nv->d_rc > 0) << "Node assigned from Node with rc == 0";
[ - - ]
1174 : 2027598672 : d_nv->inc();
1175 : : }
1176 : : else
1177 : : {
1178 [ - + ][ - + ]: 1978198574 : Assert(d_nv->d_rc > 0) << "TNode assigned from TNode with rc == 0";
[ - - ]
1179 : : }
1180 : : }
1181 : 5142195594 : return *this;
1182 : : }
1183 : :
1184 : : template <bool ref_count>
1185 : 439527894 : NodeTemplate<ref_count>& NodeTemplate<ref_count>::operator=(
1186 : : const NodeTemplate<!ref_count>& e)
1187 : : {
1188 [ - + ][ - + ]: 439527894 : Assert(d_nv != nullptr) << "Expecting a non-NULL expression value!";
[ - - ]
1189 [ - + ][ - + ]: 439527894 : Assert(e.d_nv != nullptr) << "Expecting a non-NULL expression value on RHS!";
[ - - ]
1190 [ + + ]: 439527894 : if (__builtin_expect((d_nv != e.d_nv), true))
1191 : : {
1192 : : if (ref_count)
1193 : : {
1194 : : // shouldn't ever fail
1195 [ - + ][ - + ]: 122673333 : Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
[ - - ]
1196 : 122673333 : d_nv->dec();
1197 : : }
1198 : 354967165 : d_nv = e.d_nv;
1199 : : if (ref_count)
1200 : : {
1201 [ - + ][ - + ]: 122673333 : Assert(d_nv->d_rc > 0) << "Node assigned from TNode with rc == 0";
[ - - ]
1202 : 122673333 : d_nv->inc();
1203 : : }
1204 : : else
1205 : : {
1206 : : // shouldn't ever happen
1207 [ - + ][ - + ]: 232293832 : Assert(d_nv->d_rc > 0) << "TNode assigned from Node with rc == 0";
[ - - ]
1208 : : }
1209 : : }
1210 : 439527894 : return *this;
1211 : : }
1212 : :
1213 : : template <bool ref_count>
1214 : : template <bool ref_count2>
1215 : 124143159 : NodeTemplate<true> NodeTemplate<ref_count>::eqNode(
1216 : : const NodeTemplate<ref_count2>& right) const
1217 : : {
1218 : 124143159 : assertTNodeNotExpired();
1219 : 124143159 : return d_nv->getNodeManager()->mkNode(Kind::EQUAL, *this, right);
1220 : : }
1221 : :
1222 : : template <bool ref_count>
1223 : 62157629 : NodeTemplate<true> NodeTemplate<ref_count>::notNode() const
1224 : : {
1225 : 62157629 : assertTNodeNotExpired();
1226 : 62157629 : return d_nv->getNodeManager()->mkNode(Kind::NOT, *this);
1227 : : }
1228 : :
1229 : : template <bool ref_count>
1230 : 16383177 : NodeTemplate<true> NodeTemplate<ref_count>::negate() const
1231 : : {
1232 : 16383177 : assertTNodeNotExpired();
1233 : 16383177 : return (getKind() == Kind::NOT)
1234 : 1463729 : ? NodeTemplate<true>(d_nv->getChild(0))
1235 : 17846906 : : d_nv->getNodeManager()->mkNode(Kind::NOT, *this);
1236 : : }
1237 : :
1238 : : template <bool ref_count>
1239 : : template <bool ref_count2>
1240 : 230371 : NodeTemplate<true> NodeTemplate<ref_count>::andNode(
1241 : : const NodeTemplate<ref_count2>& right) const
1242 : : {
1243 : 230371 : assertTNodeNotExpired();
1244 : 230371 : return d_nv->getNodeManager()->mkNode(Kind::AND, *this, right);
1245 : : }
1246 : :
1247 : : template <bool ref_count>
1248 : : template <bool ref_count2>
1249 : 256234 : NodeTemplate<true> NodeTemplate<ref_count>::orNode(
1250 : : const NodeTemplate<ref_count2>& right) const
1251 : : {
1252 : 256234 : assertTNodeNotExpired();
1253 : 256234 : return d_nv->getNodeManager()->mkNode(Kind::OR, *this, right);
1254 : : }
1255 : :
1256 : : template <bool ref_count>
1257 : : template <bool ref_count2, bool ref_count3>
1258 : 60833 : NodeTemplate<true> NodeTemplate<ref_count>::iteNode(
1259 : : const NodeTemplate<ref_count2>& thenpart,
1260 : : const NodeTemplate<ref_count3>& elsepart) const
1261 : : {
1262 : 60833 : assertTNodeNotExpired();
1263 : 60833 : return d_nv->getNodeManager()->mkNode(Kind::ITE, *this, thenpart, elsepart);
1264 : : }
1265 : :
1266 : : template <bool ref_count>
1267 : 767042 : NodeTemplate<true> NodeTemplate<ref_count>::iteNode(
1268 : : const TNode (&args)[2]) const
1269 : : {
1270 : 767042 : assertTNodeNotExpired();
1271 : 767042 : return d_nv->getNodeManager()->mkNode(Kind::ITE, *this, args[0], args[1]);
1272 : : }
1273 : :
1274 : : template <bool ref_count>
1275 : : template <bool ref_count2>
1276 : 177427 : NodeTemplate<true> NodeTemplate<ref_count>::impNode(
1277 : : const NodeTemplate<ref_count2>& right) const
1278 : : {
1279 : 177427 : assertTNodeNotExpired();
1280 : 177427 : return d_nv->getNodeManager()->mkNode(Kind::IMPLIES, *this, right);
1281 : : }
1282 : :
1283 : : template <bool ref_count>
1284 : : template <bool ref_count2>
1285 : 49 : NodeTemplate<true> NodeTemplate<ref_count>::xorNode(
1286 : : const NodeTemplate<ref_count2>& right) const
1287 : : {
1288 : 49 : assertTNodeNotExpired();
1289 : 49 : return d_nv->getNodeManager()->mkNode(Kind::XOR, *this, right);
1290 : : }
1291 : :
1292 : : template <bool ref_count>
1293 : : inline void NodeTemplate<ref_count>::printAst(std::ostream& out,
1294 : : int indent) const
1295 : : {
1296 : : assertTNodeNotExpired();
1297 : : d_nv->printAst(out, indent);
1298 : : }
1299 : :
1300 : : /**
1301 : : * Returns a node representing the operator of this expression.
1302 : : * If this is an APPLY_UF, then the operator will be a functional term.
1303 : : * Otherwise, it will be a node with kind BUILTIN.
1304 : : */
1305 : : template <bool ref_count>
1306 : 260569325 : NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const
1307 : : {
1308 : 260569325 : assertTNodeNotExpired();
1309 : :
1310 : 260569325 : kind::MetaKind mk = getMetaKind();
1311 [ + + ]: 260569325 : if (mk == kind::metakind::OPERATOR)
1312 : : {
1313 : : /* Returns a BUILTIN node. */
1314 : 112271215 : return d_nv->getNodeManager()->operatorOf(getKind());
1315 : : }
1316 [ - + ][ - + ]: 148298110 : Assert(mk == kind::metakind::PARAMETERIZED);
[ - - ]
1317 : : /* The operator is the first child. */
1318 : 148298110 : return Node(d_nv->d_children[0]);
1319 : : }
1320 : :
1321 : : /**
1322 : : * Returns true if the node has an operator (i.e., it's not a variable
1323 : : * or a constant).
1324 : : */
1325 : : template <bool ref_count>
1326 : 159428675 : inline bool NodeTemplate<ref_count>::hasOperator() const
1327 : : {
1328 : 159428675 : assertTNodeNotExpired();
1329 : 159428675 : return NodeManager::hasOperator(getKind());
1330 : : }
1331 : :
1332 : : template <bool ref_count>
1333 : 1173267930 : TypeNode NodeTemplate<ref_count>::getType(bool check) const
1334 : : {
1335 : 1173267930 : assertTNodeNotExpired();
1336 : 1173267930 : TypeNode tn = d_nv->getNodeManager()->getType(*this, check);
1337 [ + + ]: 1173267930 : if (tn.isNull())
1338 : : {
1339 : : // recompute with an error stream and throw a type exception
1340 : 244 : std::stringstream errOutTmp;
1341 : 244 : tn = d_nv->getNodeManager()->getType(*this, check, &errOutTmp);
1342 : 244 : throw TypeCheckingExceptionPrivate(*this, errOutTmp.str());
1343 : 244 : }
1344 : 1173267686 : return tn;
1345 : 244 : }
1346 : :
1347 : : template <bool ref_count>
1348 : 288245014 : TypeNode NodeTemplate<ref_count>::getTypeOrNull(bool check) const
1349 : : {
1350 : 288245014 : assertTNodeNotExpired();
1351 : 288245014 : return d_nv->getNodeManager()->getType(*this, check);
1352 : : }
1353 : :
1354 : : template <bool ref_count>
1355 : 570921 : inline Node NodeTemplate<ref_count>::substitute(TNode node,
1356 : : TNode replacement) const
1357 : : {
1358 [ + + ]: 570921 : if (node == *this)
1359 : : {
1360 : 100887 : return replacement;
1361 : : }
1362 : 470034 : std::unordered_map<TNode, TNode> cache;
1363 : 470034 : return substitute(node, replacement, cache);
1364 : 470034 : }
1365 : :
1366 : : template <bool ref_count>
1367 : 27778139 : Node NodeTemplate<ref_count>::substitute(
1368 : : TNode node,
1369 : : TNode replacement,
1370 : : std::unordered_map<TNode, TNode>& cache) const
1371 : : {
1372 [ - + ][ - + ]: 27778139 : Assert(node != *this);
[ - - ]
1373 : :
1374 [ + + ][ + + ]: 27778139 : if (getNumChildren() == 0 || node == replacement)
[ + + ]
1375 : : {
1376 : 6829529 : return *this;
1377 : : }
1378 : :
1379 : : // in cache?
1380 : 20948610 : typename std::unordered_map<TNode, TNode>::const_iterator i =
1381 : 41889218 : cache.find(*this);
1382 [ + + ]: 20948610 : if (i != cache.end())
1383 : : {
1384 : 6513855 : return (*i).second;
1385 : : }
1386 : :
1387 : : // otherwise compute
1388 : 14434755 : NodeBuilder nb(getNodeManager(), getKind());
1389 [ + + ]: 14434755 : if (getMetaKind() == kind::metakind::PARAMETERIZED)
1390 : : {
1391 : : // push the operator
1392 [ + + ]: 1510651 : if (getOperator() == node)
1393 : : {
1394 : 2270 : nb << replacement;
1395 : : }
1396 : : else
1397 : : {
1398 : 1508381 : nb << getOperator().substitute(node, replacement, cache);
1399 : : }
1400 : : }
1401 [ + + ]: 40573766 : for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1402 : : {
1403 [ + + ]: 26139011 : if (*it == node)
1404 : : {
1405 : 739864 : nb << replacement;
1406 : : }
1407 : : else
1408 : : {
1409 : 25399147 : nb << (*it).substitute(node, replacement, cache);
1410 : : }
1411 : : }
1412 : :
1413 : : // put in cache
1414 : 14434755 : Node n = nb;
1415 : 14434755 : cache[*this] = n;
1416 : 14434755 : return n;
1417 : 14434755 : }
1418 : :
1419 : : template <bool ref_count>
1420 : : template <class Iterator1, class Iterator2>
1421 : 22342318 : inline Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
1422 : : Iterator1 nodesEnd,
1423 : : Iterator2 replacementsBegin,
1424 : : Iterator2 replacementsEnd) const
1425 : : {
1426 : 22342318 : std::unordered_map<TNode, TNode> cache;
1427 : : return substitute(
1428 : 44684636 : nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache);
1429 : 22342318 : }
1430 : :
1431 : : template <bool ref_count>
1432 : : template <class Iterator1, class Iterator2>
1433 : 115293190 : Node NodeTemplate<ref_count>::substitute(
1434 : : Iterator1 nodesBegin,
1435 : : Iterator1 nodesEnd,
1436 : : Iterator2 replacementsBegin,
1437 : : Iterator2 replacementsEnd,
1438 : : std::unordered_map<TNode, TNode>& cache) const
1439 : : {
1440 : : // in cache?
1441 : 115293190 : typename std::unordered_map<TNode, TNode>::const_iterator i =
1442 : 224297310 : cache.find(*this);
1443 [ + + ]: 115293190 : if (i != cache.end())
1444 : : {
1445 : 8526240 : return (*i).second;
1446 : : }
1447 : :
1448 : : // otherwise compute
1449 [ - + ][ - + ]: 106766950 : Assert(std::distance(nodesBegin, nodesEnd)
[ - - ]
1450 : : == std::distance(replacementsBegin, replacementsEnd))
1451 : 0 : << "Substitution iterator ranges must be equal size";
1452 : 106766950 : Iterator1 j = std::find(nodesBegin, nodesEnd, TNode(*this));
1453 [ + + ]: 106766950 : if (j != nodesEnd)
1454 : : {
1455 : 5642943 : Iterator2 b = replacementsBegin;
1456 : 5642943 : std::advance(b, std::distance(nodesBegin, j));
1457 : 5642943 : Node n = *b;
1458 : 5642943 : cache[*this] = n;
1459 : 5642943 : return n;
1460 : 5642943 : }
1461 [ + + ]: 101124007 : else if (getNumChildren() == 0)
1462 : : {
1463 : 50340428 : cache[*this] = *this;
1464 : 50340428 : return *this;
1465 : : }
1466 : : else
1467 : : {
1468 : 50783579 : NodeBuilder nb(getNodeManager(), getKind());
1469 [ + + ]: 50783579 : if (getMetaKind() == kind::metakind::PARAMETERIZED)
1470 : : {
1471 : : // push the operator
1472 : 1570986 : nb << getOperator().substitute(
1473 : : nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache);
1474 : : }
1475 [ + + ]: 142163465 : for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1476 : : {
1477 : 91379886 : nb << (*it).substitute(
1478 : : nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache);
1479 : : }
1480 : 50783579 : Node n = nb;
1481 : 50783579 : cache[*this] = n;
1482 : 50783579 : return n;
1483 : 50783579 : }
1484 : : }
1485 : :
1486 : : template <bool ref_count>
1487 : : template <class Iterator>
1488 : 384 : inline Node NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
1489 : : Iterator substitutionsEnd) const
1490 : : {
1491 : 384 : std::unordered_map<TNode, TNode> cache;
1492 : 768 : return substitute(substitutionsBegin, substitutionsEnd, cache);
1493 : 384 : }
1494 : :
1495 : : template <bool ref_count>
1496 : 0 : inline Node NodeTemplate<ref_count>::substitute(
1497 : : std::unordered_map<TNode, TNode>& cache) const
1498 : : {
1499 : : // Since no substitution is given (other than what may already be in the
1500 : : // cache), we pass dummy iterators to conform to the main substitute method,
1501 : : // giving the same value to substitutionsBegin and substitutionsEnd.
1502 : 0 : return substitute(cache.cend(), cache.cend(), cache);
1503 : : }
1504 : :
1505 : : template <bool ref_count>
1506 : : template <class Iterator>
1507 : 1120 : Node NodeTemplate<ref_count>::substitute(
1508 : : Iterator substitutionsBegin,
1509 : : Iterator substitutionsEnd,
1510 : : std::unordered_map<TNode, TNode>& cache) const
1511 : : {
1512 : : // in cache?
1513 : 1120 : typename std::unordered_map<TNode, TNode>::const_iterator i =
1514 : 2240 : cache.find(*this);
1515 [ + + ]: 1120 : if (i != cache.end())
1516 : : {
1517 : 18 : return (*i).second;
1518 : : }
1519 : :
1520 : : // otherwise compute
1521 : : Iterator j =
1522 : 27120 : find_if(substitutionsBegin, substitutionsEnd, [this](const auto& subst) {
1523 : 26264 : return subst.first == *this;
1524 : : });
1525 [ + + ]: 1102 : if (j != substitutionsEnd)
1526 : : {
1527 : 558 : Node n = (*j).second;
1528 : 558 : cache[*this] = n;
1529 : 558 : return n;
1530 : 558 : }
1531 [ + + ]: 544 : else if (getNumChildren() == 0)
1532 : : {
1533 : 306 : cache[*this] = *this;
1534 : 306 : return *this;
1535 : : }
1536 : : else
1537 : : {
1538 : 238 : NodeBuilder nb(getNodeManager(), getKind());
1539 [ + + ]: 238 : if (getMetaKind() == kind::metakind::PARAMETERIZED)
1540 : : {
1541 : : // push the operator
1542 : 208 : nb << getOperator().substitute(
1543 : : substitutionsBegin, substitutionsEnd, cache);
1544 : : }
1545 [ + + ]: 766 : for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1546 : : {
1547 : 528 : nb << (*it).substitute(substitutionsBegin, substitutionsEnd, cache);
1548 : : }
1549 : 238 : Node n = nb;
1550 : 238 : cache[*this] = n;
1551 : 238 : return n;
1552 : 238 : }
1553 : : }
1554 : :
1555 : : } // namespace cvc5::internal
1556 : :
1557 : : #endif /* CVC5__NODE_H */
|
