GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_algorithm.cpp Lines: 321 359 89.4 %
Date: 2021-03-22 Branches: 517 1018 50.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_algorithm.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
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 Common algorithms on nodes
13
 **
14
 ** This file implements common algorithms applied to nodes, such as checking if
15
 ** a node contains a free or a bound variable.
16
 **/
17
18
#include "expr/node_algorithm.h"
19
20
#include "expr/attribute.h"
21
#include "expr/dtype.h"
22
23
namespace CVC4 {
24
namespace expr {
25
26
679106
bool hasSubterm(TNode n, TNode t, bool strict)
27
{
28
679106
  if (!strict && n == t)
29
  {
30
10
    return true;
31
  }
32
33
1358192
  std::unordered_set<TNode, TNodeHashFunction> visited;
34
1358192
  std::vector<TNode> toProcess;
35
36
679096
  toProcess.push_back(n);
37
38
  // incrementally iterate and add to toProcess
39
2047829
  for (unsigned i = 0; i < toProcess.size(); ++i)
40
  {
41
3305918
    TNode current = toProcess[i];
42
15548165
    for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
43
    {
44
26404317
      TNode child;
45
      // try children then operator
46
14757095
      if (j < j_end)
47
      {
48
13388360
        child = current[j];
49
      }
50
1368735
      else if (current.hasOperator())
51
      {
52
791072
        child = current.getOperator();
53
      }
54
      else
55
      {
56
577663
        break;
57
      }
58
14179432
      if (child == t)
59
      {
60
568452
        return true;
61
      }
62
13610980
      if (visited.find(child) != visited.end())
63
      {
64
1963758
        continue;
65
      }
66
      else
67
      {
68
11647222
        visited.insert(child);
69
11647222
        toProcess.push_back(child);
70
      }
71
    }
72
  }
73
74
110644
  return false;
75
}
76
77
bool hasSubtermMulti(TNode n, TNode t)
78
{
79
  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
80
  std::unordered_map<TNode, bool, TNodeHashFunction> contains;
81
  std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
82
  std::vector<TNode> visit;
83
  TNode cur;
84
  visit.push_back(n);
85
  do
86
  {
87
    cur = visit.back();
88
    visit.pop_back();
89
    it = visited.find(cur);
90
91
    if (it == visited.end())
92
    {
93
      if (cur == t)
94
      {
95
        visited[cur] = true;
96
        contains[cur] = true;
97
      }
98
      else
99
      {
100
        visited[cur] = false;
101
        visit.push_back(cur);
102
        for (const Node& cc : cur)
103
        {
104
          visit.push_back(cc);
105
        }
106
      }
107
    }
108
    else if (!it->second)
109
    {
110
      bool doesContain = false;
111
      for (const Node& cn : cur)
112
      {
113
        it = contains.find(cn);
114
        Assert(it != contains.end());
115
        if (it->second)
116
        {
117
          if (doesContain)
118
          {
119
            // two children have t, return true
120
            return true;
121
          }
122
          doesContain = true;
123
        }
124
      }
125
      contains[cur] = doesContain;
126
      visited[cur] = true;
127
    }
128
  } while (!visit.empty());
129
  return false;
130
}
131
132
839361
bool hasSubtermKind(Kind k, Node n)
133
{
134
1678722
  std::unordered_set<TNode, TNodeHashFunction> visited;
135
1678722
  std::vector<TNode> visit;
136
1678722
  TNode cur;
137
839361
  visit.push_back(n);
138
5813882
  do
139
  {
140
6653243
    cur = visit.back();
141
6653243
    visit.pop_back();
142
6653243
    if (visited.find(cur) == visited.end())
143
    {
144
5580712
      visited.insert(cur);
145
5580712
      if (cur.getKind() == k)
146
      {
147
124
        return true;
148
      }
149
11394569
      for (const Node& cn : cur)
150
      {
151
5813981
        visit.push_back(cn);
152
      }
153
    }
154
6653119
  } while (!visit.empty());
155
839237
  return false;
156
}
157
158
2688
bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
159
                     Node n)
160
{
161
2688
  if (ks.empty())
162
  {
163
    return false;
164
  }
165
5376
  std::unordered_set<TNode, TNodeHashFunction> visited;
166
5376
  std::vector<TNode> visit;
167
5376
  TNode cur;
168
2688
  visit.push_back(n);
169
3675
  do
170
  {
171
6363
    cur = visit.back();
172
6363
    visit.pop_back();
173
6363
    if (visited.find(cur) == visited.end())
174
    {
175
5742
      if (ks.find(cur.getKind()) != ks.end())
176
      {
177
46
        return true;
178
      }
179
5696
      visited.insert(cur);
180
5696
      visit.insert(visit.end(), cur.begin(), cur.end());
181
    }
182
6317
  } while (!visit.empty());
183
2642
  return false;
184
}
185
186
1327
bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
187
{
188
1327
  if (t.empty())
189
  {
190
    return false;
191
  }
192
1327
  if (!strict && std::find(t.begin(), t.end(), n) != t.end())
193
  {
194
4
    return true;
195
  }
196
197
2646
  std::unordered_set<TNode, TNodeHashFunction> visited;
198
2646
  std::vector<TNode> toProcess;
199
200
1323
  toProcess.push_back(n);
201
202
  // incrementally iterate and add to toProcess
203
12568
  for (unsigned i = 0; i < toProcess.size(); ++i)
204
  {
205
22742
    TNode current = toProcess[i];
206
24975
    for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
207
    {
208
32970
      TNode child;
209
      // try children then operator
210
21259
      if (j < j_end)
211
      {
212
10014
        child = current[j];
213
      }
214
11245
      else if (current.hasOperator())
215
      {
216
3716
        child = current.getOperator();
217
      }
218
      else
219
      {
220
7529
        break;
221
      }
222
13730
      if (std::find(t.begin(), t.end(), child) != t.end())
223
      {
224
252
        return true;
225
      }
226
13478
      if (visited.find(child) != visited.end())
227
      {
228
1767
        continue;
229
      }
230
      else
231
      {
232
11711
        visited.insert(child);
233
11711
        toProcess.push_back(child);
234
      }
235
    }
236
  }
237
238
1071
  return false;
239
}
240
241
struct HasBoundVarTag
242
{
243
};
244
struct HasBoundVarComputedTag
245
{
246
};
247
/** Attribute true for expressions with bound variables in them */
248
typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr;
249
typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr;
250
251
12120535
bool hasBoundVar(TNode n)
252
{
253
12120535
  if (!n.getAttribute(HasBoundVarComputedAttr()))
254
  {
255
2292734
    bool hasBv = false;
256
2292734
    if (n.getKind() == kind::BOUND_VARIABLE)
257
    {
258
64503
      hasBv = true;
259
    }
260
    else
261
    {
262
6892890
      for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
263
      {
264
5067415
        if (hasBoundVar(*i))
265
        {
266
402756
          hasBv = true;
267
402756
          break;
268
        }
269
      }
270
    }
271
2292734
    if (!hasBv && n.hasOperator())
272
    {
273
1596037
      hasBv = hasBoundVar(n.getOperator());
274
    }
275
2292734
    n.setAttribute(HasBoundVarAttr(), hasBv);
276
2292734
    n.setAttribute(HasBoundVarComputedAttr(), true);
277
4585468
    Debug("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr())
278
2292734
                 << std::endl;
279
2292734
    return hasBv;
280
  }
281
9827801
  return n.getAttribute(HasBoundVarAttr());
282
}
283
284
1320753
bool hasFreeVar(TNode n)
285
{
286
2641506
  std::unordered_set<Node, NodeHashFunction> fvs;
287
2641506
  return getFreeVariables(n, fvs, false);
288
}
289
290
struct HasClosureTag
291
{
292
};
293
struct HasClosureComputedTag
294
{
295
};
296
/** Attribute true for expressions with closures in them */
297
typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
298
typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;
299
300
2944
bool hasClosure(Node n)
301
{
302
2944
  if (!n.getAttribute(HasClosureComputedAttr()))
303
  {
304
1684
    bool hasC = false;
305
1684
    if (n.isClosure())
306
    {
307
20
      hasC = true;
308
    }
309
    else
310
    {
311
3299
      for (auto i = n.begin(); i != n.end() && !hasC; ++i)
312
      {
313
1635
        hasC = hasClosure(*i);
314
      }
315
    }
316
1684
    if (!hasC && n.hasOperator())
317
    {
318
788
      hasC = hasClosure(n.getOperator());
319
    }
320
1684
    n.setAttribute(HasClosureAttr(), hasC);
321
1684
    n.setAttribute(HasClosureComputedAttr(), true);
322
1684
    return hasC;
323
  }
324
1260
  return n.getAttribute(HasClosureAttr());
325
}
326
327
1380195
bool getFreeVariables(TNode n,
328
                      std::unordered_set<Node, NodeHashFunction>& fvs,
329
                      bool computeFv)
330
{
331
2760390
  std::unordered_set<TNode, TNodeHashFunction> scope;
332
2760390
  return getFreeVariablesScope(n, fvs, scope, computeFv);
333
}
334
335
1478684
bool getFreeVariablesScope(TNode n,
336
                           std::unordered_set<Node, NodeHashFunction>& fvs,
337
                           std::unordered_set<TNode, TNodeHashFunction>& scope,
338
                           bool computeFv)
339
{
340
2957368
  std::unordered_set<TNode, TNodeHashFunction> visited;
341
2957368
  std::vector<TNode> visit;
342
2957368
  TNode cur;
343
1478684
  visit.push_back(n);
344
3094300
  do
345
  {
346
4572984
    cur = visit.back();
347
4572984
    visit.pop_back();
348
    // can skip if it doesn't have a bound variable
349
4572984
    if (!hasBoundVar(cur))
350
    {
351
2651915
      continue;
352
    }
353
    std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
354
1921069
        visited.find(cur);
355
1921069
    if (itv == visited.end())
356
    {
357
1405118
      visited.insert(cur);
358
1405118
      if (cur.getKind() == kind::BOUND_VARIABLE)
359
      {
360
309657
        if (scope.find(cur) == scope.end())
361
        {
362
76503
          if (computeFv)
363
          {
364
76182
            fvs.insert(cur);
365
          }
366
          else
367
          {
368
642
            return true;
369
          }
370
        }
371
      }
372
1095461
      else if (cur.isClosure())
373
      {
374
        // add to scope
375
317772
        for (const TNode& cn : cur[0])
376
        {
377
          // should not shadow
378
438566
          Assert(scope.find(cn) == scope.end())
379
219283
              << "Shadowed variable " << cn << " in " << cur << "\n";
380
219283
          scope.insert(cn);
381
        }
382
        // must make recursive call to use separate cache
383
98489
        if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv)
384
        {
385
          return true;
386
        }
387
        // cleanup
388
317772
        for (const TNode& cn : cur[0])
389
        {
390
219283
          scope.erase(cn);
391
        }
392
      }
393
      else
394
      {
395
996972
        if (cur.hasOperator())
396
        {
397
996972
          visit.push_back(cur.getOperator());
398
        }
399
996972
        visit.insert(visit.end(), cur.begin(), cur.end());
400
      }
401
    }
402
4572663
  } while (!visit.empty());
403
404
1478363
  return !fvs.empty();
405
}
406
407
483
bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
408
{
409
966
  std::unordered_set<TNode, TNodeHashFunction> visited;
410
966
  std::vector<TNode> visit;
411
966
  TNode cur;
412
483
  visit.push_back(n);
413
4850
  do
414
  {
415
5333
    cur = visit.back();
416
5333
    visit.pop_back();
417
    std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
418
5333
        visited.find(cur);
419
5333
    if (itv == visited.end())
420
    {
421
4193
      if (cur.isVar())
422
      {
423
1533
        vs.insert(cur);
424
      }
425
      else
426
      {
427
2660
        visit.insert(visit.end(), cur.begin(), cur.end());
428
      }
429
4193
      visited.insert(cur);
430
    }
431
5333
  } while (!visit.empty());
432
433
966
  return !vs.empty();
434
}
435
436
4353
void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms)
437
{
438
8706
  std::unordered_set<TNode, TNodeHashFunction> visited;
439
4353
  getSymbols(n, syms, visited);
440
4353
}
441
442
21376
void getSymbols(TNode n,
443
                std::unordered_set<Node, NodeHashFunction>& syms,
444
                std::unordered_set<TNode, TNodeHashFunction>& visited)
445
{
446
42752
  std::vector<TNode> visit;
447
42752
  TNode cur;
448
21376
  visit.push_back(n);
449
652642
  do
450
  {
451
674018
    cur = visit.back();
452
674018
    visit.pop_back();
453
674018
    if (visited.find(cur) == visited.end())
454
    {
455
333573
      visited.insert(cur);
456
333573
      if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE)
457
      {
458
40959
        syms.insert(cur);
459
      }
460
333573
      if (cur.hasOperator())
461
      {
462
206327
        visit.push_back(cur.getOperator());
463
      }
464
333573
      visit.insert(visit.end(), cur.begin(), cur.end());
465
    }
466
674018
  } while (!visit.empty());
467
21376
}
468
469
125
void getKindSubterms(TNode n,
470
                     Kind k,
471
                     bool topLevel,
472
                     std::unordered_set<Node, NodeHashFunction>& ts)
473
{
474
250
  std::unordered_set<TNode, TNodeHashFunction> visited;
475
250
  std::vector<TNode> visit;
476
250
  TNode cur;
477
125
  visit.push_back(n);
478
4072
  do
479
  {
480
4197
    cur = visit.back();
481
4197
    visit.pop_back();
482
4197
    if (visited.find(cur) == visited.end())
483
    {
484
2307
      visited.insert(cur);
485
2307
      if (cur.getKind() == k)
486
      {
487
35
        ts.insert(cur);
488
35
        if (topLevel)
489
        {
490
          // only considering top-level applications
491
35
          continue;
492
        }
493
      }
494
2272
      if (cur.hasOperator())
495
      {
496
1266
        visit.push_back(cur.getOperator());
497
      }
498
2272
      visit.insert(visit.end(), cur.begin(), cur.end());
499
    }
500
4197
  } while (!visit.empty());
501
125
}
502
503
3
void getOperatorsMap(
504
    TNode n,
505
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops)
506
{
507
6
  std::unordered_set<TNode, TNodeHashFunction> visited;
508
3
  getOperatorsMap(n, ops, visited);
509
3
}
510
511
3
void getOperatorsMap(
512
    TNode n,
513
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops,
514
    std::unordered_set<TNode, TNodeHashFunction>& visited)
515
{
516
  // nodes that we still need to visit
517
6
  std::vector<TNode> visit;
518
  // current node
519
6
  TNode cur;
520
3
  visit.push_back(n);
521
86
  do
522
  {
523
89
    cur = visit.back();
524
89
    visit.pop_back();
525
    // if cur is in the cache, do nothing
526
89
    if (visited.find(cur) == visited.end())
527
    {
528
      // fetch the correct type
529
178
      TypeNode tn = cur.getType();
530
      // add the current operator to the result
531
89
      if (cur.hasOperator())
532
      {
533
94
       Node o;
534
47
       if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) {
535
7
         o = cur.getOperator();
536
       } else {
537
40
         o = NodeManager::currentNM()->operatorOf(cur.getKind());
538
       }
539
47
        ops[tn].insert(o);
540
      }
541
      // add children to visit in the future
542
89
      visit.insert(visit.end(), cur.begin(), cur.end());
543
    }
544
89
  } while (!visit.empty());
545
3
}
546
547
23062
Node substituteCaptureAvoiding(TNode n, Node src, Node dest)
548
{
549
23062
  if (n == src)
550
  {
551
    return dest;
552
  }
553
23062
  if (src == dest)
554
  {
555
    return n;
556
  }
557
46124
  std::vector<Node> srcs;
558
46124
  std::vector<Node> dests;
559
23062
  srcs.push_back(src);
560
23062
  dests.push_back(dest);
561
23062
  return substituteCaptureAvoiding(n, srcs, dests);
562
}
563
564
23655
Node substituteCaptureAvoiding(TNode n,
565
                               std::vector<Node>& src,
566
                               std::vector<Node>& dest)
567
{
568
47310
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
569
23655
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
570
47310
  std::vector<TNode> visit;
571
47310
  TNode curr;
572
23655
  visit.push_back(n);
573
23655
  Assert(src.size() == dest.size())
574
      << "Substitution domain and range must be equal size";
575
195561
  do
576
  {
577
219216
    curr = visit.back();
578
219216
    visit.pop_back();
579
219216
    it = visited.find(curr);
580
581
219216
    if (it == visited.end())
582
    {
583
141352
      auto itt = std::find(src.rbegin(), src.rend(), curr);
584
166093
      if (itt != src.rend())
585
      {
586
24741
        Assert(
587
            (std::distance(src.begin(), itt.base()) - 1) >= 0
588
            && static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1)
589
                   < dest.size());
590
24741
        visited[curr] = dest[std::distance(src.begin(), itt.base()) - 1];
591
100129
        continue;
592
      }
593
167258
      if (curr.getNumChildren() == 0)
594
      {
595
50647
        visited[curr] = curr;
596
50647
        continue;
597
      }
598
599
65964
      visited[curr] = Node::null();
600
      // if binder, rename variables to avoid capture
601
65964
      if (curr.isClosure())
602
      {
603
760
        NodeManager* nm = NodeManager::currentNM();
604
        // have new vars -> renames subs in the end of current sub
605
1686
        for (const Node& v : curr[0])
606
        {
607
926
          src.push_back(v);
608
926
          dest.push_back(nm->mkBoundVar(v.getType()));
609
        }
610
      }
611
      // save for post-visit
612
65964
      visit.push_back(curr);
613
      // visit children
614
65964
      if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
615
      {
616
        // push the operator
617
1521
        visit.push_back(curr.getOperator());
618
      }
619
194040
      for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
620
      {
621
128076
        visit.push_back(curr[i]);
622
      }
623
    }
624
77864
    else if (it->second.isNull())
625
    {
626
      // build node
627
131928
      NodeBuilder<> nb(curr.getKind());
628
65964
      if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
629
      {
630
        // push the operator
631
1521
        Assert(visited.find(curr.getOperator()) != visited.end());
632
1521
        nb << visited[curr.getOperator()];
633
      }
634
      // collect substituted children
635
194040
      for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
636
      {
637
128076
        Assert(visited.find(curr[i]) != visited.end());
638
128076
        nb << visited[curr[i]];
639
      }
640
65964
      visited[curr] = nb;
641
642
      // remove renaming
643
65964
      if (curr.isClosure())
644
      {
645
        // remove beginning of sub which correspond to renaming of variables in
646
        // this binder
647
760
        unsigned nchildren = curr[0].getNumChildren();
648
760
        src.resize(src.size() - nchildren);
649
760
        dest.resize(dest.size() - nchildren);
650
      }
651
    }
652
219216
  } while (!visit.empty());
653
23655
  Assert(visited.find(n) != visited.end());
654
47310
  return visited[n];
655
}
656
657
14961
void getComponentTypes(
658
    TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types)
659
{
660
29922
  std::vector<TypeNode> toProcess;
661
14961
  toProcess.push_back(t);
662
108
  do
663
  {
664
30138
    TypeNode curr = toProcess.back();
665
15069
    toProcess.pop_back();
666
    // if not already visited
667
15069
    if (types.find(curr) == types.end())
668
    {
669
14979
      types.insert(curr);
670
      // get component types from the children
671
15087
      for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++)
672
      {
673
108
        toProcess.push_back(curr[i]);
674
      }
675
    }
676
15069
  } while (!toProcess.empty());
677
14961
}
678
679
18
bool match(Node x,
680
           Node y,
681
           std::unordered_map<Node, Node, NodeHashFunction>& subs)
682
{
683
36
  std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
684
  std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
685
18
      it;
686
18
  std::unordered_map<Node, Node, NodeHashFunction>::iterator subsIt;
687
688
36
  std::vector<std::pair<TNode, TNode>> stack;
689
18
  stack.emplace_back(x, y);
690
36
  std::pair<TNode, TNode> curr;
691
692
66
  while (!stack.empty())
693
  {
694
36
    curr = stack.back();
695
36
    stack.pop_back();
696
36
    if (curr.first == curr.second)
697
    {
698
      // holds trivially
699
4
      continue;
700
    }
701
32
    it = visited.find(curr);
702
32
    if (it != visited.end())
703
    {
704
      // already processed
705
2
      continue;
706
    }
707
30
    visited.insert(curr);
708
30
    if (curr.first.getNumChildren() == 0)
709
    {
710
16
      if (!curr.first.getType().isComparableTo(curr.second.getType()))
711
      {
712
        // the two subterms have different types
713
2
        return false;
714
      }
715
      // if the two subterms are not equal and the first one is a bound
716
      // variable...
717
14
      if (curr.first.getKind() == kind::BOUND_VARIABLE)
718
      {
719
        // and we have not seen this variable before...
720
10
        subsIt = subs.find(curr.first);
721
10
        if (subsIt == subs.cend())
722
        {
723
          // add the two subterms to `sub`
724
4
          subs.emplace(curr.first, curr.second);
725
        }
726
        else
727
        {
728
          // if we saw this variable before, make sure that (now and before) it
729
          // maps to the same subterm
730
6
          if (curr.second != subsIt->second)
731
          {
732
2
            return false;
733
          }
734
        }
735
      }
736
      else
737
      {
738
        // the two subterms are not equal
739
4
        return false;
740
      }
741
    }
742
    else
743
    {
744
      // if the two subterms are not equal, make sure that their operators are
745
      // equal
746
      // we compare operators instead of kinds because different terms may have
747
      // the same kind (both `(id x)` and `(square x)` have kind APPLY_UF)
748
      // since many builtin operators like `PLUS` allow arbitrary number of
749
      // arguments, we also need to check if the two subterms have the same
750
      // number of children
751
28
      if (curr.first.getNumChildren() != curr.second.getNumChildren()
752
28
          || curr.first.getOperator() != curr.second.getOperator())
753
      {
754
4
        return false;
755
      }
756
      // recurse on children
757
30
      for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i)
758
      {
759
20
        stack.emplace_back(curr.first[i], curr.second[i]);
760
      }
761
    }
762
  }
763
6
  return true;
764
}
765
766
}  // namespace expr
767
26676
}  // namespace CVC4