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