src/smt/solver_engine.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * The main entry point into the cvc5 library's SMT interface.
  14  */
  15
  16 #include "smt/solver_engine.h"
  17
  18 #include "base/check.h"
  19 #include "base/exception.h"
  20 #include "base/modal_exception.h"
  21 #include "base/output.h"
  22 #include "decision/decision_engine.h"
  23 #include "expr/bound_var_manager.h"
  24 #include "expr/node.h"
  25 #include "options/base_options.h"
  26 #include "options/expr_options.h"
  27 #include "options/language.h"
  28 #include "options/main_options.h"
  29 #include "options/option_exception.h"
  30 #include "options/options_public.h"
  31 #include "options/parser_options.h"
  32 #include "options/printer_options.h"
  33 #include "options/proof_options.h"
  34 #include "options/smt_options.h"
  35 #include "options/theory_options.h"
  36 #include "printer/printer.h"
  37 #include "proof/unsat_core.h"
  38 #include "prop/prop_engine.h"
  39 #include "smt/abduction_solver.h"
  40 #include "smt/abstract_values.h"
  41 #include "smt/assertions.h"
  42 #include "smt/check_models.h"
  43 #include "smt/env.h"
  44 #include "smt/interpolation_solver.h"
  45 #include "smt/listeners.h"
  46 #include "smt/logic_exception.h"
  47 #include "smt/model_blocker.h"
  48 #include "smt/model_core_builder.h"
  49 #include "smt/preprocessor.h"
  50 #include "smt/proof_manager.h"
  51 #include "smt/quant_elim_solver.h"
  52 #include "smt/set_defaults.h"
  53 #include "smt/smt_solver.h"
  54 #include "smt/solver_engine_scope.h"
  55 #include "smt/solver_engine_state.h"
  56 #include "smt/solver_engine_stats.h"
  57 #include "smt/sygus_solver.h"
  58 #include "smt/unsat_core_manager.h"
  59 #include "theory/quantifiers/instantiation_list.h"
  60 #include "theory/quantifiers/quantifiers_attributes.h"
  61 #include "theory/quantifiers_engine.h"
  62 #include "theory/rewriter.h"
  63 #include "theory/smt_engine_subsolver.h"
  64 #include "theory/theory_engine.h"
  65 #include "util/random.h"
  66 #include "util/rational.h"
  67 #include "util/resource_manager.h"
  68 #include "util/sexpr.h"
  69 #include "util/statistics_registry.h"
  70
  71 // required for hacks related to old proofs for unsat cores
  72 #include "base/configuration.h"
  73 #include "base/configuration_private.h"
  74
  75 using namespace std;
  76 using namespace cvc5::smt;
  77 using namespace cvc5::preprocessing;
  78 using namespace cvc5::prop;
  79 using namespace cvc5::context;
  80 using namespace cvc5::theory;
  81
  82 namespace cvc5 {
  83
  84 SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
  85     : d_env(new Env(nm, optr)),
  86       d_state(new SolverEngineState(*d_env.get(), *this)),
  87       d_absValues(new AbstractValues(getNodeManager())),
  88       d_asserts(new Assertions(*d_env.get(), *d_absValues.get())),
  89       d_routListener(new ResourceOutListener(*this)),
  90       d_smtSolver(nullptr),
  91       d_checkModels(nullptr),
  92       d_pfManager(nullptr),
  93       d_ucManager(nullptr),
  94       d_sygusSolver(nullptr),
  95       d_abductSolver(nullptr),
  96       d_interpolSolver(nullptr),
  97       d_quantElimSolver(nullptr),
  98       d_isInternalSubsolver(false),
  99       d_stats(nullptr),
 100       d_scope(nullptr)
 101 {
 102   // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SolverEngine
 103   // we are constructing the current SolverEngine in scope for the lifetime of
 104   // this SolverEngine, or until another SolverEngine is constructed (that
 105   // SolverEngine is then in scope during its lifetime). This is mostly to
 106   // ensure that options are always in scope, for e.g. printing expressions,
 107   // which rely on knowing the output language. Notice that the SolverEngine may
 108   // spawn new SolverEngine "subsolvers" internally. These are created, used,
 109   // and deleted in a modular fashion while not interleaving calls to the master
 110   // SolverEngine. Thus the hack here does not break this use case. On the other
 111   // hand, this hack breaks use cases where multiple SolverEngine objects are
 112   // created by the user.
 113   d_scope.reset(new SolverEngineScope(this));
 114   // listen to resource out
 115   getResourceManager()->registerListener(d_routListener.get());
 116   // make statistics
 117   d_stats.reset(new SolverEngineStatistics());
 118   // make the SMT solver
 119   d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_absValues, *d_stats));
 120   // make the SyGuS solver
 121   d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver));
 122   // make the quantifier elimination solver
 123   d_quantElimSolver.reset(new QuantElimSolver(*d_env.get(), *d_smtSolver));
 124 }
 125
 126 bool SolverEngine::isFullyInited() const { return d_state->isFullyInited(); }
 127 bool SolverEngine::isQueryMade() const { return d_state->isQueryMade(); }
 128 size_t SolverEngine::getNumUserLevels() const
 129 {
 130   return d_state->getNumUserLevels();
 131 }
 132 SmtMode SolverEngine::getSmtMode() const { return d_state->getMode(); }
 133 bool SolverEngine::isSmtModeSat() const
 134 {
 135   SmtMode mode = getSmtMode();
 136   return mode == SmtMode::SAT || mode == SmtMode::SAT_UNKNOWN;
 137 }
 138 Result SolverEngine::getStatusOfLastCommand() const
 139 {
 140   return d_state->getStatus();
 141 }
 142 context::UserContext* SolverEngine::getUserContext()
 143 {
 144   return d_env->getUserContext();
 145 }
 146 context::Context* SolverEngine::getContext() { return d_env->getContext(); }
 147
 148 TheoryEngine* SolverEngine::getTheoryEngine()
 149 {
 150   return d_smtSolver->getTheoryEngine();
 151 }
 152
 153 prop::PropEngine* SolverEngine::getPropEngine()
 154 {
 155   return d_smtSolver->getPropEngine();
 156 }
 157
 158 void SolverEngine::finishInit()
 159 {
 160   if (d_state->isFullyInited())
 161   {
 162     // already initialized, return
 163     return;
 164   }
 165
 166   // Notice that finishInitInternal is called when options are finalized. If we
 167   // are parsing smt2, this occurs at the moment we enter "Assert mode", page 52
 168   // of SMT-LIB 2.6 standard.
 169
 170   // set the logic
 171   const LogicInfo& logic = getLogicInfo();
 172   if (!logic.isLocked())
 173   {
 174     setLogicInternal();
 175   }
 176
 177   // set the random seed
 178   Random::getRandom().setSeed(d_env->getOptions().driver.seed);
 179
 180   // Call finish init on the set defaults module. This inializes the logic
 181   // and the best default options based on our heuristics.
 182   SetDefaults sdefaults(*d_env, d_isInternalSubsolver);
 183   sdefaults.setDefaults(d_env->d_logic, getOptions());
 184
 185   if (d_env->getOptions().smt.produceProofs)
 186   {
 187     // ensure bound variable uses canonical bound variables
 188     getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
 189     // make the proof manager
 190     d_pfManager.reset(new PfManager(*d_env.get()));
 191     PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
 192     // start the unsat core manager
 193     d_ucManager.reset(new UnsatCoreManager());
 194     // enable it in the assertions pipeline
 195     d_asserts->enableProofs(pppg);
 196     // enabled proofs in the preprocessor
 197     d_smtSolver->getPreprocessor()->enableProofs(pppg);
 198   }
 199
 200   Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
 201   d_smtSolver->finishInit();
 202
 203   // now can construct the SMT-level model object
 204   TheoryEngine* te = d_smtSolver->getTheoryEngine();
 205   Assert(te != nullptr);
 206   TheoryModel* tm = te->getModel();
 207   if (tm != nullptr)
 208   {
 209     // make the check models utility
 210     d_checkModels.reset(new CheckModels(*d_env.get()));
 211   }
 212
 213   // global push/pop around everything, to ensure proper destruction
 214   // of context-dependent data structures
 215   d_state->setup();
 216
 217   // subsolvers
 218   if (d_env->getOptions().smt.produceAbducts)
 219   {
 220     d_abductSolver.reset(new AbductionSolver(*d_env.get()));
 221   }
 222   if (d_env->getOptions().smt.produceInterpols
 223       != options::ProduceInterpols::NONE)
 224   {
 225     d_interpolSolver.reset(new InterpolationSolver(*d_env));
 226   }
 227
 228   AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
 229       << "The PropEngine has pushed but the SolverEngine "
 230          "hasn't finished initializing!";
 231
 232   Assert(getLogicInfo().isLocked());
 233
 234   // store that we are finished initializing
 235   d_state->finishInit();
 236   Trace("smt-debug") << "SolverEngine::finishInit done" << std::endl;
 237 }
 238
 239 void SolverEngine::shutdown()
 240 {
 241   d_state->shutdown();
 242   d_env->shutdown();
 243 }
 244
 245 SolverEngine::~SolverEngine()
 246 {
 247   SolverEngineScope smts(this);
 248
 249   try
 250   {
 251     shutdown();
 252
 253     // global push/pop around everything, to ensure proper destruction
 254     // of context-dependent data structures
 255     d_state->cleanup();
 256
 257     // destroy all passes before destroying things that they refer to
 258     d_smtSolver->getPreprocessor()->cleanup();
 259
 260     d_pfManager.reset(nullptr);
 261     d_ucManager.reset(nullptr);
 262
 263     d_absValues.reset(nullptr);
 264     d_asserts.reset(nullptr);
 265
 266     d_abductSolver.reset(nullptr);
 267     d_interpolSolver.reset(nullptr);
 268     d_quantElimSolver.reset(nullptr);
 269     d_sygusSolver.reset(nullptr);
 270     d_smtSolver.reset(nullptr);
 271
 272     d_stats.reset(nullptr);
 273     d_routListener.reset(nullptr);
 274     // destroy the state
 275     d_state.reset(nullptr);
 276     // destroy the environment
 277     d_env.reset(nullptr);
 278   }
 279   catch (Exception& e)
 280   {
 281     d_env->warning() << "cvc5 threw an exception during cleanup." << std::endl << e << std::endl;
 282   }
 283 }
 284
 285 void SolverEngine::setLogic(const LogicInfo& logic)
 286 {
 287   SolverEngineScope smts(this);
 288   if (d_state->isFullyInited())
 289   {
 290     throw ModalException(
 291         "Cannot set logic in SolverEngine after the engine has "
 292         "finished initializing.");
 293   }
 294   d_env->d_logic = logic;
 295   d_userLogic = logic;
 296   setLogicInternal();
 297 }
 298
 299 void SolverEngine::setLogic(const std::string& s)
 300 {
 301   SolverEngineScope smts(this);
 302   try
 303   {
 304     setLogic(LogicInfo(s));
 305   }
 306   catch (IllegalArgumentException& e)
 307   {
 308     throw LogicException(e.what());
 309   }
 310 }
 311
 312 void SolverEngine::setLogic(const char* logic) { setLogic(string(logic)); }
 313
 314 const LogicInfo& SolverEngine::getLogicInfo() const
 315 {
 316   return d_env->getLogicInfo();
 317 }
 318
 319 LogicInfo SolverEngine::getUserLogicInfo() const
 320 {
 321   // Lock the logic to make sure that this logic can be queried. We create a
 322   // copy of the user logic here to keep this method const.
 323   LogicInfo res = d_userLogic;
 324   res.lock();
 325   return res;
 326 }
 327
 328 void SolverEngine::setLogicInternal()
 329 {
 330   Assert(!d_state->isFullyInited())
 331       << "setting logic in SolverEngine but the engine has already"
 332          " finished initializing for this run";
 333   d_env->d_logic.lock();
 334   d_userLogic.lock();
 335 }
 336
 337 void SolverEngine::setInfo(const std::string& key, const std::string& value)
 338 {
 339   SolverEngineScope smts(this);
 340
 341   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
 342
 343   if (key == "filename")
 344   {
 345     d_env->d_options.driver.filename = value;
 346     d_env->d_originalOptions->driver.filename = value;
 347     d_env->getStatisticsRegistry().registerValue<std::string>(
 348         "driver::filename", value);
 349   }
 350   else if (key == "smt-lib-version"
 351            && !getOptions().base.inputLanguageWasSetByUser)
 352   {
 353     if (value != "2" && value != "2.6")
 354     {
 355       d_env->warning() << "SMT-LIB version " << value
 356                 << " unsupported, defaulting to language (and semantics of) "
 357                    "SMT-LIB 2.6\n";
 358     }
 359     getOptions().base.inputLanguage = Language::LANG_SMTLIB_V2_6;
 360     // also update the output language
 361     if (!getOptions().base.outputLanguageWasSetByUser)
 362     {
 363       setOption("output-language", "smtlib2.6");
 364       getOptions().base.outputLanguageWasSetByUser = false;
 365     }
 366   }
 367   else if (key == "status")
 368   {
 369     d_state->notifyExpectedStatus(value);
 370   }
 371 }
 372
 373 bool SolverEngine::isValidGetInfoFlag(const std::string& key) const
 374 {
 375   if (key == "all-statistics" || key == "error-behavior" || key == "filename"
 376       || key == "name" || key == "version" || key == "authors"
 377       || key == "status" || key == "time" || key == "reason-unknown"
 378       || key == "assertion-stack-levels" || key == "all-options")
 379   {
 380     return true;
 381   }
 382   return false;
 383 }
 384
 385 std::string SolverEngine::getInfo(const std::string& key) const
 386 {
 387   SolverEngineScope smts(this);
 388
 389   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
 390   if (key == "all-statistics")
 391   {
 392     return toSExpr(d_env->getStatisticsRegistry().begin(),
 393                    d_env->getStatisticsRegistry().end());
 394   }
 395   if (key == "error-behavior")
 396   {
 397     return "immediate-exit";
 398   }
 399   if (key == "filename")
 400   {
 401     return d_env->getOptions().driver.filename;
 402   }
 403   if (key == "name")
 404   {
 405     return toSExpr(Configuration::getName());
 406   }
 407   if (key == "version")
 408   {
 409     return toSExpr(Configuration::getVersionString());
 410   }
 411   if (key == "authors")
 412   {
 413     return toSExpr("the " + Configuration::getName() + " authors");
 414   }
 415   if (key == "status")
 416   {
 417     // sat | unsat | unknown
 418     Result status = d_state->getStatus();
 419     switch (status.asSatisfiabilityResult().isSat())
 420     {
 421       case Result::SAT: return "sat";
 422       case Result::UNSAT: return "unsat";
 423       default: return "unknown";
 424     }
 425   }
 426   if (key == "time")
 427   {
 428     return toSExpr(std::clock());
 429   }
 430   if (key == "reason-unknown")
 431   {
 432     Result status = d_state->getStatus();
 433     if (!status.isNull() && status.isUnknown())
 434     {
 435       std::stringstream ss;
 436       ss << status.whyUnknown();
 437       std::string s = ss.str();
 438       transform(s.begin(), s.end(), s.begin(), ::tolower);
 439       return s;
 440     }
 441     else
 442     {
 443       throw RecoverableModalException(
 444           "Can't get-info :reason-unknown when the "
 445           "last result wasn't unknown!");
 446     }
 447   }
 448   if (key == "assertion-stack-levels")
 449   {
 450     size_t ulevel = d_state->getNumUserLevels();
 451     AlwaysAssert(ulevel <= std::numeric_limits<unsigned long int>::max());
 452     return toSExpr(ulevel);
 453   }
 454   Assert(key == "all-options");
 455   // get the options, like all-statistics
 456   std::vector<std::vector<std::string>> res;
 457   for (const auto& opt : options::getNames())
 458   {
 459     res.emplace_back(
 460         std::vector<std::string>{opt, options::get(getOptions(), opt)});
 461   }
 462   return toSExpr(res);
 463 }
 464
 465 void SolverEngine::debugCheckFormals(const std::vector<Node>& formals,
 466                                      Node func)
 467 {
 468   for (std::vector<Node>::const_iterator i = formals.begin();
 469        i != formals.end();
 470        ++i)
 471   {
 472     if ((*i).getKind() != kind::BOUND_VARIABLE)
 473     {
 474       stringstream ss;
 475       ss << "All formal arguments to defined functions must be "
 476             "BOUND_VARIABLEs, but in the\n"
 477          << "definition of function " << func << ", formal\n"
 478          << "  " << *i << "\n"
 479          << "has kind " << (*i).getKind();
 480       throw TypeCheckingExceptionPrivate(func, ss.str());
 481     }
 482   }
 483 }
 484
 485 void SolverEngine::debugCheckFunctionBody(Node formula,
 486                                           const std::vector<Node>& formals,
 487                                           Node func)
 488 {
 489   TypeNode formulaType = formula.getType(d_env->getOptions().expr.typeChecking);
 490   TypeNode funcType = func.getType();
 491   // We distinguish here between definitions of constants and functions,
 492   // because the type checking for them is subtly different.  Perhaps we
 493   // should instead have SolverEngine::defineFunction() and
 494   // SolverEngine::defineConstant() for better clarity, although then that
 495   // doesn't match the SMT-LIBv2 standard...
 496   if (formals.size() > 0)
 497   {
 498     TypeNode rangeType = funcType.getRangeType();
 499     if (!formulaType.isComparableTo(rangeType))
 500     {
 501       stringstream ss;
 502       ss << "Type of defined function does not match its declaration\n"
 503          << "The function  : " << func << "\n"
 504          << "Declared type : " << rangeType << "\n"
 505          << "The body      : " << formula << "\n"
 506          << "Body type     : " << formulaType;
 507       throw TypeCheckingExceptionPrivate(func, ss.str());
 508     }
 509   }
 510   else
 511   {
 512     if (!formulaType.isComparableTo(funcType))
 513     {
 514       stringstream ss;
 515       ss << "Declared type of defined constant does not match its definition\n"
 516          << "The constant   : " << func << "\n"
 517          << "Declared type  : " << funcType << "\n"
 518          << "The definition : " << formula << "\n"
 519          << "Definition type: " << formulaType;
 520       throw TypeCheckingExceptionPrivate(func, ss.str());
 521     }
 522   }
 523 }
 524
 525 void SolverEngine::defineFunction(Node func,
 526                                   const std::vector<Node>& formals,
 527                                   Node formula,
 528                                   bool global)
 529 {
 530   SolverEngineScope smts(this);
 531   finishInit();
 532   d_state->doPendingPops();
 533   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
 534   debugCheckFormals(formals, func);
 535
 536   // type check body
 537   debugCheckFunctionBody(formula, formals, func);
 538
 539   // Substitute out any abstract values in formula
 540   Node def = d_absValues->substituteAbstractValues(formula);
 541   if (!formals.empty())
 542   {
 543     NodeManager* nm = NodeManager::currentNM();
 544     def = nm->mkNode(
 545         kind::LAMBDA, nm->mkNode(kind::BOUND_VAR_LIST, formals), def);
 546   }
 547   // A define-fun is treated as a (higher-order) assertion. It is provided
 548   // to the assertions object. It will be added as a top-level substitution
 549   // within this class, possibly multiple times if global is true.
 550   Node feq = func.eqNode(def);
 551   d_asserts->addDefineFunDefinition(feq, global);
 552 }
 553
 554 void SolverEngine::defineFunctionsRec(
 555     const std::vector<Node>& funcs,
 556     const std::vector<std::vector<Node>>& formals,
 557     const std::vector<Node>& formulas,
 558     bool global)
 559 {
 560   SolverEngineScope smts(this);
 561   finishInit();
 562   d_state->doPendingPops();
 563   Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
 564
 565   if (funcs.size() != formals.size() && funcs.size() != formulas.size())
 566   {
 567     stringstream ss;
 568     ss << "Number of functions, formals, and function bodies passed to "
 569           "defineFunctionsRec do not match:"
 570        << "\n"
 571        << "        #functions : " << funcs.size() << "\n"
 572        << "        #arg lists : " << formals.size() << "\n"
 573        << "  #function bodies : " << formulas.size() << "\n";
 574     throw ModalException(ss.str());
 575   }
 576   for (unsigned i = 0, size = funcs.size(); i < size; i++)
 577   {
 578     // check formal argument list
 579     debugCheckFormals(formals[i], funcs[i]);
 580     // type check body
 581     debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
 582   }
 583
 584   NodeManager* nm = getNodeManager();
 585   for (unsigned i = 0, size = funcs.size(); i < size; i++)
 586   {
 587     // we assert a quantified formula
 588     Node func_app;
 589     // make the function application
 590     if (formals[i].empty())
 591     {
 592       // it has no arguments
 593       func_app = funcs[i];
 594     }
 595     else
 596     {
 597       std::vector<Node> children;
 598       children.push_back(funcs[i]);
 599       children.insert(children.end(), formals[i].begin(), formals[i].end());
 600       func_app = nm->mkNode(kind::APPLY_UF, children);
 601     }
 602     Node lem = nm->mkNode(kind::EQUAL, func_app, formulas[i]);
 603     if (!formals[i].empty())
 604     {
 605       // set the attribute to denote this is a function definition
 606       Node aexpr = nm->mkNode(kind::INST_ATTRIBUTE, func_app);
 607       aexpr = nm->mkNode(kind::INST_PATTERN_LIST, aexpr);
 608       FunDefAttribute fda;
 609       func_app.setAttribute(fda, true);
 610       // make the quantified formula
 611       Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]);
 612       lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr);
 613     }
 614     // Assert the quantified formula. Notice we don't call assertFormula
 615     // directly, since we should call a private member method since we have
 616     // already ensuring this SolverEngine is initialized above.
 617     // add define recursive definition to the assertions
 618     d_asserts->addDefineFunDefinition(lem, global);
 619   }
 620 }
 621
 622 void SolverEngine::defineFunctionRec(Node func,
 623                                      const std::vector<Node>& formals,
 624                                      Node formula,
 625                                      bool global)
 626 {
 627   std::vector<Node> funcs;
 628   funcs.push_back(func);
 629   std::vector<std::vector<Node>> formals_multi;
 630   formals_multi.push_back(formals);
 631   std::vector<Node> formulas;
 632   formulas.push_back(formula);
 633   defineFunctionsRec(funcs, formals_multi, formulas, global);
 634 }
 635
 636 Result SolverEngine::quickCheck()
 637 {
 638   Assert(d_state->isFullyInited());
 639   Trace("smt") << "SMT quickCheck()" << endl;
 640   const std::string& filename = d_env->getOptions().driver.filename;
 641   return Result(
 642       Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
 643 }
 644
 645 TheoryModel* SolverEngine::getAvailableModel(const char* c) const
 646 {
 647   if (!d_env->getOptions().theory.assignFunctionValues)
 648   {
 649     std::stringstream ss;
 650     ss << "Cannot " << c << " when --assign-function-values is false.";
 651     throw RecoverableModalException(ss.str().c_str());
 652   }
 653
 654   if (d_state->getMode() != SmtMode::SAT
 655       && d_state->getMode() != SmtMode::SAT_UNKNOWN)
 656   {
 657     std::stringstream ss;
 658     ss << "Cannot " << c
 659        << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
 660           "response.";
 661     throw RecoverableModalException(ss.str().c_str());
 662   }
 663
 664   if (!d_env->getOptions().smt.produceModels)
 665   {
 666     std::stringstream ss;
 667     ss << "Cannot " << c << " when produce-models options is off.";
 668     throw ModalException(ss.str().c_str());
 669   }
 670
 671   TheoryEngine* te = d_smtSolver->getTheoryEngine();
 672   Assert(te != nullptr);
 673   TheoryModel* m = te->getBuiltModel();
 674
 675   if (m == nullptr)
 676   {
 677     std::stringstream ss;
 678     ss << "Cannot " << c
 679        << " since model is not available. Perhaps the most recent call to "
 680           "check-sat was interrupted?";
 681     throw RecoverableModalException(ss.str().c_str());
 682   }
 683
 684   return m;
 685 }
 686
 687 QuantifiersEngine* SolverEngine::getAvailableQuantifiersEngine(
 688     const char* c) const
 689 {
 690   QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine();
 691   if (qe == nullptr)
 692   {
 693     std::stringstream ss;
 694     ss << "Cannot " << c << " when quantifiers are not present.";
 695     throw ModalException(ss.str().c_str());
 696   }
 697   return qe;
 698 }
 699
 700 void SolverEngine::notifyPushPre()
 701 {
 702   d_smtSolver->processAssertions(*d_asserts);
 703 }
 704
 705 void SolverEngine::notifyPushPost()
 706 {
 707   TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
 708   Assert(getPropEngine() != nullptr);
 709   getPropEngine()->push();
 710 }
 711
 712 void SolverEngine::notifyPopPre()
 713 {
 714   TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
 715   PropEngine* pe = getPropEngine();
 716   Assert(pe != nullptr);
 717   pe->pop();
 718 }
 719
 720 void SolverEngine::notifyPostSolvePre()
 721 {
 722   PropEngine* pe = getPropEngine();
 723   Assert(pe != nullptr);
 724   pe->resetTrail();
 725 }
 726
 727 void SolverEngine::notifyPostSolvePost()
 728 {
 729   TheoryEngine* te = getTheoryEngine();
 730   Assert(te != nullptr);
 731   te->postsolve();
 732 }
 733
 734 Result SolverEngine::checkSat()
 735 {
 736   Node nullNode;
 737   return checkSat(nullNode);
 738 }
 739
 740 Result SolverEngine::checkSat(const Node& assumption)
 741 {
 742   std::vector<Node> assump;
 743   if (!assumption.isNull())
 744   {
 745     assump.push_back(assumption);
 746   }
 747   return checkSatInternal(assump, false);
 748 }
 749
 750 Result SolverEngine::checkSat(const std::vector<Node>& assumptions)
 751 {
 752   return checkSatInternal(assumptions, false);
 753 }
 754
 755 Result SolverEngine::checkEntailed(const Node& node)
 756 {
 757   return checkSatInternal(
 758              node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
 759              true)
 760       .asEntailmentResult();
 761 }
 762
 763 Result SolverEngine::checkEntailed(const std::vector<Node>& nodes)
 764 {
 765   return checkSatInternal(nodes, true).asEntailmentResult();
 766 }
 767
 768 Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
 769                                       bool isEntailmentCheck)
 770 {
 771   try
 772   {
 773     SolverEngineScope smts(this);
 774     finishInit();
 775
 776     Trace("smt") << "SolverEngine::"
 777                  << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
 778                  << assumptions << ")" << endl;
 779     // check the satisfiability with the solver object
 780     Result r = d_smtSolver->checkSatisfiability(
 781         *d_asserts.get(), assumptions, isEntailmentCheck);
 782
 783     Trace("smt") << "SolverEngine::"
 784                  << (isEntailmentCheck ? "query" : "checkSat") << "("
 785                  << assumptions << ") => " << r << endl;
 786
 787     // Check that SAT results generate a model correctly.
 788     if (d_env->getOptions().smt.checkModels)
 789     {
 790       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
 791       {
 792         checkModel();
 793       }
 794     }
 795     // Check that UNSAT results generate a proof correctly.
 796     if (d_env->getOptions().smt.checkProofs)
 797     {
 798       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
 799       {
 800         checkProof();
 801       }
 802     }
 803     // Check that UNSAT results generate an unsat core correctly.
 804     if (d_env->getOptions().smt.checkUnsatCores)
 805     {
 806       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
 807       {
 808         TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
 809         checkUnsatCore();
 810       }
 811     }
 812     if (d_env->getOptions().base.statisticsEveryQuery)
 813     {
 814       printStatisticsDiff();
 815     }
 816     return r;
 817   }
 818   catch (UnsafeInterruptException& e)
 819   {
 820     AlwaysAssert(getResourceManager()->out());
 821     // Notice that we do not notify the state of this result. If we wanted to
 822     // make the solver resume a working state after an interupt, then we would
 823     // implement a different callback and use it here, e.g.
 824     // d_state.notifyCheckSatInterupt.
 825     Result::UnknownExplanation why = getResourceManager()->outOfResources()
 826                                          ? Result::RESOURCEOUT
 827                                          : Result::TIMEOUT;
 828
 829     if (d_env->getOptions().base.statisticsEveryQuery)
 830     {
 831       printStatisticsDiff();
 832     }
 833     return Result(
 834         Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename);
 835   }
 836 }
 837
 838 std::vector<Node> SolverEngine::getUnsatAssumptions(void)
 839 {
 840   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
 841   SolverEngineScope smts(this);
 842   if (!d_env->getOptions().smt.unsatAssumptions)
 843   {
 844     throw ModalException(
 845         "Cannot get unsat assumptions when produce-unsat-assumptions option "
 846         "is off.");
 847   }
 848   if (d_state->getMode() != SmtMode::UNSAT)
 849   {
 850     throw RecoverableModalException(
 851         "Cannot get unsat assumptions unless immediately preceded by "
 852         "UNSAT/ENTAILED.");
 853   }
 854   finishInit();
 855   UnsatCore core = getUnsatCoreInternal();
 856   std::vector<Node> res;
 857   std::vector<Node>& assumps = d_asserts->getAssumptions();
 858   for (const Node& e : assumps)
 859   {
 860     if (std::find(core.begin(), core.end(), e) != core.end())
 861     {
 862       res.push_back(e);
 863     }
 864   }
 865   return res;
 866 }
 867
 868 Result SolverEngine::assertFormula(const Node& formula)
 869 {
 870   SolverEngineScope smts(this);
 871   finishInit();
 872   d_state->doPendingPops();
 873
 874   Trace("smt") << "SolverEngine::assertFormula(" << formula << ")" << endl;
 875
 876   // Substitute out any abstract values in ex
 877   Node n = d_absValues->substituteAbstractValues(formula);
 878
 879   d_asserts->assertFormula(n);
 880   return quickCheck().asEntailmentResult();
 881 } /* SolverEngine::assertFormula() */
 882
 883 /*
 884    --------------------------------------------------------------------------
 885     Handling SyGuS commands
 886    --------------------------------------------------------------------------
 887 */
 888
 889 void SolverEngine::declareSygusVar(Node var)
 890 {
 891   SolverEngineScope smts(this);
 892   d_sygusSolver->declareSygusVar(var);
 893 }
 894
 895 void SolverEngine::declareSynthFun(Node func,
 896                                    TypeNode sygusType,
 897                                    bool isInv,
 898                                    const std::vector<Node>& vars)
 899 {
 900   SolverEngineScope smts(this);
 901   finishInit();
 902   d_state->doPendingPops();
 903   d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars);
 904 }
 905 void SolverEngine::declareSynthFun(Node func,
 906                                    bool isInv,
 907                                    const std::vector<Node>& vars)
 908 {
 909   // use a null sygus type
 910   TypeNode sygusType;
 911   declareSynthFun(func, sygusType, isInv, vars);
 912 }
 913
 914 void SolverEngine::assertSygusConstraint(Node n, bool isAssume)
 915 {
 916   SolverEngineScope smts(this);
 917   finishInit();
 918   d_sygusSolver->assertSygusConstraint(n, isAssume);
 919 }
 920
 921 void SolverEngine::assertSygusInvConstraint(Node inv,
 922                                             Node pre,
 923                                             Node trans,
 924                                             Node post)
 925 {
 926   SolverEngineScope smts(this);
 927   finishInit();
 928   d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
 929 }
 930
 931 Result SolverEngine::checkSynth(bool isNext)
 932 {
 933   SolverEngineScope smts(this);
 934   finishInit();
 935   if (isNext && d_state->getMode() != SmtMode::SYNTH)
 936   {
 937     throw RecoverableModalException(
 938         "Cannot check-synth-next unless immediately preceded by a successful "
 939         "call to check-synth(-next).");
 940   }
 941   Result r = d_sygusSolver->checkSynth(*d_asserts, isNext);
 942   d_state->notifyCheckSynthResult(r);
 943   return r;
 944 }
 945
 946 /*
 947    --------------------------------------------------------------------------
 948     End of Handling SyGuS commands
 949    --------------------------------------------------------------------------
 950 */
 951
 952 void SolverEngine::declarePool(const Node& p,
 953                                const std::vector<Node>& initValue)
 954 {
 955   Assert(p.isVar() && p.getType().isSet());
 956   finishInit();
 957   QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareTermPool");
 958   qe->declarePool(p, initValue);
 959 }
 960
 961 Node SolverEngine::simplify(const Node& ex)
 962 {
 963   SolverEngineScope smts(this);
 964   finishInit();
 965   d_state->doPendingPops();
 966   // ensure we've processed assertions
 967   d_smtSolver->processAssertions(*d_asserts);
 968   return d_smtSolver->getPreprocessor()->simplify(ex);
 969 }
 970
 971 Node SolverEngine::expandDefinitions(const Node& ex)
 972 {
 973   getResourceManager()->spendResource(Resource::PreprocessStep);
 974   SolverEngineScope smts(this);
 975   finishInit();
 976   d_state->doPendingPops();
 977   return d_smtSolver->getPreprocessor()->expandDefinitions(ex);
 978 }
 979
 980 // TODO(#1108): Simplify the error reporting of this method.
 981 Node SolverEngine::getValue(const Node& ex) const
 982 {
 983   SolverEngineScope smts(this);
 984
 985   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
 986   TypeNode expectedType = ex.getType();
 987
 988   // Substitute out any abstract values in ex and expand
 989   Node n = d_smtSolver->getPreprocessor()->expandDefinitions(ex);
 990
 991   Trace("smt") << "--- getting value of " << n << endl;
 992   // There are two ways model values for terms are computed (for historical
 993   // reasons).  One way is that used in check-model; the other is that
 994   // used by the Model classes.  It's not clear to me exactly how these
 995   // two are different, but they need to be unified.  This ugly hack here
 996   // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
 997
 998   // AJR : necessary?
 999   if (!n.getType().isFunction())
1000   {
1001     n = d_env->getRewriter()->rewrite(n);
1002   }
1003
1004   Trace("smt") << "--- getting value of " << n << endl;
1005   TheoryModel* m = getAvailableModel("get-value");
1006   Assert(m != nullptr);
1007   Node resultNode = m->getValue(n);
1008   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
1009   Trace("smt") << "--- type " << resultNode.getType() << endl;
1010   Trace("smt") << "--- expected type " << expectedType << endl;
1011
1012   // type-check the result we got
1013   // Notice that lambdas have function type, which does not respect the subtype
1014   // relation, so we ignore them here.
1015   Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA
1016          || resultNode.getType().isSubtypeOf(expectedType))
1017       << "Run with -t smt for details.";
1018
1019   // Ensure it's a value (constant or const-ish like real algebraic
1020   // numbers), or a lambda (for uninterpreted functions). This assertion only
1021   // holds for models that do not have approximate values.
1022   Assert(m->hasApproximations() || TheoryModel::isValue(resultNode));
1023
1024   if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray())
1025   {
1026     resultNode = d_absValues->mkAbstractValue(resultNode);
1027     Trace("smt") << "--- abstract value >> " << resultNode << endl;
1028   }
1029
1030   return resultNode;
1031 }
1032
1033 std::vector<Node> SolverEngine::getValues(const std::vector<Node>& exprs) const
1034 {
1035   std::vector<Node> result;
1036   for (const Node& e : exprs)
1037   {
1038     result.push_back(getValue(e));
1039   }
1040   return result;
1041 }
1042
1043 std::vector<Node> SolverEngine::getModelDomainElements(TypeNode tn) const
1044 {
1045   Assert(tn.isSort());
1046   TheoryModel* m = getAvailableModel("getModelDomainElements");
1047   return m->getDomainElements(tn);
1048 }
1049
1050 bool SolverEngine::isModelCoreSymbol(Node n)
1051 {
1052   SolverEngineScope smts(this);
1053   Assert(n.isVar());
1054   const Options& opts = d_env->getOptions();
1055   if (opts.smt.modelCoresMode == options::ModelCoresMode::NONE)
1056   {
1057     // if the model core mode is none, we are always a model core symbol
1058     return true;
1059   }
1060   TheoryModel* tm = getAvailableModel("isModelCoreSymbol");
1061   // compute the model core if not done so already
1062   if (!tm->isUsingModelCore())
1063   {
1064     // If we enabled model cores, we compute a model core for m based on our
1065     // (expanded) assertions using the model core builder utility. Notice that
1066     // we get the assertions using the getAssertionsInternal, which does not
1067     // impact whether we are in "sat" mode
1068     std::vector<Node> asserts = getAssertionsInternal();
1069     d_smtSolver->getPreprocessor()->expandDefinitions(asserts);
1070     ModelCoreBuilder mcb(*d_env.get());
1071     mcb.setModelCore(asserts, tm, opts.smt.modelCoresMode);
1072   }
1073   return tm->isModelCoreSymbol(n);
1074 }
1075
1076 std::string SolverEngine::getModel(const std::vector<TypeNode>& declaredSorts,
1077                                    const std::vector<Node>& declaredFuns)
1078 {
1079   SolverEngineScope smts(this);
1080   // !!! Note that all methods called here should have a version at the API
1081   // level. This is to ensure that the information associated with a model is
1082   // completely accessible by the user. This is currently not rigorously
1083   // enforced. An alternative design would be to have this method implemented
1084   // at the API level, but this makes exceptions in the text interface less
1085   // intuitive.
1086   TheoryModel* tm = getAvailableModel("get model");
1087   // use the smt::Model model utility for printing
1088   const Options& opts = d_env->getOptions();
1089   bool isKnownSat = (d_state->getMode() == SmtMode::SAT);
1090   Model m(isKnownSat, opts.driver.filename);
1091   // set the model declarations, which determines what is printed in the model
1092   for (const TypeNode& tn : declaredSorts)
1093   {
1094     m.addDeclarationSort(tn, getModelDomainElements(tn));
1095   }
1096   bool usingModelCores =
1097       (opts.smt.modelCoresMode != options::ModelCoresMode::NONE);
1098   for (const Node& n : declaredFuns)
1099   {
1100     if (usingModelCores && !tm->isModelCoreSymbol(n))
1101     {
1102       // skip if not in model core
1103       continue;
1104     }
1105     Node value = tm->getValue(n);
1106     m.addDeclarationTerm(n, value);
1107   }
1108   // for separation logic
1109   TypeNode locT, dataT;
1110   if (getSepHeapTypes(locT, dataT))
1111   {
1112     std::pair<Node, Node> sh = getSepHeapAndNilExpr();
1113     m.setHeapModel(sh.first, sh.second);
1114   }
1115   // print the model
1116   std::stringstream ssm;
1117   ssm << m;
1118   return ssm.str();
1119 }
1120
1121 Result SolverEngine::blockModel()
1122 {
1123   Trace("smt") << "SMT blockModel()" << endl;
1124   SolverEngineScope smts(this);
1125
1126   finishInit();
1127
1128   TheoryModel* m = getAvailableModel("block model");
1129
1130   if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE)
1131   {
1132     std::stringstream ss;
1133     ss << "Cannot block model when block-models is set to none.";
1134     throw RecoverableModalException(ss.str().c_str());
1135   }
1136
1137   // get expanded assertions
1138   std::vector<Node> eassertsProc = getExpandedAssertions();
1139   ModelBlocker mb(*d_env.get());
1140   Node eblocker = mb.getModelBlocker(
1141       eassertsProc, m, d_env->getOptions().smt.blockModelsMode);
1142   Trace("smt") << "Block formula: " << eblocker << std::endl;
1143   return assertFormula(eblocker);
1144 }
1145
1146 Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
1147 {
1148   Trace("smt") << "SMT blockModelValues()" << endl;
1149   SolverEngineScope smts(this);
1150
1151   finishInit();
1152
1153   TheoryModel* m = getAvailableModel("block model values");
1154
1155   // get expanded assertions
1156   std::vector<Node> eassertsProc = getExpandedAssertions();
1157   // we always do block model values mode here
1158   ModelBlocker mb(*d_env.get());
1159   Node eblocker = mb.getModelBlocker(
1160       eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
1161   return assertFormula(eblocker);
1162 }
1163
1164 std::pair<Node, Node> SolverEngine::getSepHeapAndNilExpr(void)
1165 {
1166   if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
1167   {
1168     const char* msg =
1169         "Cannot obtain separation logic expressions if not using the "
1170         "separation logic theory.";
1171     throw RecoverableModalException(msg);
1172   }
1173   Node heap;
1174   Node nil;
1175   TheoryModel* tm = getAvailableModel("get separation logic heap and nil");
1176   if (!tm->getHeapModel(heap, nil))
1177   {
1178     const char* msg =
1179         "Failed to obtain heap/nil "
1180         "expressions from theory model.";
1181     throw RecoverableModalException(msg);
1182   }
1183   return std::make_pair(heap, nil);
1184 }
1185
1186 std::vector<Node> SolverEngine::getAssertionsInternal()
1187 {
1188   Assert(d_state->isFullyInited());
1189   const context::CDList<Node>& al = d_asserts->getAssertionList();
1190   std::vector<Node> res;
1191   for (const Node& n : al)
1192   {
1193     res.emplace_back(n);
1194   }
1195   return res;
1196 }
1197
1198 const Options& SolverEngine::options() const { return d_env->getOptions(); }
1199
1200 std::vector<Node> SolverEngine::getExpandedAssertions()
1201 {
1202   std::vector<Node> easserts = getAssertions();
1203   // must expand definitions
1204   d_smtSolver->getPreprocessor()->expandDefinitions(easserts);
1205   return easserts;
1206 }
1207 Env& SolverEngine::getEnv() { return *d_env.get(); }
1208
1209 void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
1210 {
1211   if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
1212   {
1213     const char* msg =
1214         "Cannot declare heap if not using the separation logic theory.";
1215     throw RecoverableModalException(msg);
1216   }
1217   SolverEngineScope smts(this);
1218   finishInit();
1219   // check whether incremental is enabled, where separation logic is not
1220   // supported.
1221   if (d_env->getOptions().base.incrementalSolving)
1222   {
1223     throw RecoverableModalException(
1224         "Separation logic not supported in incremental mode");
1225   }
1226   TheoryEngine* te = getTheoryEngine();
1227   te->declareSepHeap(locT, dataT);
1228 }
1229
1230 bool SolverEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
1231 {
1232   SolverEngineScope smts(this);
1233   finishInit();
1234   TheoryEngine* te = getTheoryEngine();
1235   return te->getSepHeapTypes(locT, dataT);
1236 }
1237
1238 Node SolverEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
1239
1240 Node SolverEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
1241
1242 void SolverEngine::checkProof()
1243 {
1244   Assert(d_env->getOptions().smt.produceProofs);
1245   // internal check the proof
1246   PropEngine* pe = getPropEngine();
1247   Assert(pe != nullptr);
1248   if (d_env->getOptions().proof.proofCheck == options::ProofCheckMode::EAGER)
1249   {
1250     pe->checkProof(d_asserts->getAssertionList());
1251   }
1252   Assert(pe->getProof() != nullptr);
1253   std::shared_ptr<ProofNode> pePfn = pe->getProof();
1254   if (d_env->getOptions().smt.checkProofs)
1255   {
1256     d_pfManager->checkProof(pePfn, *d_asserts);
1257   }
1258 }
1259
1260 StatisticsRegistry& SolverEngine::getStatisticsRegistry()
1261 {
1262   return d_env->getStatisticsRegistry();
1263 }
1264
1265 UnsatCore SolverEngine::getUnsatCoreInternal()
1266 {
1267   if (!d_env->getOptions().smt.unsatCores)
1268   {
1269     throw ModalException(
1270         "Cannot get an unsat core when produce-unsat-cores or produce-proofs "
1271         "option is off.");
1272   }
1273   if (d_state->getMode() != SmtMode::UNSAT)
1274   {
1275     throw RecoverableModalException(
1276         "Cannot get an unsat core unless immediately preceded by "
1277         "UNSAT/ENTAILED response.");
1278   }
1279   // generate with new proofs
1280   PropEngine* pe = getPropEngine();
1281   Assert(pe != nullptr);
1282
1283   std::shared_ptr<ProofNode> pepf;
1284   if (options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS)
1285   {
1286     pepf = pe->getRefutation();
1287   }
1288   else
1289   {
1290     pepf = pe->getProof();
1291   }
1292   Assert(pepf != nullptr);
1293   std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts);
1294   std::vector<Node> core;
1295   d_ucManager->getUnsatCore(pfn, *d_asserts, core);
1296   if (options().smt.minimalUnsatCores)
1297   {
1298     core = reduceUnsatCore(core);
1299   }
1300   return UnsatCore(core);
1301 }
1302
1303 std::vector<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& core)
1304 {
1305   Assert(options().smt.unsatCores)
1306       << "cannot reduce unsat core if unsat cores are turned off";
1307
1308   d_env->verbose(1) << "SolverEngine::reduceUnsatCore(): reducing unsat core"
1309                     << std::endl;
1310   std::unordered_set<Node> removed;
1311   for (const Node& skip : core)
1312   {
1313     std::unique_ptr<SolverEngine> coreChecker;
1314     initializeSubsolver(coreChecker, *d_env.get());
1315     coreChecker->setLogic(getLogicInfo());
1316     coreChecker->getOptions().smt.checkUnsatCores = false;
1317     // disable all proof options
1318     coreChecker->getOptions().smt.produceProofs = false;
1319     coreChecker->getOptions().smt.checkProofs = false;
1320
1321     for (const Node& ucAssertion : core)
1322     {
1323       if (ucAssertion != skip && removed.find(ucAssertion) == removed.end())
1324       {
1325         Node assertionAfterExpansion = expandDefinitions(ucAssertion);
1326         coreChecker->assertFormula(assertionAfterExpansion);
1327       }
1328     }
1329     Result r;
1330     try
1331     {
1332       r = coreChecker->checkSat();
1333     }
1334     catch (...)
1335     {
1336       throw;
1337     }
1338
1339     if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
1340     {
1341       removed.insert(skip);
1342     }
1343     else if (r.asSatisfiabilityResult().isUnknown())
1344     {
1345       d_env->warning()
1346           << "SolverEngine::reduceUnsatCore(): could not reduce unsat core "
1347              "due to "
1348              "unknown result.";
1349     }
1350   }
1351
1352   if (removed.empty())
1353   {
1354     return core;
1355   }
1356   else
1357   {
1358     std::vector<Node> newUcAssertions;
1359     for (const Node& n : core)
1360     {
1361       if (removed.find(n) == removed.end())
1362       {
1363         newUcAssertions.push_back(n);
1364       }
1365     }
1366
1367     return newUcAssertions;
1368   }
1369 }
1370
1371 void SolverEngine::checkUnsatCore()
1372 {
1373   Assert(d_env->getOptions().smt.unsatCores)
1374       << "cannot check unsat core if unsat cores are turned off";
1375
1376   d_env->verbose(1) << "SolverEngine::checkUnsatCore(): generating unsat core"
1377                     << std::endl;
1378   UnsatCore core = getUnsatCore();
1379
1380   // initialize the core checker
1381   std::unique_ptr<SolverEngine> coreChecker;
1382   initializeSubsolver(coreChecker, *d_env.get());
1383   coreChecker->getOptions().smt.checkUnsatCores = false;
1384   // disable all proof options
1385   coreChecker->getOptions().smt.produceProofs = false;
1386   coreChecker->getOptions().smt.checkProofs = false;
1387
1388   // set up separation logic heap if necessary
1389   TypeNode sepLocType, sepDataType;
1390   if (getSepHeapTypes(sepLocType, sepDataType))
1391   {
1392     coreChecker->declareSepHeap(sepLocType, sepDataType);
1393   }
1394
1395   d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core assertions"
1396                     << std::endl;
1397   theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions();
1398   for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i)
1399   {
1400     Node assertionAfterExpansion = tls.apply(*i);
1401     d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core member "
1402                       << *i << ", expanded to " << assertionAfterExpansion
1403                       << std::endl;
1404     coreChecker->assertFormula(assertionAfterExpansion);
1405   }
1406   Result r;
1407   try
1408   {
1409     r = coreChecker->checkSat();
1410   }
1411   catch (...)
1412   {
1413     throw;
1414   }
1415   d_env->verbose(1) << "SolverEngine::checkUnsatCore(): result is " << r
1416                     << std::endl;
1417   if (r.asSatisfiabilityResult().isUnknown())
1418   {
1419     d_env->warning() << "SolverEngine::checkUnsatCore(): could not check core result "
1420                  "unknown."
1421               << std::endl;
1422   }
1423   else if (r.asSatisfiabilityResult().isSat())
1424   {
1425     InternalError()
1426         << "SolverEngine::checkUnsatCore(): produced core was satisfiable.";
1427   }
1428 }
1429
1430 void SolverEngine::checkModel(bool hardFailure)
1431 {
1432   const context::CDList<Node>& al = d_asserts->getAssertionList();
1433   // we always enable the assertion list, so it is able to be checked
1434
1435   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
1436
1437   d_env->verbose(1) << "SolverEngine::checkModel(): generating model"
1438                     << std::endl;
1439   TheoryModel* m = getAvailableModel("check model");
1440   Assert(m != nullptr);
1441
1442   // check the model with the theory engine for debugging
1443   if (options().smt.debugCheckModels)
1444   {
1445     TheoryEngine* te = getTheoryEngine();
1446     Assert(te != nullptr);
1447     te->checkTheoryAssertionsWithModel(hardFailure);
1448   }
1449
1450   // check the model with the check models utility
1451   Assert(d_checkModels != nullptr);
1452   d_checkModels->checkModel(m, al, hardFailure);
1453 }
1454
1455 UnsatCore SolverEngine::getUnsatCore()
1456 {
1457   Trace("smt") << "SMT getUnsatCore()" << std::endl;
1458   SolverEngineScope smts(this);
1459   finishInit();
1460   return getUnsatCoreInternal();
1461 }
1462
1463 void SolverEngine::getRelevantInstantiationTermVectors(
1464     std::map<Node, InstantiationList>& insts, bool getDebugInfo)
1465 {
1466   Assert(d_state->getMode() == SmtMode::UNSAT);
1467   // generate with new proofs
1468   PropEngine* pe = getPropEngine();
1469   Assert(pe != nullptr);
1470   Assert(pe->getProof() != nullptr);
1471   std::shared_ptr<ProofNode> pfn =
1472       d_pfManager->getFinalProof(pe->getProof(), *d_asserts);
1473   d_ucManager->getRelevantInstantiations(pfn, insts, getDebugInfo);
1474 }
1475
1476 std::string SolverEngine::getProof()
1477 {
1478   Trace("smt") << "SMT getProof()\n";
1479   SolverEngineScope smts(this);
1480   finishInit();
1481   if (!d_env->getOptions().smt.produceProofs)
1482   {
1483     throw ModalException("Cannot get a proof when proof option is off.");
1484   }
1485   if (d_state->getMode() != SmtMode::UNSAT)
1486   {
1487     throw RecoverableModalException(
1488         "Cannot get a proof unless immediately preceded by "
1489         "UNSAT/ENTAILED response.");
1490   }
1491   // the prop engine has the proof of false
1492   PropEngine* pe = getPropEngine();
1493   Assert(pe != nullptr);
1494   Assert(pe->getProof() != nullptr);
1495   Assert(d_pfManager);
1496   std::ostringstream ss;
1497   d_pfManager->printProof(ss, pe->getProof(), *d_asserts);
1498   return ss.str();
1499 }
1500
1501 void SolverEngine::printInstantiations(std::ostream& out)
1502 {
1503   SolverEngineScope smts(this);
1504   finishInit();
1505   QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
1506
1507   // First, extract and print the skolemizations
1508   bool printed = false;
1509   bool reqNames = !d_env->getOptions().printer.printInstFull;
1510   // only print when in list mode
1511   if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST)
1512   {
1513     std::map<Node, std::vector<Node>> sks;
1514     qe->getSkolemTermVectors(sks);
1515     for (const std::pair<const Node, std::vector<Node>>& s : sks)
1516     {
1517       Node name;
1518       if (!qe->getNameForQuant(s.first, name, reqNames))
1519       {
1520         // did not have a name and we are only printing formulas with names
1521         continue;
1522       }
1523       SkolemList slist(name, s.second);
1524       out << slist;
1525       printed = true;
1526     }
1527   }
1528
1529   // Second, extract and print the instantiations
1530   std::map<Node, InstantiationList> rinsts;
1531   if (d_env->getOptions().smt.produceProofs
1532       && (!d_env->getOptions().smt.unsatCores
1533           || d_env->getOptions().smt.unsatCoresMode
1534                  == options::UnsatCoresMode::FULL_PROOF)
1535       && getSmtMode() == SmtMode::UNSAT)
1536   {
1537     // minimize instantiations based on proof manager
1538     getRelevantInstantiationTermVectors(
1539         rinsts, options().driver.dumpInstantiationsDebug);
1540   }
1541   else
1542   {
1543     std::map<Node, std::vector<std::vector<Node>>> insts;
1544     getInstantiationTermVectors(insts);
1545     for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
1546     {
1547       // convert to instantiation list
1548       Node q = i.first;
1549       InstantiationList& ilq = rinsts[q];
1550       ilq.initialize(q);
1551       for (const std::vector<Node>& ii : i.second)
1552       {
1553         ilq.d_inst.push_back(InstantiationVec(ii));
1554       }
1555     }
1556   }
1557   for (std::pair<const Node, InstantiationList>& i : rinsts)
1558   {
1559     if (i.second.d_inst.empty())
1560     {
1561       // no instantiations, skip
1562       continue;
1563     }
1564     Node name;
1565     if (!qe->getNameForQuant(i.first, name, reqNames))
1566     {
1567       // did not have a name and we are only printing formulas with names
1568       continue;
1569     }
1570     // must have a name
1571     if (d_env->getOptions().printer.printInstMode
1572         == options::PrintInstMode::NUM)
1573     {
1574       out << "(num-instantiations " << name << " " << i.second.d_inst.size()
1575           << ")" << std::endl;
1576     }
1577     else
1578     {
1579       // take the name
1580       i.second.d_quant = name;
1581       Assert(d_env->getOptions().printer.printInstMode
1582              == options::PrintInstMode::LIST);
1583       out << i.second;
1584     }
1585     printed = true;
1586   }
1587   // if we did not print anything, we indicate this
1588   if (!printed)
1589   {
1590     out << "none" << std::endl;
1591   }
1592 }
1593
1594 void SolverEngine::getInstantiationTermVectors(
1595     std::map<Node, std::vector<std::vector<Node>>>& insts)
1596 {
1597   SolverEngineScope smts(this);
1598   finishInit();
1599   QuantifiersEngine* qe =
1600       getAvailableQuantifiersEngine("getInstantiationTermVectors");
1601   // get the list of all instantiations
1602   qe->getInstantiationTermVectors(insts);
1603 }
1604
1605 bool SolverEngine::getSynthSolutions(std::map<Node, Node>& solMap)
1606 {
1607   SolverEngineScope smts(this);
1608   finishInit();
1609   return d_sygusSolver->getSynthSolutions(solMap);
1610 }
1611
1612 bool SolverEngine::getSubsolverSynthSolutions(std::map<Node, Node>& solMap)
1613 {
1614   SolverEngineScope smts(this);
1615   finishInit();
1616   return d_sygusSolver->getSubsolverSynthSolutions(solMap);
1617 }
1618
1619 Node SolverEngine::getQuantifierElimination(Node q, bool doFull)
1620 {
1621   SolverEngineScope smts(this);
1622   finishInit();
1623   return d_quantElimSolver->getQuantifierElimination(
1624       *d_asserts, q, doFull, d_isInternalSubsolver);
1625 }
1626
1627 bool SolverEngine::getInterpolant(const Node& conj,
1628                                   const TypeNode& grammarType,
1629                                   Node& interpol)
1630 {
1631   SolverEngineScope smts(this);
1632   finishInit();
1633   std::vector<Node> axioms = getExpandedAssertions();
1634   bool success =
1635       d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol);
1636   // notify the state of whether the get-interpol call was successfuly, which
1637   // impacts the SMT mode.
1638   d_state->notifyGetInterpol(success);
1639   return success;
1640 }
1641
1642 bool SolverEngine::getInterpolantNext(Node& interpol)
1643 {
1644   SolverEngineScope smts(this);
1645   finishInit();
1646   if (d_state->getMode() != SmtMode::INTERPOL)
1647   {
1648     throw RecoverableModalException(
1649         "Cannot get-interpol-next unless immediately preceded by a successful "
1650         "call to get-interpol(-next).");
1651   }
1652   bool success = d_interpolSolver->getInterpolantNext(interpol);
1653   // notify the state of whether the get-interpolant-next call was successful
1654   d_state->notifyGetInterpol(success);
1655   return success;
1656 }
1657
1658 bool SolverEngine::getAbduct(const Node& conj,
1659                              const TypeNode& grammarType,
1660                              Node& abd)
1661 {
1662   SolverEngineScope smts(this);
1663   finishInit();
1664   std::vector<Node> axioms = getExpandedAssertions();
1665   bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd);
1666   // notify the state of whether the get-abduct call was successful, which
1667   // impacts the SMT mode.
1668   d_state->notifyGetAbduct(success);
1669   return success;
1670 }
1671
1672 bool SolverEngine::getAbductNext(Node& abd)
1673 {
1674   SolverEngineScope smts(this);
1675   finishInit();
1676   if (d_state->getMode() != SmtMode::ABDUCT)
1677   {
1678     throw RecoverableModalException(
1679         "Cannot get-abduct-next unless immediately preceded by a successful "
1680         "call to get-abduct(-next).");
1681   }
1682   bool success = d_abductSolver->getAbductNext(abd);
1683   // notify the state of whether the get-abduct-next call was successful
1684   d_state->notifyGetAbduct(success);
1685   return success;
1686 }
1687
1688 void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
1689 {
1690   SolverEngineScope smts(this);
1691   QuantifiersEngine* qe =
1692       getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas");
1693   qe->getInstantiatedQuantifiedFormulas(qs);
1694 }
1695
1696 void SolverEngine::getInstantiationTermVectors(
1697     Node q, std::vector<std::vector<Node>>& tvecs)
1698 {
1699   SolverEngineScope smts(this);
1700   QuantifiersEngine* qe =
1701       getAvailableQuantifiersEngine("getInstantiationTermVectors");
1702   qe->getInstantiationTermVectors(q, tvecs);
1703 }
1704
1705 std::vector<Node> SolverEngine::getAssertions()
1706 {
1707   SolverEngineScope smts(this);
1708   finishInit();
1709   d_state->doPendingPops();
1710   Trace("smt") << "SMT getAssertions()" << endl;
1711   // note we always enable assertions, so it is available here
1712   return getAssertionsInternal();
1713 }
1714
1715 void SolverEngine::getDifficultyMap(std::map<Node, Node>& dmap)
1716 {
1717   Trace("smt") << "SMT getDifficultyMap()\n";
1718   SolverEngineScope smts(this);
1719   finishInit();
1720   if (!d_env->getOptions().smt.produceDifficulty)
1721   {
1722     throw ModalException(
1723         "Cannot get difficulty when difficulty option is off.");
1724   }
1725   // the prop engine has the proof of false
1726   Assert(d_pfManager);
1727   // get difficulty map from theory engine first
1728   TheoryEngine* te = getTheoryEngine();
1729   te->getDifficultyMap(dmap);
1730   // then ask proof manager to translate dmap in terms of the input
1731   d_pfManager->translateDifficultyMap(dmap, *d_asserts);
1732 }
1733
1734 void SolverEngine::push()
1735 {
1736   SolverEngineScope smts(this);
1737   finishInit();
1738   d_state->doPendingPops();
1739   Trace("smt") << "SMT push()" << endl;
1740   d_smtSolver->processAssertions(*d_asserts);
1741   d_state->userPush();
1742 }
1743
1744 void SolverEngine::pop()
1745 {
1746   SolverEngineScope smts(this);
1747   finishInit();
1748   Trace("smt") << "SMT pop()" << endl;
1749   d_state->userPop();
1750
1751   // Clear out assertion queues etc., in case anything is still in there
1752   d_asserts->clearCurrent();
1753   // clear the learned literals from the preprocessor
1754   d_smtSolver->getPreprocessor()->clearLearnedLiterals();
1755
1756   Trace("userpushpop") << "SolverEngine: popped to level "
1757                        << getUserContext()->getLevel() << endl;
1758   // should we reset d_status here?
1759   // SMT-LIBv2 spec seems to imply no, but it would make sense to..
1760 }
1761
1762 void SolverEngine::resetAssertions()
1763 {
1764   SolverEngineScope smts(this);
1765
1766   if (!d_state->isFullyInited())
1767   {
1768     // We're still in Start Mode, nothing asserted yet, do nothing.
1769     // (see solver execution modes in the SMT-LIB standard)
1770     Assert(getContext()->getLevel() == 0);
1771     Assert(getUserContext()->getLevel() == 0);
1772     return;
1773   }
1774
1775   Trace("smt") << "SMT resetAssertions()" << endl;
1776
1777   d_asserts->clearCurrent();
1778   d_state->notifyResetAssertions();
1779   // push the state to maintain global context around everything
1780   d_state->setup();
1781
1782   // reset SmtSolver, which will construct a new prop engine
1783   d_smtSolver->resetAssertions();
1784 }
1785
1786 void SolverEngine::interrupt()
1787 {
1788   if (!d_state->isFullyInited())
1789   {
1790     return;
1791   }
1792   d_smtSolver->interrupt();
1793 }
1794
1795 void SolverEngine::setResourceLimit(uint64_t units, bool cumulative)
1796 {
1797   if (cumulative)
1798   {
1799     d_env->d_options.base.cumulativeResourceLimit = units;
1800   }
1801   else
1802   {
1803     d_env->d_options.base.perCallResourceLimit = units;
1804   }
1805 }
1806 void SolverEngine::setTimeLimit(uint64_t millis)
1807 {
1808   d_env->d_options.base.perCallMillisecondLimit = millis;
1809 }
1810
1811 unsigned long SolverEngine::getResourceUsage() const
1812 {
1813   return getResourceManager()->getResourceUsage();
1814 }
1815
1816 unsigned long SolverEngine::getTimeUsage() const
1817 {
1818   return getResourceManager()->getTimeUsage();
1819 }
1820
1821 unsigned long SolverEngine::getResourceRemaining() const
1822 {
1823   return getResourceManager()->getResourceRemaining();
1824 }
1825
1826 NodeManager* SolverEngine::getNodeManager() const
1827 {
1828   return d_env->getNodeManager();
1829 }
1830
1831 void SolverEngine::printStatisticsSafe(int fd) const
1832 {
1833   d_env->getStatisticsRegistry().printSafe(fd);
1834 }
1835
1836 void SolverEngine::printStatisticsDiff() const
1837 {
1838   d_env->getStatisticsRegistry().printDiff(*d_env->getOptions().base.err);
1839   d_env->getStatisticsRegistry().storeSnapshot();
1840 }
1841
1842 void SolverEngine::setOption(const std::string& key, const std::string& value)
1843 {
1844   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
1845   options::set(getOptions(), key, value);
1846 }
1847
1848 void SolverEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
1849
1850 bool SolverEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
1851
1852 std::string SolverEngine::getOption(const std::string& key) const
1853 {
1854   Trace("smt") << "SMT getOption(" << key << ")" << endl;
1855   return options::get(getOptions(), key);
1856 }
1857
1858 Options& SolverEngine::getOptions() { return d_env->d_options; }
1859
1860 const Options& SolverEngine::getOptions() const { return d_env->getOptions(); }
1861
1862 ResourceManager* SolverEngine::getResourceManager() const
1863 {
1864   return d_env->getResourceManager();
1865 }
1866
1867 const Printer& SolverEngine::getPrinter() const { return d_env->getPrinter(); }
1868
1869 theory::Rewriter* SolverEngine::getRewriter() { return d_env->getRewriter(); }
1870
1871 }  // namespace cvc5