src/theory/unconstrained_simplifier.cpp

   1 /*********************                                                        */
   2 /*! \file unconstrained_simplifier.cpp
   3  ** \verbatim
   4  ** Original author: Clark Barrett
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Tim King, Morgan Deters
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Simplifications based on unconstrained variables
  13  **
  14  ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions
  15  ** by variables.  Based on Roberto Bruttomesso's PhD thesis.
  16  **/
  17
  18
  19 #include "theory/unconstrained_simplifier.h"
  20 #include "theory/rewriter.h"
  21 #include "theory/logic_info.h"
  22
  23 using namespace std;
  24 using namespace CVC4;
  25 using namespace theory;
  26
  27
  28 UnconstrainedSimplifier::UnconstrainedSimplifier(context::Context* context,
  29                                                  const LogicInfo& logicInfo)
  30   : d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
  31     d_context(context), d_substitutions(context), d_logicInfo(logicInfo)
  32 {
  33   StatisticsRegistry::registerStat(&d_numUnconstrainedElim);
  34 }
  35
  36
  37 UnconstrainedSimplifier::~UnconstrainedSimplifier()
  38 {
  39   StatisticsRegistry::unregisterStat(&d_numUnconstrainedElim);
  40 }
  41
  42
  43 struct unc_preprocess_stack_element {
  44   TNode node;
  45   TNode parent;
  46   unc_preprocess_stack_element(TNode n) : node(n) {}
  47   unc_preprocess_stack_element(TNode n, TNode p) : node(n), parent(p) {}
  48 };/* struct unc_preprocess_stack_element */
  49
  50
  51 void UnconstrainedSimplifier::visitAll(TNode assertion)
  52 {
  53   // Do a topological sort of the subexpressions and substitute them
  54   vector<unc_preprocess_stack_element> toVisit;
  55   toVisit.push_back(assertion);
  56
  57   while (!toVisit.empty())
  58   {
  59     // The current node we are processing
  60     unc_preprocess_stack_element& stackHead = toVisit.back();
  61     toVisit.pop_back();
  62     TNode current = stackHead.node;
  63
  64     TNodeCountMap::iterator find = d_visited.find(current);
  65     if (find != d_visited.end()) {
  66       if (find->second == 1) {
  67         d_visitedOnce.erase(current);
  68         if (current.isVar()) {
  69           d_unconstrained.erase(current);
  70         }
  71       }
  72       ++find->second;
  73       continue;
  74     }
  75
  76     d_visited[current] = 1;
  77     d_visitedOnce[current] = stackHead.parent;
  78
  79     if (current.getNumChildren() == 0) {
  80       if (current.isVar()) {
  81         d_unconstrained.insert(current);
  82       }
  83     }
  84     else {
  85       for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
  86         TNode childNode = *child_it;
  87         toVisit.push_back(unc_preprocess_stack_element(childNode, current));
  88       }
  89     }
  90   }
  91 }
  92
  93 Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
  94 {
  95   Node n = NodeManager::currentNM()->mkSkolem("unconstrained", t, "a new var introduced because of unconstrained variable " + var.toString());
  96   return n;
  97 }
  98
  99
 100 void UnconstrainedSimplifier::processUnconstrained()
 101 {
 102   TNodeSet::iterator it = d_unconstrained.begin(), iend = d_unconstrained.end();
 103   vector<TNode> workList;
 104   for ( ; it != iend; ++it) {
 105     workList.push_back(*it);
 106   }
 107   Node currentSub;
 108   TNode parent;
 109   bool swap;
 110   bool isSigned;
 111   bool strict;
 112   vector<TNode> delayQueueLeft;
 113   vector<Node> delayQueueRight;
 114
 115   TNode current = workList.back();
 116   workList.pop_back();
 117   for (;;) {
 118     Assert(d_visitedOnce.find(current) != d_visitedOnce.end());
 119     parent = d_visitedOnce[current];
 120     if (!parent.isNull()) {
 121       swap = isSigned = strict = false;
 122       switch (parent.getKind()) {
 123
 124         // If-then-else operator - any two unconstrained children makes the parent unconstrained
 125         case kind::ITE: {
 126           Assert(parent[0] == current || parent[1] == current || parent[2] == current);
 127           bool uCond = parent[0] == current || d_unconstrained.find(parent[0]) != d_unconstrained.end();
 128           bool uThen = parent[1] == current || d_unconstrained.find(parent[1]) != d_unconstrained.end();
 129           bool uElse = parent[2] == current || d_unconstrained.find(parent[2]) != d_unconstrained.end();
 130           if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse)) {
 131             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 132                 !d_substitutions.hasSubstitution(parent)) {
 133               ++d_numUnconstrainedElim;
 134               if (uThen) {
 135                 if (parent[1] != current) {
 136                   if (parent[1].isVar()) {
 137                     currentSub = parent[1];
 138                   }
 139                   else {
 140                     Assert(d_substitutions.hasSubstitution(parent[1]));
 141                     currentSub = d_substitutions.apply(parent[1]);
 142                   }
 143                 }
 144                 else if (currentSub.isNull()) {
 145                   currentSub = current;
 146                 }
 147               }
 148               else if (parent[2] != current) {
 149                 if (parent[2].isVar()) {
 150                   currentSub = parent[2];
 151                 }
 152                 else {
 153                   Assert(d_substitutions.hasSubstitution(parent[2]));
 154                   currentSub = d_substitutions.apply(parent[2]);
 155                 }
 156               }
 157               else if (currentSub.isNull()) {
 158                 currentSub = current;
 159               }
 160               current = parent;
 161             }
 162             else {
 163               currentSub = Node();
 164             }
 165           }
 166           else if (uCond) {
 167             Cardinality card = parent.getType().getCardinality();
 168             if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) {
 169               // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result
 170               // is unconstrained
 171               Node test;
 172               if (parent.getType().isBoolean()) {
 173                 test = Rewriter::rewrite(parent[1].iffNode(parent[2]));
 174               }
 175               else {
 176                 test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
 177               }
 178               if (test == NodeManager::currentNM()->mkConst<bool>(false)) {
 179                 ++d_numUnconstrainedElim;
 180                 if (currentSub.isNull()) {
 181                   currentSub = current;
 182                 }
 183                 currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 184                 current = parent;
 185               }
 186             }
 187           }
 188           break;
 189         }
 190
 191         // Comparisons that return a different type - assuming domains are larger than 1, any
 192         // unconstrained child makes parent unconstrained as well
 193         case kind::EQUAL:
 194           if (parent[0].getType() != parent[1].getType()) {
 195             TNode other = (parent[0] == current) ? parent[1] : parent[0];
 196             if (current.getType().isSubtypeOf(other.getType())) {
 197               break;
 198             }
 199           }
 200         case kind::BITVECTOR_COMP:
 201         case kind::LT:
 202         case kind::LEQ:
 203         case kind::GT:
 204         case kind::GEQ:
 205         {
 206           if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 207               !d_substitutions.hasSubstitution(parent)) {
 208             ++d_numUnconstrainedElim;
 209             Assert(parent[0] != parent[1] &&
 210                    (parent[0] == current || parent[1] == current));
 211             if (currentSub.isNull()) {
 212               currentSub = current;
 213             }
 214             currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 215             current = parent;
 216           }
 217           else {
 218             currentSub = Node();
 219           }
 220           break;
 221         }
 222
 223         // Unary operators that propagate unconstrainedness
 224         case kind::NOT:
 225         case kind::BITVECTOR_NOT:
 226         case kind::BITVECTOR_NEG:
 227         case kind::UMINUS:
 228           ++d_numUnconstrainedElim;
 229           Assert(parent[0] == current);
 230           if (currentSub.isNull()) {
 231             currentSub = current;
 232           }
 233           current = parent;
 234           break;
 235
 236         // Unary operators that propagate unconstrainedness and return a different type
 237         case kind::BITVECTOR_EXTRACT:
 238           ++d_numUnconstrainedElim;
 239           Assert(parent[0] == current);
 240           if (currentSub.isNull()) {
 241             currentSub = current;
 242           }
 243           currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 244           current = parent;
 245           break;
 246
 247         // Operators returning same type requiring all children to be unconstrained
 248         case kind::AND:
 249         case kind::OR:
 250         case kind::IMPLIES:
 251         case kind::BITVECTOR_AND:
 252         case kind::BITVECTOR_OR:
 253         case kind::BITVECTOR_NAND:
 254         case kind::BITVECTOR_NOR:
 255         {
 256           bool allUnconstrained = true;
 257           for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
 258             if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
 259               allUnconstrained = false;
 260               break;
 261             }
 262           }
 263           if (allUnconstrained) {
 264             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 265                 !d_substitutions.hasSubstitution(parent)) {
 266               ++d_numUnconstrainedElim;
 267               if (currentSub.isNull()) {
 268                 currentSub = current;
 269               }
 270               current = parent;
 271             }
 272             else {
 273               currentSub = Node();
 274             }
 275           }
 276         }
 277         break;
 278
 279         // Require all children to be unconstrained and different
 280         case kind::BITVECTOR_SHL:
 281         case kind::BITVECTOR_LSHR:
 282         case kind::BITVECTOR_ASHR:
 283         case kind::BITVECTOR_UDIV:
 284         case kind::BITVECTOR_UREM:
 285         case kind::BITVECTOR_SDIV:
 286         case kind::BITVECTOR_SREM:
 287         case kind::BITVECTOR_SMOD: {
 288           bool allUnconstrained = true;
 289           bool allDifferent = true;
 290           for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
 291             if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
 292               allUnconstrained = false;
 293               break;
 294             }
 295             for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) {
 296               if (*child_it == *child_it2) {
 297                 allDifferent = false;
 298                 break;
 299               }
 300             }
 301           }
 302           if (allUnconstrained && allDifferent) {
 303             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 304                 !d_substitutions.hasSubstitution(parent)) {
 305               ++d_numUnconstrainedElim;
 306               if (currentSub.isNull()) {
 307                 currentSub = current;
 308               }
 309               current = parent;
 310             }
 311             else {
 312               currentSub = Node();
 313             }
 314           }
 315           break;
 316         }
 317
 318         // Requires all children to be unconstrained and different, and returns a different type
 319         case kind::BITVECTOR_CONCAT:
 320         {
 321           bool allUnconstrained = true;
 322           bool allDifferent = true;
 323           for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
 324             if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
 325               allUnconstrained = false;
 326               break;
 327             }
 328             for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) {
 329               if (*child_it == *child_it2) {
 330                 allDifferent = false;
 331                 break;
 332               }
 333             }
 334           }
 335           if (allUnconstrained && allDifferent) {
 336             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 337                 !d_substitutions.hasSubstitution(parent)) {
 338               ++d_numUnconstrainedElim;
 339               if (currentSub.isNull()) {
 340                 currentSub = current;
 341               }
 342               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 343               current = parent;
 344             }
 345             else {
 346               currentSub = Node();
 347             }
 348           }
 349         }
 350         break;
 351
 352         // N-ary operators returning same type requiring at least one child to be unconstrained
 353         case kind::PLUS:
 354         case kind::MINUS:
 355           if (current.getType().isInteger() &&
 356               !parent.getType().isInteger()) {
 357             break;
 358           }
 359         case kind::IFF:
 360         case kind::XOR:
 361         case kind::BITVECTOR_XOR:
 362         case kind::BITVECTOR_XNOR:
 363         case kind::BITVECTOR_PLUS:
 364         case kind::BITVECTOR_SUB:
 365           if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 366               !d_substitutions.hasSubstitution(parent)) {
 367             ++d_numUnconstrainedElim;
 368             if (currentSub.isNull()) {
 369               currentSub = current;
 370             }
 371             current = parent;
 372           }
 373           else {
 374             currentSub = Node();
 375           }
 376           break;
 377
 378         // Multiplication/division: must be non-integer and other operand must be non-zero
 379         case kind::MULT: {
 380         case kind::DIVISION:
 381           Assert(parent.getNumChildren() == 2);
 382           TNode other;
 383           if (parent[0] == current) {
 384             other = parent[1];
 385           }
 386           else {
 387             Assert(parent[1] == current);
 388             other = parent[0];
 389           }
 390           if (d_unconstrained.find(other) != d_unconstrained.end()) {
 391             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 392                 !d_substitutions.hasSubstitution(parent)) {
 393               if (current.getType().isInteger() && other.getType().isInteger()) {
 394                 Assert(parent.getKind() == kind::DIVISION || parent.getType().isInteger());
 395                 if (parent.getKind() == kind::DIVISION) {
 396                   break;
 397                 }
 398               }
 399               ++d_numUnconstrainedElim;
 400               if (currentSub.isNull()) {
 401                 currentSub = current;
 402               }
 403               current = parent;
 404             }
 405             else {
 406               currentSub = Node();
 407             }
 408           }
 409           else {
 410             // if only the denominator of a division is unconstrained, can't set it to 0 so the result is not unconstrained
 411             if (parent.getKind() == kind::DIVISION && current == parent[1]) {
 412               break;
 413             }
 414             NodeManager* nm = NodeManager::currentNM();
 415             // if we are an integer, the only way we are unconstrained is if we are a MULT by -1
 416             if (current.getType().isInteger()) {
 417               // div/mult by 1 should have been simplified
 418               Assert(other != nm->mkConst<Rational>(1));
 419               if (other == nm->mkConst<Rational>(-1)) {
 420                 // div by -1 should have been simplified
 421                 Assert(parent.getKind() == kind::MULT);
 422                 Assert(parent.getType().isInteger());
 423               }
 424               else {
 425                 break;
 426               }
 427             }
 428             else {
 429               // TODO: could build ITE here
 430               Node test = other.eqNode(nm->mkConst<Rational>(0));
 431               if (Rewriter::rewrite(test) != nm->mkConst<bool>(false)) {
 432                 break;
 433               }
 434             }
 435             ++d_numUnconstrainedElim;
 436             if (currentSub.isNull()) {
 437               currentSub = current;
 438             }
 439             current = parent;
 440           }
 441           break;
 442         }
 443
 444         // Bitvector MULT - current must only appear once in the children:
 445         // all other children must be unconstrained or odd
 446         case kind::BITVECTOR_MULT:
 447         {
 448           bool found = false;
 449           bool done = false;
 450           for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
 451             if ((*child_it) == current) {
 452               if (found) {
 453                 done = true;
 454                 break;
 455               }
 456               found = true;
 457               continue;
 458             }
 459             else if (d_unconstrained.find(*child_it) != d_unconstrained.end()) {
 460               continue;
 461             }
 462             else {
 463               NodeManager* nm = NodeManager::currentNM();
 464               Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0));
 465               vector<Node> children;
 466               children.push_back(*child_it);
 467               Node test = nm->mkNode(extractOp, children);
 468               BitVector one(1,unsigned(1));
 469               test = test.eqNode(nm->mkConst<BitVector>(one));
 470               if (Rewriter::rewrite(test) != nm->mkConst<bool>(true)) {
 471                 done = true;
 472                 break;
 473               }
 474             }
 475           }
 476           if (done) {
 477             break;
 478           }
 479           if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 480               !d_substitutions.hasSubstitution(parent)) {
 481             ++d_numUnconstrainedElim;
 482             if (currentSub.isNull()) {
 483               currentSub = current;
 484             }
 485             current = parent;
 486           }
 487           else {
 488             currentSub = Node();
 489           }
 490           break;
 491         }
 492
 493         // Uninterpreted function - if domain is infinite, no quantifiers are used, and any child is unconstrained, result is unconstrained
 494         case kind::APPLY_UF:
 495           if (d_logicInfo.isQuantified() || !current.getType().getCardinality().isInfinite()) {
 496             break;
 497           }
 498           if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 499               !d_substitutions.hasSubstitution(parent)) {
 500             ++d_numUnconstrainedElim;
 501             if (currentSub.isNull()) {
 502               currentSub = current;
 503             }
 504             if (parent.getType() != current.getType()) {
 505               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 506             }
 507             current = parent;
 508           }
 509           else {
 510             currentSub = Node();
 511           }
 512           break;
 513
 514         // Array select - if array is unconstrained, so is result
 515         case kind::SELECT:
 516           if (parent[0] == current) {
 517             ++d_numUnconstrainedElim;
 518             Assert(current.getType().isArray());
 519             if (currentSub.isNull()) {
 520               currentSub = current;
 521             }
 522             currentSub = newUnconstrainedVar(current.getType().getArrayConstituentType(), currentSub);
 523             current = parent;
 524           }
 525           break;
 526
 527         // Array store - if both store and value are unconstrained, so is resulting store
 528         case kind::STORE:
 529           if (((parent[0] == current &&
 530                 d_unconstrained.find(parent[2]) != d_unconstrained.end()) ||
 531                (parent[2] == current &&
 532                 d_unconstrained.find(parent[0]) != d_unconstrained.end()))) {
 533             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 534                 !d_substitutions.hasSubstitution(parent)) {
 535               ++d_numUnconstrainedElim;
 536               if (parent[0] != current) {
 537                 if (parent[0].isVar()) {
 538                   currentSub = parent[0];
 539                 }
 540                 else {
 541                   Assert(d_substitutions.hasSubstitution(parent[0]));
 542                   currentSub = d_substitutions.apply(parent[0]);
 543                 }
 544               }
 545               else if (currentSub.isNull()) {
 546                 currentSub = current;
 547               }
 548               current = parent;
 549             }
 550             else {
 551               currentSub = Node();
 552             }
 553           }
 554           break;
 555
 556         // Bit-vector comparisons: replace with new Boolean variable, but have to also conjoin with a side condition
 557         // as there is always one case when the comparison is forced to be false
 558         case kind::BITVECTOR_ULT:
 559           strict = true;
 560         case kind::BITVECTOR_UGE:
 561           goto bvineq;
 562
 563         case kind::BITVECTOR_UGT:
 564           strict = true;
 565         case kind::BITVECTOR_ULE:
 566           swap = true;
 567           goto bvineq;
 568
 569         case kind::BITVECTOR_SLT:
 570           strict = true;
 571         case kind::BITVECTOR_SGE:
 572           isSigned = true;
 573           goto bvineq;
 574
 575         case kind::BITVECTOR_SGT:
 576           strict = true;
 577         case kind::BITVECTOR_SLE:
 578           isSigned = true;
 579           swap = true;
 580
 581         bvineq: {
 582           TNode other;
 583           bool left = false;
 584           if (parent[0] == current) {
 585             other = parent[1];
 586             left = true;
 587           }
 588           else {
 589             Assert(parent[1] == current);
 590             other = parent[0];
 591           }
 592           if (d_unconstrained.find(other) != d_unconstrained.end()) {
 593             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 594                 !d_substitutions.hasSubstitution(parent)) {
 595               ++d_numUnconstrainedElim;
 596               if (currentSub.isNull()) {
 597                 currentSub = current;
 598               }
 599               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 600               current = parent;
 601             }
 602             else {
 603               currentSub = Node();
 604             }
 605           }
 606           else {
 607             unsigned size = current.getType().getBitVectorSize();
 608             BitVector bv = isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) : BitVector(size, unsigned(0));
 609             if (swap == left) {
 610               bv = ~bv;
 611             }
 612             if (currentSub.isNull()) {
 613               currentSub = current;
 614             }
 615             currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 616             current = parent;
 617             NodeManager* nm = NodeManager::currentNM();
 618             Node test = Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
 619             if (test == nm->mkConst<bool>(false)) {
 620               break;
 621             }
 622             if (strict) {
 623               currentSub = currentSub.andNode(test.notNode());
 624             }
 625             else {
 626               currentSub = currentSub.orNode(test);
 627             }
 628             // Delay adding this substitution - see comment at end of function
 629             delayQueueLeft.push_back(current);
 630             delayQueueRight.push_back(currentSub);
 631             currentSub = Node();
 632             parent = TNode();
 633           }
 634           break;
 635         }
 636
 637         // These should have been rewritten up front
 638         case kind::BITVECTOR_REPEAT:
 639         case kind::BITVECTOR_ZERO_EXTEND:
 640         case kind::BITVECTOR_ROTATE_LEFT:
 641         case kind::BITVECTOR_ROTATE_RIGHT:
 642           Unreachable();
 643           break;
 644
 645         // Do nothing
 646         case kind::BITVECTOR_SIGN_EXTEND:
 647         default:
 648           break;
 649       }
 650       if (current == parent && d_visited[parent] == 1) {
 651         d_unconstrained.insert(parent);
 652         continue;
 653       }
 654     }
 655     if (!currentSub.isNull()) {
 656       Assert(currentSub.isVar());
 657       d_substitutions.addSubstitution(current, currentSub, false);
 658     }
 659     if (workList.empty()) {
 660       break;
 661     }
 662     current = workList.back();
 663     currentSub = Node();
 664     workList.pop_back();
 665   }
 666   TNode left;
 667   Node right;
 668   // All substitutions except those arising from bitvector comparisons are
 669   // substitutions t -> x where x is a variable.  This allows us to build the
 670   // substitution very quickly (never invalidating the substitution cache).
 671   // Bitvector comparisons are more complicated and may require
 672   // back-substitution and cache-invalidation.  So we do these last.
 673   while (!delayQueueLeft.empty()) {
 674     left = delayQueueLeft.back();
 675     if (!d_substitutions.hasSubstitution(left)) {
 676       right = d_substitutions.apply(delayQueueRight.back());
 677       d_substitutions.addSubstitution(delayQueueLeft.back(), right);
 678     }
 679     delayQueueLeft.pop_back();
 680     delayQueueRight.pop_back();
 681   }
 682 }
 683
 684
 685 void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions)
 686 {
 687   d_context->push();
 688
 689   vector<Node>::iterator it = assertions.begin(), iend = assertions.end();
 690   for (; it != iend; ++it) {
 691     visitAll(*it);
 692   }
 693
 694   if (!d_unconstrained.empty()) {
 695     processUnconstrained();
 696     //    d_substitutions.print(Message.getStream());
 697     for (it = assertions.begin(); it != iend; ++it) {
 698       (*it) = Rewriter::rewrite(d_substitutions.apply(*it));
 699     }
 700   }
 701
 702   // to clear substitutions map
 703   d_context->pop();
 704
 705   d_visited.clear();
 706   d_visitedOnce.clear();
 707   d_unconstrained.clear();
 708 }