src/smt/smt_engine.cpp

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