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