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