GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node.h Lines: 296 360 82.2 %
Date: 2021-03-23 Branches: 755 3434 22.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Dejan Jovanovic, Aina Niemetz
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Reference-counted encapsulation of a pointer to node information
13
 **
14
 ** Reference-counted encapsulation of a pointer to node information.
15
 **/
16
17
#include "cvc4_private.h"
18
19
// circular dependency
20
#include "expr/node_value.h"
21
22
#ifndef CVC4__NODE_H
23
#define CVC4__NODE_H
24
25
#include <iostream>
26
#include <map>
27
#include <string>
28
#include <unordered_map>
29
#include <unordered_set>
30
#include <utility>
31
#include <vector>
32
33
#include "base/check.h"
34
#include "base/exception.h"
35
#include "base/output.h"
36
#include "expr/expr_iomanip.h"
37
#include "expr/kind.h"
38
#include "expr/metakind.h"
39
#include "options/language.h"
40
#include "options/set_language.h"
41
#include "util/hash.h"
42
#include "util/utility.h"
43
44
namespace CVC4 {
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 CVC4
129
 * Developer's Guide:
130
 * http://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#Dealing_with_expressions_.28Nodes_and_TNodes.29
131
 */
132
typedef NodeTemplate<false> TNode;
133
134
namespace expr {
135
136
class NodeValue;
137
138
  namespace attr {
139
    class AttributeManager;
140
    struct SmtAttributes;
141
  }/* CVC4::expr::attr namespace */
142
143
  class ExprSetDepth;
144
}/* CVC4::expr namespace */
145
146
namespace kind {
147
  namespace metakind {
148
    struct NodeValueConstPrinter;
149
  }/* CVC4::kind::metakind namespace */
150
}/* CVC4::kind namespace */
151
152
// for hash_maps, hash_sets..
153
struct NodeHashFunction {
154
  inline size_t operator()(Node node) const;
155
};/* struct NodeHashFunction */
156
struct TNodeHashFunction {
157
  inline size_t operator()(TNode node) const;
158
};/* struct TNodeHashFunction */
159
160
/**
161
 * Encapsulation of an NodeValue pointer.  The reference count is
162
 * maintained in the NodeValue if ref_count is true.
163
 * @param ref_count if true reference are counted in the NodeValue
164
 */
165
template <bool ref_count>
166
class NodeTemplate {
167
  /**
168
   * The NodeValue has access to the private constructors, so that the
169
   * iterators can can create new nodes.
170
   */
171
  friend class expr::NodeValue;
172
173
  /** A convenient null-valued encapsulated pointer */
174
  static NodeTemplate s_null;
175
176
  /** The referenced NodeValue */
177
  expr::NodeValue* d_nv;
178
179
  /**
180
   * This constructor is reserved for use by the NodeTemplate package; one
181
   * must construct an NodeTemplate using one of the build mechanisms of the
182
   * NodeTemplate package.
183
   *
184
   * FIXME: there's a type-system escape here to cast away the const,
185
   * since the refcount needs to be updated.  But conceptually Nodes
186
   * don't change their arguments, and it's nice to have
187
   * const_iterators over them.
188
   *
189
   * This really does needs to be explicit to avoid hard to track errors with
190
   * Nodes implicitly wrapping NodeValues
191
   */
192
  explicit NodeTemplate(const expr::NodeValue*);
193
194
  friend class NodeTemplate<true>;
195
  friend class NodeTemplate<false>;
196
  friend class TypeNode;
197
  friend class NodeManager;
198
199
  template <unsigned nchild_thresh>
200
  friend class NodeBuilder;
201
202
  friend class ::CVC4::expr::attr::AttributeManager;
203
  friend struct ::CVC4::expr::attr::SmtAttributes;
204
205
  friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
206
207
  /**
208
   * Assigns the expression value and does reference counting. No assumptions
209
   * are made on the expression, and should only be used if we know what we
210
   * are doing.
211
   *
212
   * @param ev the expression value to assign
213
   */
214
  void assignNodeValue(expr::NodeValue* ev);
215
216
  // May throw an AssertionException if the Node is not live, i.e. the ref count
217
  // is not positive.
218
26901449144
  inline void assertTNodeNotExpired() const
219
  {
220
    if(!ref_count) {
221
11850388926
      Assert(d_nv->d_rc > 0) << "TNode pointing to an expired NodeValue";
222
    }
223
26901449144
  }
224
225
public:
226
227
  /**
228
   * Cache-aware, recursive version of substitute() used by the public
229
   * member function with a similar signature.
230
   */
231
  Node substitute(TNode node, TNode replacement,
232
                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
233
234
  /**
235
   * Cache-aware, recursive version of substitute() used by the public
236
   * member function with a similar signature.
237
   */
238
  template <class Iterator1, class Iterator2>
239
  Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd,
240
                  Iterator2 replacementsBegin, Iterator2 replacementsEnd,
241
                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
242
243
  /**
244
   * Cache-aware, recursive version of substitute() used by the public
245
   * member function with a similar signature.
246
   */
247
  template <class Iterator>
248
  Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd,
249
                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
250
251
  /** Default constructor, makes a null expression. */
252
948990493
  NodeTemplate() : d_nv(&expr::NodeValue::null()) { }
253
254
  /**
255
   * Conversion between nodes that are reference-counted and those that are
256
   * not.
257
   * @param node the node to make copy of
258
   */
259
  NodeTemplate(const NodeTemplate<!ref_count>& node);
260
261
  /**
262
   * Copy constructor.  Note that GCC does NOT recognize an instantiation of
263
   * the above template as a copy constructor and problems ensue.  So we
264
   * provide an explicit one here.
265
   * @param node the node to make copy of
266
   */
267
  NodeTemplate(const NodeTemplate& node);
268
269
  /**
270
   * Assignment operator for nodes, copies the relevant information from node
271
   * to this node.
272
   * @param node the node to copy
273
   * @return reference to this node
274
   */
275
  NodeTemplate& operator=(const NodeTemplate& node);
276
277
  /**
278
   * Assignment operator for nodes, copies the relevant information from node
279
   * to this node.
280
   * @param node the node to copy
281
   * @return reference to this node
282
   */
283
  NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
284
285
  /**
286
   * Destructor. If ref_count is true it will decrement the reference count
287
   * and, if zero, collect the NodeValue.
288
   */
289
  ~NodeTemplate();
290
291
  /**
292
   * Return the null node.
293
   * @return the null node
294
   */
295
427766975
  static NodeTemplate null() {
296
427766975
    return s_null;
297
  }
298
299
  /**
300
   * Returns true if this expression is a null expression.
301
   * @return true if null
302
   */
303
3703011344
  bool isNull() const {
304
3703011344
    assertTNodeNotExpired();
305
3703011344
    return d_nv == &expr::NodeValue::null();
306
  }
307
308
  /**
309
   * Structural comparison operator for expressions.
310
   * @param node the node to compare to
311
   * @return true if expressions are equal, false otherwise
312
   */
313
  template <bool ref_count_1>
314
3531613859
  bool operator==(const NodeTemplate<ref_count_1>& node) const {
315
3531613859
    assertTNodeNotExpired();
316
3531613859
    node.assertTNodeNotExpired();
317
3531613859
    return d_nv == node.d_nv;
318
  }
319
320
  /**
321
   * Structural comparison operator for expressions.
322
   * @param node the node to compare to
323
   * @return false if expressions are equal, true otherwise
324
   */
325
  template <bool ref_count_1>
326
163454381
  bool operator!=(const NodeTemplate<ref_count_1>& node) const {
327
163454381
    assertTNodeNotExpired();
328
163454381
    node.assertTNodeNotExpired();
329
163454381
    return d_nv != node.d_nv;
330
  }
331
332
  /**
333
   * We compare by expression ids so, keeping things deterministic and having
334
   * that subexpressions have to be smaller than the enclosing expressions.
335
   * @param node the node to compare to
336
   * @return true if this expression is smaller
337
   */
338
  template <bool ref_count_1>
339
1290116277
  inline bool operator<(const NodeTemplate<ref_count_1>& node) const {
340
1290116277
    assertTNodeNotExpired();
341
1290116277
    node.assertTNodeNotExpired();
342
1290116277
    return d_nv->d_id < node.d_nv->d_id;
343
  }
344
345
  /**
346
   * We compare by expression ids so, keeping things deterministic and having
347
   * that subexpressions have to be smaller than the enclosing expressions.
348
   * @param node the node to compare to
349
   * @return true if this expression is greater
350
   */
351
  template <bool ref_count_1>
352
803131
  inline bool operator>(const NodeTemplate<ref_count_1>& node) const {
353
803131
    assertTNodeNotExpired();
354
803131
    node.assertTNodeNotExpired();
355
803131
    return d_nv->d_id > node.d_nv->d_id;
356
  }
357
358
  /**
359
   * We compare by expression ids so, keeping things deterministic and having
360
   * that subexpressions have to be smaller than the enclosing expressions.
361
   * @param node the node to compare to
362
   * @return true if this expression is smaller than or equal to
363
   */
364
  template <bool ref_count_1>
365
86
  inline bool operator<=(const NodeTemplate<ref_count_1>& node) const {
366
86
    assertTNodeNotExpired();
367
86
    node.assertTNodeNotExpired();
368
86
    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 greater than or equal to
376
   */
377
  template <bool ref_count_1>
378
44670
  inline bool operator>=(const NodeTemplate<ref_count_1>& node) const {
379
44670
    assertTNodeNotExpired();
380
44670
    node.assertTNodeNotExpired();
381
44670
    return d_nv->d_id >= node.d_nv->d_id;
382
  }
383
384
  /**
385
   * Returns the i-th child of this node.
386
   * @param i the index of the child
387
   * @return the node representing the i-th child
388
   */
389
1084885090
  NodeTemplate operator[](int i) const {
390
1084885090
    assertTNodeNotExpired();
391
1084885090
    return NodeTemplate(d_nv->getChild(i));
392
  }
393
394
  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
395
   *
396
   * It has been decided for now to hold off on implementations of
397
   * these functions, as they may only be needed in CNF conversion,
398
   * where it's pointless to do a lazy isAtomic determination by
399
   * searching through the DAG, and storing it, since the result will
400
   * only be used once.  For more details see the 4/27/2010 CVC4
401
   * developer's meeting notes at:
402
   *
403
   * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
404
   */
405
  // bool containsDecision(); // is "atomic"
406
  // bool properlyContainsDecision(); // maybe not atomic but all children are
407
408
  /**
409
   * Returns true if this node represents a constant
410
   * @return true if const
411
   */
412
  bool isConst() const;
413
414
  /**
415
   * Returns true if this node represents a variable
416
   * @return true if variable
417
   */
418
338322005
  inline bool isVar() const {
419
338322005
    assertTNodeNotExpired();
420
338322005
    return getMetaKind() == kind::metakind::VARIABLE;
421
  }
422
423
  /**
424
   * Returns true if this node represents a nullary operator
425
   */
426
29108
  inline bool isNullaryOp() const {
427
29108
    assertTNodeNotExpired();
428
29108
    return getMetaKind() == kind::metakind::NULLARY_OPERATOR;
429
  }
430
431
  /**
432
   * Returns true if this node represents a closure, that is an expression
433
   * that binds variables.
434
   */
435
42384007
  inline bool isClosure() const {
436
42384007
    assertTNodeNotExpired();
437
84760089
    return getKind() == kind::LAMBDA || getKind() == kind::FORALL
438
41998222
           || getKind() == kind::EXISTS || getKind() == kind::WITNESS
439
41996217
           || getKind() == kind::COMPREHENSION
440
84379481
           || getKind() == kind::MATCH_BIND_CASE;
441
  }
442
443
  /**
444
   * Returns the unique id of this node
445
   * @return the ud
446
   */
447
2349849293
  uint64_t getId() const
448
  {
449
2349849293
    assertTNodeNotExpired();
450
2349849293
    return d_nv->getId();
451
  }
452
453
  /**
454
   * Returns a node representing the operator of this expression.
455
   * If this is an APPLY_UF, then the operator will be a functional term.
456
   * Otherwise, it will be a node with kind BUILTIN.
457
   */
458
  NodeTemplate<true> getOperator() const;
459
460
  /**
461
   * Returns true if the node has an operator (i.e., it's not a
462
   * variable or a constant).
463
   */
464
  inline bool hasOperator() const;
465
466
  /**
467
   * Get the type for the node and optionally do type checking.
468
   *
469
   * Initial type computation will be near-constant time if
470
   * type checking is not requested. Results are memoized, so that
471
   * subsequent calls to getType() without type checking will be
472
   * constant time.
473
   *
474
   * Initial type checking is linear in the size of the expression.
475
   * Again, the results are memoized, so that subsequent calls to
476
   * getType(), with or without type checking, will be constant
477
   * time.
478
   *
479
   * NOTE: A TypeCheckingException can be thrown even when type
480
   * checking is not requested. getType() will always return a
481
   * valid and correct type and, thus, an exception will be thrown
482
   * when no valid or correct type can be computed (e.g., if the
483
   * arguments to a bit-vector operation aren't bit-vectors). When
484
   * type checking is not requested, getType() will do the minimum
485
   * amount of checking required to return a valid result.
486
   *
487
   * @param check whether we should check the type as we compute it
488
   * (default: false)
489
   */
490
  TypeNode getType(bool check = false) const;
491
492
  /**
493
   * Substitution of Nodes.
494
   */
495
  Node substitute(TNode node, TNode replacement) const;
496
497
  /**
498
   * Simultaneous substitution of Nodes.  Elements in the Iterator1
499
   * range will be replaced by their corresponding element in the
500
   * Iterator2 range.  Both ranges should have the same size.
501
   */
502
  template <class Iterator1, class Iterator2>
503
  Node substitute(Iterator1 nodesBegin,
504
                  Iterator1 nodesEnd,
505
                  Iterator2 replacementsBegin,
506
                  Iterator2 replacementsEnd) const;
507
508
  /**
509
   * Simultaneous substitution of Nodes.  Iterators should be over
510
   * pairs (x,y) for the rewrites [x->y].
511
   */
512
  template <class Iterator>
513
  Node substitute(Iterator substitutionsBegin,
514
                  Iterator substitutionsEnd) const;
515
516
  /**
517
   * Returns the kind of this node.
518
   * @return the kind
519
   */
520
5359286058
  inline Kind getKind() const {
521
5359286058
    assertTNodeNotExpired();
522
5359286058
    return Kind(d_nv->d_kind);
523
  }
524
525
  /**
526
   * Returns the metakind of this node.
527
   * @return the metakind
528
   */
529
802921527
  inline kind::MetaKind getMetaKind() const {
530
802921527
    assertTNodeNotExpired();
531
802921527
    return kind::metaKindOf(getKind());
532
  }
533
534
  /**
535
   * Returns the number of children this node has.
536
   * @return the number of children
537
   */
538
  inline size_t getNumChildren() const;
539
540
  /**
541
   * If this is a CONST_* Node, extract the constant from it.
542
   */
543
  template <class T>
544
  inline const T& getConst() const;
545
546
  /**
547
   * Returns the reference count of this node.
548
   * @return the refcount
549
   */
550
  unsigned getRefCount() const {
551
    return d_nv->getRefCount();
552
  }
553
554
  /**
555
   * Returns the value of the given attribute that this has been attached.
556
   * @param attKind the kind of the attribute
557
   * @return the value of the attribute
558
   */
559
  template <class AttrKind>
560
  inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
561
562
  // Note that there are two, distinct hasAttribute() declarations for
563
  // a reason (rather than using a pointer-valued argument with a
564
  // default value): they permit more optimized code in the underlying
565
  // hasAttribute() implementations.
566
567
  /**
568
   * Returns true if this node has been associated an attribute of given kind.
569
   * Additionaly, if a pointer to the value_kind is give, and the attribute
570
   * value has been set for this node, it will be returned.
571
   * @param attKind the kind of the attribute
572
   * @return true if this node has the requested attribute
573
   */
574
  template <class AttrKind>
575
  inline bool hasAttribute(const AttrKind& attKind) const;
576
577
  /**
578
   * Returns true if this node has been associated an attribute of given kind.
579
   * Additionaly, if a pointer to the value_kind is give, and the attribute
580
   * value has been set for this node, it will be returned.
581
   * @param attKind the kind of the attribute
582
   * @param value where to store the value if it exists
583
   * @return true if this node has the requested attribute
584
   */
585
  template <class AttrKind>
586
  inline bool getAttribute(const AttrKind& attKind,
587
                           typename AttrKind::value_type& value) const;
588
589
  /**
590
   * Sets the given attribute of this node to the given value.
591
   * @param attKind the kind of the atribute
592
   * @param value the value to set the attribute to
593
   */
594
  template <class AttrKind>
595
  inline void setAttribute(const AttrKind& attKind,
596
                           const typename AttrKind::value_type& value);
597
598
  /** Iterator allowing for scanning through the children. */
599
  typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > iterator;
600
  /** Constant iterator allowing for scanning through the children. */
601
  typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > const_iterator;
602
603
18
  class kinded_iterator {
604
    friend class NodeTemplate<ref_count>;
605
606
    NodeTemplate<ref_count> d_node;
607
    ssize_t d_child;
608
609
8
    kinded_iterator(TNode node, ssize_t child) :
610
      d_node(node),
611
8
      d_child(child) {
612
8
    }
613
614
    // These are factories to serve as clients to Node::begin<K>() and
615
    // Node::end<K>().
616
4
    static kinded_iterator begin(TNode n, Kind k) {
617
4
      return kinded_iterator(n, n.getKind() == k ? 0 : -2);
618
    }
619
4
    static kinded_iterator end(TNode n, Kind k) {
620
4
      return kinded_iterator(n, n.getKind() == k ? n.getNumChildren() : -1);
621
    }
622
623
  public:
624
    typedef NodeTemplate<ref_count> value_type;
625
    typedef std::ptrdiff_t difference_type;
626
    typedef NodeTemplate<ref_count>* pointer;
627
    typedef NodeTemplate<ref_count>& reference;
628
629
    kinded_iterator() :
630
      d_node(NodeTemplate<ref_count>::null()),
631
      d_child(-2) {
632
    }
633
634
8
    kinded_iterator(const kinded_iterator& i) :
635
      d_node(i.d_node),
636
8
      d_child(i.d_child) {
637
8
    }
638
639
8
    NodeTemplate<ref_count> operator*() {
640
8
      return d_child < 0 ? d_node : d_node[d_child];
641
    }
642
643
4
    bool operator==(const kinded_iterator& i) {
644
4
      return d_node == i.d_node && d_child == i.d_child;
645
    }
646
647
    bool operator!=(const kinded_iterator& i) {
648
      return !(*this == i);
649
    }
650
651
8
    kinded_iterator& operator++() {
652
8
      if(d_child != -1) {
653
8
        ++d_child;
654
      }
655
8
      return *this;
656
    }
657
658
8
    kinded_iterator operator++(int) {
659
8
      kinded_iterator i = *this;
660
8
      ++*this;
661
8
      return i;
662
    }
663
  };/* class NodeTemplate<ref_count>::kinded_iterator */
664
665
  typedef kinded_iterator const_kinded_iterator;
666
667
  /**
668
   * Returns the iterator pointing to the first child.
669
   * @return the iterator
670
   */
671
118445781
  inline iterator begin() {
672
118445781
    assertTNodeNotExpired();
673
118445781
    return d_nv->begin< NodeTemplate<ref_count> >();
674
  }
675
676
  /**
677
   * Returns the iterator pointing to the end of the children (one beyond the
678
   * last one).
679
   * @return the end of the children iterator.
680
   */
681
592719335
  inline iterator end() {
682
592719335
    assertTNodeNotExpired();
683
592719335
    return d_nv->end< NodeTemplate<ref_count> >();
684
  }
685
686
  /**
687
   * Returns the iterator pointing to the first child, if the node's
688
   * kind is the same as the parameter, otherwise returns the iterator
689
   * pointing to the node itself.  This is useful if you want to
690
   * pretend to iterate over a "unary" PLUS, for instance, since unary
691
   * PLUSes don't exist---begin(PLUS) will give an iterator over the
692
   * children if the node's a PLUS node, otherwise give an iterator
693
   * over the node itself, as if it were a unary PLUS.
694
   * @param kind the kind to match
695
   * @return the kinded_iterator iterating over this Node (if its kind
696
   * is not the passed kind) or its children
697
   */
698
4
  inline kinded_iterator begin(Kind kind) {
699
4
    assertTNodeNotExpired();
700
4
    return kinded_iterator::begin(*this, kind);
701
  }
702
703
  /**
704
   * Returns the iterator pointing to the end of the children (one
705
   * beyond the last one), if the node's kind is the same as the
706
   * parameter, otherwise returns the iterator pointing to the
707
   * one-of-the-node-itself.  This is useful if you want to pretend to
708
   * iterate over a "unary" PLUS, for instance, since unary PLUSes
709
   * don't exist---begin(PLUS) will give an iterator over the children
710
   * if the node's a PLUS node, otherwise give an iterator over the
711
   * node itself, as if it were a unary PLUS.
712
   * @param kind the kind to match
713
   * @return the kinded_iterator pointing off-the-end of this Node (if
714
   * its kind is not the passed kind) or off-the-end of its children
715
   */
716
4
  inline kinded_iterator end(Kind kind) {
717
4
    assertTNodeNotExpired();
718
4
    return kinded_iterator::end(*this, kind);
719
  }
720
721
  /**
722
   * Returns the const_iterator pointing to the first child.
723
   * @return the const_iterator
724
   */
725
106415647
  inline const_iterator begin() const {
726
106415647
    assertTNodeNotExpired();
727
106415647
    return d_nv->begin< NodeTemplate<ref_count> >();
728
  }
729
730
  /**
731
   * Returns the const_iterator pointing to the end of the children (one
732
   * beyond the last one.
733
   * @return the end of the children const_iterator.
734
   */
735
97361112
  inline const_iterator end() const {
736
97361112
    assertTNodeNotExpired();
737
97361112
    return d_nv->end< NodeTemplate<ref_count> >();
738
  }
739
740
  /**
741
   * Returns the iterator pointing to the first child, if the node's
742
   * kind is the same as the parameter, otherwise returns the iterator
743
   * pointing to the node itself.  This is useful if you want to
744
   * pretend to iterate over a "unary" PLUS, for instance, since unary
745
   * PLUSes don't exist---begin(PLUS) will give an iterator over the
746
   * children if the node's a PLUS node, otherwise give an iterator
747
   * over the node itself, as if it were a unary PLUS.
748
   * @param kind the kind to match
749
   * @return the kinded_iterator iterating over this Node (if its kind
750
   * is not the passed kind) or its children
751
   */
752
  inline const_kinded_iterator begin(Kind kind) const {
753
    assertTNodeNotExpired();
754
    return const_kinded_iterator::begin(*this, kind);
755
  }
756
757
  /**
758
   * Returns the iterator pointing to the end of the children (one
759
   * beyond the last one), if the node's kind is the same as the
760
   * parameter, otherwise returns the iterator pointing to the
761
   * one-of-the-node-itself.  This is useful if you want to pretend to
762
   * iterate over a "unary" PLUS, for instance, since unary PLUSes
763
   * don't exist---begin(PLUS) will give an iterator over the children
764
   * if the node's a PLUS node, otherwise give an iterator over the
765
   * node itself, as if it were a unary PLUS.
766
   * @param kind the kind to match
767
   * @return the kinded_iterator pointing off-the-end of this Node (if
768
   * its kind is not the passed kind) or off-the-end of its children
769
   */
770
  inline const_kinded_iterator end(Kind kind) const {
771
    assertTNodeNotExpired();
772
    return const_kinded_iterator::end(*this, kind);
773
  }
774
775
  /**
776
   * Converts this node into a string representation.
777
   * @return the string representation of this node.
778
   */
779
567044
  inline std::string toString() const {
780
567044
    assertTNodeNotExpired();
781
567044
    return d_nv->toString();
782
  }
783
784
  /**
785
   * Converts this node into a string representation and sends it to the
786
   * given stream
787
   *
788
   * @param out the stream to serialize this node to
789
   * @param toDepth the depth to which to print this expression, or -1 to
790
   * print it fully
791
   * @param language the language in which to output
792
   */
793
69125
  inline void toStream(
794
      std::ostream& out,
795
      int toDepth = -1,
796
      size_t dagThreshold = 1,
797
      OutputLanguage language = language::output::LANG_AUTO) const
798
  {
799
69125
    assertTNodeNotExpired();
800
69125
    d_nv->toStream(out, toDepth, dagThreshold, language);
801
69111
  }
802
803
  /**
804
   * IOStream manipulator to set the maximum depth of Nodes when
805
   * pretty-printing.  -1 means print to any depth.  E.g.:
806
   *
807
   *   // let a, b, c, and d be VARIABLEs
808
   *   Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
809
   *   out << setdepth(3) << n;
810
   *
811
   * gives "(OR a b (AND c (NOT d)))", but
812
   *
813
   *   out << setdepth(1) << [same node as above]
814
   *
815
   * gives "(OR a b (...))"
816
   */
817
  typedef expr::ExprSetDepth setdepth;
818
819
  /**
820
   * IOStream manipulator to print expressions as DAGs (or not).
821
   */
822
  typedef expr::ExprDag dag;
823
824
  /**
825
   * IOStream manipulator to set the output language for Exprs.
826
   */
827
  typedef language::SetLanguage setlanguage;
828
829
  /**
830
   * Very basic pretty printer for Node.
831
   * @param out output stream to print to.
832
   * @param indent number of spaces to indent the formula by.
833
   */
834
  inline void printAst(std::ostream& out, int indent = 0) const;
835
836
  template <bool ref_count2>
837
  NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const;
838
839
  NodeTemplate<true> notNode() const;
840
  NodeTemplate<true> negate() const;
841
  template <bool ref_count2>
842
  NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const;
843
  template <bool ref_count2>
844
  NodeTemplate<true> orNode(const NodeTemplate<ref_count2>& right) const;
845
  template <bool ref_count2, bool ref_count3>
846
  NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
847
                             const NodeTemplate<ref_count3>& elsepart) const;
848
  template <bool ref_count2>
849
  NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
850
  template <bool ref_count2>
851
  NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
852
853
};/* class NodeTemplate<ref_count> */
854
855
/**
856
 * Serializes a given node to the given stream.
857
 *
858
 * @param out the output stream to use
859
 * @param n the node to output to the stream
860
 * @return the stream
861
 */
862
58719
inline std::ostream& operator<<(std::ostream& out, TNode n) {
863
117438
  n.toStream(out,
864
58719
             Node::setdepth::getDepth(out),
865
             Node::dag::getDag(out),
866
             Node::setlanguage::getLanguage(out));
867
58705
  return out;
868
}
869
870
/**
871
 * Serialize a vector of nodes to given stream.
872
 *
873
 * @param out the output stream to use
874
 * @param container the vector of nodes to output to the stream
875
 * @return the stream
876
 */
877
template <bool RC>
878
std::ostream& operator<<(std::ostream& out,
879
                         const std::vector<NodeTemplate<RC>>& container)
880
{
881
  container_to_stream(out, container);
882
  return out;
883
}
884
885
/**
886
 * Serialize a set of nodes to the given stream.
887
 *
888
 * @param out the output stream to use
889
 * @param container the set of nodes to output to the stream
890
 * @return the stream
891
 */
892
template <bool RC>
893
std::ostream& operator<<(std::ostream& out,
894
                         const std::set<NodeTemplate<RC>>& container)
895
{
896
  container_to_stream(out, container);
897
  return out;
898
}
899
900
/**
901
 * Serialize an unordered_set of nodes to the given stream.
902
 *
903
 * @param out the output stream to use
904
 * @param container the unordered_set of nodes to output to the stream
905
 * @return the stream
906
 */
907
template <bool RC, typename hash_function>
908
std::ostream& operator<<(
909
    std::ostream& out,
910
    const std::unordered_set<NodeTemplate<RC>, hash_function>& container)
911
{
912
  container_to_stream(out, container);
913
  return out;
914
}
915
916
/**
917
 * Serialize a map of nodes to the given stream.
918
 *
919
 * @param out the output stream to use
920
 * @param container the map of nodes to output to the stream
921
 * @return the stream
922
 */
923
template <bool RC, typename V>
924
std::ostream& operator<<(
925
    std::ostream& out,
926
    const std::map<NodeTemplate<RC>, V>& container)
927
{
928
  container_to_stream(out, container);
929
  return out;
930
}
931
932
/**
933
 * Serialize an unordered_map of nodes to the given stream.
934
 *
935
 * @param out the output stream to use
936
 * @param container the unordered_map of nodes to output to the stream
937
 * @return the stream
938
 */
939
template <bool RC, typename V, typename HF>
940
std::ostream& operator<<(
941
    std::ostream& out,
942
    const std::unordered_map<NodeTemplate<RC>, V, HF>& container)
943
{
944
  container_to_stream(out, container);
945
  return out;
946
}
947
948
}/* CVC4 namespace */
949
950
//#include "expr/attribute.h"
951
#include "expr/node_manager.h"
952
953
namespace CVC4 {
954
955
983175027
inline size_t NodeHashFunction::operator()(Node node) const {
956
983175027
  return node.getId();
957
}
958
1351258865
inline size_t TNodeHashFunction::operator()(TNode node) const {
959
1351258865
  return node.getId();
960
}
961
962
using TNodePairHashFunction =
963
    PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction>;
964
965
template <bool ref_count>
966
748573660
inline size_t NodeTemplate<ref_count>::getNumChildren() const {
967
748573660
  assertTNodeNotExpired();
968
748573660
  return d_nv->getNumChildren();
969
}
970
971
template <bool ref_count>
972
template <class T>
973
476743042
inline const T& NodeTemplate<ref_count>::getConst() const {
974
476743042
  assertTNodeNotExpired();
975
476743042
  return d_nv->getConst<T>();
976
}
977
978
template <bool ref_count>
979
template <class AttrKind>
980
139758918
inline typename AttrKind::value_type NodeTemplate<ref_count>::
981
getAttribute(const AttrKind&) const {
982
139758918
  Assert(NodeManager::currentNM() != NULL)
983
      << "There is no current CVC4::NodeManager associated to this thread.\n"
984
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
985
986
139758918
  assertTNodeNotExpired();
987
988
139758918
  return NodeManager::currentNM()->getAttribute(*this, AttrKind());
989
}
990
991
template <bool ref_count>
992
template <class AttrKind>
993
163731885
inline bool NodeTemplate<ref_count>::
994
hasAttribute(const AttrKind&) const {
995
163731885
  Assert(NodeManager::currentNM() != NULL)
996
      << "There is no current CVC4::NodeManager associated to this thread.\n"
997
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
998
999
163731885
  assertTNodeNotExpired();
1000
1001
163731885
  return NodeManager::currentNM()->hasAttribute(*this, AttrKind());
1002
}
1003
1004
template <bool ref_count>
1005
template <class AttrKind>
1006
83179196
inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
1007
                                                  typename AttrKind::value_type& ret) const {
1008
83179196
  Assert(NodeManager::currentNM() != NULL)
1009
      << "There is no current CVC4::NodeManager associated to this thread.\n"
1010
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
1011
1012
83179196
  assertTNodeNotExpired();
1013
1014
83179196
  return NodeManager::currentNM()->getAttribute(*this, AttrKind(), ret);
1015
}
1016
1017
template <bool ref_count>
1018
template <class AttrKind>
1019
39679439
inline void NodeTemplate<ref_count>::
1020
setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
1021
39679439
  Assert(NodeManager::currentNM() != NULL)
1022
      << "There is no current CVC4::NodeManager associated to this thread.\n"
1023
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
1024
1025
39679439
  assertTNodeNotExpired();
1026
1027
39679439
  NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
1028
39679439
}
1029
1030
template <bool ref_count>
1031
3478424
NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::null());
1032
1033
// FIXME: escape from type system convenient but is there a better
1034
// way?  Nodes conceptually don't change their expr values but of
1035
// course they do modify the refcount.  But it's nice to be able to
1036
// support node_iterators over const NodeValue*.  So.... hm.
1037
template <bool ref_count>
1038
2265172717
NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
1039
2265172717
  d_nv(const_cast<expr::NodeValue*> (ev)) {
1040
2265172717
  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
1041
  if(ref_count) {
1042
1369391624
    d_nv->inc();
1043
  } else {
1044
895781093
    Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null())
1045
        << "TNode constructed from NodeValue with rc == 0";
1046
  }
1047
2265172717
}
1048
1049
// the code for these two following constructors ("conversion/copy
1050
// constructors") is identical, but we need both.  see comment in the
1051
// class.
1052
1053
template <bool ref_count>
1054
4868053744
NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
1055
4868053744
  Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!";
1056
4868053744
  d_nv = e.d_nv;
1057
  if(ref_count) {
1058
1659822749
    Assert(d_nv->d_rc > 0) << "Node constructed from TNode with rc == 0";
1059
1659822749
    d_nv->inc();
1060
  } else {
1061
    // shouldn't ever fail
1062
3208230995
    Assert(d_nv->d_rc > 0) << "TNode constructed from Node with rc == 0";
1063
  }
1064
4868053744
}
1065
1066
template <bool ref_count>
1067
19900108386
NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
1068
19900108386
  Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!";
1069
19900108386
  d_nv = e.d_nv;
1070
  if(ref_count) {
1071
    // shouldn't ever fail
1072
10421473585
    Assert(d_nv->d_rc > 0) << "Node constructed from Node with rc == 0";
1073
10421473585
    d_nv->inc();
1074
  } else {
1075
9478634801
    Assert(d_nv->d_rc > 0) << "TNode constructed from TNode with rc == 0";
1076
  }
1077
19900108386
}
1078
1079
template <bool ref_count>
1080
27982315371
NodeTemplate<ref_count>::~NodeTemplate() {
1081
27982315371
  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
1082
  if(ref_count) {
1083
    // shouldn't ever fail
1084
14233316883
    Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
1085
14233316883
    d_nv->dec();
1086
  }
1087
27982315371
}
1088
1089
template <bool ref_count>
1090
void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
1091
  d_nv = ev;
1092
  if(ref_count) {
1093
    d_nv->inc();
1094
  } else {
1095
    Assert(d_nv->d_rc > 0) << "TNode assigned to NodeValue with rc == 0";
1096
  }
1097
}
1098
1099
template <bool ref_count>
1100
1099589518
NodeTemplate<ref_count>& NodeTemplate<ref_count>::
1101
operator=(const NodeTemplate& e) {
1102
1099589518
  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
1103
1099589518
  Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!";
1104
1099589518
  if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
1105
    if(ref_count) {
1106
      // shouldn't ever fail
1107
592679061
      Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
1108
592679061
      d_nv->dec();
1109
    }
1110
687929874
    d_nv = e.d_nv;
1111
    if(ref_count) {
1112
      // shouldn't ever fail
1113
592679061
      Assert(d_nv->d_rc > 0) << "Node assigned from Node with rc == 0";
1114
592679061
      d_nv->inc();
1115
    } else {
1116
95250813
      Assert(d_nv->d_rc > 0) << "TNode assigned from TNode with rc == 0";
1117
    }
1118
  }
1119
1099589518
  return *this;
1120
}
1121
1122
template <bool ref_count>
1123
120935806
NodeTemplate<ref_count>& NodeTemplate<ref_count>::
1124
operator=(const NodeTemplate<!ref_count>& e) {
1125
120935806
  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
1126
120935806
  Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!";
1127
120935806
  if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
1128
    if(ref_count) {
1129
      // shouldn't ever fail
1130
9482227
      Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
1131
9482227
      d_nv->dec();
1132
    }
1133
118745990
    d_nv = e.d_nv;
1134
    if(ref_count) {
1135
9482227
      Assert(d_nv->d_rc > 0) << "Node assigned from TNode with rc == 0";
1136
9482227
      d_nv->inc();
1137
    } else {
1138
      // shouldn't ever happen
1139
109263763
      Assert(d_nv->d_rc > 0) << "TNode assigned from Node with rc == 0";
1140
    }
1141
  }
1142
120935806
  return *this;
1143
}
1144
1145
template <bool ref_count>
1146
template <bool ref_count2>
1147
NodeTemplate<true>
1148
28251659
NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count2>& right) const {
1149
28251659
  assertTNodeNotExpired();
1150
28251659
  return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
1151
}
1152
1153
template <bool ref_count>
1154
60468470
NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
1155
60468470
  assertTNodeNotExpired();
1156
60468470
  return NodeManager::currentNM()->mkNode(kind::NOT, *this);
1157
}
1158
1159
template <bool ref_count>
1160
7147259
NodeTemplate<true> NodeTemplate<ref_count>::negate() const {
1161
7147259
  assertTNodeNotExpired();
1162
7147259
  return (getKind() == kind::NOT) ? NodeTemplate<true>(d_nv->getChild(0)) : NodeManager::currentNM()->mkNode(kind::NOT, *this);
1163
}
1164
1165
template <bool ref_count>
1166
template <bool ref_count2>
1167
NodeTemplate<true>
1168
109262
NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count2>& right) const {
1169
109262
  assertTNodeNotExpired();
1170
109262
  return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
1171
}
1172
1173
template <bool ref_count>
1174
template <bool ref_count2>
1175
NodeTemplate<true>
1176
111439
NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count2>& right) const {
1177
111439
  assertTNodeNotExpired();
1178
111439
  return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
1179
}
1180
1181
template <bool ref_count>
1182
template <bool ref_count2, bool ref_count3>
1183
NodeTemplate<true>
1184
220180
NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart,
1185
                                 const NodeTemplate<ref_count3>& elsepart) const {
1186
220180
  assertTNodeNotExpired();
1187
220180
  return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
1188
}
1189
1190
template <bool ref_count>
1191
template <bool ref_count2>
1192
NodeTemplate<true>
1193
95828
NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const {
1194
95828
  assertTNodeNotExpired();
1195
95828
  return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
1196
}
1197
1198
template <bool ref_count>
1199
template <bool ref_count2>
1200
NodeTemplate<true>
1201
92
NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count2>& right) const {
1202
92
  assertTNodeNotExpired();
1203
92
  return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
1204
}
1205
1206
template <bool ref_count>
1207
inline void
1208
NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
1209
  assertTNodeNotExpired();
1210
  d_nv->printAst(out, indent);
1211
}
1212
1213
/**
1214
 * Returns a node representing the operator of this expression.
1215
 * If this is an APPLY_UF, then the operator will be a functional term.
1216
 * Otherwise, it will be a node with kind BUILTIN.
1217
 */
1218
template <bool ref_count>
1219
43875528
NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const
1220
{
1221
43875528
  Assert(NodeManager::currentNM() != NULL)
1222
      << "There is no current CVC4::NodeManager associated to this thread.\n"
1223
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
1224
1225
43875528
  assertTNodeNotExpired();
1226
1227
43875528
  kind::MetaKind mk = getMetaKind();
1228
43875528
  if (mk == kind::metakind::OPERATOR)
1229
  {
1230
    /* Returns a BUILTIN node. */
1231
5993466
    return NodeManager::currentNM()->operatorOf(getKind());
1232
  }
1233
37882062
  Assert(mk == kind::metakind::PARAMETERIZED);
1234
  /* The operator is the first child. */
1235
37882062
  return Node(d_nv->d_children[0]);
1236
}
1237
1238
/**
1239
 * Returns true if the node has an operator (i.e., it's not a variable
1240
 * or a constant).
1241
 */
1242
template <bool ref_count>
1243
14779500
inline bool NodeTemplate<ref_count>::hasOperator() const {
1244
14779500
  assertTNodeNotExpired();
1245
14779500
  return NodeManager::hasOperator(getKind());
1246
}
1247
1248
template <bool ref_count>
1249
453634260
TypeNode NodeTemplate<ref_count>::getType(bool check) const
1250
{
1251
453634260
  Assert(NodeManager::currentNM() != NULL)
1252
      << "There is no current CVC4::NodeManager associated to this thread.\n"
1253
         "Perhaps a public-facing function is missing a NodeManagerScope ?";
1254
1255
453634260
  assertTNodeNotExpired();
1256
1257
453634261
  return NodeManager::currentNM()->getType(*this, check);
1258
}
1259
1260
template <bool ref_count>
1261
inline Node
1262
2313372
NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
1263
2313372
  if (node == *this) {
1264
25530
    return replacement;
1265
  }
1266
4575684
  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
1267
2287842
  return substitute(node, replacement, cache);
1268
}
1269
1270
template <bool ref_count>
1271
Node
1272
59360673
NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
1273
                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
1274
59360673
  Assert(node != *this);
1275
1276
59360673
  if (getNumChildren() == 0 || node == replacement)
1277
  {
1278
28696941
    return *this;
1279
  }
1280
1281
  // in cache?
1282
30663732
  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
1283
30663732
  if(i != cache.end()) {
1284
7336173
    return (*i).second;
1285
  }
1286
1287
  // otherwise compute
1288
46655118
  NodeBuilder<> nb(getKind());
1289
23327559
  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1290
    // push the operator
1291
6052019
    if(getOperator() == node) {
1292
1037
      nb << replacement;
1293
    } else {
1294
6050982
      nb << getOperator().substitute(node, replacement, cache);
1295
    }
1296
  }
1297
74534618
  for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1298
  {
1299
51207059
    if (*it == node)
1300
    {
1301
799709
      nb << replacement;
1302
    }
1303
    else
1304
    {
1305
50407350
      nb << (*it).substitute(node, replacement, cache);
1306
    }
1307
  }
1308
1309
  // put in cache
1310
46655118
  Node n = nb;
1311
23327559
  cache[*this] = n;
1312
23327559
  return n;
1313
}
1314
1315
template <bool ref_count>
1316
template <class Iterator1, class Iterator2>
1317
inline Node
1318
9714998
NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
1319
                                    Iterator1 nodesEnd,
1320
                                    Iterator2 replacementsBegin,
1321
                                    Iterator2 replacementsEnd) const {
1322
19429996
  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
1323
  return substitute(nodesBegin, nodesEnd,
1324
19429996
                    replacementsBegin, replacementsEnd, cache);
1325
}
1326
1327
template <bool ref_count>
1328
template <class Iterator1, class Iterator2>
1329
Node
1330
64053341
NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
1331
                                    Iterator1 nodesEnd,
1332
                                    Iterator2 replacementsBegin,
1333
                                    Iterator2 replacementsEnd,
1334
                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
1335
  // in cache?
1336
64053341
  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
1337
64053341
  if(i != cache.end()) {
1338
24533331
    return (*i).second;
1339
  }
1340
1341
  // otherwise compute
1342
39520010
  Assert(std::distance(nodesBegin, nodesEnd)
1343
         == std::distance(replacementsBegin, replacementsEnd))
1344
      << "Substitution iterator ranges must be equal size";
1345
39520010
  Iterator1 j = std::find(nodesBegin, nodesEnd, TNode(*this));
1346
39520010
  if(j != nodesEnd) {
1347
4688527
    Iterator2 b = replacementsBegin;
1348
4688527
    std::advance(b, std::distance(nodesBegin, j));
1349
9377054
    Node n = *b;
1350
4688527
    cache[*this] = n;
1351
4688527
    return n;
1352
34831483
  } else if(getNumChildren() == 0) {
1353
15498624
    cache[*this] = *this;
1354
15498624
    return *this;
1355
  } else {
1356
38665718
    NodeBuilder<> nb(getKind());
1357
19332859
    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1358
      // push the operator
1359
1712054
      nb << getOperator().substitute(nodesBegin, nodesEnd,
1360
                                     replacementsBegin, replacementsEnd,
1361
                                     cache);
1362
    }
1363
71959148
    for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1364
    {
1365
52626289
      nb << (*it).substitute(
1366
          nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache);
1367
    }
1368
38665718
    Node n = nb;
1369
19332859
    cache[*this] = n;
1370
19332859
    return n;
1371
  }
1372
}
1373
1374
template <bool ref_count>
1375
template <class Iterator>
1376
inline Node
1377
32
NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
1378
                                    Iterator substitutionsEnd) const {
1379
64
  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
1380
64
  return substitute(substitutionsBegin, substitutionsEnd, cache);
1381
}
1382
1383
template <bool ref_count>
1384
template <class Iterator>
1385
Node
1386
168
NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
1387
                                    Iterator substitutionsEnd,
1388
                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
1389
  // in cache?
1390
168
  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
1391
168
  if(i != cache.end()) {
1392
8
    return (*i).second;
1393
  }
1394
1395
  // otherwise compute
1396
160
  Iterator j = find_if(
1397
      substitutionsBegin,
1398
      substitutionsEnd,
1399
524
      [this](const auto& subst){ return subst.first == *this; });
1400
160
  if(j != substitutionsEnd) {
1401
40
    Node n = (*j).second;
1402
20
    cache[*this] = n;
1403
20
    return n;
1404
140
  } else if(getNumChildren() == 0) {
1405
72
    cache[*this] = *this;
1406
72
    return *this;
1407
  } else {
1408
136
    NodeBuilder<> nb(getKind());
1409
68
    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1410
      // push the operator
1411
      nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache);
1412
    }
1413
204
    for (const_iterator it = begin(), iend = end(); it != iend; ++it)
1414
    {
1415
136
      nb << (*it).substitute(substitutionsBegin, substitutionsEnd, cache);
1416
    }
1417
136
    Node n = nb;
1418
68
    cache[*this] = n;
1419
68
    return n;
1420
  }
1421
}
1422
1423
#ifdef CVC4_DEBUG
1424
/**
1425
 * Pretty printer for use within gdb.  This is not intended to be used
1426
 * outside of gdb.  This writes to the Warning() stream and immediately
1427
 * flushes the stream.
1428
 *
1429
 * Note that this function cannot be a template, since the compiler
1430
 * won't instantiate it.  Even if we explicitly instantiate.  (Odd?)
1431
 * So we implement twice.  We mark as __attribute__((used)) so that
1432
 * GCC emits code for it even though static analysis indicates it's
1433
 * never called.
1434
 *
1435
 * Tim's Note: I moved this into the node.h file because this allows gdb
1436
 * to find the symbol, and use it, which is the first standard this code needs
1437
 * to meet. A cleaner solution is welcomed.
1438
 */
1439
static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
1440
  Warning() << Node::setdepth(-1)
1441
            << Node::dag(true)
1442
            << Node::setlanguage(language::output::LANG_AST)
1443
            << n << std::endl;
1444
  Warning().flush();
1445
}
1446
static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate<true>& n) {
1447
  Warning() << Node::setdepth(-1)
1448
            << Node::dag(false)
1449
            << Node::setlanguage(language::output::LANG_AST)
1450
            << n << std::endl;
1451
  Warning().flush();
1452
}
1453
static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) {
1454
  n.printAst(Warning(), 0);
1455
  Warning().flush();
1456
}
1457
1458
static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
1459
  Warning() << Node::setdepth(-1)
1460
            << Node::dag(true)
1461
            << Node::setlanguage(language::output::LANG_AST)
1462
            << n << std::endl;
1463
  Warning().flush();
1464
}
1465
static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate<false>& n) {
1466
  Warning() << Node::setdepth(-1)
1467
            << Node::dag(false)
1468
            << Node::setlanguage(language::output::LANG_AST)
1469
            << n << std::endl;
1470
  Warning().flush();
1471
}
1472
static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) {
1473
  n.printAst(Warning(), 0);
1474
  Warning().flush();
1475
}
1476
#endif /* CVC4_DEBUG */
1477
1478
}/* CVC4 namespace */
1479
1480
#endif /* CVC4__NODE_H */