src/preprocessing/passes/ite_simp.cpp

   1 /*********************                                                        */
   2 /*! \file ite_simp.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Tim King, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief ITE simplification preprocessing pass.
  13  **/
  14
  15 #include "preprocessing/passes/ite_simp.h"
  16
  17 #include <vector>
  18
  19 #include "options/smt_options.h"
  20 #include "smt/smt_statistics_registry.h"
  21 #include "smt_util/nary_builder.h"
  22 #include "theory/arith/arith_ite_utils.h"
  23
  24 using namespace CVC4;
  25 using namespace CVC4::theory;
  26
  27 namespace CVC4 {
  28 namespace preprocessing {
  29 namespace passes {
  30
  31 /* -------------------------------------------------------------------------- */
  32
  33 namespace {
  34
  35 Node simpITE(util::ITEUtilities* ite_utils, TNode assertion)
  36 {
  37   if (!ite_utils->containsTermITE(assertion))
  38   {
  39     return assertion;
  40   }
  41   else
  42   {
  43     Node result = ite_utils->simpITE(assertion);
  44     Node res_rewritten = Rewriter::rewrite(result);
  45
  46     if (options::simplifyWithCareEnabled())
  47     {
  48       Chat() << "starting simplifyWithCare()" << endl;
  49       Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten);
  50       Chat() << "ending simplifyWithCare()"
  51              << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
  52       result = Rewriter::rewrite(postSimpWithCare);
  53     }
  54     else
  55     {
  56       result = res_rewritten;
  57     }
  58     return result;
  59   }
  60 }
  61
  62 /**
  63  * Ensures the assertions asserted after index 'before' now effectively come
  64  * before 'real_assertions_end'.
  65  */
  66 void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess,
  67                                   size_t before)
  68 {
  69   size_t cur_size = assertionsToPreprocess->size();
  70   if (before >= cur_size || assertionsToPreprocess->getRealAssertionsEnd() <= 0
  71       || assertionsToPreprocess->getRealAssertionsEnd() >= cur_size)
  72   {
  73     return;
  74   }
  75
  76   // assertions
  77   // original: [0 ... assertionsToPreprocess.getRealAssertionsEnd())
  78   //  can be modified
  79   // ites skolems [assertionsToPreprocess.getRealAssertionsEnd(), before)
  80   //  cannot be moved
  81   // added [before, cur_size)
  82   //  can be modified
  83   Assert(0 < assertionsToPreprocess->getRealAssertionsEnd());
  84   Assert(assertionsToPreprocess->getRealAssertionsEnd() <= before);
  85   Assert(before < cur_size);
  86
  87   std::vector<Node> intoConjunction;
  88   for (size_t i = before; i < cur_size; ++i)
  89   {
  90     intoConjunction.push_back((*assertionsToPreprocess)[i]);
  91   }
  92   assertionsToPreprocess->resize(before);
  93   size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1;
  94   intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]);
  95   Node newLast = CVC4::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
  96   assertionsToPreprocess->replace(lastBeforeItes, newLast);
  97   Assert(assertionsToPreprocess->size() == before);
  98 }
  99
 100 }  // namespace
 101
 102 /* -------------------------------------------------------------------------- */
 103
 104 ITESimp::Statistics::Statistics()
 105     : d_arithSubstitutionsAdded(
 106           "preprocessing::passes::ITESimp::ArithSubstitutionsAdded", 0)
 107 {
 108   smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
 109 }
 110
 111 ITESimp::Statistics::~Statistics()
 112 {
 113   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 114 }
 115
 116 bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
 117 {
 118   Assert(!options::unsatCores());
 119   bool result = true;
 120   bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
 121   if (simpDidALotOfWork)
 122   {
 123     if (options::compressItes())
 124     {
 125       result = d_iteUtilities.compress(assertionsToPreprocess);
 126     }
 127
 128     if (result)
 129     {
 130       // if false, don't bother to reclaim memory here.
 131       NodeManager* nm = NodeManager::currentNM();
 132       if (nm->poolSize() >= options::zombieHuntThreshold())
 133       {
 134         Chat() << "..ite simplifier did quite a bit of work.. "
 135                << nm->poolSize() << endl;
 136         Chat() << "....node manager contains " << nm->poolSize()
 137                << " nodes before cleanup" << endl;
 138         d_iteUtilities.clear();
 139         Rewriter::clearCaches();
 140         nm->reclaimZombiesUntil(options::zombieHuntThreshold());
 141         Chat() << "....node manager contains " << nm->poolSize()
 142                << " nodes after cleanup" << endl;
 143       }
 144     }
 145   }
 146
 147   // Do theory specific preprocessing passes
 148   TheoryEngine* theory_engine = d_preprocContext->getTheoryEngine();
 149   if (theory_engine->getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH)
 150       && !options::incrementalSolving())
 151   {
 152     if (!simpDidALotOfWork)
 153     {
 154       util::ContainsTermITEVisitor& contains =
 155           *(d_iteUtilities.getContainsVisitor());
 156       arith::ArithIteUtils aiteu(contains,
 157                                  d_preprocContext->getUserContext(),
 158                                  theory_engine->getModel());
 159       bool anyItes = false;
 160       for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
 161       {
 162         Node curr = (*assertionsToPreprocess)[i];
 163         if (contains.containsTermITE(curr))
 164         {
 165           anyItes = true;
 166           Node res = aiteu.reduceVariablesInItes(curr);
 167           Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl
 168                                    << "   ->" << res << endl;
 169           if (curr != res)
 170           {
 171             Node more = aiteu.reduceConstantIteByGCD(res);
 172             Debug("arith::ite::red") << "  gcd->" << more << endl;
 173             Node morer = Rewriter::rewrite(more);
 174             assertionsToPreprocess->replace(i, morer);
 175           }
 176         }
 177       }
 178       if (!anyItes)
 179       {
 180         unsigned prevSubCount = aiteu.getSubCount();
 181         aiteu.learnSubstitutions(assertionsToPreprocess->ref());
 182         if (prevSubCount < aiteu.getSubCount())
 183         {
 184           d_statistics.d_arithSubstitutionsAdded +=
 185               aiteu.getSubCount() - prevSubCount;
 186           bool anySuccess = false;
 187           for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
 188           {
 189             Node curr = (*assertionsToPreprocess)[i];
 190             Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
 191             Node res = aiteu.reduceVariablesInItes(next);
 192             Debug("arith::ite::red") << "@ " << i << " ... " << next << endl
 193                                      << "   ->" << res << endl;
 194             Node more = aiteu.reduceConstantIteByGCD(res);
 195             Debug("arith::ite::red") << "  gcd->" << more << endl;
 196             if (more != next)
 197             {
 198               anySuccess = true;
 199               break;
 200             }
 201           }
 202           for (size_t i = 0, N = assertionsToPreprocess->size();
 203                anySuccess && i < N;
 204                ++i)
 205           {
 206             Node curr = (*assertionsToPreprocess)[i];
 207             Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
 208             Node res = aiteu.reduceVariablesInItes(next);
 209             Debug("arith::ite::red") << "@ " << i << " ... " << next << endl
 210                                      << "   ->" << res << endl;
 211             Node more = aiteu.reduceConstantIteByGCD(res);
 212             Debug("arith::ite::red") << "  gcd->" << more << endl;
 213             Node morer = Rewriter::rewrite(more);
 214             assertionsToPreprocess->replace(i, morer);
 215           }
 216         }
 217       }
 218     }
 219   }
 220   return result;
 221 }
 222
 223 /* -------------------------------------------------------------------------- */
 224
 225 ITESimp::ITESimp(PreprocessingPassContext* preprocContext)
 226     : PreprocessingPass(preprocContext, "ite-simp")
 227 {
 228 }
 229
 230 PreprocessingPassResult ITESimp::applyInternal(
 231     AssertionPipeline* assertionsToPreprocess)
 232 {
 233   d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 234
 235   size_t nasserts = assertionsToPreprocess->size();
 236   for (size_t i = 0; i < nasserts; ++i)
 237   {
 238     d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 239     Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]);
 240     assertionsToPreprocess->replace(i, simp);
 241     if (simp.isConst() && !simp.getConst<bool>())
 242     {
 243       return PreprocessingPassResult::CONFLICT;
 244     }
 245   }
 246   bool done = doneSimpITE(assertionsToPreprocess);
 247   if (nasserts < assertionsToPreprocess->size())
 248   {
 249     compressBeforeRealAssertions(assertionsToPreprocess, nasserts);
 250   }
 251   return done ? PreprocessingPassResult::NO_CONFLICT
 252               : PreprocessingPassResult::CONFLICT;
 253 }
 254
 255
 256 /* -------------------------------------------------------------------------- */
 257
 258 }  // namespace passes
 259 }  // namespace preprocessing
 260 }  // namespace CVC4