src/preprocessing/util/ite_utilities.cpp

   1 /*********************                                                        */
   2 /*! \file ite_utilities.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Aina Niemetz, Clark Barrett
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Simplifications for ITE expressions
  13  **
  14  ** This module implements preprocessing phases designed to simplify ITE
  15  ** expressions.  Based on:
  16  ** Kim, Somenzi, Jin.  Efficient Term-ITE Conversion for SMT.  FMCAD 2009.
  17  ** Burch, Jerry.  Techniques for Verifying Superscalar Microprocessors.  DAC
  18  *'96
  19  **/
  20 #include "preprocessing/util/ite_utilities.h"
  21
  22 #include <utility>
  23
  24 #include "preprocessing/assertion_pipeline.h"
  25 #include "preprocessing/passes/rewrite.h"
  26 #include "smt/smt_statistics_registry.h"
  27 #include "theory/rewriter.h"
  28 #include "theory/theory.h"
  29
  30 using namespace std;
  31 namespace cvc5 {
  32 namespace preprocessing {
  33 namespace util {
  34
  35 namespace ite {
  36
  37 inline static bool isTermITE(TNode e)
  38 {
  39   return (e.getKind() == kind::ITE && !e.getType().isBoolean());
  40 }
  41
  42 inline static bool triviallyContainsNoTermITEs(TNode e)
  43 {
  44   return e.isConst() || e.isVar();
  45 }
  46
  47 static bool isTheoryAtom(TNode a)
  48 {
  49   using namespace kind;
  50   switch (a.getKind())
  51   {
  52     case EQUAL:
  53     case DISTINCT: return !(a[0].getType().isBoolean());
  54
  55     /* from uf */
  56     case APPLY_UF: return a.getType().isBoolean();
  57     case CARDINALITY_CONSTRAINT:
  58     case DIVISIBLE:
  59     case LT:
  60     case LEQ:
  61     case GT:
  62     case GEQ:
  63     case IS_INTEGER:
  64     case BITVECTOR_COMP:
  65     case BITVECTOR_ULT:
  66     case BITVECTOR_ULE:
  67     case BITVECTOR_UGT:
  68     case BITVECTOR_UGE:
  69     case BITVECTOR_SLT:
  70     case BITVECTOR_SLE:
  71     case BITVECTOR_SGT:
  72     case BITVECTOR_SGE: return true;
  73     default: return false;
  74   }
  75 }
  76
  77 struct CTIVStackElement
  78 {
  79   TNode curr;
  80   unsigned pos;
  81   CTIVStackElement() : curr(), pos(0) {}
  82   CTIVStackElement(TNode c) : curr(c), pos(0) {}
  83 }; /* CTIVStackElement */
  84
  85 }  // namespace ite
  86
  87 ITEUtilities::ITEUtilities()
  88     : d_containsVisitor(new ContainsTermITEVisitor()),
  89       d_compressor(NULL),
  90       d_simplifier(NULL),
  91       d_careSimp(NULL)
  92 {
  93   Assert(d_containsVisitor != NULL);
  94 }
  95
  96 ITEUtilities::~ITEUtilities()
  97 {
  98   if (d_simplifier != NULL)
  99   {
 100     delete d_simplifier;
 101   }
 102   if (d_compressor != NULL)
 103   {
 104     delete d_compressor;
 105   }
 106   if (d_careSimp != NULL)
 107   {
 108     delete d_careSimp;
 109   }
 110 }
 111
 112 Node ITEUtilities::simpITE(TNode assertion)
 113 {
 114   if (d_simplifier == NULL)
 115   {
 116     d_simplifier = new ITESimplifier(d_containsVisitor.get());
 117   }
 118   return d_simplifier->simpITE(assertion);
 119 }
 120
 121 bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const
 122 {
 123   if (d_simplifier == NULL)
 124   {
 125     return false;
 126   }
 127   else
 128   {
 129     return d_simplifier->doneALotOfWorkHeuristic();
 130   }
 131 }
 132
 133 /* returns false if an assertion is discovered to be equal to false. */
 134 bool ITEUtilities::compress(AssertionPipeline* assertionsToPreprocess)
 135 {
 136   if (d_compressor == NULL)
 137   {
 138     d_compressor = new ITECompressor(d_containsVisitor.get());
 139   }
 140   return d_compressor->compress(assertionsToPreprocess);
 141 }
 142
 143 Node ITEUtilities::simplifyWithCare(TNode e)
 144 {
 145   if (d_careSimp == NULL)
 146   {
 147     d_careSimp = new ITECareSimplifier();
 148   }
 149   return d_careSimp->simplifyWithCare(e);
 150 }
 151
 152 void ITEUtilities::clear()
 153 {
 154   if (d_simplifier != NULL)
 155   {
 156     d_simplifier->clearSimpITECaches();
 157   }
 158   if (d_compressor != NULL)
 159   {
 160     d_compressor->garbageCollect();
 161   }
 162   if (d_careSimp != NULL)
 163   {
 164     d_careSimp->clear();
 165   }
 166   d_containsVisitor->garbageCollect();
 167 }
 168
 169 /*********************                                                        */
 170 /* ContainsTermITEVisitor
 171  */
 172 ContainsTermITEVisitor::ContainsTermITEVisitor() : d_cache() {}
 173 ContainsTermITEVisitor::~ContainsTermITEVisitor() {}
 174 bool ContainsTermITEVisitor::containsTermITE(TNode e)
 175 {
 176   /* throughout execution skip through NOT nodes. */
 177   e = (e.getKind() == kind::NOT) ? e[0] : e;
 178   if (ite::triviallyContainsNoTermITEs(e))
 179   {
 180     return false;
 181   }
 182
 183   NodeBoolMap::const_iterator end = d_cache.end();
 184   NodeBoolMap::const_iterator tmp_it = d_cache.find(e);
 185   if (tmp_it != end)
 186   {
 187     return (*tmp_it).second;
 188   }
 189
 190   bool foundTermIte = false;
 191   std::vector<ite::CTIVStackElement> stack;
 192   stack.push_back(ite::CTIVStackElement(e));
 193   while (!foundTermIte && !stack.empty())
 194   {
 195     ite::CTIVStackElement& top = stack.back();
 196     TNode curr = top.curr;
 197     if (top.pos >= curr.getNumChildren())
 198     {
 199       // all of the children have been visited
 200       // no term ites were found
 201       d_cache[curr] = false;
 202       stack.pop_back();
 203     }
 204     else
 205     {
 206       // this is someone's child
 207       TNode child = curr[top.pos];
 208       child = (child.getKind() == kind::NOT) ? child[0] : child;
 209       ++top.pos;
 210       if (ite::triviallyContainsNoTermITEs(child))
 211       {
 212         // skip
 213       }
 214       else
 215       {
 216         tmp_it = d_cache.find(child);
 217         if (tmp_it != end)
 218         {
 219           foundTermIte = (*tmp_it).second;
 220         }
 221         else
 222         {
 223           stack.push_back(ite::CTIVStackElement(child));
 224           foundTermIte = ite::isTermITE(child);
 225         }
 226       }
 227     }
 228   }
 229   if (foundTermIte)
 230   {
 231     while (!stack.empty())
 232     {
 233       TNode curr = stack.back().curr;
 234       stack.pop_back();
 235       d_cache[curr] = true;
 236     }
 237   }
 238   return foundTermIte;
 239 }
 240 void ContainsTermITEVisitor::garbageCollect() { d_cache.clear(); }
 241
 242 /*********************                                                        */
 243 /* IncomingArcCounter
 244  */
 245 IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants)
 246     : d_reachCount(), d_skipVariables(skipVars), d_skipConstants(skipConstants)
 247 {
 248 }
 249 IncomingArcCounter::~IncomingArcCounter() {}
 250
 251 void IncomingArcCounter::computeReachability(
 252     const std::vector<Node>& assertions)
 253 {
 254   std::vector<TNode> tovisit(assertions.begin(), assertions.end());
 255
 256   while (!tovisit.empty())
 257   {
 258     TNode back = tovisit.back();
 259     tovisit.pop_back();
 260
 261     bool skip = false;
 262     switch (back.getMetaKind())
 263     {
 264       case kind::metakind::CONSTANT: skip = d_skipConstants; break;
 265       case kind::metakind::VARIABLE: skip = d_skipVariables; break;
 266       default: break;
 267     }
 268
 269     if (skip)
 270     {
 271       continue;
 272     }
 273     if (d_reachCount.find(back) != d_reachCount.end())
 274     {
 275       d_reachCount[back] = 1 + d_reachCount[back];
 276     }
 277     else
 278     {
 279       d_reachCount[back] = 1;
 280       for (TNode::iterator cit = back.begin(), end = back.end(); cit != end;
 281            ++cit)
 282       {
 283         tovisit.push_back(*cit);
 284       }
 285     }
 286   }
 287 }
 288
 289 void IncomingArcCounter::clear() { d_reachCount.clear(); }
 290
 291 /*********************                                                        */
 292 /* ITECompressor
 293  */
 294 ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
 295     : d_contains(contains), d_assertions(NULL), d_incoming(true, true)
 296 {
 297   Assert(d_contains != NULL);
 298
 299   d_true = NodeManager::currentNM()->mkConst<bool>(true);
 300   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 301 }
 302
 303 ITECompressor::~ITECompressor() { reset(); }
 304
 305 void ITECompressor::reset()
 306 {
 307   d_incoming.clear();
 308   d_compressed.clear();
 309 }
 310
 311 void ITECompressor::garbageCollect() { reset(); }
 312
 313 ITECompressor::Statistics::Statistics()
 314     : d_compressCalls("ite-simp::compressCalls", 0),
 315       d_skolemsAdded("ite-simp::skolems", 0)
 316 {
 317   smtStatisticsRegistry()->registerStat(&d_compressCalls);
 318   smtStatisticsRegistry()->registerStat(&d_skolemsAdded);
 319 }
 320 ITECompressor::Statistics::~Statistics()
 321 {
 322   smtStatisticsRegistry()->unregisterStat(&d_compressCalls);
 323   smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded);
 324 }
 325
 326 Node ITECompressor::push_back_boolean(Node original, Node compressed)
 327 {
 328   Node rewritten = theory::Rewriter::rewrite(compressed);
 329   // There is a bug if the rewritter takes a pure boolean expression
 330   // and changes its theory
 331   if (rewritten.isConst())
 332   {
 333     d_compressed[compressed] = rewritten;
 334     d_compressed[original] = rewritten;
 335     d_compressed[rewritten] = rewritten;
 336     return rewritten;
 337   }
 338   else if (d_compressed.find(rewritten) != d_compressed.end())
 339   {
 340     Node res = d_compressed[rewritten];
 341     d_compressed[original] = res;
 342     d_compressed[compressed] = res;
 343     return res;
 344   }
 345   else if (rewritten.isVar()
 346            || (rewritten.getKind() == kind::NOT && rewritten[0].isVar()))
 347   {
 348     d_compressed[original] = rewritten;
 349     d_compressed[compressed] = rewritten;
 350     d_compressed[rewritten] = rewritten;
 351     return rewritten;
 352   }
 353   else
 354   {
 355     NodeManager* nm = NodeManager::currentNM();
 356     Node skolem = nm->mkSkolem("compress", nm->booleanType());
 357     d_compressed[rewritten] = skolem;
 358     d_compressed[original] = skolem;
 359     d_compressed[compressed] = skolem;
 360
 361     Node iff = skolem.eqNode(rewritten);
 362     d_assertions->push_back(iff);
 363     ++(d_statistics.d_skolemsAdded);
 364     return skolem;
 365   }
 366 }
 367
 368 bool ITECompressor::multipleParents(TNode c)
 369 {
 370   return d_incoming.lookupIncoming(c) >= 2;
 371 }
 372
 373 Node ITECompressor::compressBooleanITEs(Node toCompress)
 374 {
 375   Assert(toCompress.getKind() == kind::ITE);
 376   Assert(toCompress.getType().isBoolean());
 377
 378   if (!(toCompress[1] == d_false || toCompress[2] == d_false))
 379   {
 380     Node cmpCnd = compressBoolean(toCompress[0]);
 381     if (cmpCnd.isConst())
 382     {
 383       Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
 384       Node res = compressBoolean(branch);
 385       d_compressed[toCompress] = res;
 386       return res;
 387     }
 388     else
 389     {
 390       Node cmpThen = compressBoolean(toCompress[1]);
 391       Node cmpElse = compressBoolean(toCompress[2]);
 392       Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
 393       if (multipleParents(toCompress))
 394       {
 395         return push_back_boolean(toCompress, newIte);
 396       }
 397       else
 398       {
 399         return newIte;
 400       }
 401     }
 402   }
 403
 404   NodeBuilder<> nb(kind::AND);
 405   Node curr = toCompress;
 406   while (curr.getKind() == kind::ITE
 407          && (curr[1] == d_false || curr[2] == d_false)
 408          && (!multipleParents(curr) || curr == toCompress))
 409   {
 410     bool negateCnd = (curr[1] == d_false);
 411     Node compressCnd = compressBoolean(curr[0]);
 412     if (compressCnd.isConst())
 413     {
 414       if (compressCnd.getConst<bool>() == negateCnd)
 415       {
 416         return push_back_boolean(toCompress, d_false);
 417       }
 418       else
 419       {
 420         // equivalent to true don't push back
 421       }
 422     }
 423     else
 424     {
 425       Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
 426       nb << pb;
 427     }
 428     curr = negateCnd ? curr[2] : curr[1];
 429   }
 430   Assert(toCompress != curr);
 431
 432   nb << compressBoolean(curr);
 433   Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
 434   return push_back_boolean(toCompress, res);
 435 }
 436
 437 Node ITECompressor::compressTerm(Node toCompress)
 438 {
 439   if (toCompress.isConst() || toCompress.isVar())
 440   {
 441     return toCompress;
 442   }
 443
 444   if (d_compressed.find(toCompress) != d_compressed.end())
 445   {
 446     return d_compressed[toCompress];
 447   }
 448   if (toCompress.getKind() == kind::ITE)
 449   {
 450     Node cmpCnd = compressBoolean(toCompress[0]);
 451     if (cmpCnd.isConst())
 452     {
 453       Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
 454       Node res = compressTerm(branch);
 455       d_compressed[toCompress] = res;
 456       return res;
 457     }
 458     else
 459     {
 460       Node cmpThen = compressTerm(toCompress[1]);
 461       Node cmpElse = compressTerm(toCompress[2]);
 462       Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
 463       d_compressed[toCompress] = newIte;
 464       return newIte;
 465     }
 466   }
 467
 468   NodeBuilder<> nb(toCompress.getKind());
 469
 470   if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
 471   {
 472     nb << (toCompress.getOperator());
 473   }
 474   for (Node::iterator it = toCompress.begin(), end = toCompress.end();
 475        it != end;
 476        ++it)
 477   {
 478     nb << compressTerm(*it);
 479   }
 480   Node compressed = (Node)nb;
 481   if (multipleParents(toCompress))
 482   {
 483     d_compressed[toCompress] = compressed;
 484   }
 485   return compressed;
 486 }
 487
 488 Node ITECompressor::compressBoolean(Node toCompress)
 489 {
 490   static int instance = 0;
 491   ++instance;
 492   if (toCompress.isConst() || toCompress.isVar())
 493   {
 494     return toCompress;
 495   }
 496   if (d_compressed.find(toCompress) != d_compressed.end())
 497   {
 498     return d_compressed[toCompress];
 499   }
 500   else if (toCompress.getKind() == kind::ITE)
 501   {
 502     return compressBooleanITEs(toCompress);
 503   }
 504   else
 505   {
 506     bool ta = ite::isTheoryAtom(toCompress);
 507     NodeBuilder<> nb(toCompress.getKind());
 508     if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
 509     {
 510       nb << (toCompress.getOperator());
 511     }
 512     for (Node::iterator it = toCompress.begin(), end = toCompress.end();
 513          it != end;
 514          ++it)
 515     {
 516       Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
 517       nb << pb;
 518     }
 519     Node compressed = nb;
 520     if (ta || multipleParents(toCompress))
 521     {
 522       return push_back_boolean(toCompress, compressed);
 523     }
 524     else
 525     {
 526       return compressed;
 527     }
 528   }
 529 }
 530
 531 bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess)
 532 {
 533   reset();
 534
 535   d_assertions = assertionsToPreprocess;
 536   d_incoming.computeReachability(assertionsToPreprocess->ref());
 537
 538   ++(d_statistics.d_compressCalls);
 539   Chat() << "Computed reachability" << endl;
 540
 541   bool nofalses = true;
 542   const std::vector<Node>& assertions = assertionsToPreprocess->ref();
 543   size_t original_size = assertions.size();
 544   Chat() << "compressing " << original_size << endl;
 545   for (size_t i = 0; i < original_size && nofalses; ++i)
 546   {
 547     Node assertion = assertions[i];
 548     Node compressed = compressBoolean(assertion);
 549     Node rewritten = theory::Rewriter::rewrite(compressed);
 550     // replace
 551     assertionsToPreprocess->replace(i, rewritten);
 552     Assert(!d_contains->containsTermITE(rewritten));
 553
 554     nofalses = (rewritten != d_false);
 555   }
 556
 557   d_assertions = NULL;
 558
 559   return nofalses;
 560 }
 561
 562 TermITEHeightCounter::TermITEHeightCounter() : d_termITEHeight() {}
 563
 564 TermITEHeightCounter::~TermITEHeightCounter() {}
 565
 566 void TermITEHeightCounter::clear() { d_termITEHeight.clear(); }
 567
 568 size_t TermITEHeightCounter::cache_size() const
 569 {
 570   return d_termITEHeight.size();
 571 }
 572
 573 namespace ite {
 574 struct TITEHStackElement
 575 {
 576   TNode curr;
 577   unsigned pos;
 578   uint32_t maxChildHeight;
 579   TITEHStackElement() : curr(), pos(0), maxChildHeight(0) {}
 580   TITEHStackElement(TNode c) : curr(c), pos(0), maxChildHeight(0) {}
 581 };
 582 } /* namespace ite */
 583
 584 uint32_t TermITEHeightCounter::termITEHeight(TNode e)
 585 {
 586   if (ite::triviallyContainsNoTermITEs(e))
 587   {
 588     return 0;
 589   }
 590
 591   NodeCountMap::const_iterator end = d_termITEHeight.end();
 592   NodeCountMap::const_iterator tmp_it = d_termITEHeight.find(e);
 593   if (tmp_it != end)
 594   {
 595     return (*tmp_it).second;
 596   }
 597
 598   uint32_t returnValue = 0;
 599   // This is initially 0 as the very first call this is included in the max,
 600   // but this has no effect.
 601   std::vector<ite::TITEHStackElement> stack;
 602   stack.push_back(ite::TITEHStackElement(e));
 603   while (!stack.empty())
 604   {
 605     ite::TITEHStackElement& top = stack.back();
 606     top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
 607     TNode curr = top.curr;
 608     if (top.pos >= curr.getNumChildren())
 609     {
 610       // done with the current node
 611       returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
 612       d_termITEHeight[curr] = returnValue;
 613       stack.pop_back();
 614       continue;
 615     }
 616     else
 617     {
 618       if (top.pos == 0 && curr.getKind() == kind::ITE)
 619       {
 620         ++top.pos;
 621         returnValue = 0;
 622         continue;
 623       }
 624       // this is someone's child
 625       TNode child = curr[top.pos];
 626       ++top.pos;
 627       if (ite::triviallyContainsNoTermITEs(child))
 628       {
 629         returnValue = 0;
 630       }
 631       else
 632       {
 633         tmp_it = d_termITEHeight.find(child);
 634         if (tmp_it != end)
 635         {
 636           returnValue = (*tmp_it).second;
 637         }
 638         else
 639         {
 640           stack.push_back(ite::TITEHStackElement(child));
 641         }
 642       }
 643     }
 644   }
 645   return returnValue;
 646 }
 647
 648 ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains)
 649     : d_containsVisitor(contains),
 650       d_termITEHeight(),
 651       d_constantLeaves(),
 652       d_allocatedConstantLeaves(),
 653       d_citeEqConstApplications(0),
 654       d_constantIteEqualsConstantCache(),
 655       d_replaceOverCache(),
 656       d_replaceOverTermIteCache(),
 657       d_leavesConstCache(),
 658       d_simpConstCache(),
 659       d_simpContextCache(),
 660       d_simpITECache()
 661 {
 662   Assert(d_containsVisitor != NULL);
 663   d_true = NodeManager::currentNM()->mkConst<bool>(true);
 664   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 665 }
 666
 667 ITESimplifier::~ITESimplifier()
 668 {
 669   clearSimpITECaches();
 670   Assert(d_constantLeaves.empty());
 671   Assert(d_allocatedConstantLeaves.empty());
 672 }
 673
 674 bool ITESimplifier::leavesAreConst(TNode e)
 675 {
 676   return leavesAreConst(e, theory::Theory::theoryOf(e));
 677 }
 678
 679 void ITESimplifier::clearSimpITECaches()
 680 {
 681   Chat() << "clear ite caches " << endl;
 682   for (size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i)
 683   {
 684     NodeVec* curr = d_allocatedConstantLeaves[i];
 685     delete curr;
 686   }
 687   d_citeEqConstApplications = 0;
 688   d_constantLeaves.clear();
 689   d_allocatedConstantLeaves.clear();
 690   d_termITEHeight.clear();
 691   d_constantIteEqualsConstantCache.clear();
 692   d_replaceOverCache.clear();
 693   d_replaceOverTermIteCache.clear();
 694   d_simpITECache.clear();
 695   d_simpVars.clear();
 696   d_simpConstCache.clear();
 697   d_leavesConstCache.clear();
 698   d_simpContextCache.clear();
 699 }
 700
 701 bool ITESimplifier::doneALotOfWorkHeuristic() const
 702 {
 703   static const size_t SIZE_BOUND = 1000;
 704   Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications
 705          << endl;
 706   return (d_citeEqConstApplications > SIZE_BOUND);
 707 }
 708
 709 ITESimplifier::Statistics::Statistics()
 710     : d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
 711       d_unexpected("ite-simp::unexpected", 0),
 712       d_unsimplified("ite-simp::unsimplified", 0),
 713       d_exactMatchFold("ite-simp::exactMatchFold", 0),
 714       d_binaryPredFold("ite-simp::binaryPredFold", 0),
 715       d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
 716       d_simpITEVisits("ite-simp::simpITE.visits", 0),
 717       d_inSmaller("ite-simp::inSmaller")
 718 {
 719   smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded);
 720   smtStatisticsRegistry()->registerStat(&d_unexpected);
 721   smtStatisticsRegistry()->registerStat(&d_unsimplified);
 722   smtStatisticsRegistry()->registerStat(&d_exactMatchFold);
 723   smtStatisticsRegistry()->registerStat(&d_binaryPredFold);
 724   smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds);
 725   smtStatisticsRegistry()->registerStat(&d_simpITEVisits);
 726   smtStatisticsRegistry()->registerStat(&d_inSmaller);
 727 }
 728
 729 ITESimplifier::Statistics::~Statistics()
 730 {
 731   smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded);
 732   smtStatisticsRegistry()->unregisterStat(&d_unexpected);
 733   smtStatisticsRegistry()->unregisterStat(&d_unsimplified);
 734   smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold);
 735   smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold);
 736   smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds);
 737   smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits);
 738   smtStatisticsRegistry()->unregisterStat(&d_inSmaller);
 739 }
 740
 741 bool ITESimplifier::isConstantIte(TNode e)
 742 {
 743   if (e.isConst())
 744   {
 745     return true;
 746   }
 747   else if (ite::isTermITE(e))
 748   {
 749     NodeVec* constants = computeConstantLeaves(e);
 750     return constants != NULL;
 751   }
 752   else
 753   {
 754     return false;
 755   }
 756 }
 757
 758 ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite)
 759 {
 760   Assert(ite::isTermITE(ite));
 761   ConstantLeavesMap::const_iterator it = d_constantLeaves.find(ite);
 762   ConstantLeavesMap::const_iterator end = d_constantLeaves.end();
 763   if (it != end)
 764   {
 765     return (*it).second;
 766   }
 767   TNode thenB = ite[1];
 768   TNode elseB = ite[2];
 769
 770   // special case 2 constant children
 771   if (thenB.isConst() && elseB.isConst())
 772   {
 773     NodeVec* pair = new NodeVec(2);
 774     d_allocatedConstantLeaves.push_back(pair);
 775
 776     (*pair)[0] = std::min(thenB, elseB);
 777     (*pair)[1] = std::max(thenB, elseB);
 778     d_constantLeaves[ite] = pair;
 779     return pair;
 780   }
 781   // At least 1 is an ITE
 782   if (!(thenB.isConst() || thenB.getKind() == kind::ITE)
 783       || !(elseB.isConst() || elseB.getKind() == kind::ITE))
 784   {
 785     // Cannot be a termITE tree
 786     d_constantLeaves[ite] = NULL;
 787     return NULL;
 788   }
 789
 790   // At least 1 is not a constant
 791   TNode definitelyITE = thenB.isConst() ? elseB : thenB;
 792   TNode maybeITE = thenB.isConst() ? thenB : elseB;
 793
 794   NodeVec* defChildren = computeConstantLeaves(definitelyITE);
 795   if (defChildren == NULL)
 796   {
 797     d_constantLeaves[ite] = NULL;
 798     return NULL;
 799   }
 800
 801   NodeVec scratch;
 802   NodeVec* maybeChildren = NULL;
 803   if (maybeITE.getKind() == kind::ITE)
 804   {
 805     maybeChildren = computeConstantLeaves(maybeITE);
 806   }
 807   else
 808   {
 809     scratch.push_back(maybeITE);
 810     maybeChildren = &scratch;
 811   }
 812   if (maybeChildren == NULL)
 813   {
 814     d_constantLeaves[ite] = NULL;
 815     return NULL;
 816   }
 817
 818   NodeVec* both = new NodeVec(defChildren->size() + maybeChildren->size());
 819   d_allocatedConstantLeaves.push_back(both);
 820   NodeVec::iterator newEnd;
 821   newEnd = std::set_union(defChildren->begin(),
 822                           defChildren->end(),
 823                           maybeChildren->begin(),
 824                           maybeChildren->end(),
 825                           both->begin());
 826   both->resize(newEnd - both->begin());
 827   d_constantLeaves[ite] = both;
 828   return both;
 829 }
 830
 831 // This is uncached! Better for protoyping or getting limited size examples
 832 struct IteTreeSearchData
 833 {
 834   set<Node> visited;
 835   set<Node> constants;
 836   set<Node> nonConstants;
 837   int maxConstants;
 838   int maxNonconstants;
 839   int maxDepth;
 840   bool failure;
 841   IteTreeSearchData()
 842       : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
 843   {
 844   }
 845 };
 846 void iteTreeSearch(Node e, int depth, IteTreeSearchData& search)
 847 {
 848   if (search.maxDepth >= 0 && depth > search.maxDepth)
 849   {
 850     search.failure = true;
 851   }
 852   if (search.failure)
 853   {
 854     return;
 855   }
 856   if (search.visited.find(e) != search.visited.end())
 857   {
 858     return;
 859   }
 860   else
 861   {
 862     search.visited.insert(e);
 863   }
 864
 865   if (e.isConst())
 866   {
 867     search.constants.insert(e);
 868     if (search.maxConstants >= 0
 869         && search.constants.size() > (unsigned)search.maxConstants)
 870     {
 871       search.failure = true;
 872     }
 873   }
 874   else if (e.getKind() == kind::ITE)
 875   {
 876     iteTreeSearch(e[1], depth + 1, search);
 877     iteTreeSearch(e[2], depth + 1, search);
 878   }
 879   else
 880   {
 881     search.nonConstants.insert(e);
 882     if (search.maxNonconstants >= 0
 883         && search.nonConstants.size() > (unsigned)search.maxNonconstants)
 884     {
 885       search.failure = true;
 886     }
 887   }
 888 }
 889
 890 Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar)
 891 {
 892   if (n == simpVar)
 893   {
 894     return replaceWith;
 895   }
 896   else if (n.getNumChildren() == 0)
 897   {
 898     return n;
 899   }
 900   Assert(n.getNumChildren() > 0);
 901   Assert(!n.isVar());
 902
 903   pair<Node, Node> p = make_pair(n, replaceWith);
 904   if (d_replaceOverCache.find(p) != d_replaceOverCache.end())
 905   {
 906     return d_replaceOverCache[p];
 907   }
 908
 909   NodeBuilder<> builder(n.getKind());
 910   if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
 911   {
 912     builder << n.getOperator();
 913   }
 914   unsigned i = 0;
 915   for (; i < n.getNumChildren(); ++i)
 916   {
 917     Node newChild = replaceOver(n[i], replaceWith, simpVar);
 918     builder << newChild;
 919   }
 920   // Mark the substitution and continue
 921   Node result = builder;
 922   d_replaceOverCache[p] = result;
 923   return result;
 924 }
 925
 926 Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar)
 927 {
 928   if (e.getKind() == kind::ITE)
 929   {
 930     pair<Node, Node> p = make_pair(e, simpAtom);
 931     if (d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end())
 932     {
 933       return d_replaceOverTermIteCache[p];
 934     }
 935     Assert(!e.getType().isBoolean());
 936     Node cnd = e[0];
 937     Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar);
 938     Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar);
 939     Node newIte = cnd.iteNode(newThen, newElse);
 940     d_replaceOverTermIteCache[p] = newIte;
 941     return newIte;
 942   }
 943   else
 944   {
 945     return replaceOver(simpAtom, e, simpVar);
 946   }
 947 }
 948
 949 Node ITESimplifier::attemptLiftEquality(TNode atom)
 950 {
 951   if (atom.getKind() == kind::EQUAL)
 952   {
 953     TNode left = atom[0];
 954     TNode right = atom[1];
 955     if ((left.getKind() == kind::ITE || right.getKind() == kind::ITE)
 956         && !(left.getKind() == kind::ITE && right.getKind() == kind::ITE))
 957     {
 958       // exactly 1 is an ite
 959       TNode ite = left.getKind() == kind::ITE ? left : right;
 960       TNode notIte = left.getKind() == kind::ITE ? right : left;
 961
 962       if (notIte == ite[1])
 963       {
 964         ++(d_statistics.d_exactMatchFold);
 965         return ite[0].iteNode(d_true, notIte.eqNode(ite[2]));
 966       }
 967       else if (notIte == ite[2])
 968       {
 969         ++(d_statistics.d_exactMatchFold);
 970         return ite[0].iteNode(notIte.eqNode(ite[1]), d_true);
 971       }
 972       if (notIte.isConst() && (ite[1].isConst() || ite[2].isConst()))
 973       {
 974         ++(d_statistics.d_exactMatchFold);
 975         return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2]));
 976       }
 977     }
 978   }
 979
 980   // try a similar more relaxed version for non-equality operators
 981   if (atom.getMetaKind() == kind::metakind::OPERATOR
 982       && atom.getNumChildren() == 2 && !atom[1].getType().isBoolean())
 983   {
 984     TNode left = atom[0];
 985     TNode right = atom[1];
 986     if ((left.getKind() == kind::ITE || right.getKind() == kind::ITE)
 987         && !(left.getKind() == kind::ITE && right.getKind() == kind::ITE))
 988     {
 989       // exactly 1 is an ite
 990       bool leftIsIte = left.getKind() == kind::ITE;
 991       Node ite = leftIsIte ? left : right;
 992       Node notIte = leftIsIte ? right : left;
 993
 994       if (notIte.isConst())
 995       {
 996         IteTreeSearchData search;
 997         search.maxNonconstants = 2;
 998         iteTreeSearch(ite, 0, search);
 999         if (!search.failure)
1000         {
1001           d_statistics.d_maxNonConstantsFolded.maxAssign(
1002               search.nonConstants.size());
1003           Debug("ite::simpite") << "used " << search.nonConstants.size()
1004                                 << " nonconstants" << endl;
1005           NodeManager* nm = NodeManager::currentNM();
1006           Node simpVar = getSimpVar(notIte.getType());
1007           TNode newLeft = leftIsIte ? simpVar : notIte;
1008           TNode newRight = leftIsIte ? notIte : simpVar;
1009           Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
1010
1011           ++(d_statistics.d_binaryPredFold);
1012           return replaceOverTermIte(ite, newAtom, simpVar);
1013         }
1014       }
1015     }
1016   }
1017
1018   // TODO "This is way too tailored. Must generalize!"
1019   if (atom.getKind() == kind::EQUAL && atom.getNumChildren() == 2
1020       && ite::isTermITE(atom[0]) && atom[1].getKind() == kind::MULT
1021       && atom[1].getNumChildren() == 2 && atom[1][0].isConst()
1022       && atom[1][0].getConst<Rational>().isNegativeOne()
1023       && ite::isTermITE(atom[1][1])
1024       && d_termITEHeight.termITEHeight(atom[0]) == 1
1025       && d_termITEHeight.termITEHeight(atom[1][1]) == 1
1026       && (atom[0][1].isConst() || atom[0][2].isConst())
1027       && (atom[1][1][1].isConst() || atom[1][1][2].isConst()))
1028   {
1029     // expand all 4 cases
1030
1031     Node negOne = atom[1][0];
1032
1033     Node lite = atom[0];
1034     Node lC = lite[0];
1035     Node lT = lite[1];
1036     Node lE = lite[2];
1037
1038     NodeManager* nm = NodeManager::currentNM();
1039     Node negRite = atom[1][1];
1040     Node rC = negRite[0];
1041     Node rT = nm->mkNode(kind::MULT, negOne, negRite[1]);
1042     Node rE = nm->mkNode(kind::MULT, negOne, negRite[2]);
1043
1044     // (ite lC lT lE) = (ite rC rT rE)
1045     // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE))))
1046     // (ite lc (ite rC (= lT rT) (= lT rE))
1047     //         (ite rC (= lE rT) (= lE rE)))
1048
1049     Node eqTT = lT.eqNode(rT);
1050     Node eqTE = lT.eqNode(rE);
1051     Node eqET = lE.eqNode(rT);
1052     Node eqEE = lE.eqNode(rE);
1053     Node thenLC = rC.iteNode(eqTT, eqTE);
1054     Node elseLC = rC.iteNode(eqET, eqEE);
1055     Node newIte = lC.iteNode(thenLC, elseLC);
1056
1057     ++(d_statistics.d_specialEqualityFolds);
1058     return newIte;
1059   }
1060   return Node::null();
1061 }
1062
1063 // Interesting classes of atoms:
1064 // 2. Contains constants and 1 constant term ite
1065 // 3. Contains 2 constant term ites
1066 Node ITESimplifier::transformAtom(TNode atom)
1067 {
1068   if (!d_containsVisitor->containsTermITE(atom))
1069   {
1070     if (atom.getKind() == kind::EQUAL && atom[0].isConst() && atom[1].isConst())
1071     {
1072       // constant equality
1073       return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]);
1074     }
1075     return Node::null();
1076   }
1077   else
1078   {
1079     Node acr = attemptConstantRemoval(atom);
1080     if (!acr.isNull())
1081     {
1082       return acr;
1083     }
1084     // Node ale = attemptLiftEquality(atom);
1085     // if(!ale.isNull()){
1086     //   //return ale;
1087     // }
1088     return Node::null();
1089   }
1090 }
1091
1092 static unsigned numBranches = 0;
1093 static unsigned numFalseBranches = 0;
1094 static unsigned itesMade = 0;
1095
1096 Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant)
1097 {
1098   static int instance = 0;
1099   ++instance;
1100   Debug("ite::constantIteEqualsConstant")
1101       << instance << "constantIteEqualsConstant(" << cite << ", " << constant
1102       << ")" << endl;
1103   if (cite.isConst())
1104   {
1105     Node res = (cite == constant) ? d_true : d_false;
1106     Debug("ite::constantIteEqualsConstant") << instance << "->" << res << endl;
1107     return res;
1108   }
1109   std::pair<Node, Node> pair = make_pair(cite, constant);
1110
1111   NodePairMap::const_iterator eq_pos =
1112       d_constantIteEqualsConstantCache.find(pair);
1113   if (eq_pos != d_constantIteEqualsConstantCache.end())
1114   {
1115     Debug("ite::constantIteEqualsConstant")
1116         << instance << "->" << (*eq_pos).second << endl;
1117     return (*eq_pos).second;
1118   }
1119
1120   ++d_citeEqConstApplications;
1121
1122   NodeVec* leaves = computeConstantLeaves(cite);
1123   Assert(leaves != NULL);
1124   if (std::binary_search(leaves->begin(), leaves->end(), constant))
1125   {
1126     if (leaves->size() == 1)
1127     {
1128       // probably unreachable
1129       d_constantIteEqualsConstantCache[pair] = d_true;
1130       Debug("ite::constantIteEqualsConstant")
1131           << instance << "->" << d_true << endl;
1132       return d_true;
1133     }
1134     else
1135     {
1136       Assert(cite.getKind() == kind::ITE);
1137       TNode cnd = cite[0];
1138       TNode tB = cite[1];
1139       TNode fB = cite[2];
1140       Node tEqs = constantIteEqualsConstant(tB, constant);
1141       Node fEqs = constantIteEqualsConstant(fB, constant);
1142       Node boolIte = cnd.iteNode(tEqs, fEqs);
1143       if (!(tEqs.isConst() || fEqs.isConst()))
1144       {
1145         ++numBranches;
1146       }
1147       if (!(tEqs == d_false || fEqs == d_false))
1148       {
1149         ++numFalseBranches;
1150       }
1151       ++itesMade;
1152       d_constantIteEqualsConstantCache[pair] = boolIte;
1153       // Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte
1154       // << endl;
1155       return boolIte;
1156     }
1157   }
1158   else
1159   {
1160     d_constantIteEqualsConstantCache[pair] = d_false;
1161     Debug("ite::constantIteEqualsConstant")
1162         << instance << "->" << d_false << endl;
1163     return d_false;
1164   }
1165 }
1166
1167 Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite)
1168 {
1169   // intersect the constant ite trees lcite and rcite
1170
1171   if (lcite.isConst() || rcite.isConst())
1172   {
1173     bool lIsConst = lcite.isConst();
1174     TNode constant = lIsConst ? lcite : rcite;
1175     TNode cite = lIsConst ? rcite : lcite;
1176
1177     (d_statistics.d_inSmaller) << 1;
1178     unsigned preItesMade = itesMade;
1179     unsigned preNumBranches = numBranches;
1180     unsigned preNumFalseBranches = numFalseBranches;
1181     Node bterm = constantIteEqualsConstant(cite, constant);
1182     Debug("intersectConstantIte") << (numBranches - preNumBranches) << " "
1183                                   << (numFalseBranches - preNumFalseBranches)
1184                                   << " " << (itesMade - preItesMade) << endl;
1185     return bterm;
1186   }
1187   Assert(lcite.getKind() == kind::ITE);
1188   Assert(rcite.getKind() == kind::ITE);
1189
1190   NodeVec* leftValues = computeConstantLeaves(lcite);
1191   NodeVec* rightValues = computeConstantLeaves(rcite);
1192
1193   uint32_t smaller = std::min(leftValues->size(), rightValues->size());
1194
1195   (d_statistics.d_inSmaller) << smaller;
1196   NodeVec intersection(smaller, Node::null());
1197   NodeVec::iterator newEnd;
1198   newEnd = std::set_intersection(leftValues->begin(),
1199                                  leftValues->end(),
1200                                  rightValues->begin(),
1201                                  rightValues->end(),
1202                                  intersection.begin());
1203   intersection.resize(newEnd - intersection.begin());
1204   if (intersection.empty())
1205   {
1206     return d_false;
1207   }
1208   else
1209   {
1210     NodeBuilder<> nb(kind::OR);
1211     NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
1212     for (; it != end; ++it)
1213     {
1214       Node inBoth = *it;
1215       Node lefteq = constantIteEqualsConstant(lcite, inBoth);
1216       Node righteq = constantIteEqualsConstant(rcite, inBoth);
1217       Node bothHold = lefteq.andNode(righteq);
1218       nb << bothHold;
1219     }
1220     Node result = (nb.getNumChildren() > 1) ? (Node)nb : nb[0];
1221     return result;
1222   }
1223 }
1224
1225 Node ITESimplifier::attemptEagerRemoval(TNode atom)
1226 {
1227   if (atom.getKind() == kind::EQUAL)
1228   {
1229     TNode left = atom[0];
1230     TNode right = atom[1];
1231     if ((left.isConst() && right.getKind() == kind::ITE && isConstantIte(right))
1232         || (right.isConst() && left.getKind() == kind::ITE
1233             && isConstantIte(left)))
1234     {
1235       TNode constant = left.isConst() ? left : right;
1236       TNode cite = left.isConst() ? right : left;
1237
1238       std::pair<Node, Node> pair = make_pair(cite, constant);
1239       NodePairMap::const_iterator eq_pos =
1240           d_constantIteEqualsConstantCache.find(pair);
1241       if (eq_pos != d_constantIteEqualsConstantCache.end())
1242       {
1243         Node ret = (*eq_pos).second;
1244         if (ret.isConst())
1245         {
1246           return ret;
1247         }
1248         else
1249         {
1250           return Node::null();
1251         }
1252       }
1253
1254       NodeVec* leaves = computeConstantLeaves(cite);
1255       Assert(leaves != NULL);
1256       if (!std::binary_search(leaves->begin(), leaves->end(), constant))
1257       {
1258         d_constantIteEqualsConstantCache[pair] = d_false;
1259         return d_false;
1260       }
1261     }
1262   }
1263   return Node::null();
1264 }
1265
1266 Node ITESimplifier::attemptConstantRemoval(TNode atom)
1267 {
1268   if (atom.getKind() == kind::EQUAL)
1269   {
1270     TNode left = atom[0];
1271     TNode right = atom[1];
1272     if (isConstantIte(left) && isConstantIte(right))
1273     {
1274       return intersectConstantIte(left, right);
1275     }
1276   }
1277   return Node::null();
1278 }
1279
1280 bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid)
1281 {
1282   Assert((e.getKind() == kind::ITE && !e.getType().isBoolean())
1283          || theory::Theory::theoryOf(e) != theory::THEORY_BOOL);
1284   if (e.isConst())
1285   {
1286     return true;
1287   }
1288
1289   unordered_map<Node, bool, NodeHashFunction>::iterator it;
1290   it = d_leavesConstCache.find(e);
1291   if (it != d_leavesConstCache.end())
1292   {
1293     return (*it).second;
1294   }
1295
1296   if (!containsTermITE(e) && theory::Theory::isLeafOf(e, tid))
1297   {
1298     d_leavesConstCache[e] = false;
1299     return false;
1300   }
1301
1302   Assert(e.getNumChildren() > 0);
1303   size_t k = 0, sz = e.getNumChildren();
1304
1305   if (e.getKind() == kind::ITE)
1306   {
1307     k = 1;
1308   }
1309
1310   for (; k < sz; ++k)
1311   {
1312     if (!leavesAreConst(e[k], tid))
1313     {
1314       d_leavesConstCache[e] = false;
1315       return false;
1316     }
1317   }
1318   d_leavesConstCache[e] = true;
1319   return true;
1320 }
1321
1322 Node ITESimplifier::simpConstants(TNode simpContext,
1323                                   TNode iteNode,
1324                                   TNode simpVar)
1325 {
1326   NodePairMap::iterator it;
1327   it = d_simpConstCache.find(pair<Node, Node>(simpContext, iteNode));
1328   if (it != d_simpConstCache.end())
1329   {
1330     return (*it).second;
1331   }
1332
1333   if (iteNode.getKind() == kind::ITE)
1334   {
1335     NodeBuilder<> builder(kind::ITE);
1336     builder << iteNode[0];
1337     unsigned i = 1;
1338     for (; i < iteNode.getNumChildren(); ++i)
1339     {
1340       Node n = simpConstants(simpContext, iteNode[i], simpVar);
1341       if (n.isNull())
1342       {
1343         return n;
1344       }
1345       builder << n;
1346     }
1347     // Mark the substitution and continue
1348     Node result = builder;
1349     result = theory::Rewriter::rewrite(result);
1350     d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
1351     return result;
1352   }
1353
1354   if (!containsTermITE(iteNode))
1355   {
1356     Node n =
1357         theory::Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
1358     d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
1359     return n;
1360   }
1361
1362   Node iteNode2;
1363   Node simpVar2;
1364   d_simpContextCache.clear();
1365   Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
1366   if (!simpContext2.isNull())
1367   {
1368     Assert(!iteNode2.isNull());
1369     simpContext2 = simpContext.substitute(simpVar, simpContext2);
1370     Node n = simpConstants(simpContext2, iteNode2, simpVar2);
1371     if (n.isNull())
1372     {
1373       return n;
1374     }
1375     d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
1376     return n;
1377   }
1378   return Node();
1379 }
1380
1381 Node ITESimplifier::getSimpVar(TypeNode t)
1382 {
1383   std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
1384   it = d_simpVars.find(t);
1385   if (it != d_simpVars.end())
1386   {
1387     return (*it).second;
1388   }
1389   else
1390   {
1391     Node var = NodeManager::currentNM()->mkSkolem(
1392         "iteSimp", t, "is a variable resulting from ITE simplification");
1393     d_simpVars[t] = var;
1394     return var;
1395   }
1396 }
1397
1398 Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
1399 {
1400   NodeMap::iterator it;
1401   it = d_simpContextCache.find(c);
1402   if (it != d_simpContextCache.end())
1403   {
1404     return (*it).second;
1405   }
1406
1407   if (!containsTermITE(c))
1408   {
1409     d_simpContextCache[c] = c;
1410     return c;
1411   }
1412
1413   if (c.getKind() == kind::ITE && !c.getType().isBoolean())
1414   {
1415     // Currently only support one ite node in a simp context
1416     // Return Null if more than one is found
1417     if (!iteNode.isNull())
1418     {
1419       return Node();
1420     }
1421     simpVar = getSimpVar(c.getType());
1422     if (simpVar.isNull())
1423     {
1424       return Node();
1425     }
1426     d_simpContextCache[c] = simpVar;
1427     iteNode = c;
1428     return simpVar;
1429   }
1430
1431   NodeBuilder<> builder(c.getKind());
1432   if (c.getMetaKind() == kind::metakind::PARAMETERIZED)
1433   {
1434     builder << c.getOperator();
1435   }
1436   unsigned i = 0;
1437   for (; i < c.getNumChildren(); ++i)
1438   {
1439     Node newChild = createSimpContext(c[i], iteNode, simpVar);
1440     if (newChild.isNull())
1441     {
1442       return newChild;
1443     }
1444     builder << newChild;
1445   }
1446   // Mark the substitution and continue
1447   Node result = builder;
1448   d_simpContextCache[c] = result;
1449   return result;
1450 }
1451 typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
1452 void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached)
1453 {
1454   if (visited.find(x) != visited.end())
1455   {
1456     return;
1457   }
1458   visited.insert(x);
1459   if (x.getKind() == k)
1460   {
1461     ++reached;
1462   }
1463   for (unsigned i = 0, N = x.getNumChildren(); i < N; ++i)
1464   {
1465     countReachable_(x[i], k, visited, reached);
1466   }
1467 }
1468
1469 uint32_t countReachable(TNode x, Kind k)
1470 {
1471   NodeSet visited;
1472   uint32_t reached = 0;
1473   countReachable_(x, k, visited, reached);
1474   return reached;
1475 }
1476
1477 Node ITESimplifier::simpITEAtom(TNode atom)
1478 {
1479   static int CVC4_UNUSED instance = 0;
1480   Debug("ite::atom") << "still simplifying " << (++instance) << endl;
1481   Node attempt = transformAtom(atom);
1482   Debug("ite::atom") << "  finished " << instance << endl;
1483   if (!attempt.isNull())
1484   {
1485     Node rewritten = theory::Rewriter::rewrite(attempt);
1486     Debug("ite::print-success")
1487         << instance << " "
1488         << "rewriting " << countReachable(rewritten, kind::ITE) << " from "
1489         << countReachable(atom, kind::ITE) << endl
1490         << "\t rewritten " << rewritten << endl
1491         << "\t input " << atom << endl;
1492     return rewritten;
1493   }
1494
1495   if (leavesAreConst(atom))
1496   {
1497     Node iteNode;
1498     Node simpVar;
1499     d_simpContextCache.clear();
1500     Node simpContext = createSimpContext(atom, iteNode, simpVar);
1501     if (!simpContext.isNull())
1502     {
1503       if (iteNode.isNull())
1504       {
1505         Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
1506         ++(d_statistics.d_unexpected);
1507         Debug("ite::simpite") << instance << " "
1508                               << "how about?" << atom << endl;
1509         Debug("ite::simpite") << instance << " "
1510                               << "\t" << simpContext << endl;
1511         return theory::Rewriter::rewrite(simpContext);
1512       }
1513       Node n = simpConstants(simpContext, iteNode, simpVar);
1514       if (!n.isNull())
1515       {
1516         ++(d_statistics.d_unexpected);
1517         Debug("ite::simpite") << instance << " "
1518                               << "here?" << atom << endl;
1519         Debug("ite::simpite") << instance << " "
1520                               << "\t" << n << endl;
1521         return n;
1522       }
1523     }
1524   }
1525   if (Debug.isOn("ite::simpite"))
1526   {
1527     if (countReachable(atom, kind::ITE) > 0)
1528     {
1529       Debug("ite::simpite") << instance << " "
1530                             << "remaining " << atom << endl;
1531     }
1532   }
1533   ++(d_statistics.d_unsimplified);
1534   return atom;
1535 }
1536
1537 struct preprocess_stack_element
1538 {
1539   TNode d_node;
1540   bool d_children_added;
1541   preprocess_stack_element(TNode node) : d_node(node), d_children_added(false)
1542   {
1543   }
1544 }; /* struct preprocess_stack_element */
1545
1546 Node ITESimplifier::simpITE(TNode assertion)
1547 {
1548   // Do a topological sort of the subexpressions and substitute them
1549   vector<preprocess_stack_element> toVisit;
1550   toVisit.push_back(assertion);
1551
1552   static int call = 0;
1553   ++call;
1554   int iteration = 0;
1555
1556   while (!toVisit.empty())
1557   {
1558     iteration++;
1559     // cout << "call  " << call << " : " << iteration << endl;
1560     // The current node we are processing
1561     preprocess_stack_element& stackHead = toVisit.back();
1562     TNode current = stackHead.d_node;
1563
1564     // If node has no ITE's or already in the cache we're done, pop from the
1565     // stack
1566     if (current.getNumChildren() == 0
1567         || (theory::Theory::theoryOf(current) != theory::THEORY_BOOL
1568             && !containsTermITE(current)))
1569     {
1570       d_simpITECache[current] = current;
1571       ++(d_statistics.d_simpITEVisits);
1572       toVisit.pop_back();
1573       continue;
1574     }
1575
1576     NodeMap::iterator find = d_simpITECache.find(current);
1577     if (find != d_simpITECache.end())
1578     {
1579       toVisit.pop_back();
1580       continue;
1581     }
1582
1583     // Not yet substituted, so process
1584     if (stackHead.d_children_added)
1585     {
1586       // Children have been processed, so substitute
1587       NodeBuilder<> builder(current.getKind());
1588       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
1589       {
1590         builder << current.getOperator();
1591       }
1592       for (unsigned i = 0; i < current.getNumChildren(); ++i)
1593       {
1594         Assert(d_simpITECache.find(current[i]) != d_simpITECache.end());
1595         Node child = current[i];
1596         Node childRes = d_simpITECache[current[i]];
1597         builder << childRes;
1598       }
1599       // Mark the substitution and continue
1600       Node result = builder;
1601
1602       // If this is an atom, we process it
1603       if (theory::Theory::theoryOf(result) != theory::THEORY_BOOL
1604           && result.getType().isBoolean())
1605       {
1606         result = simpITEAtom(result);
1607       }
1608
1609       // if(current != result && result.isConst()){
1610       //   static int instance = 0;
1611       //   //cout << instance << " " << result << current << endl;
1612       // }
1613
1614       result = theory::Rewriter::rewrite(result);
1615       d_simpITECache[current] = result;
1616       ++(d_statistics.d_simpITEVisits);
1617       toVisit.pop_back();
1618     }
1619     else
1620     {
1621       // Mark that we have added the children if any
1622       if (current.getNumChildren() > 0)
1623       {
1624         stackHead.d_children_added = true;
1625         // We need to add the children
1626         for (TNode::iterator child_it = current.begin();
1627              child_it != current.end();
1628              ++child_it)
1629         {
1630           TNode childNode = *child_it;
1631           NodeMap::iterator childFind = d_simpITECache.find(childNode);
1632           if (childFind == d_simpITECache.end())
1633           {
1634             toVisit.push_back(childNode);
1635           }
1636         }
1637       }
1638       else
1639       {
1640         // No children, so we're done
1641         d_simpITECache[current] = current;
1642         ++(d_statistics.d_simpITEVisits);
1643         toVisit.pop_back();
1644       }
1645     }
1646   }
1647   return d_simpITECache[assertion];
1648 }
1649
1650 ITECareSimplifier::ITECareSimplifier() : d_careSetsOutstanding(0), d_usedSets()
1651 {
1652   d_true = NodeManager::currentNM()->mkConst<bool>(true);
1653   d_false = NodeManager::currentNM()->mkConst<bool>(false);
1654 }
1655
1656 ITECareSimplifier::~ITECareSimplifier()
1657 {
1658   Assert(d_usedSets.empty());
1659   Assert(d_careSetsOutstanding == 0);
1660 }
1661
1662 void ITECareSimplifier::clear()
1663 {
1664   Assert(d_usedSets.empty());
1665   Assert(d_careSetsOutstanding == 0);
1666 }
1667
1668 ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
1669 {
1670   if (d_usedSets.empty())
1671   {
1672     d_careSetsOutstanding++;
1673     return ITECareSimplifier::CareSetPtr::mkNew(*this);
1674   }
1675   else
1676   {
1677     ITECareSimplifier::CareSetPtr cs =
1678         ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
1679     cs.getCareSet().clear();
1680     d_usedSets.pop_back();
1681     return cs;
1682   }
1683 }
1684
1685 void ITECareSimplifier::updateQueue(CareMap& queue,
1686                                     TNode e,
1687                                     ITECareSimplifier::CareSetPtr& careSet)
1688 {
1689   CareMap::iterator it = queue.find(e), iend = queue.end();
1690   if (it != iend)
1691   {
1692     set<Node>& cs2 = (*it).second.getCareSet();
1693     ITECareSimplifier::CareSetPtr csNew = getNewSet();
1694     set_intersection(careSet.getCareSet().begin(),
1695                      careSet.getCareSet().end(),
1696                      cs2.begin(),
1697                      cs2.end(),
1698                      inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
1699     (*it).second = csNew;
1700   }
1701   else
1702   {
1703     queue[e] = careSet;
1704   }
1705 }
1706
1707 Node ITECareSimplifier::substitute(TNode e,
1708                                    TNodeMap& substTable,
1709                                    TNodeMap& cache)
1710 {
1711   TNodeMap::iterator it = cache.find(e), iend = cache.end();
1712   if (it != iend)
1713   {
1714     return it->second;
1715   }
1716
1717   // do substitution?
1718   it = substTable.find(e);
1719   iend = substTable.end();
1720   if (it != iend)
1721   {
1722     Node result = substitute(it->second, substTable, cache);
1723     cache[e] = result;
1724     return result;
1725   }
1726
1727   size_t sz = e.getNumChildren();
1728   if (sz == 0)
1729   {
1730     cache[e] = e;
1731     return e;
1732   }
1733
1734   NodeBuilder<> builder(e.getKind());
1735   if (e.getMetaKind() == kind::metakind::PARAMETERIZED)
1736   {
1737     builder << e.getOperator();
1738   }
1739   for (unsigned i = 0; i < e.getNumChildren(); ++i)
1740   {
1741     builder << substitute(e[i], substTable, cache);
1742   }
1743
1744   Node result = builder;
1745   // it = substTable.find(result);
1746   // if (it != iend) {
1747   //   result = substitute(it->second, substTable, cache);
1748   // }
1749   cache[e] = result;
1750   return result;
1751 }
1752
1753 Node ITECareSimplifier::simplifyWithCare(TNode e)
1754 {
1755   TNodeMap substTable;
1756
1757   /* This extra block is to trigger the destructors for cs and cs2
1758    * before starting garbage collection.
1759    */
1760   {
1761     CareMap queue;
1762     CareMap::iterator it;
1763     ITECareSimplifier::CareSetPtr cs = getNewSet();
1764     ITECareSimplifier::CareSetPtr cs2;
1765     queue[e] = cs;
1766
1767     TNode v;
1768     bool done;
1769     unsigned i;
1770
1771     while (!queue.empty())
1772     {
1773       it = queue.end();
1774       --it;
1775       v = it->first;
1776       cs = it->second;
1777       set<Node>& css = cs.getCareSet();
1778       queue.erase(v);
1779
1780       done = false;
1781       set<Node>::iterator iCare, iCareEnd = css.end();
1782
1783       switch (v.getKind())
1784       {
1785         case kind::ITE:
1786         {
1787           iCare = css.find(v[0]);
1788           if (iCare != iCareEnd)
1789           {
1790             Assert(substTable.find(v) == substTable.end());
1791             substTable[v] = v[1];
1792             updateQueue(queue, v[1], cs);
1793             done = true;
1794             break;
1795           }
1796           else
1797           {
1798             iCare = css.find(v[0].negate());
1799             if (iCare != iCareEnd)
1800             {
1801               Assert(substTable.find(v) == substTable.end());
1802               substTable[v] = v[2];
1803               updateQueue(queue, v[2], cs);
1804               done = true;
1805               break;
1806             }
1807           }
1808           updateQueue(queue, v[0], cs);
1809           cs2 = getNewSet();
1810           cs2.getCareSet() = css;
1811           cs2.getCareSet().insert(v[0]);
1812           updateQueue(queue, v[1], cs2);
1813           cs2 = getNewSet();
1814           cs2.getCareSet() = css;
1815           cs2.getCareSet().insert(v[0].negate());
1816           updateQueue(queue, v[2], cs2);
1817           done = true;
1818           break;
1819         }
1820         case kind::AND:
1821         {
1822           for (i = 0; i < v.getNumChildren(); ++i)
1823           {
1824             iCare = css.find(v[i].negate());
1825             if (iCare != iCareEnd)
1826             {
1827               Assert(substTable.find(v) == substTable.end());
1828               substTable[v] = d_false;
1829               done = true;
1830               break;
1831             }
1832           }
1833           if (done) break;
1834
1835           Assert(v.getNumChildren() > 1);
1836           updateQueue(queue, v[0], cs);
1837           cs2 = getNewSet();
1838           cs2.getCareSet() = css;
1839           cs2.getCareSet().insert(v[0]);
1840           for (i = 1; i < v.getNumChildren(); ++i)
1841           {
1842             updateQueue(queue, v[i], cs2);
1843           }
1844           done = true;
1845           break;
1846         }
1847         case kind::OR:
1848         {
1849           for (i = 0; i < v.getNumChildren(); ++i)
1850           {
1851             iCare = css.find(v[i]);
1852             if (iCare != iCareEnd)
1853             {
1854               Assert(substTable.find(v) == substTable.end());
1855               substTable[v] = d_true;
1856               done = true;
1857               break;
1858             }
1859           }
1860           if (done) break;
1861
1862           Assert(v.getNumChildren() > 1);
1863           updateQueue(queue, v[0], cs);
1864           cs2 = getNewSet();
1865           cs2.getCareSet() = css;
1866           cs2.getCareSet().insert(v[0].negate());
1867           for (i = 1; i < v.getNumChildren(); ++i)
1868           {
1869             updateQueue(queue, v[i], cs2);
1870           }
1871           done = true;
1872           break;
1873         }
1874         default: break;
1875       }
1876
1877       if (done)
1878       {
1879         continue;
1880       }
1881
1882       for (i = 0; i < v.getNumChildren(); ++i)
1883       {
1884         updateQueue(queue, v[i], cs);
1885       }
1886     }
1887   }
1888   /* Perform garbage collection. */
1889   while (!d_usedSets.empty())
1890   {
1891     CareSetPtrVal* used = d_usedSets.back();
1892     d_usedSets.pop_back();
1893     Assert(used->safeToGarbageCollect());
1894     delete used;
1895     Assert(d_careSetsOutstanding > 0);
1896     d_careSetsOutstanding--;
1897   }
1898
1899   TNodeMap cache;
1900   return substitute(e, substTable, cache);
1901 }
1902
1903 ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew(
1904     ITECareSimplifier& simp)
1905 {
1906   CareSetPtrVal* val = new CareSetPtrVal(simp);
1907   return CareSetPtr(val);
1908 }
1909
1910 }  // namespace util
1911 }  // namespace preprocessing
1912 }  // namespace cvc5