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