GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/util/ite_utilities.cpp Lines: 471 998 47.2 %
Date: 2021-03-22 Branches: 800 3729 21.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ite_utilities.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Aina Niemetz, Clark Barrett
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 Simplifications for ITE expressions
13
 **
14
 ** This module implements preprocessing phases designed to simplify ITE
15
 ** expressions.  Based on:
16
 ** Kim, Somenzi, Jin.  Efficient Term-ITE Conversion for SMT.  FMCAD 2009.
17
 ** Burch, Jerry.  Techniques for Verifying Superscalar Microprocessors.  DAC
18
 *'96
19
 **/
20
#include "preprocessing/util/ite_utilities.h"
21
22
#include <utility>
23
24
#include "preprocessing/assertion_pipeline.h"
25
#include "preprocessing/passes/rewrite.h"
26
#include "smt/smt_statistics_registry.h"
27
#include "theory/rewriter.h"
28
#include "theory/theory.h"
29
30
using namespace std;
31
namespace CVC4 {
32
namespace preprocessing {
33
namespace util {
34
35
namespace ite {
36
37
77258
inline static bool isTermITE(TNode e)
38
{
39
77258
  return (e.getKind() == kind::ITE && !e.getType().isBoolean());
40
}
41
42
102696
inline static bool triviallyContainsNoTermITEs(TNode e)
43
{
44
102696
  return e.isConst() || e.isVar();
45
}
46
47
5258
static bool isTheoryAtom(TNode a)
48
{
49
  using namespace kind;
50
5258
  switch (a.getKind())
51
  {
52
109
    case EQUAL:
53
109
    case DISTINCT: return !(a[0].getType().isBoolean());
54
55
    /* from uf */
56
    case APPLY_UF: return a.getType().isBoolean();
57
44
    case CARDINALITY_CONSTRAINT:
58
    case DIVISIBLE:
59
    case LT:
60
    case LEQ:
61
    case GT:
62
    case GEQ:
63
    case IS_INTEGER:
64
    case BITVECTOR_COMP:
65
    case BITVECTOR_ULT:
66
    case BITVECTOR_ULE:
67
    case BITVECTOR_UGT:
68
    case BITVECTOR_UGE:
69
    case BITVECTOR_SLT:
70
    case BITVECTOR_SLE:
71
    case BITVECTOR_SGT:
72
44
    case BITVECTOR_SGE: return true;
73
5105
    default: return false;
74
  }
75
}
76
77
199907
struct CTIVStackElement
78
{
79
  TNode curr;
80
  unsigned pos;
81
  CTIVStackElement() : curr(), pos(0) {}
82
45323
  CTIVStackElement(TNode c) : curr(c), pos(0) {}
83
}; /* CTIVStackElement */
84
85
}  // namespace ite
86
87
8995
ITEUtilities::ITEUtilities()
88
8995
    : d_containsVisitor(new ContainsTermITEVisitor()),
89
      d_compressor(NULL),
90
      d_simplifier(NULL),
91
17990
      d_careSimp(NULL)
92
{
93
8995
  Assert(d_containsVisitor != NULL);
94
8995
}
95
96
17984
ITEUtilities::~ITEUtilities()
97
{
98
8992
  if (d_simplifier != NULL)
99
  {
100
1
    delete d_simplifier;
101
  }
102
8992
  if (d_compressor != NULL)
103
  {
104
1
    delete d_compressor;
105
  }
106
8992
  if (d_careSimp != NULL)
107
  {
108
    delete d_careSimp;
109
  }
110
8992
}
111
112
1
Node ITEUtilities::simpITE(TNode assertion)
113
{
114
1
  if (d_simplifier == NULL)
115
  {
116
1
    d_simplifier = new ITESimplifier(d_containsVisitor.get());
117
  }
118
1
  return d_simplifier->simpITE(assertion);
119
}
120
121
1
bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const
122
{
123
1
  if (d_simplifier == NULL)
124
  {
125
    return false;
126
  }
127
  else
128
  {
129
1
    return d_simplifier->doneALotOfWorkHeuristic();
130
  }
131
}
132
133
/* returns false if an assertion is discovered to be equal to false. */
134
1
bool ITEUtilities::compress(AssertionPipeline* assertionsToPreprocess)
135
{
136
1
  if (d_compressor == NULL)
137
  {
138
1
    d_compressor = new ITECompressor(d_containsVisitor.get());
139
  }
140
1
  return d_compressor->compress(assertionsToPreprocess);
141
}
142
143
Node ITEUtilities::simplifyWithCare(TNode e)
144
{
145
  if (d_careSimp == NULL)
146
  {
147
    d_careSimp = new ITECareSimplifier();
148
  }
149
  return d_careSimp->simplifyWithCare(e);
150
}
151
152
void ITEUtilities::clear()
153
{
154
  if (d_simplifier != NULL)
155
  {
156
    d_simplifier->clearSimpITECaches();
157
  }
158
  if (d_compressor != NULL)
159
  {
160
    d_compressor->garbageCollect();
161
  }
162
  if (d_careSimp != NULL)
163
  {
164
    d_careSimp->clear();
165
  }
166
  d_containsVisitor->garbageCollect();
167
}
168
169
/*********************                                                        */
170
/* ContainsTermITEVisitor
171
 */
172
24745
ContainsTermITEVisitor::ContainsTermITEVisitor() : d_cache() {}
173
24742
ContainsTermITEVisitor::~ContainsTermITEVisitor() {}
174
18526
bool ContainsTermITEVisitor::containsTermITE(TNode e)
175
{
176
  /* throughout execution skip through NOT nodes. */
177
18526
  e = (e.getKind() == kind::NOT) ? e[0] : e;
178
18526
  if (ite::triviallyContainsNoTermITEs(e))
179
  {
180
5295
    return false;
181
  }
182
183
13231
  NodeBoolMap::const_iterator end = d_cache.end();
184
13231
  NodeBoolMap::const_iterator tmp_it = d_cache.find(e);
185
13231
  if (tmp_it != end)
186
  {
187
1178
    return (*tmp_it).second;
188
  }
189
190
12053
  bool foundTermIte = false;
191
24106
  std::vector<ite::CTIVStackElement> stack;
192
12053
  stack.push_back(ite::CTIVStackElement(e));
193
267069
  while (!foundTermIte && !stack.empty())
194
  {
195
127508
    ite::CTIVStackElement& top = stack.back();
196
255016
    TNode curr = top.curr;
197
127508
    if (top.pos >= curr.getNumChildren())
198
    {
199
      // all of the children have been visited
200
      // no term ites were found
201
43338
      d_cache[curr] = false;
202
43338
      stack.pop_back();
203
    }
204
    else
205
    {
206
      // this is someone's child
207
168340
      TNode child = curr[top.pos];
208
84170
      child = (child.getKind() == kind::NOT) ? child[0] : child;
209
84170
      ++top.pos;
210
84170
      if (ite::triviallyContainsNoTermITEs(child))
211
      {
212
        // skip
213
      }
214
      else
215
      {
216
34423
        tmp_it = d_cache.find(child);
217
34423
        if (tmp_it != end)
218
        {
219
1153
          foundTermIte = (*tmp_it).second;
220
        }
221
        else
222
        {
223
33270
          stack.push_back(ite::CTIVStackElement(child));
224
33270
          foundTermIte = ite::isTermITE(child);
225
        }
226
      }
227
    }
228
  }
229
12053
  if (foundTermIte)
230
  {
231
5497
    while (!stack.empty())
232
    {
233
3970
      TNode curr = stack.back().curr;
234
1985
      stack.pop_back();
235
1985
      d_cache[curr] = true;
236
    }
237
  }
238
12053
  return foundTermIte;
239
}
240
void ContainsTermITEVisitor::garbageCollect() { d_cache.clear(); }
241
242
/*********************                                                        */
243
/* IncomingArcCounter
244
 */
245
1
IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants)
246
1
    : d_reachCount(), d_skipVariables(skipVars), d_skipConstants(skipConstants)
247
{
248
1
}
249
1
IncomingArcCounter::~IncomingArcCounter() {}
250
251
1
void IncomingArcCounter::computeReachability(
252
    const std::vector<Node>& assertions)
253
{
254
2
  std::vector<TNode> tovisit(assertions.begin(), assertions.end());
255
256
229045
  while (!tovisit.empty())
257
  {
258
228530
    TNode back = tovisit.back();
259
114522
    tovisit.pop_back();
260
261
114522
    bool skip = false;
262
114522
    switch (back.getMetaKind())
263
    {
264
304
      case kind::metakind::CONSTANT: skip = d_skipConstants; break;
265
210
      case kind::metakind::VARIABLE: skip = d_skipVariables; break;
266
114008
      default: break;
267
    }
268
269
114522
    if (skip)
270
    {
271
514
      continue;
272
    }
273
114008
    if (d_reachCount.find(back) != d_reachCount.end())
274
    {
275
106422
      d_reachCount[back] = 1 + d_reachCount[back];
276
    }
277
    else
278
    {
279
7586
      d_reachCount[back] = 1;
280
122106
      for (TNode::iterator cit = back.begin(), end = back.end(); cit != end;
281
           ++cit)
282
      {
283
114520
        tovisit.push_back(*cit);
284
      }
285
    }
286
  }
287
1
}
288
289
2
void IncomingArcCounter::clear() { d_reachCount.clear(); }
290
291
/*********************                                                        */
292
/* ITECompressor
293
 */
294
1
ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
295
1
    : d_contains(contains), d_assertions(NULL), d_incoming(true, true)
296
{
297
1
  Assert(d_contains != NULL);
298
299
1
  d_true = NodeManager::currentNM()->mkConst<bool>(true);
300
1
  d_false = NodeManager::currentNM()->mkConst<bool>(false);
301
1
}
302
303
1
ITECompressor::~ITECompressor() { reset(); }
304
305
2
void ITECompressor::reset()
306
{
307
2
  d_incoming.clear();
308
2
  d_compressed.clear();
309
2
}
310
311
void ITECompressor::garbageCollect() { reset(); }
312
313
1
ITECompressor::Statistics::Statistics()
314
    : d_compressCalls("ite-simp::compressCalls", 0),
315
1
      d_skolemsAdded("ite-simp::skolems", 0)
316
{
317
1
  smtStatisticsRegistry()->registerStat(&d_compressCalls);
318
1
  smtStatisticsRegistry()->registerStat(&d_skolemsAdded);
319
1
}
320
2
ITECompressor::Statistics::~Statistics()
321
{
322
1
  smtStatisticsRegistry()->unregisterStat(&d_compressCalls);
323
1
  smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded);
324
1
}
325
326
1720
Node ITECompressor::push_back_boolean(Node original, Node compressed)
327
{
328
3440
  Node rewritten = theory::Rewriter::rewrite(compressed);
329
  // There is a bug if the rewritter takes a pure boolean expression
330
  // and changes its theory
331
1720
  if (rewritten.isConst())
332
  {
333
    d_compressed[compressed] = rewritten;
334
    d_compressed[original] = rewritten;
335
    d_compressed[rewritten] = rewritten;
336
    return rewritten;
337
  }
338
1720
  else if (d_compressed.find(rewritten) != d_compressed.end())
339
  {
340
    Node res = d_compressed[rewritten];
341
    d_compressed[original] = res;
342
    d_compressed[compressed] = res;
343
    return res;
344
  }
345
3440
  else if (rewritten.isVar()
346
3440
           || (rewritten.getKind() == kind::NOT && rewritten[0].isVar()))
347
  {
348
511
    d_compressed[original] = rewritten;
349
511
    d_compressed[compressed] = rewritten;
350
511
    d_compressed[rewritten] = rewritten;
351
511
    return rewritten;
352
  }
353
  else
354
  {
355
1209
    NodeManager* nm = NodeManager::currentNM();
356
2418
    Node skolem = nm->mkSkolem("compress", nm->booleanType());
357
1209
    d_compressed[rewritten] = skolem;
358
1209
    d_compressed[original] = skolem;
359
1209
    d_compressed[compressed] = skolem;
360
361
2418
    Node iff = skolem.eqNode(rewritten);
362
1209
    d_assertions->push_back(iff);
363
1209
    ++(d_statistics.d_skolemsAdded);
364
1209
    return skolem;
365
  }
366
}
367
368
7109
bool ITECompressor::multipleParents(TNode c)
369
{
370
7109
  return d_incoming.lookupIncoming(c) >= 2;
371
}
372
373
1920
Node ITECompressor::compressBooleanITEs(Node toCompress)
374
{
375
1920
  Assert(toCompress.getKind() == kind::ITE);
376
1920
  Assert(toCompress.getType().isBoolean());
377
378
1920
  if (!(toCompress[1] == d_false || toCompress[2] == d_false))
379
  {
380
3840
    Node cmpCnd = compressBoolean(toCompress[0]);
381
1920
    if (cmpCnd.isConst())
382
    {
383
      Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
384
      Node res = compressBoolean(branch);
385
      d_compressed[toCompress] = res;
386
      return res;
387
    }
388
    else
389
    {
390
3840
      Node cmpThen = compressBoolean(toCompress[1]);
391
3840
      Node cmpElse = compressBoolean(toCompress[2]);
392
3840
      Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
393
1920
      if (multipleParents(toCompress))
394
      {
395
534
        return push_back_boolean(toCompress, newIte);
396
      }
397
      else
398
      {
399
1386
        return newIte;
400
      }
401
    }
402
  }
403
404
  NodeBuilder<> nb(kind::AND);
405
  Node curr = toCompress;
406
  while (curr.getKind() == kind::ITE
407
         && (curr[1] == d_false || curr[2] == d_false)
408
         && (!multipleParents(curr) || curr == toCompress))
409
  {
410
    bool negateCnd = (curr[1] == d_false);
411
    Node compressCnd = compressBoolean(curr[0]);
412
    if (compressCnd.isConst())
413
    {
414
      if (compressCnd.getConst<bool>() == negateCnd)
415
      {
416
        return push_back_boolean(toCompress, d_false);
417
      }
418
      else
419
      {
420
        // equivalent to true don't push back
421
      }
422
    }
423
    else
424
    {
425
      Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
426
      nb << pb;
427
    }
428
    curr = negateCnd ? curr[2] : curr[1];
429
  }
430
  Assert(toCompress != curr);
431
432
  nb << compressBoolean(curr);
433
  Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
434
  return push_back_boolean(toCompress, res);
435
}
436
437
1122
Node ITECompressor::compressTerm(Node toCompress)
438
{
439
1122
  if (toCompress.isConst() || toCompress.isVar())
440
  {
441
513
    return toCompress;
442
  }
443
444
609
  if (d_compressed.find(toCompress) != d_compressed.end())
445
  {
446
201
    return d_compressed[toCompress];
447
  }
448
408
  if (toCompress.getKind() == kind::ITE)
449
  {
450
648
    Node cmpCnd = compressBoolean(toCompress[0]);
451
324
    if (cmpCnd.isConst())
452
    {
453
      Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
454
      Node res = compressTerm(branch);
455
      d_compressed[toCompress] = res;
456
      return res;
457
    }
458
    else
459
    {
460
648
      Node cmpThen = compressTerm(toCompress[1]);
461
648
      Node cmpElse = compressTerm(toCompress[2]);
462
648
      Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
463
324
      d_compressed[toCompress] = newIte;
464
324
      return newIte;
465
    }
466
  }
467
468
168
  NodeBuilder<> nb(toCompress.getKind());
469
470
84
  if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
471
  {
472
    nb << (toCompress.getOperator());
473
  }
474
252
  for (Node::iterator it = toCompress.begin(), end = toCompress.end();
475
252
       it != end;
476
       ++it)
477
  {
478
168
    nb << compressTerm(*it);
479
  }
480
168
  Node compressed = (Node)nb;
481
84
  if (multipleParents(toCompress))
482
  {
483
13
    d_compressed[toCompress] = compressed;
484
  }
485
84
  return compressed;
486
}
487
488
113400
Node ITECompressor::compressBoolean(Node toCompress)
489
{
490
  static int instance = 0;
491
113400
  ++instance;
492
113400
  if (toCompress.isConst() || toCompress.isVar())
493
  {
494
1
    return toCompress;
495
  }
496
113399
  if (d_compressed.find(toCompress) != d_compressed.end())
497
  {
498
106221
    return d_compressed[toCompress];
499
  }
500
7178
  else if (toCompress.getKind() == kind::ITE)
501
  {
502
1920
    return compressBooleanITEs(toCompress);
503
  }
504
  else
505
  {
506
5258
    bool ta = ite::isTheoryAtom(toCompress);
507
10516
    NodeBuilder<> nb(toCompress.getKind());
508
5258
    if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
509
    {
510
      nb << (toCompress.getOperator());
511
    }
512
112878
    for (Node::iterator it = toCompress.begin(), end = toCompress.end();
513
112878
         it != end;
514
         ++it)
515
    {
516
215240
      Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
517
107620
      nb << pb;
518
    }
519
10516
    Node compressed = nb;
520
5258
    if (ta || multipleParents(toCompress))
521
    {
522
1186
      return push_back_boolean(toCompress, compressed);
523
    }
524
    else
525
    {
526
4072
      return compressed;
527
    }
528
  }
529
}
530
531
1
bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess)
532
{
533
1
  reset();
534
535
1
  d_assertions = assertionsToPreprocess;
536
1
  d_incoming.computeReachability(assertionsToPreprocess->ref());
537
538
1
  ++(d_statistics.d_compressCalls);
539
1
  Chat() << "Computed reachability" << endl;
540
541
1
  bool nofalses = true;
542
1
  const std::vector<Node>& assertions = assertionsToPreprocess->ref();
543
1
  size_t original_size = assertions.size();
544
1
  Chat() << "compressing " << original_size << endl;
545
3
  for (size_t i = 0; i < original_size && nofalses; ++i)
546
  {
547
4
    Node assertion = assertions[i];
548
4
    Node compressed = compressBoolean(assertion);
549
4
    Node rewritten = theory::Rewriter::rewrite(compressed);
550
    // replace
551
2
    assertionsToPreprocess->replace(i, rewritten);
552
2
    Assert(!d_contains->containsTermITE(rewritten));
553
554
2
    nofalses = (rewritten != d_false);
555
  }
556
557
1
  d_assertions = NULL;
558
559
1
  return nofalses;
560
}
561
562
1
TermITEHeightCounter::TermITEHeightCounter() : d_termITEHeight() {}
563
564
1
TermITEHeightCounter::~TermITEHeightCounter() {}
565
566
1
void TermITEHeightCounter::clear() { d_termITEHeight.clear(); }
567
568
size_t TermITEHeightCounter::cache_size() const
569
{
570
  return d_termITEHeight.size();
571
}
572
573
namespace ite {
574
struct TITEHStackElement
575
{
576
  TNode curr;
577
  unsigned pos;
578
  uint32_t maxChildHeight;
579
  TITEHStackElement() : curr(), pos(0), maxChildHeight(0) {}
580
  TITEHStackElement(TNode c) : curr(c), pos(0), maxChildHeight(0) {}
581
};
582
} /* namespace ite */
583
584
uint32_t TermITEHeightCounter::termITEHeight(TNode e)
585
{
586
  if (ite::triviallyContainsNoTermITEs(e))
587
  {
588
    return 0;
589
  }
590
591
  NodeCountMap::const_iterator end = d_termITEHeight.end();
592
  NodeCountMap::const_iterator tmp_it = d_termITEHeight.find(e);
593
  if (tmp_it != end)
594
  {
595
    return (*tmp_it).second;
596
  }
597
598
  uint32_t returnValue = 0;
599
  // This is initially 0 as the very first call this is included in the max,
600
  // but this has no effect.
601
  std::vector<ite::TITEHStackElement> stack;
602
  stack.push_back(ite::TITEHStackElement(e));
603
  while (!stack.empty())
604
  {
605
    ite::TITEHStackElement& top = stack.back();
606
    top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
607
    TNode curr = top.curr;
608
    if (top.pos >= curr.getNumChildren())
609
    {
610
      // done with the current node
611
      returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
612
      d_termITEHeight[curr] = returnValue;
613
      stack.pop_back();
614
      continue;
615
    }
616
    else
617
    {
618
      if (top.pos == 0 && curr.getKind() == kind::ITE)
619
      {
620
        ++top.pos;
621
        returnValue = 0;
622
        continue;
623
      }
624
      // this is someone's child
625
      TNode child = curr[top.pos];
626
      ++top.pos;
627
      if (ite::triviallyContainsNoTermITEs(child))
628
      {
629
        returnValue = 0;
630
      }
631
      else
632
      {
633
        tmp_it = d_termITEHeight.find(child);
634
        if (tmp_it != end)
635
        {
636
          returnValue = (*tmp_it).second;
637
        }
638
        else
639
        {
640
          stack.push_back(ite::TITEHStackElement(child));
641
        }
642
      }
643
    }
644
  }
645
  return returnValue;
646
}
647
648
1
ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains)
649
    : d_containsVisitor(contains),
650
      d_termITEHeight(),
651
      d_constantLeaves(),
652
      d_allocatedConstantLeaves(),
653
      d_citeEqConstApplications(0),
654
      d_constantIteEqualsConstantCache(),
655
      d_replaceOverCache(),
656
      d_replaceOverTermIteCache(),
657
      d_leavesConstCache(),
658
      d_simpConstCache(),
659
      d_simpContextCache(),
660
1
      d_simpITECache()
661
{
662
1
  Assert(d_containsVisitor != NULL);
663
1
  d_true = NodeManager::currentNM()->mkConst<bool>(true);
664
1
  d_false = NodeManager::currentNM()->mkConst<bool>(false);
665
1
}
666
667
2
ITESimplifier::~ITESimplifier()
668
{
669
1
  clearSimpITECaches();
670
1
  Assert(d_constantLeaves.empty());
671
1
  Assert(d_allocatedConstantLeaves.empty());
672
1
}
673
674
156
bool ITESimplifier::leavesAreConst(TNode e)
675
{
676
156
  return leavesAreConst(e, theory::Theory::theoryOf(e));
677
}
678
679
1
void ITESimplifier::clearSimpITECaches()
680
{
681
1
  Chat() << "clear ite caches " << endl;
682
756
  for (size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i)
683
  {
684
755
    NodeVec* curr = d_allocatedConstantLeaves[i];
685
755
    delete curr;
686
  }
687
1
  d_citeEqConstApplications = 0;
688
1
  d_constantLeaves.clear();
689
1
  d_allocatedConstantLeaves.clear();
690
1
  d_termITEHeight.clear();
691
1
  d_constantIteEqualsConstantCache.clear();
692
1
  d_replaceOverCache.clear();
693
1
  d_replaceOverTermIteCache.clear();
694
1
  d_simpITECache.clear();
695
1
  d_simpVars.clear();
696
1
  d_simpConstCache.clear();
697
1
  d_leavesConstCache.clear();
698
1
  d_simpContextCache.clear();
699
1
}
700
701
1
bool ITESimplifier::doneALotOfWorkHeuristic() const
702
{
703
  static const size_t SIZE_BOUND = 1000;
704
1
  Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications
705
         << endl;
706
1
  return (d_citeEqConstApplications > SIZE_BOUND);
707
}
708
709
1
ITESimplifier::Statistics::Statistics()
710
    : d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
711
      d_unexpected("ite-simp::unexpected", 0),
712
      d_unsimplified("ite-simp::unsimplified", 0),
713
      d_exactMatchFold("ite-simp::exactMatchFold", 0),
714
      d_binaryPredFold("ite-simp::binaryPredFold", 0),
715
      d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
716
      d_simpITEVisits("ite-simp::simpITE.visits", 0),
717
1
      d_inSmaller("ite-simp::inSmaller")
718
{
719
1
  smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded);
720
1
  smtStatisticsRegistry()->registerStat(&d_unexpected);
721
1
  smtStatisticsRegistry()->registerStat(&d_unsimplified);
722
1
  smtStatisticsRegistry()->registerStat(&d_exactMatchFold);
723
1
  smtStatisticsRegistry()->registerStat(&d_binaryPredFold);
724
1
  smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds);
725
1
  smtStatisticsRegistry()->registerStat(&d_simpITEVisits);
726
1
  smtStatisticsRegistry()->registerStat(&d_inSmaller);
727
1
}
728
729
2
ITESimplifier::Statistics::~Statistics()
730
{
731
1
  smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded);
732
1
  smtStatisticsRegistry()->unregisterStat(&d_unexpected);
733
1
  smtStatisticsRegistry()->unregisterStat(&d_unsimplified);
734
1
  smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold);
735
1
  smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold);
736
1
  smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds);
737
1
  smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits);
738
1
  smtStatisticsRegistry()->unregisterStat(&d_inSmaller);
739
1
}
740
741
1253
bool ITESimplifier::isConstantIte(TNode e)
742
{
743
1253
  if (e.isConst())
744
  {
745
573
    return true;
746
  }
747
680
  else if (ite::isTermITE(e))
748
  {
749
680
    NodeVec* constants = computeConstantLeaves(e);
750
680
    return constants != NULL;
751
  }
752
  else
753
  {
754
    return false;
755
  }
756
}
757
758
43308
ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite)
759
{
760
43308
  Assert(ite::isTermITE(ite));
761
43308
  ConstantLeavesMap::const_iterator it = d_constantLeaves.find(ite);
762
43308
  ConstantLeavesMap::const_iterator end = d_constantLeaves.end();
763
43308
  if (it != end)
764
  {
765
42446
    return (*it).second;
766
  }
767
1724
  TNode thenB = ite[1];
768
1724
  TNode elseB = ite[2];
769
770
  // special case 2 constant children
771
862
  if (thenB.isConst() && elseB.isConst())
772
  {
773
152
    NodeVec* pair = new NodeVec(2);
774
152
    d_allocatedConstantLeaves.push_back(pair);
775
776
152
    (*pair)[0] = std::min(thenB, elseB);
777
152
    (*pair)[1] = std::max(thenB, elseB);
778
152
    d_constantLeaves[ite] = pair;
779
152
    return pair;
780
  }
781
  // At least 1 is an ITE
782
1739
  if (!(thenB.isConst() || thenB.getKind() == kind::ITE)
783
1314
      || !(elseB.isConst() || elseB.getKind() == kind::ITE))
784
  {
785
    // Cannot be a termITE tree
786
107
    d_constantLeaves[ite] = NULL;
787
107
    return NULL;
788
  }
789
790
  // At least 1 is not a constant
791
1206
  TNode definitelyITE = thenB.isConst() ? elseB : thenB;
792
1206
  TNode maybeITE = thenB.isConst() ? thenB : elseB;
793
794
603
  NodeVec* defChildren = computeConstantLeaves(definitelyITE);
795
603
  if (defChildren == NULL)
796
  {
797
    d_constantLeaves[ite] = NULL;
798
    return NULL;
799
  }
800
801
1206
  NodeVec scratch;
802
603
  NodeVec* maybeChildren = NULL;
803
603
  if (maybeITE.getKind() == kind::ITE)
804
  {
805
192
    maybeChildren = computeConstantLeaves(maybeITE);
806
  }
807
  else
808
  {
809
411
    scratch.push_back(maybeITE);
810
411
    maybeChildren = &scratch;
811
  }
812
603
  if (maybeChildren == NULL)
813
  {
814
    d_constantLeaves[ite] = NULL;
815
    return NULL;
816
  }
817
818
603
  NodeVec* both = new NodeVec(defChildren->size() + maybeChildren->size());
819
603
  d_allocatedConstantLeaves.push_back(both);
820
603
  NodeVec::iterator newEnd;
821
603
  newEnd = std::set_union(defChildren->begin(),
822
                          defChildren->end(),
823
                          maybeChildren->begin(),
824
                          maybeChildren->end(),
825
603
                          both->begin());
826
603
  both->resize(newEnd - both->begin());
827
603
  d_constantLeaves[ite] = both;
828
603
  return both;
829
}
830
831
// This is uncached! Better for protoyping or getting limited size examples
832
struct IteTreeSearchData
833
{
834
  set<Node> visited;
835
  set<Node> constants;
836
  set<Node> nonConstants;
837
  int maxConstants;
838
  int maxNonconstants;
839
  int maxDepth;
840
  bool failure;
841
  IteTreeSearchData()
842
      : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
843
  {
844
  }
845
};
846
void iteTreeSearch(Node e, int depth, IteTreeSearchData& search)
847
{
848
  if (search.maxDepth >= 0 && depth > search.maxDepth)
849
  {
850
    search.failure = true;
851
  }
852
  if (search.failure)
853
  {
854
    return;
855
  }
856
  if (search.visited.find(e) != search.visited.end())
857
  {
858
    return;
859
  }
860
  else
861
  {
862
    search.visited.insert(e);
863
  }
864
865
  if (e.isConst())
866
  {
867
    search.constants.insert(e);
868
    if (search.maxConstants >= 0
869
        && search.constants.size() > (unsigned)search.maxConstants)
870
    {
871
      search.failure = true;
872
    }
873
  }
874
  else if (e.getKind() == kind::ITE)
875
  {
876
    iteTreeSearch(e[1], depth + 1, search);
877
    iteTreeSearch(e[2], depth + 1, search);
878
  }
879
  else
880
  {
881
    search.nonConstants.insert(e);
882
    if (search.maxNonconstants >= 0
883
        && search.nonConstants.size() > (unsigned)search.maxNonconstants)
884
    {
885
      search.failure = true;
886
    }
887
  }
888
}
889
890
Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar)
891
{
892
  if (n == simpVar)
893
  {
894
    return replaceWith;
895
  }
896
  else if (n.getNumChildren() == 0)
897
  {
898
    return n;
899
  }
900
  Assert(n.getNumChildren() > 0);
901
  Assert(!n.isVar());
902
903
  pair<Node, Node> p = make_pair(n, replaceWith);
904
  if (d_replaceOverCache.find(p) != d_replaceOverCache.end())
905
  {
906
    return d_replaceOverCache[p];
907
  }
908
909
  NodeBuilder<> builder(n.getKind());
910
  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
911
  {
912
    builder << n.getOperator();
913
  }
914
  unsigned i = 0;
915
  for (; i < n.getNumChildren(); ++i)
916
  {
917
    Node newChild = replaceOver(n[i], replaceWith, simpVar);
918
    builder << newChild;
919
  }
920
  // Mark the substitution and continue
921
  Node result = builder;
922
  d_replaceOverCache[p] = result;
923
  return result;
924
}
925
926
Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar)
927
{
928
  if (e.getKind() == kind::ITE)
929
  {
930
    pair<Node, Node> p = make_pair(e, simpAtom);
931
    if (d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end())
932
    {
933
      return d_replaceOverTermIteCache[p];
934
    }
935
    Assert(!e.getType().isBoolean());
936
    Node cnd = e[0];
937
    Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar);
938
    Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar);
939
    Node newIte = cnd.iteNode(newThen, newElse);
940
    d_replaceOverTermIteCache[p] = newIte;
941
    return newIte;
942
  }
943
  else
944
  {
945
    return replaceOver(simpAtom, e, simpVar);
946
  }
947
}
948
949
Node ITESimplifier::attemptLiftEquality(TNode atom)
950
{
951
  if (atom.getKind() == kind::EQUAL)
952
  {
953
    TNode left = atom[0];
954
    TNode right = atom[1];
955
    if ((left.getKind() == kind::ITE || right.getKind() == kind::ITE)
956
        && !(left.getKind() == kind::ITE && right.getKind() == kind::ITE))
957
    {
958
      // exactly 1 is an ite
959
      TNode ite = left.getKind() == kind::ITE ? left : right;
960
      TNode notIte = left.getKind() == kind::ITE ? right : left;
961
962
      if (notIte == ite[1])
963
      {
964
        ++(d_statistics.d_exactMatchFold);
965
        return ite[0].iteNode(d_true, notIte.eqNode(ite[2]));
966
      }
967
      else if (notIte == ite[2])
968
      {
969
        ++(d_statistics.d_exactMatchFold);
970
        return ite[0].iteNode(notIte.eqNode(ite[1]), d_true);
971
      }
972
      if (notIte.isConst() && (ite[1].isConst() || ite[2].isConst()))
973
      {
974
        ++(d_statistics.d_exactMatchFold);
975
        return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2]));
976
      }
977
    }
978
  }
979
980
  // try a similar more relaxed version for non-equality operators
981
  if (atom.getMetaKind() == kind::metakind::OPERATOR
982
      && atom.getNumChildren() == 2 && !atom[1].getType().isBoolean())
983
  {
984
    TNode left = atom[0];
985
    TNode right = atom[1];
986
    if ((left.getKind() == kind::ITE || right.getKind() == kind::ITE)
987
        && !(left.getKind() == kind::ITE && right.getKind() == kind::ITE))
988
    {
989
      // exactly 1 is an ite
990
      bool leftIsIte = left.getKind() == kind::ITE;
991
      Node ite = leftIsIte ? left : right;
992
      Node notIte = leftIsIte ? right : left;
993
994
      if (notIte.isConst())
995
      {
996
        IteTreeSearchData search;
997
        search.maxNonconstants = 2;
998
        iteTreeSearch(ite, 0, search);
999
        if (!search.failure)
1000
        {
1001
          d_statistics.d_maxNonConstantsFolded.maxAssign(
1002
              search.nonConstants.size());
1003
          Debug("ite::simpite") << "used " << search.nonConstants.size()
1004
                                << " nonconstants" << endl;
1005
          NodeManager* nm = NodeManager::currentNM();
1006
          Node simpVar = getSimpVar(notIte.getType());
1007
          TNode newLeft = leftIsIte ? simpVar : notIte;
1008
          TNode newRight = leftIsIte ? notIte : simpVar;
1009
          Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
1010
1011
          ++(d_statistics.d_binaryPredFold);
1012
          return replaceOverTermIte(ite, newAtom, simpVar);
1013
        }
1014
      }
1015
    }
1016
  }
1017
1018
  // TODO "This is way too tailored. Must generalize!"
1019
  if (atom.getKind() == kind::EQUAL && atom.getNumChildren() == 2
1020
      && ite::isTermITE(atom[0]) && atom[1].getKind() == kind::MULT
1021
      && atom[1].getNumChildren() == 2 && atom[1][0].isConst()
1022
      && atom[1][0].getConst<Rational>().isNegativeOne()
1023
      && ite::isTermITE(atom[1][1])
1024
      && d_termITEHeight.termITEHeight(atom[0]) == 1
1025
      && d_termITEHeight.termITEHeight(atom[1][1]) == 1
1026
      && (atom[0][1].isConst() || atom[0][2].isConst())
1027
      && (atom[1][1][1].isConst() || atom[1][1][2].isConst()))
1028
  {
1029
    // expand all 4 cases
1030
1031
    Node negOne = atom[1][0];
1032
1033
    Node lite = atom[0];
1034
    Node lC = lite[0];
1035
    Node lT = lite[1];
1036
    Node lE = lite[2];
1037
1038
    NodeManager* nm = NodeManager::currentNM();
1039
    Node negRite = atom[1][1];
1040
    Node rC = negRite[0];
1041
    Node rT = nm->mkNode(kind::MULT, negOne, negRite[1]);
1042
    Node rE = nm->mkNode(kind::MULT, negOne, negRite[2]);
1043
1044
    // (ite lC lT lE) = (ite rC rT rE)
1045
    // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE))))
1046
    // (ite lc (ite rC (= lT rT) (= lT rE))
1047
    //         (ite rC (= lE rT) (= lE rE)))
1048
1049
    Node eqTT = lT.eqNode(rT);
1050
    Node eqTE = lT.eqNode(rE);
1051
    Node eqET = lE.eqNode(rT);
1052
    Node eqEE = lE.eqNode(rE);
1053
    Node thenLC = rC.iteNode(eqTT, eqTE);
1054
    Node elseLC = rC.iteNode(eqET, eqEE);
1055
    Node newIte = lC.iteNode(thenLC, elseLC);
1056
1057
    ++(d_statistics.d_specialEqualityFolds);
1058
    return newIte;
1059
  }
1060
  return Node::null();
1061
}
1062
1063
// Interesting classes of atoms:
1064
// 2. Contains constants and 1 constant term ite
1065
// 3. Contains 2 constant term ites
1066
729
Node ITESimplifier::transformAtom(TNode atom)
1067
{
1068
729
  if (!d_containsVisitor->containsTermITE(atom))
1069
  {
1070
    if (atom.getKind() == kind::EQUAL && atom[0].isConst() && atom[1].isConst())
1071
    {
1072
      // constant equality
1073
      return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]);
1074
    }
1075
    return Node::null();
1076
  }
1077
  else
1078
  {
1079
1458
    Node acr = attemptConstantRemoval(atom);
1080
729
    if (!acr.isNull())
1081
    {
1082
573
      return acr;
1083
    }
1084
    // Node ale = attemptLiftEquality(atom);
1085
    // if(!ale.isNull()){
1086
    //   //return ale;
1087
    // }
1088
156
    return Node::null();
1089
  }
1090
}
1091
1092
static unsigned numBranches = 0;
1093
static unsigned numFalseBranches = 0;
1094
static unsigned itesMade = 0;
1095
1096
67339
Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant)
1097
{
1098
  static int instance = 0;
1099
67339
  ++instance;
1100
134678
  Debug("ite::constantIteEqualsConstant")
1101
67339
      << instance << "constantIteEqualsConstant(" << cite << ", " << constant
1102
67339
      << ")" << endl;
1103
67339
  if (cite.isConst())
1104
  {
1105
45678
    Node res = (cite == constant) ? d_true : d_false;
1106
22839
    Debug("ite::constantIteEqualsConstant") << instance << "->" << res << endl;
1107
22839
    return res;
1108
  }
1109
89000
  std::pair<Node, Node> pair = make_pair(cite, constant);
1110
1111
  NodePairMap::const_iterator eq_pos =
1112
44500
      d_constantIteEqualsConstantCache.find(pair);
1113
44500
  if (eq_pos != d_constantIteEqualsConstantCache.end())
1114
  {
1115
5334
    Debug("ite::constantIteEqualsConstant")
1116
2667
        << instance << "->" << (*eq_pos).second << endl;
1117
2667
    return (*eq_pos).second;
1118
  }
1119
1120
41833
  ++d_citeEqConstApplications;
1121
1122
41833
  NodeVec* leaves = computeConstantLeaves(cite);
1123
41833
  Assert(leaves != NULL);
1124
41833
  if (std::binary_search(leaves->begin(), leaves->end(), constant))
1125
  {
1126
33383
    if (leaves->size() == 1)
1127
    {
1128
      // probably unreachable
1129
      d_constantIteEqualsConstantCache[pair] = d_true;
1130
      Debug("ite::constantIteEqualsConstant")
1131
          << instance << "->" << d_true << endl;
1132
      return d_true;
1133
    }
1134
    else
1135
    {
1136
33383
      Assert(cite.getKind() == kind::ITE);
1137
66766
      TNode cnd = cite[0];
1138
66766
      TNode tB = cite[1];
1139
66766
      TNode fB = cite[2];
1140
66766
      Node tEqs = constantIteEqualsConstant(tB, constant);
1141
66766
      Node fEqs = constantIteEqualsConstant(fB, constant);
1142
66766
      Node boolIte = cnd.iteNode(tEqs, fEqs);
1143
33383
      if (!(tEqs.isConst() || fEqs.isConst()))
1144
      {
1145
1924
        ++numBranches;
1146
      }
1147
33383
      if (!(tEqs == d_false || fEqs == d_false))
1148
      {
1149
2211
        ++numFalseBranches;
1150
      }
1151
33383
      ++itesMade;
1152
33383
      d_constantIteEqualsConstantCache[pair] = boolIte;
1153
      // Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte
1154
      // << endl;
1155
33383
      return boolIte;
1156
    }
1157
  }
1158
  else
1159
  {
1160
8450
    d_constantIteEqualsConstantCache[pair] = d_false;
1161
16900
    Debug("ite::constantIteEqualsConstant")
1162
8450
        << instance << "->" << d_false << endl;
1163
8450
    return d_false;
1164
  }
1165
}
1166
1167
573
Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite)
1168
{
1169
  // intersect the constant ite trees lcite and rcite
1170
1171
573
  if (lcite.isConst() || rcite.isConst())
1172
  {
1173
573
    bool lIsConst = lcite.isConst();
1174
1146
    TNode constant = lIsConst ? lcite : rcite;
1175
1146
    TNode cite = lIsConst ? rcite : lcite;
1176
1177
573
    (d_statistics.d_inSmaller) << 1;
1178
573
    unsigned preItesMade = itesMade;
1179
573
    unsigned preNumBranches = numBranches;
1180
573
    unsigned preNumFalseBranches = numFalseBranches;
1181
1146
    Node bterm = constantIteEqualsConstant(cite, constant);
1182
1146
    Debug("intersectConstantIte") << (numBranches - preNumBranches) << " "
1183
1146
                                  << (numFalseBranches - preNumFalseBranches)
1184
573
                                  << " " << (itesMade - preItesMade) << endl;
1185
573
    return bterm;
1186
  }
1187
  Assert(lcite.getKind() == kind::ITE);
1188
  Assert(rcite.getKind() == kind::ITE);
1189
1190
  NodeVec* leftValues = computeConstantLeaves(lcite);
1191
  NodeVec* rightValues = computeConstantLeaves(rcite);
1192
1193
  uint32_t smaller = std::min(leftValues->size(), rightValues->size());
1194
1195
  (d_statistics.d_inSmaller) << smaller;
1196
  NodeVec intersection(smaller, Node::null());
1197
  NodeVec::iterator newEnd;
1198
  newEnd = std::set_intersection(leftValues->begin(),
1199
                                 leftValues->end(),
1200
                                 rightValues->begin(),
1201
                                 rightValues->end(),
1202
                                 intersection.begin());
1203
  intersection.resize(newEnd - intersection.begin());
1204
  if (intersection.empty())
1205
  {
1206
    return d_false;
1207
  }
1208
  else
1209
  {
1210
    NodeBuilder<> nb(kind::OR);
1211
    NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
1212
    for (; it != end; ++it)
1213
    {
1214
      Node inBoth = *it;
1215
      Node lefteq = constantIteEqualsConstant(lcite, inBoth);
1216
      Node righteq = constantIteEqualsConstant(rcite, inBoth);
1217
      Node bothHold = lefteq.andNode(righteq);
1218
      nb << bothHold;
1219
    }
1220
    Node result = (nb.getNumChildren() > 1) ? (Node)nb : nb[0];
1221
    return result;
1222
  }
1223
}
1224
1225
Node ITESimplifier::attemptEagerRemoval(TNode atom)
1226
{
1227
  if (atom.getKind() == kind::EQUAL)
1228
  {
1229
    TNode left = atom[0];
1230
    TNode right = atom[1];
1231
    if ((left.isConst() && right.getKind() == kind::ITE && isConstantIte(right))
1232
        || (right.isConst() && left.getKind() == kind::ITE
1233
            && isConstantIte(left)))
1234
    {
1235
      TNode constant = left.isConst() ? left : right;
1236
      TNode cite = left.isConst() ? right : left;
1237
1238
      std::pair<Node, Node> pair = make_pair(cite, constant);
1239
      NodePairMap::const_iterator eq_pos =
1240
          d_constantIteEqualsConstantCache.find(pair);
1241
      if (eq_pos != d_constantIteEqualsConstantCache.end())
1242
      {
1243
        Node ret = (*eq_pos).second;
1244
        if (ret.isConst())
1245
        {
1246
          return ret;
1247
        }
1248
        else
1249
        {
1250
          return Node::null();
1251
        }
1252
      }
1253
1254
      NodeVec* leaves = computeConstantLeaves(cite);
1255
      Assert(leaves != NULL);
1256
      if (!std::binary_search(leaves->begin(), leaves->end(), constant))
1257
      {
1258
        d_constantIteEqualsConstantCache[pair] = d_false;
1259
        return d_false;
1260
      }
1261
    }
1262
  }
1263
  return Node::null();
1264
}
1265
1266
729
Node ITESimplifier::attemptConstantRemoval(TNode atom)
1267
{
1268
729
  if (atom.getKind() == kind::EQUAL)
1269
  {
1270
787
    TNode left = atom[0];
1271
787
    TNode right = atom[1];
1272
680
    if (isConstantIte(left) && isConstantIte(right))
1273
    {
1274
573
      return intersectConstantIte(left, right);
1275
    }
1276
  }
1277
156
  return Node::null();
1278
}
1279
1280
550
bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid)
1281
{
1282
550
  Assert((e.getKind() == kind::ITE && !e.getType().isBoolean())
1283
         || theory::Theory::theoryOf(e) != theory::THEORY_BOOL);
1284
550
  if (e.isConst())
1285
  {
1286
27
    return true;
1287
  }
1288
1289
523
  unordered_map<Node, bool, NodeHashFunction>::iterator it;
1290
523
  it = d_leavesConstCache.find(e);
1291
523
  if (it != d_leavesConstCache.end())
1292
  {
1293
122
    return (*it).second;
1294
  }
1295
1296
401
  if (!containsTermITE(e) && theory::Theory::isLeafOf(e, tid))
1297
  {
1298
34
    d_leavesConstCache[e] = false;
1299
34
    return false;
1300
  }
1301
1302
367
  Assert(e.getNumChildren() > 0);
1303
367
  size_t k = 0, sz = e.getNumChildren();
1304
1305
367
  if (e.getKind() == kind::ITE)
1306
  {
1307
161
    k = 1;
1308
  }
1309
1310
421
  for (; k < sz; ++k)
1311
  {
1312
394
    if (!leavesAreConst(e[k], tid))
1313
    {
1314
367
      d_leavesConstCache[e] = false;
1315
367
      return false;
1316
    }
1317
  }
1318
  d_leavesConstCache[e] = true;
1319
  return true;
1320
}
1321
1322
Node ITESimplifier::simpConstants(TNode simpContext,
1323
                                  TNode iteNode,
1324
                                  TNode simpVar)
1325
{
1326
  NodePairMap::iterator it;
1327
  it = d_simpConstCache.find(pair<Node, Node>(simpContext, iteNode));
1328
  if (it != d_simpConstCache.end())
1329
  {
1330
    return (*it).second;
1331
  }
1332
1333
  if (iteNode.getKind() == kind::ITE)
1334
  {
1335
    NodeBuilder<> builder(kind::ITE);
1336
    builder << iteNode[0];
1337
    unsigned i = 1;
1338
    for (; i < iteNode.getNumChildren(); ++i)
1339
    {
1340
      Node n = simpConstants(simpContext, iteNode[i], simpVar);
1341
      if (n.isNull())
1342
      {
1343
        return n;
1344
      }
1345
      builder << n;
1346
    }
1347
    // Mark the substitution and continue
1348
    Node result = builder;
1349
    result = theory::Rewriter::rewrite(result);
1350
    d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
1351
    return result;
1352
  }
1353
1354
  if (!containsTermITE(iteNode))
1355
  {
1356
    Node n =
1357
        theory::Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
1358
    d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
1359
    return n;
1360
  }
1361
1362
  Node iteNode2;
1363
  Node simpVar2;
1364
  d_simpContextCache.clear();
1365
  Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
1366
  if (!simpContext2.isNull())
1367
  {
1368
    Assert(!iteNode2.isNull());
1369
    simpContext2 = simpContext.substitute(simpVar, simpContext2);
1370
    Node n = simpConstants(simpContext2, iteNode2, simpVar2);
1371
    if (n.isNull())
1372
    {
1373
      return n;
1374
    }
1375
    d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
1376
    return n;
1377
  }
1378
  return Node();
1379
}
1380
1381
Node ITESimplifier::getSimpVar(TypeNode t)
1382
{
1383
  std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
1384
  it = d_simpVars.find(t);
1385
  if (it != d_simpVars.end())
1386
  {
1387
    return (*it).second;
1388
  }
1389
  else
1390
  {
1391
    Node var = NodeManager::currentNM()->mkSkolem(
1392
        "iteSimp", t, "is a variable resulting from ITE simplification");
1393
    d_simpVars[t] = var;
1394
    return var;
1395
  }
1396
}
1397
1398
Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
1399
{
1400
  NodeMap::iterator it;
1401
  it = d_simpContextCache.find(c);
1402
  if (it != d_simpContextCache.end())
1403
  {
1404
    return (*it).second;
1405
  }
1406
1407
  if (!containsTermITE(c))
1408
  {
1409
    d_simpContextCache[c] = c;
1410
    return c;
1411
  }
1412
1413
  if (c.getKind() == kind::ITE && !c.getType().isBoolean())
1414
  {
1415
    // Currently only support one ite node in a simp context
1416
    // Return Null if more than one is found
1417
    if (!iteNode.isNull())
1418
    {
1419
      return Node();
1420
    }
1421
    simpVar = getSimpVar(c.getType());
1422
    if (simpVar.isNull())
1423
    {
1424
      return Node();
1425
    }
1426
    d_simpContextCache[c] = simpVar;
1427
    iteNode = c;
1428
    return simpVar;
1429
  }
1430
1431
  NodeBuilder<> builder(c.getKind());
1432
  if (c.getMetaKind() == kind::metakind::PARAMETERIZED)
1433
  {
1434
    builder << c.getOperator();
1435
  }
1436
  unsigned i = 0;
1437
  for (; i < c.getNumChildren(); ++i)
1438
  {
1439
    Node newChild = createSimpContext(c[i], iteNode, simpVar);
1440
    if (newChild.isNull())
1441
    {
1442
      return newChild;
1443
    }
1444
    builder << newChild;
1445
  }
1446
  // Mark the substitution and continue
1447
  Node result = builder;
1448
  d_simpContextCache[c] = result;
1449
  return result;
1450
}
1451
typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
1452
40741410
void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached)
1453
{
1454
40741410
  if (visited.find(x) != visited.end())
1455
  {
1456
37305643
    return;
1457
  }
1458
3435767
  visited.insert(x);
1459
3435767
  if (x.getKind() == k)
1460
  {
1461
1086180
    ++reached;
1462
  }
1463
44176031
  for (unsigned i = 0, N = x.getNumChildren(); i < N; ++i)
1464
  {
1465
40740264
    countReachable_(x[i], k, visited, reached);
1466
  }
1467
}
1468
1469
1146
uint32_t countReachable(TNode x, Kind k)
1470
{
1471
2292
  NodeSet visited;
1472
1146
  uint32_t reached = 0;
1473
1146
  countReachable_(x, k, visited, reached);
1474
2292
  return reached;
1475
}
1476
1477
729
Node ITESimplifier::simpITEAtom(TNode atom)
1478
{
1479
  static int CVC4_UNUSED instance = 0;
1480
729
  Debug("ite::atom") << "still simplifying " << (++instance) << endl;
1481
1458
  Node attempt = transformAtom(atom);
1482
729
  Debug("ite::atom") << "  finished " << instance << endl;
1483
729
  if (!attempt.isNull())
1484
  {
1485
1146
    Node rewritten = theory::Rewriter::rewrite(attempt);
1486
1146
    Debug("ite::print-success")
1487
573
        << instance << " "
1488
1146
        << "rewriting " << countReachable(rewritten, kind::ITE) << " from "
1489
1146
        << countReachable(atom, kind::ITE) << endl
1490
573
        << "\t rewritten " << rewritten << endl
1491
573
        << "\t input " << atom << endl;
1492
573
    return rewritten;
1493
  }
1494
1495
156
  if (leavesAreConst(atom))
1496
  {
1497
    Node iteNode;
1498
    Node simpVar;
1499
    d_simpContextCache.clear();
1500
    Node simpContext = createSimpContext(atom, iteNode, simpVar);
1501
    if (!simpContext.isNull())
1502
    {
1503
      if (iteNode.isNull())
1504
      {
1505
        Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
1506
        ++(d_statistics.d_unexpected);
1507
        Debug("ite::simpite") << instance << " "
1508
                              << "how about?" << atom << endl;
1509
        Debug("ite::simpite") << instance << " "
1510
                              << "\t" << simpContext << endl;
1511
        return theory::Rewriter::rewrite(simpContext);
1512
      }
1513
      Node n = simpConstants(simpContext, iteNode, simpVar);
1514
      if (!n.isNull())
1515
      {
1516
        ++(d_statistics.d_unexpected);
1517
        Debug("ite::simpite") << instance << " "
1518
                              << "here?" << atom << endl;
1519
        Debug("ite::simpite") << instance << " "
1520
                              << "\t" << n << endl;
1521
        return n;
1522
      }
1523
    }
1524
  }
1525
156
  if (Debug.isOn("ite::simpite"))
1526
  {
1527
    if (countReachable(atom, kind::ITE) > 0)
1528
    {
1529
      Debug("ite::simpite") << instance << " "
1530
                            << "remaining " << atom << endl;
1531
    }
1532
  }
1533
156
  ++(d_statistics.d_unsimplified);
1534
156
  return atom;
1535
}
1536
1537
11456
struct preprocess_stack_element
1538
{
1539
  TNode d_node;
1540
  bool d_children_added;
1541
2454
  preprocess_stack_element(TNode node) : d_node(node), d_children_added(false)
1542
  {
1543
2454
  }
1544
}; /* struct preprocess_stack_element */
1545
1546
1
Node ITESimplifier::simpITE(TNode assertion)
1547
{
1548
  // Do a topological sort of the subexpressions and substitute them
1549
2
  vector<preprocess_stack_element> toVisit;
1550
1
  toVisit.push_back(assertion);
1551
1552
  static int call = 0;
1553
1
  ++call;
1554
1
  int iteration = 0;
1555
1556
8745
  while (!toVisit.empty())
1557
  {
1558
4372
    iteration++;
1559
    // cout << "call  " << call << " : " << iteration << endl;
1560
    // The current node we are processing
1561
4372
    preprocess_stack_element& stackHead = toVisit.back();
1562
8208
    TNode current = stackHead.d_node;
1563
1564
    // If node has no ITE's or already in the cache we're done, pop from the
1565
    // stack
1566
9269
    if (current.getNumChildren() == 0
1567
13641
        || (theory::Theory::theoryOf(current) != theory::THEORY_BOOL
1568
6014
            && !containsTermITE(current)))
1569
    {
1570
525
      d_simpITECache[current] = current;
1571
525
      ++(d_statistics.d_simpITEVisits);
1572
525
      toVisit.pop_back();
1573
525
      continue;
1574
    }
1575
1576
3847
    NodeMap::iterator find = d_simpITECache.find(current);
1577
3858
    if (find != d_simpITECache.end())
1578
    {
1579
11
      toVisit.pop_back();
1580
11
      continue;
1581
    }
1582
1583
    // Not yet substituted, so process
1584
3836
    if (stackHead.d_children_added)
1585
    {
1586
      // Children have been processed, so substitute
1587
3836
      NodeBuilder<> builder(current.getKind());
1588
1918
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
1589
      {
1590
        builder << current.getOperator();
1591
      }
1592
6869
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
1593
      {
1594
4951
        Assert(d_simpITECache.find(current[i]) != d_simpITECache.end());
1595
9902
        Node child = current[i];
1596
9902
        Node childRes = d_simpITECache[current[i]];
1597
4951
        builder << childRes;
1598
      }
1599
      // Mark the substitution and continue
1600
3836
      Node result = builder;
1601
1602
      // If this is an atom, we process it
1603
5754
      if (theory::Theory::theoryOf(result) != theory::THEORY_BOOL
1604
5754
          && result.getType().isBoolean())
1605
      {
1606
729
        result = simpITEAtom(result);
1607
      }
1608
1609
      // if(current != result && result.isConst()){
1610
      //   static int instance = 0;
1611
      //   //cout << instance << " " << result << current << endl;
1612
      // }
1613
1614
1918
      result = theory::Rewriter::rewrite(result);
1615
1918
      d_simpITECache[current] = result;
1616
1918
      ++(d_statistics.d_simpITEVisits);
1617
1918
      toVisit.pop_back();
1618
    }
1619
    else
1620
    {
1621
      // Mark that we have added the children if any
1622
1918
      if (current.getNumChildren() > 0)
1623
      {
1624
1918
        stackHead.d_children_added = true;
1625
        // We need to add the children
1626
6869
        for (TNode::iterator child_it = current.begin();
1627
6869
             child_it != current.end();
1628
             ++child_it)
1629
        {
1630
9902
          TNode childNode = *child_it;
1631
4951
          NodeMap::iterator childFind = d_simpITECache.find(childNode);
1632
4951
          if (childFind == d_simpITECache.end())
1633
          {
1634
2453
            toVisit.push_back(childNode);
1635
          }
1636
        }
1637
      }
1638
      else
1639
      {
1640
        // No children, so we're done
1641
        d_simpITECache[current] = current;
1642
        ++(d_statistics.d_simpITEVisits);
1643
        toVisit.pop_back();
1644
      }
1645
    }
1646
  }
1647
2
  return d_simpITECache[assertion];
1648
}
1649
1650
ITECareSimplifier::ITECareSimplifier() : d_careSetsOutstanding(0), d_usedSets()
1651
{
1652
  d_true = NodeManager::currentNM()->mkConst<bool>(true);
1653
  d_false = NodeManager::currentNM()->mkConst<bool>(false);
1654
}
1655
1656
ITECareSimplifier::~ITECareSimplifier()
1657
{
1658
  Assert(d_usedSets.empty());
1659
  Assert(d_careSetsOutstanding == 0);
1660
}
1661
1662
void ITECareSimplifier::clear()
1663
{
1664
  Assert(d_usedSets.empty());
1665
  Assert(d_careSetsOutstanding == 0);
1666
}
1667
1668
ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
1669
{
1670
  if (d_usedSets.empty())
1671
  {
1672
    d_careSetsOutstanding++;
1673
    return ITECareSimplifier::CareSetPtr::mkNew(*this);
1674
  }
1675
  else
1676
  {
1677
    ITECareSimplifier::CareSetPtr cs =
1678
        ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
1679
    cs.getCareSet().clear();
1680
    d_usedSets.pop_back();
1681
    return cs;
1682
  }
1683
}
1684
1685
void ITECareSimplifier::updateQueue(CareMap& queue,
1686
                                    TNode e,
1687
                                    ITECareSimplifier::CareSetPtr& careSet)
1688
{
1689
  CareMap::iterator it = queue.find(e), iend = queue.end();
1690
  if (it != iend)
1691
  {
1692
    set<Node>& cs2 = (*it).second.getCareSet();
1693
    ITECareSimplifier::CareSetPtr csNew = getNewSet();
1694
    set_intersection(careSet.getCareSet().begin(),
1695
                     careSet.getCareSet().end(),
1696
                     cs2.begin(),
1697
                     cs2.end(),
1698
                     inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
1699
    (*it).second = csNew;
1700
  }
1701
  else
1702
  {
1703
    queue[e] = careSet;
1704
  }
1705
}
1706
1707
Node ITECareSimplifier::substitute(TNode e,
1708
                                   TNodeMap& substTable,
1709
                                   TNodeMap& cache)
1710
{
1711
  TNodeMap::iterator it = cache.find(e), iend = cache.end();
1712
  if (it != iend)
1713
  {
1714
    return it->second;
1715
  }
1716
1717
  // do substitution?
1718
  it = substTable.find(e);
1719
  iend = substTable.end();
1720
  if (it != iend)
1721
  {
1722
    Node result = substitute(it->second, substTable, cache);
1723
    cache[e] = result;
1724
    return result;
1725
  }
1726
1727
  size_t sz = e.getNumChildren();
1728
  if (sz == 0)
1729
  {
1730
    cache[e] = e;
1731
    return e;
1732
  }
1733
1734
  NodeBuilder<> builder(e.getKind());
1735
  if (e.getMetaKind() == kind::metakind::PARAMETERIZED)
1736
  {
1737
    builder << e.getOperator();
1738
  }
1739
  for (unsigned i = 0; i < e.getNumChildren(); ++i)
1740
  {
1741
    builder << substitute(e[i], substTable, cache);
1742
  }
1743
1744
  Node result = builder;
1745
  // it = substTable.find(result);
1746
  // if (it != iend) {
1747
  //   result = substitute(it->second, substTable, cache);
1748
  // }
1749
  cache[e] = result;
1750
  return result;
1751
}
1752
1753
Node ITECareSimplifier::simplifyWithCare(TNode e)
1754
{
1755
  TNodeMap substTable;
1756
1757
  /* This extra block is to trigger the destructors for cs and cs2
1758
   * before starting garbage collection.
1759
   */
1760
  {
1761
    CareMap queue;
1762
    CareMap::iterator it;
1763
    ITECareSimplifier::CareSetPtr cs = getNewSet();
1764
    ITECareSimplifier::CareSetPtr cs2;
1765
    queue[e] = cs;
1766
1767
    TNode v;
1768
    bool done;
1769
    unsigned i;
1770
1771
    while (!queue.empty())
1772
    {
1773
      it = queue.end();
1774
      --it;
1775
      v = it->first;
1776
      cs = it->second;
1777
      set<Node>& css = cs.getCareSet();
1778
      queue.erase(v);
1779
1780
      done = false;
1781
      set<Node>::iterator iCare, iCareEnd = css.end();
1782
1783
      switch (v.getKind())
1784
      {
1785
        case kind::ITE:
1786
        {
1787
          iCare = css.find(v[0]);
1788
          if (iCare != iCareEnd)
1789
          {
1790
            Assert(substTable.find(v) == substTable.end());
1791
            substTable[v] = v[1];
1792
            updateQueue(queue, v[1], cs);
1793
            done = true;
1794
            break;
1795
          }
1796
          else
1797
          {
1798
            iCare = css.find(v[0].negate());
1799
            if (iCare != iCareEnd)
1800
            {
1801
              Assert(substTable.find(v) == substTable.end());
1802
              substTable[v] = v[2];
1803
              updateQueue(queue, v[2], cs);
1804
              done = true;
1805
              break;
1806
            }
1807
          }
1808
          updateQueue(queue, v[0], cs);
1809
          cs2 = getNewSet();
1810
          cs2.getCareSet() = css;
1811
          cs2.getCareSet().insert(v[0]);
1812
          updateQueue(queue, v[1], cs2);
1813
          cs2 = getNewSet();
1814
          cs2.getCareSet() = css;
1815
          cs2.getCareSet().insert(v[0].negate());
1816
          updateQueue(queue, v[2], cs2);
1817
          done = true;
1818
          break;
1819
        }
1820
        case kind::AND:
1821
        {
1822
          for (i = 0; i < v.getNumChildren(); ++i)
1823
          {
1824
            iCare = css.find(v[i].negate());
1825
            if (iCare != iCareEnd)
1826
            {
1827
              Assert(substTable.find(v) == substTable.end());
1828
              substTable[v] = d_false;
1829
              done = true;
1830
              break;
1831
            }
1832
          }
1833
          if (done) break;
1834
1835
          Assert(v.getNumChildren() > 1);
1836
          updateQueue(queue, v[0], cs);
1837
          cs2 = getNewSet();
1838
          cs2.getCareSet() = css;
1839
          cs2.getCareSet().insert(v[0]);
1840
          for (i = 1; i < v.getNumChildren(); ++i)
1841
          {
1842
            updateQueue(queue, v[i], cs2);
1843
          }
1844
          done = true;
1845
          break;
1846
        }
1847
        case kind::OR:
1848
        {
1849
          for (i = 0; i < v.getNumChildren(); ++i)
1850
          {
1851
            iCare = css.find(v[i]);
1852
            if (iCare != iCareEnd)
1853
            {
1854
              Assert(substTable.find(v) == substTable.end());
1855
              substTable[v] = d_true;
1856
              done = true;
1857
              break;
1858
            }
1859
          }
1860
          if (done) break;
1861
1862
          Assert(v.getNumChildren() > 1);
1863
          updateQueue(queue, v[0], cs);
1864
          cs2 = getNewSet();
1865
          cs2.getCareSet() = css;
1866
          cs2.getCareSet().insert(v[0].negate());
1867
          for (i = 1; i < v.getNumChildren(); ++i)
1868
          {
1869
            updateQueue(queue, v[i], cs2);
1870
          }
1871
          done = true;
1872
          break;
1873
        }
1874
        default: break;
1875
      }
1876
1877
      if (done)
1878
      {
1879
        continue;
1880
      }
1881
1882
      for (i = 0; i < v.getNumChildren(); ++i)
1883
      {
1884
        updateQueue(queue, v[i], cs);
1885
      }
1886
    }
1887
  }
1888
  /* Perform garbage collection. */
1889
  while (!d_usedSets.empty())
1890
  {
1891
    CareSetPtrVal* used = d_usedSets.back();
1892
    d_usedSets.pop_back();
1893
    Assert(used->safeToGarbageCollect());
1894
    delete used;
1895
    Assert(d_careSetsOutstanding > 0);
1896
    d_careSetsOutstanding--;
1897
  }
1898
1899
  TNodeMap cache;
1900
  return substitute(e, substTable, cache);
1901
}
1902
1903
ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew(
1904
    ITECareSimplifier& simp)
1905
{
1906
  CareSetPtrVal* val = new CareSetPtrVal(simp);
1907
  return CareSetPtr(val);
1908
}
1909
1910
}  // namespace util
1911
}  // namespace preprocessing
1912
158770927
}  // namespace CVC4