GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/unconstrained_simplifier.cpp Lines: 337 404 83.4 %
Date: 2021-03-23 Branches: 725 1721 42.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file unconstrained_simplifier.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Clark Barrett, Andres Noetzli, Andrew Reynolds
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 based on unconstrained variables
13
 **
14
 ** This module implements a preprocessing phase which replaces certain
15
 ** "unconstrained" expressions by variables.  Based on Roberto
16
 ** Bruttomesso's PhD thesis.
17
 **/
18
19
#include "preprocessing/passes/unconstrained_simplifier.h"
20
21
#include "expr/dtype.h"
22
#include "preprocessing/assertion_pipeline.h"
23
#include "preprocessing/preprocessing_pass_context.h"
24
#include "smt/logic_exception.h"
25
#include "smt/smt_statistics_registry.h"
26
#include "theory/logic_info.h"
27
#include "theory/rewriter.h"
28
29
namespace CVC4 {
30
namespace preprocessing {
31
namespace passes {
32
33
using namespace std;
34
using namespace CVC4::theory;
35
36
8997
UnconstrainedSimplifier::UnconstrainedSimplifier(
37
8997
    PreprocessingPassContext* preprocContext)
38
    : PreprocessingPass(preprocContext, "unconstrained-simplifier"),
39
      d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
40
8997
      d_context(preprocContext->getDecisionContext()),
41
17994
      d_substitutions(preprocContext->getDecisionContext())
42
{
43
8997
  smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim);
44
8997
}
45
46
26982
UnconstrainedSimplifier::~UnconstrainedSimplifier()
47
{
48
8994
  smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim);
49
17988
}
50
51
444956
struct unc_preprocess_stack_element
52
{
53
  TNode node;
54
  TNode parent;
55
1007
  unc_preprocess_stack_element(TNode n) : node(n) {}
56
128367
  unc_preprocess_stack_element(TNode n, TNode p) : node(n), parent(p) {}
57
}; /* struct unc_preprocess_stack_element */
58
59
1007
void UnconstrainedSimplifier::visitAll(TNode assertion)
60
{
61
  // Do a topological sort of the subexpressions and substitute them
62
2014
  vector<unc_preprocess_stack_element> toVisit;
63
1007
  toVisit.push_back(assertion);
64
65
259755
  while (!toVisit.empty())
66
  {
67
    // The current node we are processing
68
170476
    TNode current = toVisit.back().node;
69
170476
    TNode parent = toVisit.back().parent;
70
129374
    toVisit.pop_back();
71
72
129374
    TNodeCountMap::iterator find = d_visited.find(current);
73
129374
    if (find != d_visited.end())
74
    {
75
88272
      if (find->second == 1)
76
      {
77
11411
        d_visitedOnce.erase(current);
78
11411
        if (current.isVar())
79
        {
80
3045
          d_unconstrained.erase(current);
81
        }
82
        else
83
        {
84
          // Also erase the children from the visited-once set when we visit a
85
          // node a second time, otherwise variables in this node are not
86
          // erased from the set of unconstrained variables.
87
20136
          for (TNode childNode : current)
88
          {
89
11770
            toVisit.push_back(unc_preprocess_stack_element(childNode, current));
90
          }
91
        }
92
      }
93
88272
      ++find->second;
94
88272
      continue;
95
    }
96
97
41102
    d_visited[current] = 1;
98
41102
    d_visitedOnce[current] = parent;
99
100
41102
    if (current.getNumChildren() == 0)
101
    {
102
14164
      if (current.getKind() == kind::VARIABLE
103
7082
          || current.getKind() == kind::SKOLEM)
104
      {
105
4147
        d_unconstrained.insert(current);
106
      }
107
    }
108
34020
    else if (current.isClosure())
109
    {
110
      // Throw an exception. This should never happen in practice unless the
111
      // user specifically enabled unconstrained simplification in an illegal
112
      // logic.
113
      throw LogicException(
114
          "Cannot use unconstrained simplification in this logic, due to "
115
          "(possibly internally introduced) quantified formula.");
116
    }
117
    else
118
    {
119
150617
      for (TNode childNode : current)
120
      {
121
116597
        toVisit.push_back(unc_preprocess_stack_element(childNode, current));
122
      }
123
    }
124
  }
125
1007
}
126
127
164
Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
128
{
129
  Node n = NodeManager::currentNM()->mkSkolem(
130
      "unconstrained",
131
      t,
132
      "a new var introduced because of unconstrained variable "
133
164
          + var.toString());
134
164
  return n;
135
}
136
137
122
void UnconstrainedSimplifier::processUnconstrained()
138
{
139
122
  NodeManager* nm = NodeManager::currentNM();
140
141
244
  vector<TNode> workList(d_unconstrained.begin(), d_unconstrained.end());
142
244
  Node currentSub;
143
244
  TNode parent;
144
  bool swap;
145
  bool isSigned;
146
  bool strict;
147
244
  vector<TNode> delayQueueLeft;
148
244
  vector<Node> delayQueueRight;
149
150
244
  TNode current = workList.back();
151
122
  workList.pop_back();
152
  for (;;)
153
  {
154
1348
    Assert(d_visitedOnce.find(current) != d_visitedOnce.end());
155
1348
    parent = d_visitedOnce[current];
156
1348
    if (!parent.isNull())
157
    {
158
1311
      swap = isSigned = strict = false;
159
1311
      bool checkParent = false;
160
1311
      switch (parent.getKind())
161
      {
162
        // If-then-else operator - any two unconstrained children makes the
163
        // parent unconstrained
164
94
        case kind::ITE:
165
        {
166
94
          Assert(parent[0] == current || parent[1] == current
167
                 || parent[2] == current);
168
          bool uCond =
169
282
              parent[0] == current
170
282
              || d_unconstrained.find(parent[0]) != d_unconstrained.end();
171
          bool uThen =
172
282
              parent[1] == current
173
282
              || d_unconstrained.find(parent[1]) != d_unconstrained.end();
174
          bool uElse =
175
282
              parent[2] == current
176
282
              || d_unconstrained.find(parent[2]) != d_unconstrained.end();
177
94
          if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse))
178
          {
179
126
            if (d_unconstrained.find(parent) == d_unconstrained.end()
180
84
                && !d_substitutions.hasSubstitution(parent))
181
            {
182
29
              ++d_numUnconstrainedElim;
183
29
              if (uThen)
184
              {
185
20
                if (parent[1] != current)
186
                {
187
15
                  if (parent[1].isVar())
188
                  {
189
15
                    currentSub = parent[1];
190
                  }
191
                  else
192
                  {
193
                    Assert(d_substitutions.hasSubstitution(parent[1]));
194
                    currentSub = d_substitutions.apply(parent[1]);
195
                  }
196
                }
197
5
                else if (currentSub.isNull())
198
                {
199
4
                  currentSub = current;
200
                }
201
              }
202
9
              else if (parent[2] != current)
203
              {
204
5
                if (parent[2].isVar())
205
                {
206
5
                  currentSub = parent[2];
207
                }
208
                else
209
                {
210
                  Assert(d_substitutions.hasSubstitution(parent[2]));
211
                  currentSub = d_substitutions.apply(parent[2]);
212
                }
213
              }
214
4
              else if (currentSub.isNull())
215
              {
216
4
                currentSub = current;
217
              }
218
29
              current = parent;
219
            }
220
            else
221
            {
222
13
              currentSub = Node();
223
            }
224
          }
225
52
          else if (uCond)
226
          {
227
48
            Cardinality card = parent.getType().getCardinality();
228
72
            if (card.isFinite() && !card.isLargeFinite()
229
63
                && card.getFiniteCardinality() == 2)
230
            {
231
              // Special case: condition is unconstrained, then and else are
232
              // different, and total cardinality of the type is 2, then the
233
              // result is unconstrained
234
6
              Node test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
235
3
              if (test == nm->mkConst<bool>(false))
236
              {
237
3
                ++d_numUnconstrainedElim;
238
3
                if (currentSub.isNull())
239
                {
240
                  currentSub = current;
241
                }
242
3
                currentSub = newUnconstrainedVar(parent.getType(), currentSub);
243
3
                current = parent;
244
              }
245
            }
246
          }
247
94
          break;
248
        }
249
250
        // Comparisons that return a different type - assuming domains are
251
        // larger than 1, any unconstrained child makes parent unconstrained as
252
        // well
253
62
        case kind::EQUAL:
254
62
          if (parent[0].getType() != parent[1].getType())
255
          {
256
2
            TNode other = (parent[0] == current) ? parent[1] : parent[0];
257
2
            if (current.getType().isSubtypeOf(other.getType()))
258
            {
259
2
              break;
260
            }
261
          }
262
60
          if (parent[0].getType().getCardinality().isOne())
263
          {
264
            break;
265
          }
266
60
          if (parent[0].getType().isDatatype())
267
          {
268
            TypeNode tn = parent[0].getType();
269
            const DType& dt = tn.getDType();
270
            if (dt.isRecursiveSingleton(tn))
271
            {
272
              // domain size may be 1
273
              break;
274
            }
275
          }
276
60
          if (parent[0].getType().isBoolean())
277
          {
278
1
            checkParent = true;
279
1
            break;
280
          }
281
          CVC4_FALLTHROUGH;
282
        case kind::BITVECTOR_COMP:
283
        case kind::LT:
284
        case kind::LEQ:
285
        case kind::GT:
286
        case kind::GEQ:
287
        {
288
130
          if (d_unconstrained.find(parent) == d_unconstrained.end()
289
130
              && !d_substitutions.hasSubstitution(parent))
290
          {
291
65
            ++d_numUnconstrainedElim;
292
65
            Assert(parent[0] != parent[1]
293
                   && (parent[0] == current || parent[1] == current));
294
65
            if (currentSub.isNull())
295
            {
296
18
              currentSub = current;
297
            }
298
65
            currentSub = newUnconstrainedVar(parent.getType(), currentSub);
299
65
            current = parent;
300
          }
301
          else
302
          {
303
            currentSub = Node();
304
          }
305
65
          break;
306
        }
307
308
        // Unary operators that propagate unconstrainedness
309
44
        case kind::NOT:
310
        case kind::BITVECTOR_NOT:
311
        case kind::BITVECTOR_NEG:
312
        case kind::UMINUS:
313
44
          ++d_numUnconstrainedElim;
314
44
          Assert(parent[0] == current);
315
44
          if (currentSub.isNull())
316
          {
317
2
            currentSub = current;
318
          }
319
44
          current = parent;
320
44
          break;
321
322
        // Unary operators that propagate unconstrainedness and return a
323
        // different type
324
6
        case kind::BITVECTOR_EXTRACT:
325
6
          ++d_numUnconstrainedElim;
326
6
          Assert(parent[0] == current);
327
6
          if (currentSub.isNull())
328
          {
329
4
            currentSub = current;
330
          }
331
6
          currentSub = newUnconstrainedVar(parent.getType(), currentSub);
332
6
          current = parent;
333
6
          break;
334
335
        // Operators returning same type requiring all children to be
336
        // unconstrained
337
42
        case kind::AND:
338
        case kind::OR:
339
        case kind::IMPLIES:
340
        case kind::BITVECTOR_AND:
341
        case kind::BITVECTOR_OR:
342
        case kind::BITVECTOR_NAND:
343
        case kind::BITVECTOR_NOR:
344
        {
345
42
          bool allUnconstrained = true;
346
99
          for (TNode child : parent)
347
          {
348
80
            if (d_unconstrained.find(child) == d_unconstrained.end())
349
            {
350
23
              allUnconstrained = false;
351
23
              break;
352
            }
353
          }
354
42
          if (allUnconstrained)
355
          {
356
19
            checkParent = true;
357
          }
358
        }
359
42
        break;
360
361
        // Require all children to be unconstrained and different
362
28
        case kind::BITVECTOR_SHL:
363
        case kind::BITVECTOR_LSHR:
364
        case kind::BITVECTOR_ASHR:
365
        case kind::BITVECTOR_UDIV:
366
        case kind::BITVECTOR_UREM:
367
        case kind::BITVECTOR_SDIV:
368
        case kind::BITVECTOR_SREM:
369
        case kind::BITVECTOR_SMOD:
370
        {
371
28
          bool allUnconstrained = true;
372
28
          bool allDifferent = true;
373
70
          for (TNode::iterator child_it = parent.begin();
374
70
               child_it != parent.end();
375
               ++child_it)
376
          {
377
49
            if (d_unconstrained.find(*child_it) == d_unconstrained.end())
378
            {
379
7
              allUnconstrained = false;
380
7
              break;
381
            }
382
63
            for (TNode::iterator child_it2 = child_it + 1;
383
63
                 child_it2 != parent.end();
384
                 ++child_it2)
385
            {
386
21
              if (*child_it == *child_it2)
387
              {
388
                allDifferent = false;
389
                break;
390
              }
391
            }
392
          }
393
28
          if (allUnconstrained && allDifferent)
394
          {
395
21
            checkParent = true;
396
          }
397
28
          break;
398
        }
399
400
        // Requires all children to be unconstrained and different, and returns
401
        // a different type
402
20
        case kind::BITVECTOR_CONCAT:
403
        {
404
20
          bool allUnconstrained = true;
405
20
          bool allDifferent = true;
406
31
          for (TNode::iterator child_it = parent.begin();
407
31
               child_it != parent.end();
408
               ++child_it)
409
          {
410
30
            if (d_unconstrained.find(*child_it) == d_unconstrained.end())
411
            {
412
19
              allUnconstrained = false;
413
19
              break;
414
            }
415
21
            for (TNode::iterator child_it2 = child_it + 1;
416
21
                 child_it2 != parent.end();
417
                 ++child_it2)
418
            {
419
10
              if (*child_it == *child_it2)
420
              {
421
                allDifferent = false;
422
                break;
423
              }
424
            }
425
          }
426
20
          if (allUnconstrained && allDifferent)
427
          {
428
2
            if (d_unconstrained.find(parent) == d_unconstrained.end()
429
2
                && !d_substitutions.hasSubstitution(parent))
430
            {
431
1
              ++d_numUnconstrainedElim;
432
1
              if (currentSub.isNull())
433
              {
434
                currentSub = current;
435
              }
436
1
              currentSub = newUnconstrainedVar(parent.getType(), currentSub);
437
1
              current = parent;
438
            }
439
            else
440
            {
441
              currentSub = Node();
442
            }
443
          }
444
        }
445
20
        break;
446
447
        // N-ary operators returning same type requiring at least one child to
448
        // be unconstrained
449
3
        case kind::PLUS:
450
        case kind::MINUS:
451
3
          if (current.getType().isInteger() && !parent.getType().isInteger())
452
          {
453
            break;
454
          }
455
          CVC4_FALLTHROUGH;
456
        case kind::XOR:
457
        case kind::BITVECTOR_XOR:
458
        case kind::BITVECTOR_XNOR:
459
        case kind::BITVECTOR_PLUS:
460
9
        case kind::BITVECTOR_SUB: checkParent = true; break;
461
462
        // Multiplication/division: must be non-integer and other operand must
463
        // be non-zero
464
5
        case kind::MULT:
465
        case kind::DIVISION:
466
        {
467
5
          Assert(parent.getNumChildren() == 2);
468
10
          TNode other;
469
5
          if (parent[0] == current)
470
          {
471
            other = parent[1];
472
          }
473
          else
474
          {
475
5
            Assert(parent[1] == current);
476
5
            other = parent[0];
477
          }
478
5
          if (d_unconstrained.find(other) != d_unconstrained.end())
479
          {
480
            if (d_unconstrained.find(parent) == d_unconstrained.end()
481
                && !d_substitutions.hasSubstitution(parent))
482
            {
483
              if (current.getType().isInteger() && other.getType().isInteger())
484
              {
485
                Assert(parent.getKind() == kind::DIVISION
486
                       || parent.getType().isInteger());
487
                if (parent.getKind() == kind::DIVISION)
488
                {
489
                  break;
490
                }
491
              }
492
              ++d_numUnconstrainedElim;
493
              if (currentSub.isNull())
494
              {
495
                currentSub = current;
496
              }
497
              current = parent;
498
            }
499
            else
500
            {
501
              currentSub = Node();
502
            }
503
          }
504
          else
505
          {
506
            // if only the denominator of a division is unconstrained, can't
507
            // set it to 0 so the result is not unconstrained
508
5
            if (parent.getKind() == kind::DIVISION && current == parent[1])
509
            {
510
              break;
511
            }
512
            // if we are an integer, the only way we are unconstrained is if
513
            // we are a MULT by -1
514
5
            if (current.getType().isInteger())
515
            {
516
              // div/mult by 1 should have been simplified
517
3
              Assert(other != nm->mkConst<Rational>(1));
518
              // div by -1 should have been simplified
519
3
              if (other != nm->mkConst<Rational>(-1))
520
              {
521
2
                break;
522
              }
523
              else
524
              {
525
1
                Assert(parent.getKind() == kind::MULT);
526
1
                Assert(parent.getType().isInteger());
527
              }
528
            }
529
            else
530
            {
531
              // TODO(#2377): could build ITE here
532
4
              Node test = other.eqNode(nm->mkConst<Rational>(0));
533
2
              if (Rewriter::rewrite(test) != nm->mkConst<bool>(false))
534
              {
535
                break;
536
              }
537
            }
538
3
            ++d_numUnconstrainedElim;
539
3
            if (currentSub.isNull())
540
            {
541
3
              currentSub = current;
542
            }
543
3
            current = parent;
544
          }
545
3
          break;
546
        }
547
548
        // Bitvector MULT - current must only appear once in the children:
549
        // all other children must be unconstrained or odd
550
867
        case kind::BITVECTOR_MULT:
551
        {
552
867
          bool found = false;
553
867
          bool done = false;
554
555
870
          for (TNode child : parent)
556
          {
557
2277
            if (child == current)
558
            {
559
705
              if (found)
560
              {
561
                done = true;
562
                break;
563
              }
564
705
              found = true;
565
705
              continue;
566
            }
567
867
            else if (d_unconstrained.find(child) == d_unconstrained.end())
568
            {
569
              Node extractOp =
570
866
                  nm->mkConst<BitVectorExtract>(BitVectorExtract(0, 0));
571
866
              vector<Node> children;
572
865
              children.push_back(child);
573
866
              Node test = nm->mkNode(extractOp, children);
574
866
              BitVector one(1, unsigned(1));
575
865
              test = test.eqNode(nm->mkConst<BitVector>(one));
576
865
              if (Rewriter::rewrite(test) != nm->mkConst<bool>(true))
577
              {
578
864
                done = true;
579
864
                break;
580
              }
581
            }
582
          }
583
867
          if (done)
584
          {
585
864
            break;
586
          }
587
3
          checkParent = true;
588
3
          break;
589
        }
590
591
        // Uninterpreted function - if domain is infinite, no quantifiers are
592
        // used, and any child is unconstrained, result is unconstrained
593
31
        case kind::APPLY_UF:
594
62
          if (d_preprocContext->getLogicInfo().isQuantified()
595
62
              || !current.getType().getCardinality().isInfinite())
596
          {
597
            break;
598
          }
599
62
          if (d_unconstrained.find(parent) == d_unconstrained.end()
600
62
              && !d_substitutions.hasSubstitution(parent))
601
          {
602
31
            ++d_numUnconstrainedElim;
603
31
            if (currentSub.isNull())
604
            {
605
              currentSub = current;
606
            }
607
            // always introduce a new variable; it is unsound to try to reuse
608
            // currentSub as the variable, see issue #4469.
609
31
            currentSub = newUnconstrainedVar(parent.getType(), currentSub);
610
31
            current = parent;
611
          }
612
          else
613
          {
614
            currentSub = Node();
615
          }
616
31
          break;
617
618
        // Array select - if array is unconstrained, so is result
619
20
        case kind::SELECT:
620
20
          if (parent[0] == current)
621
          {
622
18
            ++d_numUnconstrainedElim;
623
18
            Assert(current.getType().isArray());
624
18
            if (currentSub.isNull())
625
            {
626
18
              currentSub = current;
627
            }
628
54
            currentSub = newUnconstrainedVar(
629
36
                current.getType().getArrayConstituentType(), currentSub);
630
18
            current = parent;
631
          }
632
20
          break;
633
634
        // Array store - if both store and value are unconstrained, so is
635
        // resulting store
636
12
        case kind::STORE:
637
36
          if (((parent[0] == current
638
24
                && d_unconstrained.find(parent[2]) != d_unconstrained.end())
639
60
               || (parent[2] == current
640
12
                   && d_unconstrained.find(parent[0])
641
12
                          != d_unconstrained.end())))
642
          {
643
            if (d_unconstrained.find(parent) == d_unconstrained.end()
644
                && !d_substitutions.hasSubstitution(parent))
645
            {
646
              ++d_numUnconstrainedElim;
647
              if (parent[0] != current)
648
              {
649
                if (parent[0].isVar())
650
                {
651
                  currentSub = parent[0];
652
                }
653
                else
654
                {
655
                  Assert(d_substitutions.hasSubstitution(parent[0]));
656
                  currentSub = d_substitutions.apply(parent[0]);
657
                }
658
              }
659
              else if (currentSub.isNull())
660
              {
661
                currentSub = current;
662
              }
663
              current = parent;
664
            }
665
            else
666
            {
667
              currentSub = Node();
668
            }
669
          }
670
12
          break;
671
672
        // Bit-vector comparisons: replace with new Boolean variable, but have
673
        // to also conjoin with a side condition as there is always one case
674
        // when the comparison is forced to be false
675
44
        case kind::BITVECTOR_ULT:
676
        case kind::BITVECTOR_UGE:
677
        case kind::BITVECTOR_UGT:
678
        case kind::BITVECTOR_ULE:
679
        case kind::BITVECTOR_SLT:
680
        case kind::BITVECTOR_SGE:
681
        case kind::BITVECTOR_SGT:
682
        case kind::BITVECTOR_SLE:
683
        {
684
          // Tuples over (signed, swap, strict).
685
44
          switch (parent.getKind())
686
          {
687
            case kind::BITVECTOR_UGE: break;
688
22
            case kind::BITVECTOR_ULT: strict = true; break;
689
            case kind::BITVECTOR_ULE: swap = true; break;
690
            case kind::BITVECTOR_UGT:
691
              swap = true;
692
              strict = true;
693
              break;
694
            case kind::BITVECTOR_SGE: isSigned = true; break;
695
22
            case kind::BITVECTOR_SLT:
696
22
              isSigned = true;
697
22
              strict = true;
698
22
              break;
699
            case kind::BITVECTOR_SLE:
700
              isSigned = true;
701
              swap = true;
702
              break;
703
            case kind::BITVECTOR_SGT:
704
              isSigned = true;
705
              swap = true;
706
              strict = true;
707
              break;
708
            default: Unreachable();
709
          }
710
88
          TNode other;
711
44
          bool left = false;
712
44
          if (parent[0] == current)
713
          {
714
21
            other = parent[1];
715
21
            left = true;
716
          }
717
          else
718
          {
719
23
            Assert(parent[1] == current);
720
23
            other = parent[0];
721
          }
722
44
          if (d_unconstrained.find(other) != d_unconstrained.end())
723
          {
724
18
            if (d_unconstrained.find(parent) == d_unconstrained.end()
725
18
                && !d_substitutions.hasSubstitution(parent))
726
            {
727
5
              ++d_numUnconstrainedElim;
728
5
              if (currentSub.isNull())
729
              {
730
4
                currentSub = current;
731
              }
732
5
              currentSub = newUnconstrainedVar(parent.getType(), currentSub);
733
5
              current = parent;
734
            }
735
            else
736
            {
737
4
              currentSub = Node();
738
            }
739
          }
740
          else
741
          {
742
35
            unsigned size = current.getType().getBitVectorSize();
743
            BitVector bv =
744
52
                isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1))
745
83
                         : BitVector(size, unsigned(0));
746
35
            if (swap == left)
747
            {
748
19
              bv = ~bv;
749
            }
750
35
            if (currentSub.isNull())
751
            {
752
27
              currentSub = current;
753
            }
754
35
            currentSub = newUnconstrainedVar(parent.getType(), currentSub);
755
35
            current = parent;
756
            Node test =
757
66
                Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
758
35
            if (test == nm->mkConst<bool>(false))
759
            {
760
4
              break;
761
            }
762
31
            currentSub = strict ? currentSub.andNode(test.notNode())
763
                                : currentSub.orNode(test);
764
            // Delay adding this substitution - see comment at end of function
765
31
            delayQueueLeft.push_back(current);
766
31
            delayQueueRight.push_back(currentSub);
767
31
            currentSub = Node();
768
31
            parent = TNode();
769
          }
770
40
          break;
771
        }
772
773
        // Do nothing
774
21
        case kind::BITVECTOR_SIGN_EXTEND:
775
        case kind::BITVECTOR_ZERO_EXTEND:
776
        case kind::BITVECTOR_REPEAT:
777
        case kind::BITVECTOR_ROTATE_LEFT:
778
        case kind::BITVECTOR_ROTATE_RIGHT:
779
780
21
        default: break;
781
      }
782
1311
      if (checkParent)
783
      {
784
        // run for various cases from above
785
106
        if (d_unconstrained.find(parent) == d_unconstrained.end()
786
106
            && !d_substitutions.hasSubstitution(parent))
787
        {
788
37
          ++d_numUnconstrainedElim;
789
37
          if (currentSub.isNull())
790
          {
791
16
            currentSub = current;
792
          }
793
37
          current = parent;
794
        }
795
        else
796
        {
797
16
          currentSub = Node();
798
        }
799
      }
800
1557
      if (current == parent && d_visited[parent] == 1)
801
      {
802
246
        d_unconstrained.insert(parent);
803
246
        continue;
804
      }
805
    }
806
1102
    if (!currentSub.isNull())
807
    {
808
138
      Trace("unc-simp")
809
69
          << "UnconstrainedSimplifier::processUnconstrained: introduce "
810
69
          << currentSub << " for " << current << ", parent " << parent
811
69
          << std::endl;
812
69
      Assert(currentSub.isVar());
813
69
      d_substitutions.addSubstitution(current, currentSub, false);
814
    }
815
1102
    if (workList.empty())
816
    {
817
122
      break;
818
    }
819
980
    current = workList.back();
820
980
    currentSub = Node();
821
980
    workList.pop_back();
822
1226
  }
823
244
  TNode left;
824
244
  Node right;
825
  // All substitutions except those arising from bitvector comparisons are
826
  // substitutions t -> x where x is a variable.  This allows us to build the
827
  // substitution very quickly (never invalidating the substitution cache).
828
  // Bitvector comparisons are more complicated and may require
829
  // back-substitution and cache-invalidation.  So we do these last.
830
184
  while (!delayQueueLeft.empty())
831
  {
832
31
    left = delayQueueLeft.back();
833
31
    if (!d_substitutions.hasSubstitution(left))
834
    {
835
30
      right = d_substitutions.apply(delayQueueRight.back());
836
30
      d_substitutions.addSubstitution(delayQueueLeft.back(), right);
837
    }
838
31
    delayQueueLeft.pop_back();
839
31
    delayQueueRight.pop_back();
840
  }
841
122
}
842
843
411
PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
844
    AssertionPipeline* assertionsToPreprocess)
845
{
846
411
  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
847
848
411
  const std::vector<Node>& assertions = assertionsToPreprocess->ref();
849
850
411
  d_context->push();
851
852
1418
  for (const Node& assertion : assertions)
853
  {
854
1007
    visitAll(assertion);
855
  }
856
857
411
  if (!d_unconstrained.empty())
858
  {
859
122
    processUnconstrained();
860
    //    d_substitutions.print(CVC4Message.getStream());
861
420
    for (size_t i = 0, asize = assertions.size(); i < asize; ++i)
862
    {
863
596
      Node a = assertions[i];
864
596
      Node as = Rewriter::rewrite(d_substitutions.apply(a));
865
      // replace the assertion
866
298
      assertionsToPreprocess->replace(i, as);
867
    }
868
  }
869
870
  // to clear substitutions map
871
411
  d_context->pop();
872
873
411
  d_visited.clear();
874
411
  d_visitedOnce.clear();
875
411
  d_unconstrained.clear();
876
877
411
  return PreprocessingPassResult::NO_CONFLICT;
878
}
879
880
881
}  // namespace passes
882
}  // namespace preprocessing
883
26685
}  // namespace CVC4