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 && parent.getType().getCardinality().isFinite() && parent.getType().getCardinality().getFiniteCardinality() == 2) {
 167             // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result
 168             // is unconstrained
 169             Node test;
 170             if (parent.getType().isBoolean()) {
 171               test = Rewriter::rewrite(parent[1].iffNode(parent[2]));
 172             }
 173             else {
 174               test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
 175             }
 176             if (test == NodeManager::currentNM()->mkConst<bool>(false)) {
 177               ++d_numUnconstrainedElim;
 178               if (currentSub.isNull()) {
 179                 currentSub = current;
 180               }
 181               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 182               current = parent;
 183             }
 184           }
 185           break;
 186         }
 187
 188         // Comparisons that return a different type - assuming domains are larger than 1, any
 189         // unconstrained child makes parent unconstrained as well
 190         case kind::EQUAL:
 191           if (parent[0].getType() != parent[1].getType()) {
 192             TNode other = (parent[0] == current) ? parent[1] : parent[0];
 193             if (current.getType().isSubtypeOf(other.getType())) {
 194               break;
 195             }
 196           }
 197         case kind::BITVECTOR_COMP:
 198         case kind::LT:
 199         case kind::LEQ:
 200         case kind::GT:
 201         case kind::GEQ:
 202         {
 203           if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 204               !d_substitutions.hasSubstitution(parent)) {
 205             ++d_numUnconstrainedElim;
 206             Assert(parent[0] != parent[1] &&
 207                    (parent[0] == current || parent[1] == current));
 208             if (currentSub.isNull()) {
 209               currentSub = current;
 210             }
 211             currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 212             current = parent;
 213           }
 214           else {
 215             currentSub = Node();
 216           }
 217           break;
 218         }
 219
 220         // Unary operators that propagate unconstrainedness
 221         case kind::NOT:
 222         case kind::BITVECTOR_NOT:
 223         case kind::BITVECTOR_NEG:
 224         case kind::UMINUS:
 225           ++d_numUnconstrainedElim;
 226           Assert(parent[0] == current);
 227           if (currentSub.isNull()) {
 228             currentSub = current;
 229           }
 230           current = parent;
 231           break;
 232
 233         // Unary operators that propagate unconstrainedness and return a different type
 234         case kind::BITVECTOR_EXTRACT:
 235           ++d_numUnconstrainedElim;
 236           Assert(parent[0] == current);
 237           if (currentSub.isNull()) {
 238             currentSub = current;
 239           }
 240           currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 241           current = parent;
 242           break;
 243
 244         // Operators returning same type requiring all children to be unconstrained
 245         case kind::AND:
 246         case kind::OR:
 247         case kind::IMPLIES:
 248         case kind::BITVECTOR_AND:
 249         case kind::BITVECTOR_OR:
 250         case kind::BITVECTOR_NAND:
 251         case kind::BITVECTOR_NOR:
 252         {
 253           bool allUnconstrained = true;
 254           for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
 255             if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
 256               allUnconstrained = false;
 257               break;
 258             }
 259           }
 260           if (allUnconstrained) {
 261             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 262                 !d_substitutions.hasSubstitution(parent)) {
 263               ++d_numUnconstrainedElim;
 264               if (currentSub.isNull()) {
 265                 currentSub = current;
 266               }
 267               current = parent;
 268             }
 269             else {
 270               currentSub = Node();
 271             }
 272           }
 273         }
 274         break;
 275
 276         // Require all children to be unconstrained and different
 277         case kind::BITVECTOR_SHL:
 278         case kind::BITVECTOR_LSHR:
 279         case kind::BITVECTOR_ASHR:
 280         case kind::BITVECTOR_UDIV:
 281         case kind::BITVECTOR_UREM:
 282         case kind::BITVECTOR_SDIV:
 283         case kind::BITVECTOR_SREM:
 284         case kind::BITVECTOR_SMOD: {
 285           bool allUnconstrained = true;
 286           bool allDifferent = true;
 287           for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
 288             if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
 289               allUnconstrained = false;
 290               break;
 291             }
 292             for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) {
 293               if (*child_it == *child_it2) {
 294                 allDifferent = false;
 295                 break;
 296               }
 297             }
 298           }
 299           if (allUnconstrained && allDifferent) {
 300             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 301                 !d_substitutions.hasSubstitution(parent)) {
 302               ++d_numUnconstrainedElim;
 303               if (currentSub.isNull()) {
 304                 currentSub = current;
 305               }
 306               current = parent;
 307             }
 308             else {
 309               currentSub = Node();
 310             }
 311           }
 312           break;
 313         }
 314
 315         // Requires all children to be unconstrained and different, and returns a different type
 316         case kind::BITVECTOR_CONCAT:
 317         {
 318           bool allUnconstrained = true;
 319           bool allDifferent = true;
 320           for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
 321             if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
 322               allUnconstrained = false;
 323               break;
 324             }
 325             for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) {
 326               if (*child_it == *child_it2) {
 327                 allDifferent = false;
 328                 break;
 329               }
 330             }
 331           }
 332           if (allUnconstrained && allDifferent) {
 333             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 334                 !d_substitutions.hasSubstitution(parent)) {
 335               ++d_numUnconstrainedElim;
 336               if (currentSub.isNull()) {
 337                 currentSub = current;
 338               }
 339               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 340               current = parent;
 341             }
 342             else {
 343               currentSub = Node();
 344             }
 345           }
 346         }
 347         break;
 348
 349         // N-ary operators returning same type requiring at least one child to be unconstrained
 350         case kind::PLUS:
 351         case kind::MINUS:
 352           if (current.getType().isInteger() &&
 353               !parent.getType().isInteger()) {
 354             break;
 355           }
 356         case kind::IFF:
 357         case kind::XOR:
 358         case kind::BITVECTOR_XOR:
 359         case kind::BITVECTOR_XNOR:
 360         case kind::BITVECTOR_PLUS:
 361         case kind::BITVECTOR_SUB:
 362           if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 363               !d_substitutions.hasSubstitution(parent)) {
 364             ++d_numUnconstrainedElim;
 365             if (currentSub.isNull()) {
 366               currentSub = current;
 367             }
 368             current = parent;
 369           }
 370           else {
 371             currentSub = Node();
 372           }
 373           break;
 374
 375         // Multiplication/division: must be non-integer and other operand must be non-zero
 376         case kind::MULT: {
 377         case kind::DIVISION:
 378           Assert(parent.getNumChildren() == 2);
 379           TNode other;
 380           if (parent[0] == current) {
 381             other = parent[1];
 382           }
 383           else {
 384             Assert(parent[1] == current);
 385             other = parent[0];
 386           }
 387           if (d_unconstrained.find(other) != d_unconstrained.end()) {
 388             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 389                 !d_substitutions.hasSubstitution(parent)) {
 390               if (current.getType().isInteger() && other.getType().isInteger()) {
 391                 Assert(parent.getKind() == kind::DIVISION || parent.getType().isInteger());
 392                 if (parent.getKind() == kind::DIVISION) {
 393                   break;
 394                 }
 395               }
 396               ++d_numUnconstrainedElim;
 397               if (currentSub.isNull()) {
 398                 currentSub = current;
 399               }
 400               current = parent;
 401             }
 402             else {
 403               currentSub = Node();
 404             }
 405           }
 406           else {
 407             // if only the denominator of a division is unconstrained, can't set it to 0 so the result is not unconstrained
 408             if (parent.getKind() == kind::DIVISION && current == parent[1]) {
 409               break;
 410             }
 411             NodeManager* nm = NodeManager::currentNM();
 412             // if we are an integer, the only way we are unconstrained is if we are a MULT by -1
 413             if (current.getType().isInteger()) {
 414               // div/mult by 1 should have been simplified
 415               Assert(other != nm->mkConst<Rational>(1));
 416               if (other == nm->mkConst<Rational>(-1)) {
 417                 // div by -1 should have been simplified
 418                 Assert(parent.getKind() == kind::MULT);
 419                 Assert(parent.getType().isInteger());
 420               }
 421               else {
 422                 break;
 423               }
 424             }
 425             else {
 426               // TODO: could build ITE here
 427               Node test = other.eqNode(nm->mkConst<Rational>(0));
 428               if (Rewriter::rewrite(test) != nm->mkConst<bool>(false)) {
 429                 break;
 430               }
 431             }
 432             ++d_numUnconstrainedElim;
 433             if (currentSub.isNull()) {
 434               currentSub = current;
 435             }
 436             current = parent;
 437           }
 438           break;
 439         }
 440
 441         // Bitvector MULT - current must only appear once in the children:
 442         // all other children must be unconstrained or odd
 443         case kind::BITVECTOR_MULT:
 444         {
 445           bool found = false;
 446           bool done = false;
 447           for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
 448             if ((*child_it) == current) {
 449               if (found) {
 450                 done = true;
 451                 break;
 452               }
 453               found = true;
 454               continue;
 455             }
 456             else if (d_unconstrained.find(*child_it) != d_unconstrained.end()) {
 457               continue;
 458             }
 459             else {
 460               NodeManager* nm = NodeManager::currentNM();
 461               Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0));
 462               vector<Node> children;
 463               children.push_back(*child_it);
 464               Node test = nm->mkNode(extractOp, children);
 465               BitVector one(1,unsigned(1));
 466               test = test.eqNode(nm->mkConst<BitVector>(one));
 467               if (Rewriter::rewrite(test) != nm->mkConst<bool>(true)) {
 468                 done = true;
 469                 break;
 470               }
 471             }
 472           }
 473           if (done) {
 474             break;
 475           }
 476           if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 477               !d_substitutions.hasSubstitution(parent)) {
 478             ++d_numUnconstrainedElim;
 479             if (currentSub.isNull()) {
 480               currentSub = current;
 481             }
 482             current = parent;
 483           }
 484           else {
 485             currentSub = Node();
 486           }
 487           break;
 488         }
 489
 490         // Uninterpreted function - if domain is infinite, no quantifiers are used, and any child is unconstrained, result is unconstrained
 491         case kind::APPLY_UF:
 492           if (d_logicInfo.isQuantified() || !current.getType().getCardinality().isInfinite()) {
 493             break;
 494           }
 495           if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 496               !d_substitutions.hasSubstitution(parent)) {
 497             ++d_numUnconstrainedElim;
 498             if (currentSub.isNull()) {
 499               currentSub = current;
 500             }
 501             if (parent.getType() != current.getType()) {
 502               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 503             }
 504             current = parent;
 505           }
 506           else {
 507             currentSub = Node();
 508           }
 509           break;
 510
 511         // Array select - if array is unconstrained, so is result
 512         case kind::SELECT:
 513           if (parent[0] == current) {
 514             ++d_numUnconstrainedElim;
 515             Assert(current.getType().isArray());
 516             if (currentSub.isNull()) {
 517               currentSub = current;
 518             }
 519             currentSub = newUnconstrainedVar(current.getType().getArrayConstituentType(), currentSub);
 520             current = parent;
 521           }
 522           break;
 523
 524         // Array store - if both store and value are unconstrained, so is resulting store
 525         case kind::STORE:
 526           if (((parent[0] == current &&
 527                 d_unconstrained.find(parent[2]) != d_unconstrained.end()) ||
 528                (parent[2] == current &&
 529                 d_unconstrained.find(parent[0]) != d_unconstrained.end()))) {
 530             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 531                 !d_substitutions.hasSubstitution(parent)) {
 532               ++d_numUnconstrainedElim;
 533               if (parent[0] != current) {
 534                 if (parent[0].isVar()) {
 535                   currentSub = parent[0];
 536                 }
 537                 else {
 538                   Assert(d_substitutions.hasSubstitution(parent[0]));
 539                   currentSub = d_substitutions.apply(parent[0]);
 540                 }
 541               }
 542               else if (currentSub.isNull()) {
 543                 currentSub = current;
 544               }
 545               current = parent;
 546             }
 547             else {
 548               currentSub = Node();
 549             }
 550           }
 551           break;
 552
 553         // Bit-vector comparisons: replace with new Boolean variable, but have to also conjoin with a side condition
 554         // as there is always one case when the comparison is forced to be false
 555         case kind::BITVECTOR_ULT:
 556           strict = true;
 557         case kind::BITVECTOR_UGE:
 558           goto bvineq;
 559
 560         case kind::BITVECTOR_UGT:
 561           strict = true;
 562         case kind::BITVECTOR_ULE:
 563           swap = true;
 564           goto bvineq;
 565
 566         case kind::BITVECTOR_SLT:
 567           strict = true;
 568         case kind::BITVECTOR_SGE:
 569           isSigned = true;
 570           goto bvineq;
 571
 572         case kind::BITVECTOR_SGT:
 573           strict = true;
 574         case kind::BITVECTOR_SLE:
 575           isSigned = true;
 576           swap = true;
 577
 578         bvineq: {
 579           TNode other;
 580           bool left = false;
 581           if (parent[0] == current) {
 582             other = parent[1];
 583             left = true;
 584           }
 585           else {
 586             Assert(parent[1] == current);
 587             other = parent[0];
 588           }
 589           if (d_unconstrained.find(other) != d_unconstrained.end()) {
 590             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
 591                 !d_substitutions.hasSubstitution(parent)) {
 592               ++d_numUnconstrainedElim;
 593               if (currentSub.isNull()) {
 594                 currentSub = current;
 595               }
 596               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 597               current = parent;
 598             }
 599             else {
 600               currentSub = Node();
 601             }
 602           }
 603           else {
 604             unsigned size = current.getType().getBitVectorSize();
 605             BitVector bv = isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) : BitVector(size, unsigned(0));
 606             if (swap == left) {
 607               bv = ~bv;
 608             }
 609             if (currentSub.isNull()) {
 610               currentSub = current;
 611             }
 612             currentSub = newUnconstrainedVar(parent.getType(), currentSub);
 613             current = parent;
 614             NodeManager* nm = NodeManager::currentNM();
 615             Node test = Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
 616             if (test == nm->mkConst<bool>(false)) {
 617               break;
 618             }
 619             if (strict) {
 620               currentSub = currentSub.andNode(test.notNode());
 621             }
 622             else {
 623               currentSub = currentSub.orNode(test);
 624             }
 625             // Delay adding this substitution - see comment at end of function
 626             delayQueueLeft.push_back(current);
 627             delayQueueRight.push_back(currentSub);
 628             currentSub = Node();
 629             parent = TNode();
 630           }
 631           break;
 632         }
 633
 634         // These should have been rewritten up front
 635         case kind::BITVECTOR_REPEAT:
 636         case kind::BITVECTOR_ZERO_EXTEND:
 637         case kind::BITVECTOR_ROTATE_LEFT:
 638         case kind::BITVECTOR_ROTATE_RIGHT:
 639           Unreachable();
 640           break;
 641
 642         // Do nothing
 643         case kind::BITVECTOR_SIGN_EXTEND:
 644         default:
 645           break;
 646       }
 647       if (current == parent && d_visited[parent] == 1) {
 648         d_unconstrained.insert(parent);
 649         continue;
 650       }
 651     }
 652     if (!currentSub.isNull()) {
 653       Assert(currentSub.isVar());
 654       d_substitutions.addSubstitution(current, currentSub, false);
 655     }
 656     if (workList.empty()) {
 657       break;
 658     }
 659     current = workList.back();
 660     currentSub = Node();
 661     workList.pop_back();
 662   }
 663   TNode left;
 664   Node right;
 665   // All substitutions except those arising from bitvector comparisons are
 666   // substitutions t -> x where x is a variable.  This allows us to build the
 667   // substitution very quickly (never invalidating the substitution cache).
 668   // Bitvector comparisons are more complicated and may require
 669   // back-substitution and cache-invalidation.  So we do these last.
 670   while (!delayQueueLeft.empty()) {
 671     left = delayQueueLeft.back();
 672     if (!d_substitutions.hasSubstitution(left)) {
 673       right = d_substitutions.apply(delayQueueRight.back());
 674       d_substitutions.addSubstitution(delayQueueLeft.back(), right);
 675     }
 676     delayQueueLeft.pop_back();
 677     delayQueueRight.pop_back();
 678   }
 679 }
 680
 681
 682 void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions)
 683 {
 684   d_context->push();
 685
 686   vector<Node>::iterator it = assertions.begin(), iend = assertions.end();
 687   for (; it != iend; ++it) {
 688     visitAll(*it);
 689   }
 690
 691   if (!d_unconstrained.empty()) {
 692     processUnconstrained();
 693     //    d_substitutions.print(Message.getStream());
 694     for (it = assertions.begin(); it != iend; ++it) {
 695       (*it) = Rewriter::rewrite(d_substitutions.apply(*it));
 696     }
 697   }
 698
 699   // to clear substitutions map
 700   d_context->pop();
 701
 702   d_visited.clear();
 703   d_visitedOnce.clear();
 704   d_unconstrained.clear();
 705 }