Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Morgan Deters, Dejan Jovanovic, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Reference-counted encapsulation of a pointer to node information.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__NODE_H
19 : : #define CVC5__NODE_H
20 : :
21 : : #include <cvc5/cvc5_skolem_id.h>
22 : :
23 : : #include <iostream>
24 : : #include <map>
25 : : #include <sstream>
26 : : #include <string>
27 : : #include <unordered_map>
28 : : #include <unordered_set>
29 : : #include <utility>
30 : : #include <vector>
31 : :
32 : : #include "base/check.h"
33 : : #include "base/exception.h"
34 : : #include "base/output.h"
35 : : #include "expr/internal_skolem_id.h"
36 : : #include "expr/kind.h"
37 : : #include "expr/metakind.h"
38 : : #include "expr/node_value.h"
39 : : #include "options/io_utils.h"
40 : : #include "options/language.h"
41 : : #include "util/hash.h"
42 : : #include "util/utility.h"
43 : :
44 : : namespace cvc5::internal {
45 : :
46 : : class TypeNode;
47 : : class NodeManager;
48 : :
49 : : template <bool ref_count>
50 : : class NodeTemplate;
51 : :
52 : : /**
53 : : * Exception thrown during the type-checking phase, it can be
54 : : * thrown by node.getType().
55 : : */
56 : : class TypeCheckingExceptionPrivate : public Exception {
57 : : private:
58 : : /** The node responsible for the failure */
59 : : NodeTemplate<true>* d_node;
60 : :
61 : : public:
62 : : /**
63 : : * Construct the exception with the problematic node and the message
64 : : * @param node the problematic node
65 : : * @param message the message explaining the failure
66 : : */
67 : : TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message);
68 : :
69 : : /** Destructor */
70 : : ~TypeCheckingExceptionPrivate() override;
71 : :
72 : : /**
73 : : * Get the Node that caused the type-checking to fail.
74 : : * @return the node
75 : : */
76 : : NodeTemplate<true> getNode() const;
77 : :
78 : : /**
79 : : * Returns the message corresponding to the type-checking failure.
80 : : * We prefer toStream() to toString() because that keeps the expr-depth
81 : : * and expr-language settings present in the stream.
82 : : */
83 : : void toStream(std::ostream& out) const override;
84 : :
85 : : };/* class TypeCheckingExceptionPrivate */
86 : :
87 : : class UnknownTypeException : public TypeCheckingExceptionPrivate {
88 : : public:
89 : : UnknownTypeException(NodeTemplate<false> node);
90 : : };/* class UnknownTypeException */
91 : :
92 : : /**
93 : : * \typedef NodeTemplate<true> Node;
94 : : *
95 : : * The Node class encapsulates the NodeValue with reference counting.
96 : : *
97 : : * One should use generally use Nodes to manipulate expressions, to be safe.
98 : : * Every outstanding Node that references a NodeValue is counted in that
99 : : * NodeValue's reference count. Reference counts are maintained correctly
100 : : * on assignment of the Node object (to point to another NodeValue), and,
101 : : * upon destruction of the Node object, the NodeValue's reference count is
102 : : * decremented and, if zero, it becomes eligible for reclamation by the
103 : : * system.
104 : : */
105 : : typedef NodeTemplate<true> Node;
106 : :
107 : : /**
108 : : * \typedef NodeTemplate<false> TNode;
109 : : *
110 : : * The TNode class encapsulates the NodeValue but doesn't count references.
111 : : *
112 : : * TNodes are just like Nodes, but they don't update the reference count.
113 : : * Therefore, there is less overhead (copying a TNode is just the cost of
114 : : * the underlying pointer copy). Generally speaking, this is unsafe!
115 : : * However, there are certain situations where a TNode can be used safely.
116 : : *
117 : : * The largest class of uses for TNodes are when you need to use them in a
118 : : * "temporary," scoped fashion (hence the "T" in "TNode"). In general,
119 : : * it is safe to use TNode as a function parameter type, since the calling
120 : : * function (or some other function on the call stack) presumably has a Node
121 : : * reference to the expression data. It is generally _not_ safe, however,
122 : : * to return a TNode _from_ a function. (Functions that return Nodes often
123 : : * create the expression they return; such new expressions may not be
124 : : * referenced on the call stack, and have a reference count of 1 on
125 : : * creation. If this is returned as a TNode rather than a Node, the
126 : : * count drops to zero, marking the expression as eligible for reclamation.)
127 : : *
128 : : * More guidelines on when to use TNodes is available in the cvc5
129 : : * Developer's Guide:
130 : : * https://github.com/cvc5/cvc5/wiki/Developer-Guide#dealing-with-expressions-nodes-and-tnodes
131 : : */
132 : : typedef NodeTemplate<false> TNode;
133 : :
134 : : } // namespace cvc5::internal
135 : :
136 : : namespace std {
137 : :
138 : : template <>
139 : : struct hash<cvc5::internal::Node>
140 : : {
141 : : size_t operator()(const cvc5::internal::Node& node) const;
142 : : };
143 : :
144 : : template <>
145 : : struct hash<cvc5::internal::TNode>
146 : : {
147 : : size_t operator()(const cvc5::internal::TNode& node) const;
148 : : };
149 : :
150 : : } // namespace std
151 : :
152 : : namespace cvc5::internal {
153 : : namespace expr {
154 : :
155 : : class NodeValue;
156 : :
157 : : namespace attr {
158 : : class AttributeManager;
159 : : struct SmtAttributes;
160 : : } // namespace attr
161 : :
162 : : class ExprSetDepth;
163 : : } // namespace expr
164 : :
165 : : /**
166 : : * Encapsulation of an NodeValue pointer. The reference count is
167 : : * maintained in the NodeValue if ref_count is true.
168 : : * @param ref_count if true reference are counted in the NodeValue
169 : : */
170 : : template <bool ref_count>
171 : : class NodeTemplate {
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 :>10444*10^7 : inline void assertTNodeNotExpired() const
221 : : {
222 : : if(!ref_count) {
223 [ - + ][ - + ]:55174585149 : Assert(d_nv->d_rc > 0) << "TNode pointing to an expired NodeValue";
[ - - ]
224 : : }
225 :>10444*10^7 : }
226 : :
227 : : public:
228 : :
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 : 3052924495 : 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 : 1248087028 : 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 : 9285431280 : bool isNull() const
312 : : {
313 : 9285431280 : assertTNodeNotExpired();
314 : 9285431280 : 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 :13179930437 : bool operator==(const NodeTemplate<ref_count_1>& node) const {
324 :13179930437 : assertTNodeNotExpired();
325 :13179930437 : node.assertTNodeNotExpired();
326 :13179930437 : return d_nv == node.d_nv;
327 : : }
328 : :
329 : : /**
330 : : * Structural comparison operator for expressions.
331 : : * @param node the node to compare to
332 : : * @return false if expressions are equal, true otherwise
333 : : */
334 : : template <bool ref_count_1>
335 : 447806435 : bool operator!=(const NodeTemplate<ref_count_1>& node) const {
336 : 447806435 : assertTNodeNotExpired();
337 : 447806435 : node.assertTNodeNotExpired();
338 : 447806435 : return d_nv != node.d_nv;
339 : : }
340 : :
341 : : /**
342 : : * We compare by expression ids so, keeping things deterministic and having
343 : : * that subexpressions have to be smaller than the enclosing expressions.
344 : : * @param node the node to compare to
345 : : * @return true if this expression is smaller
346 : : */
347 : : template <bool ref_count_1>
348 :10149773051 : inline bool operator<(const NodeTemplate<ref_count_1>& node) const {
349 :10149773051 : assertTNodeNotExpired();
350 :10149773051 : node.assertTNodeNotExpired();
351 :10149773051 : return d_nv->d_id < node.d_nv->d_id;
352 : : }
353 : :
354 : : /**
355 : : * We compare by expression ids so, keeping things deterministic and having
356 : : * that subexpressions have to be smaller than the enclosing expressions.
357 : : * @param node the node to compare to
358 : : * @return true if this expression is greater
359 : : */
360 : : template <bool ref_count_1>
361 : 16691160 : inline bool operator>(const NodeTemplate<ref_count_1>& node) const {
362 : 16691160 : assertTNodeNotExpired();
363 : 16691160 : node.assertTNodeNotExpired();
364 : 16691160 : return d_nv->d_id > node.d_nv->d_id;
365 : : }
366 : :
367 : : /**
368 : : * We compare by expression ids so, keeping things deterministic and having
369 : : * that subexpressions have to be smaller than the enclosing expressions.
370 : : * @param node the node to compare to
371 : : * @return true if this expression is smaller than or equal to
372 : : */
373 : : template <bool ref_count_1>
374 : 15679 : inline bool operator<=(const NodeTemplate<ref_count_1>& node) const {
375 : 15679 : assertTNodeNotExpired();
376 : 15679 : node.assertTNodeNotExpired();
377 : 15679 : return d_nv->d_id <= node.d_nv->d_id;
378 : : }
379 : :
380 : : /**
381 : : * We compare by expression ids so, keeping things deterministic and having
382 : : * that subexpressions have to be smaller than the enclosing expressions.
383 : : * @param node the node to compare to
384 : : * @return true if this expression is greater than or equal to
385 : : */
386 : : template <bool ref_count_1>
387 : 141801 : inline bool operator>=(const NodeTemplate<ref_count_1>& node) const {
388 : 141801 : assertTNodeNotExpired();
389 : 141801 : node.assertTNodeNotExpired();
390 : 141801 : return d_nv->d_id >= node.d_nv->d_id;
391 : : }
392 : :
393 : : /**
394 : : * Returns the i-th child of this node.
395 : : * @param i the index of the child
396 : : * @return the node representing the i-th child
397 : : */
398 : 3561925684 : NodeTemplate operator[](int i) const {
399 : 3561925684 : assertTNodeNotExpired();
400 : 3561925684 : return NodeTemplate(d_nv->getChild(i));
401 : : }
402 : :
403 : : /**
404 : : * Returns true if this node represents a constant
405 : : * @return true if const
406 : : */
407 : : bool isConst() const;
408 : :
409 : : /**
410 : : * Returns true if this node represents a variable
411 : : * @return true if variable
412 : : */
413 : 826145041 : inline bool isVar() const {
414 : 826145041 : assertTNodeNotExpired();
415 : 826145041 : return getMetaKind() == kind::metakind::VARIABLE;
416 : : }
417 : :
418 : : /**
419 : : * Returns true if this node represents a nullary operator
420 : : */
421 : : inline bool isNullaryOp() const {
422 : : assertTNodeNotExpired();
423 : : return getMetaKind() == kind::metakind::NULLARY_OPERATOR;
424 : : }
425 : :
426 : : /**
427 : : * Returns true if this node represents a closure, that is an expression
428 : : * that binds variables.
429 : : */
430 : 183560500 : inline bool isClosure() const {
431 : 183560500 : assertTNodeNotExpired();
432 : 183560500 : return isClosureKind(getKind());
433 : : }
434 : :
435 : : /**
436 : : * Returns the unique id of this node
437 : : * @return the ud
438 : : */
439 : 9941740002 : uint64_t getId() const
440 : : {
441 : 9941740002 : assertTNodeNotExpired();
442 : 9941740002 : return d_nv->getId();
443 : : }
444 : :
445 : : /**
446 : : * Returns the associated node manager
447 : : */
448 : 4703091170 : NodeManager* getNodeManager() const
449 : : {
450 : 4703091170 : assertTNodeNotExpired();
451 : 4703091170 : return d_nv->getNodeManager();
452 : : }
453 : :
454 : : /**
455 : : * Returns a node representing the operator of this expression.
456 : : * If this is an APPLY_UF, then the operator will be a functional term.
457 : : * Otherwise, it will be a node with kind BUILTIN.
458 : : */
459 : : NodeTemplate<true> getOperator() const;
460 : :
461 : : /**
462 : : * Returns true if the node has an operator (i.e., it's not a
463 : : * variable or a constant).
464 : : */
465 : : inline bool hasOperator() const;
466 : :
467 : : /**
468 : : * Get the type for the node and optionally do type checking.
469 : : *
470 : : * Initial type computation will be near-constant time if
471 : : * type checking is not requested. Results are memoized, so that
472 : : * subsequent calls to getType() without type checking will be
473 : : * constant time.
474 : : *
475 : : * Initial type checking is linear in the size of the expression.
476 : : * Again, the results are memoized, so that subsequent calls to
477 : : * getType(), with or without type checking, will be constant
478 : : * time.
479 : : *
480 : : * NOTE: A TypeCheckingException can be thrown even when type
481 : : * checking is not requested. getType() will always return a
482 : : * valid and correct type and, thus, an exception will be thrown
483 : : * when no valid or correct type can be computed (e.g., if the
484 : : * arguments to a bit-vector operation aren't bit-vectors). When
485 : : * type checking is not requested, getType() will do the minimum
486 : : * amount of checking required to return a valid result.
487 : : *
488 : : * @param check whether we should check the type as we compute it
489 : : * (default: false)
490 : : */
491 : : TypeNode getType(bool check = false) const;
492 : : /**
493 : : * Same as getType, but does not throw a type exception if this term is
494 : : * not well-typed. Instead, this method will return the null type.
495 : : */
496 : : TypeNode getTypeOrNull(bool check = false) const;
497 : :
498 : : /**
499 : : * Has name? Return true if this node has an associated variable
500 : : * name (via the attribute expr::VarNameAttr). This is true typically for
501 : : * user-created variables.
502 : : */
503 : : bool hasName() const;
504 : : /**
505 : : * Get the name. Returns the string value of the expr::VarNameAttr attribute
506 : : * for this node.
507 : : */
508 : : std::string getName() const;
509 : :
510 : : /**
511 : : * Substitution of Nodes.
512 : : */
513 : : Node substitute(TNode node, TNode replacement) const;
514 : :
515 : : /**
516 : : * Simultaneous substitution of Nodes. Elements in the Iterator1
517 : : * range will be replaced by their corresponding element in the
518 : : * Iterator2 range. Both ranges should have the same size.
519 : : */
520 : : template <class Iterator1, class Iterator2>
521 : : Node substitute(Iterator1 nodesBegin,
522 : : Iterator1 nodesEnd,
523 : : Iterator2 replacementsBegin,
524 : : Iterator2 replacementsEnd) const;
525 : :
526 : : /**
527 : : * Simultaneous substitution of Nodes. Iterators should be over
528 : : * pairs (x,y) for the rewrites [x->y].
529 : : */
530 : : template <class Iterator>
531 : : Node substitute(Iterator substitutionsBegin,
532 : : Iterator substitutionsEnd) const;
533 : :
534 : : /**
535 : : * Simultaneous substitution of Nodes in cache.
536 : : */
537 : : Node substitute(std::unordered_map<TNode, TNode>& cache) const;
538 : :
539 : : /**
540 : : * Returns the kind of this node.
541 : : * @return the kind
542 : : */
543 :14626520910 : inline Kind getKind() const {
544 :14626520910 : assertTNodeNotExpired();
545 :14626520910 : return Kind(d_nv->d_kind);
546 : : }
547 : :
548 : : /**
549 : : * Returns the metakind of this node.
550 : : * @return the metakind
551 : : */
552 : 3132660439 : inline kind::MetaKind getMetaKind() const {
553 : 3132660439 : assertTNodeNotExpired();
554 : 3132660439 : return kind::metaKindOf(getKind());
555 : : }
556 : :
557 : : /**
558 : : * Returns the number of children this node has.
559 : : * @return the number of children
560 : : */
561 : : inline size_t getNumChildren() const;
562 : :
563 : : /**
564 : : * If this is a CONST_* Node, extract the constant from it.
565 : : */
566 : : template <class T>
567 : : inline const T& getConst() const;
568 : :
569 : : /**
570 : : * @return true if this is a skolem function.
571 : : */
572 : : bool isSkolem() const;
573 : :
574 : : /**
575 : : * @return the skolem identifier of this node.
576 : : */
577 : : SkolemId getSkolemId() const;
578 : :
579 : : /**
580 : : * @return the skolem indices of this node.
581 : : */
582 : : std::vector<Node> getSkolemIndices() const;
583 : :
584 : : /**
585 : : * @return the internal skolem function id, for skolems whose id is
586 : : * SkolemId::INTERNAL.
587 : : */
588 : : InternalSkolemId getInternalSkolemId() const;
589 : :
590 : : /**
591 : : * Returns the reference count of this node.
592 : : * @return the refcount
593 : : */
594 : : unsigned getRefCount() const {
595 : : return d_nv->getRefCount();
596 : : }
597 : :
598 : : /**
599 : : * Returns the value of the given attribute that this has been attached.
600 : : * @param attKind the kind of the attribute
601 : : * @return the value of the attribute
602 : : */
603 : : template <class AttrKind>
604 : : inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
605 : :
606 : : // Note that there are two, distinct hasAttribute() declarations for
607 : : // a reason (rather than using a pointer-valued argument with a
608 : : // default value): they permit more optimized code in the underlying
609 : : // hasAttribute() implementations.
610 : :
611 : : /**
612 : : * Returns true if this node has been associated an attribute of given kind.
613 : : * Additionaly, if a pointer to the value_kind is give, and the attribute
614 : : * value has been set for this node, it will be returned.
615 : : * @param attKind the kind of the attribute
616 : : * @return true if this node has the requested attribute
617 : : */
618 : : template <class AttrKind>
619 : : inline bool hasAttribute(const AttrKind& attKind) const;
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 : : * @param value where to store the value if it exists
627 : : * @return true if this node has the requested attribute
628 : : */
629 : : template <class AttrKind>
630 : : inline bool getAttribute(const AttrKind& attKind,
631 : : typename AttrKind::value_type& value) const;
632 : :
633 : : /**
634 : : * Sets the given attribute of this node to the given value.
635 : : * @param attKind the kind of the atribute
636 : : * @param value the value to set the attribute to
637 : : */
638 : : template <class AttrKind>
639 : : inline void setAttribute(const AttrKind& attKind,
640 : : const typename AttrKind::value_type& value);
641 : :
642 : : /** Iterator allowing for scanning through the children. */
643 : : typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > iterator;
644 : : /** Constant iterator allowing for scanning through the children. */
645 : : using const_iterator =
646 : : typename expr::NodeValue::iterator<NodeTemplate<ref_count>>;
647 : : /**
648 : : * Reverse constant iterator allowing for scanning through the children in
649 : : * reverse order.
650 : : */
651 : : using const_reverse_iterator = std::reverse_iterator<
652 : : typename expr::NodeValue::iterator<NodeTemplate<ref_count>>>;
653 : :
654 : : class kinded_iterator {
655 : : friend class NodeTemplate<ref_count>;
656 : :
657 : : NodeTemplate<ref_count> d_node;
658 : : ssize_t d_child;
659 : :
660 : 4 : kinded_iterator(TNode node, ssize_t child) :
661 : : d_node(node),
662 : 4 : d_child(child) {
663 : 4 : }
664 : :
665 : : // These are factories to serve as clients to Node::begin<K>() and
666 : : // Node::end<K>().
667 : 2 : static kinded_iterator begin(TNode n, Kind k) {
668 [ + + ]: 2 : return kinded_iterator(n, n.getKind() == k ? 0 : -2);
669 : : }
670 : 2 : static kinded_iterator end(TNode n, Kind k) {
671 [ + + ]: 2 : return kinded_iterator(n, n.getKind() == k ? n.getNumChildren() : -1);
672 : : }
673 : :
674 : : public:
675 : : typedef NodeTemplate<ref_count> value_type;
676 : : typedef std::ptrdiff_t difference_type;
677 : : typedef NodeTemplate<ref_count>* pointer;
678 : : typedef NodeTemplate<ref_count>& reference;
679 : :
680 : : kinded_iterator() :
681 : : d_node(NodeTemplate<ref_count>::null()),
682 : : d_child(-2) {
683 : : }
684 : :
685 : 4 : kinded_iterator(const kinded_iterator& i) :
686 : 4 : d_node(i.d_node),
687 : 4 : d_child(i.d_child) {
688 : 4 : }
689 : :
690 : 4 : NodeTemplate<ref_count> operator*() {
691 [ + + ]: 4 : return d_child < 0 ? d_node : d_node[d_child];
692 : : }
693 : :
694 : 2 : bool operator==(const kinded_iterator& i) {
695 [ + - ][ + - ]: 2 : return d_node == i.d_node && d_child == i.d_child;
696 : : }
697 : :
698 : 0 : bool operator!=(const kinded_iterator& i) {
699 : 0 : return !(*this == i);
700 : : }
701 : :
702 : 4 : kinded_iterator& operator++() {
703 [ + - ]: 4 : if(d_child != -1) {
704 : 4 : ++d_child;
705 : : }
706 : 4 : return *this;
707 : : }
708 : :
709 : 4 : kinded_iterator operator++(int) {
710 : 4 : kinded_iterator i = *this;
711 : 4 : ++*this;
712 : 4 : return i;
713 : : }
714 : : };/* class NodeTemplate<ref_count>::kinded_iterator */
715 : :
716 : : typedef kinded_iterator const_kinded_iterator;
717 : :
718 : : /**
719 : : * Returns the iterator pointing to the first child.
720 : : * @return the iterator
721 : : */
722 : 843544419 : inline iterator begin() {
723 : 843544419 : assertTNodeNotExpired();
724 : 843544419 : return d_nv->begin< NodeTemplate<ref_count> >();
725 : : }
726 : :
727 : : /**
728 : : * Returns the iterator pointing to the end of the children (one beyond the
729 : : * last one).
730 : : * @return the end of the children iterator.
731 : : */
732 : 1476375428 : inline iterator end() {
733 : 1476375428 : assertTNodeNotExpired();
734 : 1476375428 : return d_nv->end< NodeTemplate<ref_count> >();
735 : : }
736 : :
737 : : /**
738 : : * Returns the iterator pointing to the first child, if the node's
739 : : * kind is the same as the parameter, otherwise returns the iterator
740 : : * pointing to the node itself. This is useful if you want to
741 : : * pretend to iterate over a "unary" ADD, for instance, since unary
742 : : * PLUSes don't exist---begin(ADD) will give an iterator over the
743 : : * children if the node's an ADD node, otherwise give an iterator
744 : : * over the node itself, as if it were a unary ADD.
745 : : * @param kind the kind to match
746 : : * @return the kinded_iterator iterating over this Node (if its kind
747 : : * is not the passed kind) or its children
748 : : */
749 : 2 : inline kinded_iterator begin(Kind kind) {
750 : 2 : assertTNodeNotExpired();
751 : 2 : return kinded_iterator::begin(*this, kind);
752 : : }
753 : :
754 : : /**
755 : : * Returns the iterator pointing to the end of the children (one
756 : : * beyond the last one), if the node's kind is the same as the
757 : : * parameter, otherwise returns the iterator pointing to the
758 : : * one-of-the-node-itself. This is useful if you want to pretend to
759 : : * iterate over a "unary" ADD, for instance, since unary PLUSes
760 : : * don't exist---begin(ADD) will give an iterator over the children
761 : : * if the node's an ADD node, otherwise give an iterator over the
762 : : * node itself, as if it were a unary ADD.
763 : : * @param kind the kind to match
764 : : * @return the kinded_iterator pointing off-the-end of this Node (if
765 : : * its kind is not the passed kind) or off-the-end of its children
766 : : */
767 : 2 : inline kinded_iterator end(Kind kind) {
768 : 2 : assertTNodeNotExpired();
769 : 2 : return kinded_iterator::end(*this, kind);
770 : : }
771 : :
772 : : /**
773 : : * Returns the const_iterator pointing to the first child.
774 : : * @return the const_iterator
775 : : */
776 : 174154720 : const_iterator begin() const
777 : : {
778 : 174154720 : assertTNodeNotExpired();
779 : 174154720 : return d_nv->begin< NodeTemplate<ref_count> >();
780 : : }
781 : :
782 : : /**
783 : : * Returns the const_iterator pointing to the end of the children (one
784 : : * beyond the last one.
785 : : * @return the end of the children const_iterator.
786 : : */
787 : 169661719 : const_iterator end() const
788 : : {
789 : 169661719 : assertTNodeNotExpired();
790 : 169661719 : return d_nv->end< NodeTemplate<ref_count> >();
791 : : }
792 : :
793 : : /**
794 : : * Returns the const_reverse_iterator pointing to the last child.
795 : : * @return the const_reverse_iterator
796 : : */
797 : 14771002 : const_reverse_iterator rbegin() const
798 : : {
799 : 14771002 : assertTNodeNotExpired();
800 : 14771002 : return std::make_reverse_iterator(d_nv->end<NodeTemplate<ref_count>>());
801 : : }
802 : :
803 : : /**
804 : : * Returns the const_reverse_iterator pointing to one before the first child.
805 : : * @return the end of the const_reverse_iterator.
806 : : */
807 : 14771002 : const_reverse_iterator rend() const
808 : : {
809 : 14771002 : assertTNodeNotExpired();
810 : 14771002 : return std::make_reverse_iterator(d_nv->begin<NodeTemplate<ref_count>>());
811 : : }
812 : :
813 : : /**
814 : : * Returns the iterator pointing to the first child, if the node's
815 : : * kind is the same as the parameter, otherwise returns the iterator
816 : : * pointing to the node itself. This is useful if you want to
817 : : * pretend to iterate over a "unary" ADD, for instance, since unary
818 : : * PLUSes don't exist---begin(ADD) will give an iterator over the
819 : : * children if the node's an ADD node, otherwise give an iterator
820 : : * over the node itself, as if it were a unary ADD.
821 : : * @param kind the kind to match
822 : : * @return the kinded_iterator iterating over this Node (if its kind
823 : : * is not the passed kind) or its children
824 : : */
825 : : inline const_kinded_iterator begin(Kind kind) const {
826 : : assertTNodeNotExpired();
827 : : return const_kinded_iterator::begin(*this, kind);
828 : : }
829 : :
830 : : /**
831 : : * Returns the iterator pointing to the end of the children (one
832 : : * beyond the last one), if the node's kind is the same as the
833 : : * parameter, otherwise returns the iterator pointing to the
834 : : * one-of-the-node-itself. This is useful if you want to pretend to
835 : : * iterate over a "unary" ADD, for instance, since unary PLUSes
836 : : * don't exist---begin(ADD) will give an iterator over the children
837 : : * if the node's an ADD node, otherwise give an iterator over the
838 : : * node itself, as if it were a unary ADD.
839 : : * @param kind the kind to match
840 : : * @return the kinded_iterator pointing off-the-end of this Node (if
841 : : * its kind is not the passed kind) or off-the-end of its children
842 : : */
843 : : inline const_kinded_iterator end(Kind kind) const {
844 : : assertTNodeNotExpired();
845 : : return const_kinded_iterator::end(*this, kind);
846 : : }
847 : :
848 : : /**
849 : : * Converts this node into a string representation.
850 : : * @return the string representation of this node.
851 : : */
852 : 7106 : inline std::string toString() const {
853 : 7106 : assertTNodeNotExpired();
854 : 7106 : return d_nv->toString();
855 : : }
856 : :
857 : : /**
858 : : * Converts this node into a string representation and sends it to the
859 : : * given stream
860 : : *
861 : : * @param out the stream to serialize this node to
862 : : */
863 : 10439790 : inline void toStream(std::ostream& out) const
864 : : {
865 : 10439790 : assertTNodeNotExpired();
866 : 10439790 : d_nv->toStream(out);
867 : 10439790 : }
868 : :
869 : 101 : void constToStream(std::ostream& out) const
870 : : {
871 : 101 : kind::metakind::nodeValueConstantToStream(out, d_nv);
872 : 101 : }
873 : :
874 : : /**
875 : : * Very basic pretty printer for Node.
876 : : * @param out output stream to print to.
877 : : * @param indent number of spaces to indent the formula by.
878 : : */
879 : : inline void printAst(std::ostream& out, int indent = 0) const;
880 : :
881 : : template <bool ref_count2>
882 : : NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const;
883 : :
884 : : NodeTemplate<true> notNode() const;
885 : : NodeTemplate<true> negate() const;
886 : : template <bool ref_count2>
887 : : NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const;
888 : : template <bool ref_count2>
889 : : NodeTemplate<true> orNode(const NodeTemplate<ref_count2>& right) const;
890 : : template <bool ref_count2, bool ref_count3>
891 : : NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
892 : : const NodeTemplate<ref_count3>& elsepart) const;
893 : : template <bool ref_count2>
894 : : NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
895 : : template <bool ref_count2>
896 : : NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
897 : :
898 : : };/* class NodeTemplate<ref_count> */
899 : :
900 : : /**
901 : : * Serializes a given node to the given stream.
902 : : *
903 : : * @param out the output stream to use
904 : : * @param n the node to output to the stream
905 : : * @return the stream
906 : : */
907 : 5020248 : inline std::ostream& operator<<(std::ostream& out, TNode n) {
908 : 5020248 : n.toStream(out);
909 : 5020248 : return out;
910 : : }
911 : :
912 : : /**
913 : : * Serialize a vector of nodes to given stream.
914 : : *
915 : : * @param out the output stream to use
916 : : * @param container the vector of nodes to output to the stream
917 : : * @return the stream
918 : : */
919 : : template <bool RC>
920 : 0 : std::ostream& operator<<(std::ostream& out,
921 : : const std::vector<NodeTemplate<RC>>& container)
922 : : {
923 : 0 : container_to_stream(out, container);
924 : 0 : return out;
925 : : }
926 : :
927 : : /**
928 : : * Serialize a set of nodes to the given stream.
929 : : *
930 : : * @param out the output stream to use
931 : : * @param container the set of nodes to output to the stream
932 : : * @return the stream
933 : : */
934 : : template <bool RC>
935 : 0 : std::ostream& operator<<(std::ostream& out,
936 : : const std::set<NodeTemplate<RC>>& container)
937 : : {
938 : 0 : container_to_stream(out, container);
939 : 0 : return out;
940 : : }
941 : :
942 : : /**
943 : : * Serialize an unordered_set of nodes to the given stream.
944 : : *
945 : : * @param out the output stream to use
946 : : * @param container the unordered_set of nodes to output to the stream
947 : : * @return the stream
948 : : */
949 : : template <bool RC, typename hash_function>
950 : 0 : std::ostream& operator<<(
951 : : std::ostream& out,
952 : : const std::unordered_set<NodeTemplate<RC>, hash_function>& container)
953 : : {
954 : 0 : container_to_stream(out, container);
955 : 0 : return out;
956 : : }
957 : :
958 : : /**
959 : : * Serialize a map of nodes to the given stream.
960 : : *
961 : : * @param out the output stream to use
962 : : * @param container the map of nodes to output to the stream
963 : : * @return the stream
964 : : */
965 : : template <bool RC, typename V>
966 : 0 : std::ostream& operator<<(
967 : : std::ostream& out,
968 : : const std::map<NodeTemplate<RC>, V>& container)
969 : : {
970 : 0 : container_to_stream(out, container);
971 : 0 : return out;
972 : : }
973 : :
974 : : /**
975 : : * Serialize an unordered_map of nodes to the given stream.
976 : : *
977 : : * @param out the output stream to use
978 : : * @param container the unordered_map of nodes to output to the stream
979 : : * @return the stream
980 : : */
981 : : template <bool RC, typename V, typename HF>
982 : : std::ostream& operator<<(
983 : : std::ostream& out,
984 : : const std::unordered_map<NodeTemplate<RC>, V, HF>& container)
985 : : {
986 : : container_to_stream(out, container);
987 : : return out;
988 : : }
989 : :
990 : : } // namespace cvc5::internal
991 : :
992 : : //#include "expr/attribute.h"
993 : : #include "expr/node_manager.h"
994 : :
995 : : namespace cvc5::internal {
996 : :
997 : : using TNodePairHashFunction =
998 : : PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>;
999 : :
1000 : : template <bool ref_count>
1001 : 1913705536 : inline size_t NodeTemplate<ref_count>::getNumChildren() const {
1002 : 1913705536 : assertTNodeNotExpired();
1003 : 1913705536 : return d_nv->getNumChildren();
1004 : : }
1005 : :
1006 : : template <bool ref_count>
1007 : : template <class T>
1008 : 795567787 : inline const T& NodeTemplate<ref_count>::getConst() const {
1009 : 795567787 : assertTNodeNotExpired();
1010 : 795567787 : return d_nv->getConst<T>();
1011 : : }
1012 : :
1013 : : template <bool ref_count>
1014 : : template <class AttrKind>
1015 : 1105910457 : inline typename AttrKind::value_type NodeTemplate<ref_count>::
1016 : : getAttribute(const AttrKind&) const {
1017 : 1105910457 : assertTNodeNotExpired();
1018 : :
1019 : 1105910457 : return d_nv->getNodeManager()->getAttribute(*this, AttrKind());
1020 : : }
1021 : :
1022 : : template <bool ref_count>
1023 : : template <class AttrKind>
1024 : 428257587 : inline bool NodeTemplate<ref_count>::
1025 : : hasAttribute(const AttrKind&) const {
1026 : 428257587 : assertTNodeNotExpired();
1027 : :
1028 : 428257587 : return d_nv->getNodeManager()->hasAttribute(*this, AttrKind());
1029 : : }
1030 : :
1031 : : template <bool ref_count>
1032 : : template <class AttrKind>
1033 : 177018800 : inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
1034 : : typename AttrKind::value_type& ret) const {
1035 : 177018800 : assertTNodeNotExpired();
1036 : :
1037 : 177018800 : return d_nv->getNodeManager()->getAttribute(*this, AttrKind(), ret);
1038 : : }
1039 : :
1040 : : template <bool ref_count>
1041 : : template <class AttrKind>
1042 : 179751319 : inline void NodeTemplate<ref_count>::
1043 : : setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
1044 : 179751319 : assertTNodeNotExpired();
1045 : :
1046 : 179751319 : d_nv->getNodeManager()->setAttribute(*this, AttrKind(), value);
1047 : 179751319 : }
1048 : :
1049 : : template <bool ref_count>
1050 : : NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::null());
1051 : :
1052 : : // FIXME: escape from type system convenient but is there a better
1053 : : // way? Nodes conceptually don't change their expr values but of
1054 : : // course they do modify the refcount. But it's nice to be able to
1055 : : // support node_iterators over const NodeValue*. So.... hm.
1056 : : template <bool ref_count>
1057 : 7902059151 : NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
1058 : 7902059151 : d_nv(const_cast<expr::NodeValue*> (ev)) {
1059 [ - + ][ - + ]: 7902059151 : Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
[ - - ]
1060 : 3929784562 : if(ref_count) {
1061 : 3972274589 : d_nv->inc();
1062 : : } else {
1063 [ - + ][ - - ]: 3929784562 : Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null())
[ - + ][ - - ]
1064 : 0 : << "TNode constructed from NodeValue with rc == 0";
1065 : : }
1066 : 7902059151 : }
1067 : :
1068 : : // the code for these two following constructors ("conversion/copy
1069 : : // constructors") is identical, but we need both. see comment in the
1070 : : // class.
1071 : :
1072 : : template <bool ref_count>
1073 :13471031348 : NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
1074 [ - + ][ - + ]:13471031348 : Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!";
[ - - ]
1075 :13471031348 : d_nv = e.d_nv;
1076 : 8980077009 : if(ref_count) {
1077 [ - + ][ - + ]: 4490954339 : Assert(d_nv->d_rc > 0) << "Node constructed from TNode with rc == 0";
[ - - ]
1078 : 4490954339 : d_nv->inc();
1079 : : } else {
1080 : : // shouldn't ever fail
1081 [ - + ][ - + ]: 8980077009 : Assert(d_nv->d_rc > 0) << "TNode constructed from Node with rc == 0";
[ - - ]
1082 : : }
1083 :13471031348 : }
1084 : :
1085 : : template <bool ref_count>
1086 :49515049486 : NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
1087 [ - + ][ - + ]:49515049486 : Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!";
[ - - ]
1088 :49515049486 : d_nv = e.d_nv;
1089 :28971585988 : if(ref_count) {
1090 : : // shouldn't ever fail
1091 [ - + ][ - + ]:20543463498 : Assert(d_nv->d_rc > 0) << "Node constructed from Node with rc == 0";
[ - - ]
1092 :20543463498 : d_nv->inc();
1093 : : } else {
1094 [ - + ][ - + ]:28971585988 : Assert(d_nv->d_rc > 0) << "TNode constructed from TNode with rc == 0";
[ - - ]
1095 : : }
1096 :49515049486 : }
1097 : :
1098 : : template <bool ref_count>
1099 :73940858704 : NodeTemplate<ref_count>::~NodeTemplate() {
1100 [ - + ][ - + ]:73940858704 : Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
1101 : : if(ref_count) {
1102 : : // shouldn't ever fail
1103 [ - + ][ - + ]:31248078770 : Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
1104 :31248078770 : d_nv->dec();
1105 : : }
1106 :73940858704 : }
1107 : :
1108 : : template <bool ref_count>
1109 : : void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
1110 : : d_nv = ev;
1111 : : if(ref_count) {
1112 : : d_nv->inc();
1113 : : } else {
1114 : : Assert(d_nv->d_rc > 0) << "TNode assigned to NodeValue with rc == 0";
1115 : : }
1116 : : }
1117 : :
1118 : : template <bool ref_count>
1119 : 5698324978 : NodeTemplate<ref_count>& NodeTemplate<ref_count>::
1120 : : operator=(const NodeTemplate& e) {
1121 [ - + ][ - + ]: 5698324978 : Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
[ - - ]
1122 [ - + ][ - + ]: 5698324978 : Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!";
[ - - ]
1123 [ + + ]: 5698324978 : if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
1124 : : if(ref_count) {
1125 : : // shouldn't ever fail
1126 [ - + ][ - + ]: 2334493657 : Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
[ - - ]
1127 : 2334493657 : d_nv->dec();
1128 : : }
1129 : 4261165012 : d_nv = e.d_nv;
1130 : : if(ref_count) {
1131 : : // shouldn't ever fail
1132 [ - + ][ - + ]: 2334493657 : Assert(d_nv->d_rc > 0) << "Node assigned from Node with rc == 0";
[ - - ]
1133 : 2334493657 : d_nv->inc();
1134 : : } else {
1135 [ - + ][ - + ]: 1926671355 : Assert(d_nv->d_rc > 0) << "TNode assigned from TNode with rc == 0";
[ - - ]
1136 : : }
1137 : : }
1138 : 5698324978 : return *this;
1139 : : }
1140 : :
1141 : : template <bool ref_count>
1142 : 452163050 : NodeTemplate<ref_count>& NodeTemplate<ref_count>::
1143 : : operator=(const NodeTemplate<!ref_count>& e) {
1144 [ - + ][ - + ]: 452163050 : Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
[ - - ]
1145 [ - + ][ - + ]: 452163050 : Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!";
[ - - ]
1146 [ + + ]: 452163050 : if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
1147 : : if(ref_count) {
1148 : : // shouldn't ever fail
1149 [ - + ][ - + ]: 106287000 : Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
[ - - ]
1150 : 106287000 : d_nv->dec();
1151 : : }
1152 : 388149050 : d_nv = e.d_nv;
1153 : : if(ref_count) {
1154 [ - + ][ - + ]: 106287000 : Assert(d_nv->d_rc > 0) << "Node assigned from TNode with rc == 0";
[ - - ]
1155 : 106287000 : d_nv->inc();
1156 : : } else {
1157 : : // shouldn't ever happen
1158 [ - + ][ - + ]: 281862050 : Assert(d_nv->d_rc > 0) << "TNode assigned from Node with rc == 0";
[ - - ]
1159 : : }
1160 : : }
1161 : 452163050 : return *this;
1162 : : }
1163 : :
1164 : : template <bool ref_count>
1165 : : template <bool ref_count2>
1166 : : NodeTemplate<true>
1167 : 146843812 : NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count2>& right) const {
1168 : 146843812 : assertTNodeNotExpired();
1169 : 146843812 : return d_nv->getNodeManager()->mkNode(Kind::EQUAL, *this, right);
1170 : : }
1171 : :
1172 : : template <bool ref_count>
1173 : 200260801 : NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
1174 : 200260801 : assertTNodeNotExpired();
1175 : 200260801 : return d_nv->getNodeManager()->mkNode(Kind::NOT, *this);
1176 : : }
1177 : :
1178 : : template <bool ref_count>
1179 : 16223762 : NodeTemplate<true> NodeTemplate<ref_count>::negate() const {
1180 : 16223762 : assertTNodeNotExpired();
1181 : 16223762 : return (getKind() == Kind::NOT)
1182 : 1446327 : ? NodeTemplate<true>(d_nv->getChild(0))
1183 : 17670082 : : d_nv->getNodeManager()->mkNode(Kind::NOT, *this);
1184 : : }
1185 : :
1186 : : template <bool ref_count>
1187 : : template <bool ref_count2>
1188 : : NodeTemplate<true>
1189 : 214010 : NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count2>& right) const {
1190 : 214010 : assertTNodeNotExpired();
1191 : 214010 : return d_nv->getNodeManager()->mkNode(Kind::AND, *this, right);
1192 : : }
1193 : :
1194 : : template <bool ref_count>
1195 : : template <bool ref_count2>
1196 : : NodeTemplate<true>
1197 : 266191 : NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count2>& right) const {
1198 : 266191 : assertTNodeNotExpired();
1199 : 266191 : return d_nv->getNodeManager()->mkNode(Kind::OR, *this, right);
1200 : : }
1201 : :
1202 : : template <bool ref_count>
1203 : : template <bool ref_count2, bool ref_count3>
1204 : : NodeTemplate<true>
1205 : 541225 : NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart,
1206 : : const NodeTemplate<ref_count3>& elsepart) const {
1207 : 541225 : assertTNodeNotExpired();
1208 : 541225 : return d_nv->getNodeManager()->mkNode(Kind::ITE, *this, thenpart, elsepart);
1209 : : }
1210 : :
1211 : : template <bool ref_count>
1212 : : template <bool ref_count2>
1213 : : NodeTemplate<true>
1214 : 176505 : NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const {
1215 : 176505 : assertTNodeNotExpired();
1216 : 176505 : return d_nv->getNodeManager()->mkNode(Kind::IMPLIES, *this, right);
1217 : : }
1218 : :
1219 : : template <bool ref_count>
1220 : : template <bool ref_count2>
1221 : : NodeTemplate<true>
1222 : 49 : NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count2>& right) const {
1223 : 49 : assertTNodeNotExpired();
1224 : 49 : return d_nv->getNodeManager()->mkNode(Kind::XOR, *this, right);
1225 : : }
1226 : :
1227 : : template <bool ref_count>
1228 : : inline void
1229 : : NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
1230 : : assertTNodeNotExpired();
1231 : : d_nv->printAst(out, indent);
1232 : : }
1233 : :
1234 : : /**
1235 : : * Returns a node representing the operator of this expression.
1236 : : * If this is an APPLY_UF, then the operator will be a functional term.
1237 : : * Otherwise, it will be a node with kind BUILTIN.
1238 : : */
1239 : : template <bool ref_count>
1240 : 357066821 : NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const
1241 : : {
1242 : 357066821 : assertTNodeNotExpired();
1243 : :
1244 : 357066821 : kind::MetaKind mk = getMetaKind();
1245 [ + + ]: 357066821 : if (mk == kind::metakind::OPERATOR)
1246 : : {
1247 : : /* Returns a BUILTIN node. */
1248 : 84281500 : return d_nv->getNodeManager()->operatorOf(getKind());
1249 : : }
1250 [ - + ][ - + ]: 272785821 : Assert(mk == kind::metakind::PARAMETERIZED);
[ - - ]
1251 : : /* The operator is the first child. */
1252 : 272785821 : return Node(d_nv->d_children[0]);
1253 : : }
1254 : :
1255 : : /**
1256 : : * Returns true if the node has an operator (i.e., it's not a variable
1257 : : * or a constant).
1258 : : */
1259 : : template <bool ref_count>
1260 : 294702503 : inline bool NodeTemplate<ref_count>::hasOperator() const {
1261 : 294702503 : assertTNodeNotExpired();
1262 : 294702503 : return NodeManager::hasOperator(getKind());
1263 : : }
1264 : :
1265 : : template <bool ref_count>
1266 : 1271877927 : TypeNode NodeTemplate<ref_count>::getType(bool check) const
1267 : : {
1268 : 1271877927 : assertTNodeNotExpired();
1269 : 2543747854 : TypeNode tn = d_nv->getNodeManager()->getType(*this, check);
1270 [ + + ]: 1271877927 : if (tn.isNull())
1271 : : {
1272 : : // recompute with an error stream and throw a type exception
1273 : 476 : std::stringstream errOutTmp;
1274 : 238 : tn = d_nv->getNodeManager()->getType(*this, check, &errOutTmp);
1275 : 238 : throw TypeCheckingExceptionPrivate(*this, errOutTmp.str());
1276 : : }
1277 : 1271877922 : return tn;
1278 : : }
1279 : :
1280 : : template <bool ref_count>
1281 : 313650714 : TypeNode NodeTemplate<ref_count>::getTypeOrNull(bool check) const
1282 : : {
1283 : 313650714 : assertTNodeNotExpired();
1284 : 313650714 : return d_nv->getNodeManager()->getType(*this, check);
1285 : : }
1286 : :
1287 : : template <bool ref_count>
1288 : : inline Node
1289 : 1185430 : NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
1290 [ + + ]: 1185430 : if (node == *this) {
1291 : 473429 : return replacement;
1292 : : }
1293 : 712000 : std::unordered_map<TNode, TNode> cache;
1294 : 712000 : return substitute(node, replacement, cache);
1295 : : }
1296 : :
1297 : : template <bool ref_count>
1298 : 26436682 : Node NodeTemplate<ref_count>::substitute(
1299 : : TNode node,
1300 : : TNode replacement,
1301 : : std::unordered_map<TNode, TNode>& cache) const
1302 : : {
1303 [ - + ][ - + ]: 26436682 : Assert(node != *this);
[ - - ]
1304 : :
1305 [ + + ][ + + ]: 26436682 : if (getNumChildren() == 0 || node == replacement)
[ + + ]
1306 : : {
1307 : 7762922 : return *this;
1308 : : }
1309 : :
1310 : : // in cache?
1311 : 18673690 : typename std::unordered_map<TNode, TNode>::const_iterator i =
1312 : : cache.find(*this);
1313 [ + + ]: 18673690 : if(i != cache.end()) {
1314 : 6263082 : return (*i).second;
1315 : : }
1316 : :
1317 : : // otherwise compute
1318 : 24821256 : NodeBuilder nb(getNodeManager(), getKind());
1319 [ + + ]: 12410678 : if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1320 : : // push the operator
1321 [ + + ]: 892159 : if(getOperator() == node) {
1322 : 869 : nb << replacement;
1323 : : } else {
1324 : 891290 : nb << getOperator().substitute(node, replacement, cache);
1325 : : }
1326 : : }
1327 [ + + ]: 37740776 : for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1328 : : {
1329 [ + + ]: 25330098 : if (*it == node)
1330 : : {
1331 : 998405 : nb << replacement;
1332 : : }
1333 : : else
1334 : : {
1335 : 24331742 : nb << (*it).substitute(node, replacement, cache);
1336 : : }
1337 : : }
1338 : :
1339 : : // put in cache
1340 : 24821256 : Node n = nb;
1341 : 12410678 : cache[*this] = n;
1342 : 12410678 : return n;
1343 : : }
1344 : :
1345 : : template <bool ref_count>
1346 : : template <class Iterator1, class Iterator2>
1347 : : inline Node
1348 : 22549643 : NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
1349 : : Iterator1 nodesEnd,
1350 : : Iterator2 replacementsBegin,
1351 : : Iterator2 replacementsEnd) const {
1352 : 45099386 : std::unordered_map<TNode, TNode> cache;
1353 : : return substitute(nodesBegin, nodesEnd,
1354 : 45099386 : replacementsBegin, replacementsEnd, cache);
1355 : : }
1356 : :
1357 : : template <bool ref_count>
1358 : : template <class Iterator1, class Iterator2>
1359 : 163158180 : Node NodeTemplate<ref_count>::substitute(
1360 : : Iterator1 nodesBegin,
1361 : : Iterator1 nodesEnd,
1362 : : Iterator2 replacementsBegin,
1363 : : Iterator2 replacementsEnd,
1364 : : std::unordered_map<TNode, TNode>& cache) const
1365 : : {
1366 : : // in cache?
1367 : 163158180 : typename std::unordered_map<TNode, TNode>::const_iterator i =
1368 : : cache.find(*this);
1369 [ + + ]: 163158180 : if(i != cache.end()) {
1370 : 33941870 : return (*i).second;
1371 : : }
1372 : :
1373 : : // otherwise compute
1374 [ - + ][ - + ]: 129216416 : Assert(std::distance(nodesBegin, nodesEnd)
[ - - ]
1375 : : == std::distance(replacementsBegin, replacementsEnd))
1376 : 0 : << "Substitution iterator ranges must be equal size";
1377 : 129216416 : Iterator1 j = std::find(nodesBegin, nodesEnd, TNode(*this));
1378 [ + + ]: 129216416 : if(j != nodesEnd) {
1379 : 8567833 : Iterator2 b = replacementsBegin;
1380 : 8567833 : std::advance(b, std::distance(nodesBegin, j));
1381 : 17135652 : Node n = *b;
1382 : 8567833 : cache[*this] = n;
1383 : 8567833 : return n;
1384 [ + + ]: 120648587 : } else if(getNumChildren() == 0) {
1385 : 51755269 : cache[*this] = *this;
1386 : 51755269 : return *this;
1387 : : } else {
1388 : 137786744 : NodeBuilder nb(getNodeManager(), getKind());
1389 [ + + ]: 68893316 : if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1390 : : // push the operator
1391 : 1676804 : nb << getOperator().substitute(nodesBegin, nodesEnd,
1392 : : replacementsBegin, replacementsEnd,
1393 : : cache);
1394 : : }
1395 [ + + ]: 207824916 : for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1396 : : {
1397 : 138931728 : nb << (*it).substitute(
1398 : : nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache);
1399 : : }
1400 : 137786744 : Node n = nb;
1401 : 68893316 : cache[*this] = n;
1402 : 68893316 : return n;
1403 : : }
1404 : : }
1405 : :
1406 : : template <bool ref_count>
1407 : : template <class Iterator>
1408 : : inline Node
1409 : 364 : NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
1410 : : Iterator substitutionsEnd) const {
1411 : 728 : std::unordered_map<TNode, TNode> cache;
1412 : 728 : return substitute(substitutionsBegin, substitutionsEnd, cache);
1413 : : }
1414 : :
1415 : : template <bool ref_count>
1416 : 0 : inline Node NodeTemplate<ref_count>::substitute(
1417 : : std::unordered_map<TNode, TNode>& cache) const
1418 : : {
1419 : : // Since no substitution is given (other than what may already be in the
1420 : : // cache), we pass dummy iterators to conform to the main substitute method,
1421 : : // giving the same value to substitutionsBegin and substitutionsEnd.
1422 : 0 : return substitute(cache.cend(), cache.cend(), cache);
1423 : : }
1424 : :
1425 : : template <bool ref_count>
1426 : : template <class Iterator>
1427 : 1096 : Node NodeTemplate<ref_count>::substitute(
1428 : : Iterator substitutionsBegin,
1429 : : Iterator substitutionsEnd,
1430 : : std::unordered_map<TNode, TNode>& cache) const
1431 : : {
1432 : : // in cache?
1433 : 1096 : typename std::unordered_map<TNode, TNode>::const_iterator i =
1434 : : cache.find(*this);
1435 [ + + ]: 1096 : if(i != cache.end()) {
1436 : 18 : return (*i).second;
1437 : : }
1438 : :
1439 : : // otherwise compute
1440 : 1078 : Iterator j = find_if(
1441 : : substitutionsBegin,
1442 : : substitutionsEnd,
1443 : 25266 : [this](const auto& subst){ return subst.first == *this; });
1444 [ + + ]: 1078 : if(j != substitutionsEnd) {
1445 : 1076 : Node n = (*j).second;
1446 : 538 : cache[*this] = n;
1447 : 538 : return n;
1448 [ + + ]: 540 : } else if(getNumChildren() == 0) {
1449 : 304 : cache[*this] = *this;
1450 : 304 : return *this;
1451 : : } else {
1452 : 472 : NodeBuilder nb(getNodeManager(), getKind());
1453 [ + + ]: 236 : if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1454 : : // push the operator
1455 : 206 : nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache);
1456 : : }
1457 [ + + ]: 762 : for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1458 : : {
1459 : 526 : nb << (*it).substitute(substitutionsBegin, substitutionsEnd, cache);
1460 : : }
1461 : 472 : Node n = nb;
1462 : 236 : cache[*this] = n;
1463 : 236 : return n;
1464 : : }
1465 : : }
1466 : :
1467 : : } // namespace cvc5::internal
1468 : :
1469 : : #endif /* CVC5__NODE_H */
|
