src/smt/process_assertions.cpp

   1 /*********************                                                        */
   2 /*! \file process_assertions.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Yoni Zohar, Mathias Preiner
   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 Implementation of module for processing assertions for an SMT engine.
  13  **/
  14
  15 #include "smt/process_assertions.h"
  16
  17 #include <stack>
  18 #include <utility>
  19
  20 #include "expr/node_manager_attributes.h"
  21 #include "options/arith_options.h"
  22 #include "options/base_options.h"
  23 #include "options/bv_options.h"
  24 #include "options/quantifiers_options.h"
  25 #include "options/sep_options.h"
  26 #include "options/smt_options.h"
  27 #include "options/uf_options.h"
  28 #include "preprocessing/assertion_pipeline.h"
  29 #include "preprocessing/preprocessing_pass_registry.h"
  30 #include "printer/printer.h"
  31 #include "smt/defined_function.h"
  32 #include "smt/dump.h"
  33 #include "smt/smt_engine.h"
  34 #include "theory/logic_info.h"
  35 #include "theory/theory_engine.h"
  36
  37 using namespace CVC4::preprocessing;
  38 using namespace CVC4::theory;
  39 using namespace CVC4::kind;
  40
  41 namespace CVC4 {
  42 namespace smt {
  43
  44 /** Useful for counting the number of recursive calls. */
  45 class ScopeCounter
  46 {
  47  public:
  48   ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
  49   ~ScopeCounter() { --d_depth; }
  50
  51  private:
  52   unsigned& d_depth;
  53 };
  54
  55 ProcessAssertions::ProcessAssertions(SmtEngine& smt,
  56                                      ExpandDefs& exDefs,
  57                                      ResourceManager& rm,
  58                                      SmtEngineStatistics& stats)
  59     : d_smt(smt),
  60       d_exDefs(exDefs),
  61       d_resourceManager(rm),
  62       d_smtStats(stats),
  63       d_preprocessingPassContext(nullptr)
  64 {
  65   d_true = NodeManager::currentNM()->mkConst(true);
  66 }
  67
  68 ProcessAssertions::~ProcessAssertions()
  69 {
  70 }
  71
  72 void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
  73 {
  74   Assert(d_preprocessingPassContext == nullptr);
  75   d_preprocessingPassContext = pc;
  76
  77   PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
  78   // TODO: this will likely change when we add support for actually assembling
  79   // preprocessing pipelines. For now, we just create an instance of each
  80   // available preprocessing pass.
  81   std::vector<std::string> passNames = ppReg.getAvailablePasses();
  82   for (const std::string& passName : passNames)
  83   {
  84     d_passes[passName].reset(
  85         ppReg.createPass(d_preprocessingPassContext, passName));
  86   }
  87 }
  88
  89 void ProcessAssertions::cleanup() { d_passes.clear(); }
  90
  91 void ProcessAssertions::spendResource(ResourceManager::Resource r)
  92 {
  93   d_resourceManager.spendResource(r);
  94 }
  95
  96 bool ProcessAssertions::apply(Assertions& as)
  97 {
  98   AssertionPipeline& assertions = as.getAssertionPipeline();
  99   Assert(d_preprocessingPassContext != nullptr);
 100   // Dump the assertions
 101   dumpAssertions("pre-everything", assertions);
 102
 103   Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
 104   Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
 105
 106   Debug("smt") << "#Assertions : " << assertions.size() << endl;
 107   Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;
 108
 109   if (assertions.size() == 0)
 110   {
 111     // nothing to do
 112     return true;
 113   }
 114
 115   if (options::bvGaussElim())
 116   {
 117     d_passes["bv-gauss"]->apply(&assertions);
 118   }
 119
 120   // Add dummy assertion in last position - to be used as a
 121   // placeholder for any new assertions to get added
 122   assertions.push_back(d_true);
 123   // any assertions added beyond realAssertionsEnd must NOT affect the
 124   // equisatisfiability
 125   assertions.updateRealAssertionsEnd();
 126
 127   // Assertions are NOT guaranteed to be rewritten by this point
 128
 129   Trace("smt-proc")
 130       << "ProcessAssertions::processAssertions() : pre-definition-expansion"
 131       << endl;
 132   dumpAssertions("pre-definition-expansion", assertions);
 133   // Expand definitions, which replaces defined functions with their definition
 134   // and does beta reduction. Notice we pass true as the second argument since
 135   // we do not want to call theories to expand definitions here, since we want
 136   // to give the opportunity to rewrite/preprocess terms before expansion.
 137   d_exDefs.expandAssertions(assertions, true);
 138   Trace("smt-proc")
 139       << "ProcessAssertions::processAssertions() : post-definition-expansion"
 140       << endl;
 141   dumpAssertions("post-definition-expansion", assertions);
 142
 143   Debug("smt") << " assertions     : " << assertions.size() << endl;
 144
 145   if (options::globalNegate())
 146   {
 147     // global negation of the formula
 148     d_passes["global-negate"]->apply(&assertions);
 149     as.flipGlobalNegated();
 150   }
 151
 152   if (options::nlExtPurify())
 153   {
 154     d_passes["nl-ext-purify"]->apply(&assertions);
 155   }
 156
 157   if (options::solveRealAsInt())
 158   {
 159     d_passes["real-to-int"]->apply(&assertions);
 160   }
 161
 162   if (options::solveIntAsBV() > 0)
 163   {
 164     d_passes["int-to-bv"]->apply(&assertions);
 165   }
 166
 167   if (options::ackermann())
 168   {
 169     d_passes["ackermann"]->apply(&assertions);
 170   }
 171
 172   if (options::bvAbstraction())
 173   {
 174     d_passes["bv-abstraction"]->apply(&assertions);
 175   }
 176
 177   Debug("smt") << " assertions     : " << assertions.size() << endl;
 178
 179   bool noConflict = true;
 180
 181   if (options::extRewPrep())
 182   {
 183     d_passes["ext-rew-pre"]->apply(&assertions);
 184   }
 185
 186   // Unconstrained simplification
 187   if (options::unconstrainedSimp())
 188   {
 189     d_passes["rewrite"]->apply(&assertions);
 190     d_passes["unconstrained-simplifier"]->apply(&assertions);
 191   }
 192
 193   if (options::bvIntroducePow2())
 194   {
 195     d_passes["bv-intro-pow2"]->apply(&assertions);
 196   }
 197
 198   // Lift bit-vectors of size 1 to bool
 199   if (options::bitvectorToBool())
 200   {
 201     d_passes["bv-to-bool"]->apply(&assertions);
 202   }
 203   if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
 204   {
 205     d_passes["bv-to-int"]->apply(&assertions);
 206   }
 207   if (options::foreignTheoryRewrite())
 208   {
 209     d_passes["foreign-theory-rewrite"]->apply(&assertions);
 210   }
 211
 212   // Since this pass is not robust for the information tracking necessary for
 213   // unsat cores, it's only applied if we are not doing unsat core computation
 214   d_passes["apply-substs"]->apply(&assertions);
 215
 216   // Assertions MUST BE guaranteed to be rewritten by this point
 217   d_passes["rewrite"]->apply(&assertions);
 218
 219   // Convert non-top-level Booleans to bit-vectors of size 1
 220   if (options::boolToBitvector() != options::BoolToBVMode::OFF)
 221   {
 222     d_passes["bool-to-bv"]->apply(&assertions);
 223   }
 224   if (options::sepPreSkolemEmp())
 225   {
 226     d_passes["sep-skolem-emp"]->apply(&assertions);
 227   }
 228
 229   if (d_smt.getLogicInfo().isQuantified())
 230   {
 231     // remove rewrite rules, apply pre-skolemization to existential quantifiers
 232     d_passes["quantifiers-preprocess"]->apply(&assertions);
 233     if (options::macrosQuant())
 234     {
 235       // quantifiers macro expansion
 236       d_passes["quantifier-macros"]->apply(&assertions);
 237     }
 238
 239     // fmf-fun : assume admissible functions, applying preprocessing reduction
 240     // to FMF
 241     if (options::fmfFunWellDefined())
 242     {
 243       d_passes["fun-def-fmf"]->apply(&assertions);
 244     }
 245   }
 246
 247   if (options::sortInference() || options::ufssFairnessMonotone())
 248   {
 249     d_passes["sort-inference"]->apply(&assertions);
 250   }
 251
 252   if (options::pbRewrites())
 253   {
 254     d_passes["pseudo-boolean-processor"]->apply(&assertions);
 255   }
 256
 257   // rephrasing normal inputs as sygus problems
 258   if (!d_smt.isInternalSubsolver())
 259   {
 260     if (options::sygusInference())
 261     {
 262       d_passes["sygus-infer"]->apply(&assertions);
 263     }
 264     else if (options::sygusRewSynthInput())
 265     {
 266       // do candidate rewrite rule synthesis
 267       d_passes["synth-rr"]->apply(&assertions);
 268     }
 269   }
 270
 271   Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
 272                     << endl;
 273   dumpAssertions("pre-simplify", assertions);
 274   Chat() << "simplifying assertions..." << endl;
 275   noConflict = simplifyAssertions(assertions);
 276   if (!noConflict)
 277   {
 278     ++(d_smtStats.d_simplifiedToFalse);
 279   }
 280   Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
 281                     << endl;
 282   dumpAssertions("post-simplify", assertions);
 283
 284   if (options::doStaticLearning())
 285   {
 286     d_passes["static-learning"]->apply(&assertions);
 287   }
 288   Debug("smt") << " assertions     : " << assertions.size() << endl;
 289
 290   if (options::earlyIteRemoval())
 291   {
 292     d_smtStats.d_numAssertionsPre += assertions.size();
 293     d_passes["ite-removal"]->apply(&assertions);
 294     // This is needed because when solving incrementally, removeITEs may
 295     // introduce skolems that were solved for earlier and thus appear in the
 296     // substitution map.
 297     d_passes["apply-substs"]->apply(&assertions);
 298     d_smtStats.d_numAssertionsPost += assertions.size();
 299   }
 300
 301   dumpAssertions("pre-repeat-simplify", assertions);
 302   if (options::repeatSimp())
 303   {
 304     Trace("smt-proc")
 305         << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
 306         << endl;
 307     Chat() << "re-simplifying assertions..." << endl;
 308     ScopeCounter depth(d_simplifyAssertionsDepth);
 309     noConflict &= simplifyAssertions(assertions);
 310     Trace("smt-proc")
 311         << "ProcessAssertions::processAssertions() : post-repeat-simplify"
 312         << endl;
 313   }
 314   dumpAssertions("post-repeat-simplify", assertions);
 315
 316   if (options::ufHo())
 317   {
 318     d_passes["ho-elim"]->apply(&assertions);
 319   }
 320
 321   // begin: INVARIANT to maintain: no reordering of assertions or
 322   // introducing new ones
 323
 324   Debug("smt") << " assertions     : " << assertions.size() << endl;
 325
 326   Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
 327                << endl;
 328   Debug("smt") << " assertions     : " << assertions.size() << endl;
 329
 330   // ensure rewritten
 331   d_passes["rewrite"]->apply(&assertions);
 332   // rewrite equalities based on theory-specific rewriting
 333   d_passes["theory-rewrite-eq"]->apply(&assertions);
 334   // apply theory preprocess, which includes ITE removal
 335   d_passes["theory-preprocess"]->apply(&assertions);
 336   // This is needed because when solving incrementally, removeITEs may
 337   // introduce skolems that were solved for earlier and thus appear in the
 338   // substitution map.
 339   d_passes["apply-substs"]->apply(&assertions);
 340
 341   if (options::bitblastMode() == options::BitblastMode::EAGER)
 342   {
 343     d_passes["bv-eager-atoms"]->apply(&assertions);
 344   }
 345
 346   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
 347   dumpAssertions("post-everything", assertions);
 348
 349   return noConflict;
 350 }
 351
 352 // returns false if simplification led to "false"
 353 bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
 354 {
 355   spendResource(ResourceManager::Resource::PreprocessStep);
 356   try
 357   {
 358     ScopeCounter depth(d_simplifyAssertionsDepth);
 359
 360     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
 361
 362     if (options::simplificationMode() != options::SimplificationMode::NONE)
 363     {
 364       // Perform non-clausal simplification
 365       PreprocessingPassResult res =
 366           d_passes["non-clausal-simp"]->apply(&assertions);
 367       if (res == PreprocessingPassResult::CONFLICT)
 368       {
 369         return false;
 370       }
 371
 372       // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
 373       // do the miplib trick.
 374       if (  // check that option is on
 375           options::arithMLTrick() &&
 376           // only useful in arith
 377           d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
 378           // we add new assertions and need this (in practice, this
 379           // restriction only disables miplib processing during
 380           // re-simplification, which we don't expect to be useful anyway)
 381           assertions.getRealAssertionsEnd() == assertions.size())
 382       {
 383         d_passes["miplib-trick"]->apply(&assertions);
 384       }
 385       else
 386       {
 387         Trace("simplify") << "SmtEnginePrivate::simplify(): "
 388                           << "skipping miplib pseudobooleans pass..." << endl;
 389       }
 390     }
 391
 392     Debug("smt") << " assertions     : " << assertions.size() << endl;
 393
 394     // ITE simplification
 395     if (options::doITESimp()
 396         && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
 397     {
 398       PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
 399       if (res == PreprocessingPassResult::CONFLICT)
 400       {
 401         Chat() << "...ITE simplification found unsat..." << endl;
 402         return false;
 403       }
 404     }
 405
 406     Debug("smt") << " assertions     : " << assertions.size() << endl;
 407
 408     // Unconstrained simplification
 409     if (options::unconstrainedSimp())
 410     {
 411       d_passes["unconstrained-simplifier"]->apply(&assertions);
 412     }
 413
 414     if (options::repeatSimp()
 415         && options::simplificationMode() != options::SimplificationMode::NONE)
 416     {
 417       PreprocessingPassResult res =
 418           d_passes["non-clausal-simp"]->apply(&assertions);
 419       if (res == PreprocessingPassResult::CONFLICT)
 420       {
 421         return false;
 422       }
 423     }
 424
 425     dumpAssertions("post-repeatsimp", assertions);
 426     Trace("smt") << "POST repeatSimp" << endl;
 427     Debug("smt") << " assertions     : " << assertions.size() << endl;
 428   }
 429   catch (TypeCheckingExceptionPrivate& tcep)
 430   {
 431     // Calls to this function should have already weeded out any
 432     // typechecking exceptions via (e.g.) ensureBoolean().  But a
 433     // theory could still create a new expression that isn't
 434     // well-typed, and we don't want the C++ runtime to abort our
 435     // process without any error notice.
 436     InternalError()
 437         << "A bad expression was produced.  Original exception follows:\n"
 438         << tcep;
 439   }
 440   return true;
 441 }
 442
 443 void ProcessAssertions::dumpAssertions(const char* key,
 444                                        const AssertionPipeline& assertionList)
 445 {
 446   if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
 447   {
 448     // Push the simplified assertions to the dump output stream
 449     for (unsigned i = 0; i < assertionList.size(); ++i)
 450     {
 451       TNode n = assertionList[i];
 452       d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
 453           d_smt.getOutputManager().getDumpOut(), n);
 454     }
 455   }
 456 }
 457
 458 }  // namespace smt
 459 }  // namespace CVC4