src/smt/solver_engine.cpp

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