src/smt/solver_engine.cpp

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