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