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