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