src/preprocessing/passes/unconstrained_simplifier.cpp

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