Merge branch 'master' into issue6636

7 files changed, 50 insertions, 56 deletions

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 647981ab3..1381ef87c 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -104,9 +104,9 @@ ResourceManager* Env::getResourceManager() const
 
 const Printer& Env::getPrinter()
 {
-  return *Printer::getPrinter(d_options[options::outputLanguage]);
+  return *Printer::getPrinter(d_options.base.outputLanguage);
 }
 
-std::ostream& Env::getDumpOut() { return *d_options.getOut(); }
+std::ostream& Env::getDumpOut() { return *d_options.base.out; }
 
 }  // namespace cvc5
diff --git a/src/smt/env.h b/src/smt/env.h
index 667497683..29a360209 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -91,12 +91,6 @@ class Env
   /** Get a pointer to the underlying dump manager. */
   smt::DumpManager* getDumpManager();
 
-  template <typename Opt>
-  const auto& getOption(Opt opt) const
-  {
-    return d_options[opt];
-  }
-
   /** Get the options object (const version only) owned by this Env. */
   const Options& getOptions() const;
 
diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 3fc58ff05..37541751e 100644
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -71,7 +71,7 @@ void OptionsManager::notifySetOption(const std::string& key)
                << std::endl;
   if (key == options::expr::defaultExprDepth__name)
   {
-    int depth = (*d_options)[options::defaultExprDepth];
+    int depth = d_options->expr.defaultExprDepth;
     Debug.getStream() << expr::ExprSetDepth(depth);
     Trace.getStream() << expr::ExprSetDepth(depth);
     Notice.getStream() << expr::ExprSetDepth(depth);
@@ -82,7 +82,7 @@ void OptionsManager::notifySetOption(const std::string& key)
   }
   else if (key == options::expr::defaultDagThresh__name)
   {
-    int dag = (*d_options)[options::defaultDagThresh];
+    int dag = d_options->expr.defaultDagThresh;
     Debug.getStream() << expr::ExprDag(dag);
     Trace.getStream() << expr::ExprDag(dag);
     Notice.getStream() << expr::ExprDag(dag);
@@ -93,12 +93,12 @@ void OptionsManager::notifySetOption(const std::string& key)
   }
   else if (key == options::smt::dumpModeString__name)
   {
-    const std::string& value = (*d_options)[options::dumpModeString];
+    const std::string& value = d_options->smt.dumpModeString;
     Dump.setDumpFromString(value);
   }
   else if (key == options::base::printSuccess__name)
   {
-    bool value = (*d_options)[options::printSuccess];
+    bool value = d_options->base.printSuccess;
     Debug.getStream() << Command::printsuccess(value);
     Trace.getStream() << Command::printsuccess(value);
     Notice.getStream() << Command::printsuccess(value);
diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp
index 6395a4c2c..aa91bb184 100644
--- a/src/smt/output_manager.cpp
+++ b/src/smt/output_manager.cpp
@@ -15,6 +15,7 @@
 
 #include "smt/output_manager.h"
 
+#include "options/base_options.h"
 #include "smt/smt_engine.h"
 
 namespace cvc5 {
@@ -25,7 +26,7 @@ const Printer& OutputManager::getPrinter() const { return d_smt->getPrinter(); }
 
 std::ostream& OutputManager::getDumpOut() const
 {
-  return *d_smt->getOptions().getOut();
+  return *d_smt->getOptions().base.out;
 }
 
 }  // namespace cvc5
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index ad1e40c77..55cfc1f15 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -130,9 +130,8 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
   Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n";
 
   // Now make the final scope, which ensures that the only open leaves of the
-  // proof are the assertions, unless we are doing proofs to generate unsat
-  // cores, in which case we do not care.
-  d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCores());
+  // proof are the assertions.
+  d_finalProof = d_pnm->mkScope(pfn, assertions);
   Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
 }
 
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 135fabf5f..96081e97b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1523,12 +1523,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (opts.wasSetByUser(options::nlCad))
     {
       std::stringstream ss;
-      ss << "Cannot use " << options::nlCad.name << " without configuring with --poly.";
+      ss << "Cannot use " << options::arith::nlCad__name << " without configuring with --poly.";
       throw OptionException(ss.str());
     }
     else
     {
-      Notice() << "Cannot use --" << options::nlCad.name
+      Notice() << "Cannot use --" << options::arith::nlCad__name
                << " without configuring with --poly." << std::endl;
       opts.arith.nlCad = false;
       opts.arith.nlExt = options::NlExtMode::FULL;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7abeac44f..c84a29055 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -193,7 +193,7 @@ void SmtEngine::finishInit()
   }
 
   // set the random seed
-  Random::getRandom().setSeed(d_env->getOption(options::seed));
+  Random::getRandom().setSeed(d_env->getOptions().driver.seed);
 
   // Call finish init on the options manager. This inializes the resource
   // manager based on the options, and sets up the best default options
@@ -201,7 +201,7 @@ void SmtEngine::finishInit()
   d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver);
 
   ProofNodeManager* pnm = nullptr;
-  if (d_env->getOption(options::produceProofs))
+  if (d_env->getOptions().smt.produceProofs)
   {
     // ensure bound variable uses canonical bound variables
     getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
@@ -262,11 +262,11 @@ void SmtEngine::finishInit()
   getDumpManager()->finishInit();
 
   // subsolvers
-  if (d_env->getOption(options::produceAbducts))
+  if (d_env->getOptions().smt.produceAbducts)
   {
     d_abductSolver.reset(new AbductionSolver(this));
   }
-  if (d_env->getOption(options::produceInterpols)
+  if (d_env->getOptions().smt.produceInterpols
       != options::ProduceInterpols::NONE)
   {
     d_interpolSolver.reset(new InterpolationSolver(this));
@@ -459,10 +459,10 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
     if (!Options::current().wasSetByUser(options::outputLanguage))
     {
       language::output::Language olang = language::toOutputLanguage(ilang);
-      if (d_env->getOption(options::outputLanguage) != olang)
+      if (d_env->getOptions().base.outputLanguage != olang)
       {
         getOptions().base.outputLanguage = olang;
-        *d_env->getOption(options::out) << language::SetLanguage(olang);
+        *d_env->getOptions().base.out << language::SetLanguage(olang);
       }
     }
   }
@@ -575,7 +575,7 @@ void SmtEngine::debugCheckFunctionBody(Node formula,
                                        Node func)
 {
   TypeNode formulaType =
-      formula.getType(d_env->getOption(options::typeChecking));
+      formula.getType(d_env->getOptions().expr.typeChecking);
   TypeNode funcType = func.getType();
   // We distinguish here between definitions of constants and functions,
   // because the type checking for them is subtly different.  Perhaps we
@@ -741,7 +741,7 @@ Result SmtEngine::quickCheck() {
 
 Model* SmtEngine::getAvailableModel(const char* c) const
 {
-  if (!d_env->getOption(options::assignFunctionValues))
+  if (!d_env->getOptions().theory.assignFunctionValues)
   {
     std::stringstream ss;
     ss << "Cannot " << c << " when --assign-function-values is false.";
@@ -758,7 +758,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const
     throw RecoverableModalException(ss.str().c_str());
   }
 
-  if (!d_env->getOption(options::produceModels))
+  if (!d_env->getOptions().smt.produceModels)
   {
     std::stringstream ss;
     ss << "Cannot " << c << " when produce-models options is off.";
@@ -902,7 +902,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
                  << "(" << assumptions << ") => " << r << endl;
 
     // Check that SAT results generate a model correctly.
-    if (d_env->getOption(options::checkModels))
+    if (d_env->getOptions().smt.checkModels)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
       {
@@ -910,14 +910,14 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate a proof correctly.
-    if (d_env->getOption(options::checkProofs)
-        || d_env->getOption(options::proofEagerChecking))
+    if (d_env->getOptions().smt.checkProofs
+        || d_env->getOptions().proof.proofEagerChecking)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
-        if ((d_env->getOption(options::checkProofs)
-             || d_env->getOption(options::proofEagerChecking))
-            && !d_env->getOption(options::produceProofs))
+        if ((d_env->getOptions().smt.checkProofs
+             || d_env->getOptions().proof.proofEagerChecking)
+            && !d_env->getOptions().smt.produceProofs)
         {
           throw ModalException(
               "Cannot check-proofs because proofs were disabled.");
@@ -926,7 +926,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate an unsat core correctly.
-    if (d_env->getOption(options::checkUnsatCores))
+    if (d_env->getOptions().smt.checkUnsatCores)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
@@ -955,7 +955,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
 {
   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
   SmtScope smts(this);
-  if (!d_env->getOption(options::unsatAssumptions))
+  if (!d_env->getOptions().smt.unsatAssumptions)
   {
     throw ModalException(
         "Cannot get unsat assumptions when produce-unsat-assumptions option "
@@ -1166,7 +1166,7 @@ Node SmtEngine::getValue(const Node& ex) const
   Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
          || resultNode.isConst());
 
-  if (d_env->getOption(options::abstractValues)
+  if (d_env->getOptions().smt.abstractValues
       && resultNode.getType().isArray())
   {
     resultNode = d_absValues->mkAbstractValue(resultNode);
@@ -1207,7 +1207,7 @@ Model* SmtEngine::getModel() {
   Assert(te != nullptr);
   te->setEagerModelBuilding();
 
-  if (d_env->getOption(options::modelCoresMode)
+  if (d_env->getOptions().smt.modelCoresMode
       != options::ModelCoresMode::NONE)
   {
     // If we enabled model cores, we compute a model core for m based on our
@@ -1215,7 +1215,7 @@ Model* SmtEngine::getModel() {
     std::vector<Node> eassertsProc = getExpandedAssertions();
     ModelCoreBuilder::setModelCore(eassertsProc,
                                    m->getTheoryModel(),
-                                   d_env->getOption(options::modelCoresMode));
+                                   d_env->getOptions().smt.modelCoresMode);
   }
   // set the information on the SMT-level model
   Assert(m != nullptr);
@@ -1238,7 +1238,7 @@ Result SmtEngine::blockModel()
 
   Model* m = getAvailableModel("block model");
 
-  if (d_env->getOption(options::blockModelsMode)
+  if (d_env->getOptions().smt.blockModelsMode
       == options::BlockModelsMode::NONE)
   {
     std::stringstream ss;
@@ -1251,7 +1251,7 @@ Result SmtEngine::blockModel()
   Node eblocker =
       ModelBlocker::getModelBlocker(eassertsProc,
                                     m->getTheoryModel(),
-                                    d_env->getOption(options::blockModelsMode));
+                                    d_env->getOptions().smt.blockModelsMode);
   Trace("smt") << "Block formula: " << eblocker << std::endl;
   return assertFormula(eblocker);
 }
@@ -1349,17 +1349,17 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
 void SmtEngine::checkProof()
 {
-  Assert(d_env->getOption(options::produceProofs));
+  Assert(d_env->getOptions().smt.produceProofs);
   // internal check the proof
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
-  if (d_env->getOption(options::proofEagerChecking))
+  if (d_env->getOptions().proof.proofEagerChecking)
   {
     pe->checkProof(d_asserts->getAssertionList());
   }
   Assert(pe->getProof() != nullptr);
   std::shared_ptr<ProofNode> pePfn = pe->getProof();
-  if (d_env->getOption(options::checkProofs))
+  if (d_env->getOptions().smt.checkProofs)
   {
     d_pfManager->checkProof(pePfn, *d_asserts);
   }
@@ -1372,7 +1372,7 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry()
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
-  if (!d_env->getOption(options::unsatCores))
+  if (!d_env->getOptions().smt.unsatCores)
   {
     throw ModalException(
         "Cannot get an unsat core when produce-unsat-cores or produce-proofs "
@@ -1405,7 +1405,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
 }
 
 void SmtEngine::checkUnsatCore() {
-  Assert(d_env->getOption(options::unsatCores))
+  Assert(d_env->getOptions().smt.unsatCores)
       << "cannot check unsat core if unsat cores are turned off";
 
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
@@ -1514,7 +1514,7 @@ std::string SmtEngine::getProof()
   {
     getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
   }
-  if (!d_env->getOption(options::produceProofs))
+  if (!d_env->getOptions().smt.produceProofs)
   {
     throw ModalException("Cannot get a proof when proof option is off.");
   }
@@ -1537,7 +1537,7 @@ std::string SmtEngine::getProof()
 void SmtEngine::printInstantiations( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();
-  if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS)
+  if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
   {
     out << "% SZS output start Proof for " << d_state->getFilename()
         << std::endl;
@@ -1546,9 +1546,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
 
   // First, extract and print the skolemizations
   bool printed = false;
-  bool reqNames = !d_env->getOption(options::printInstFull);
+  bool reqNames = !d_env->getOptions().printer.printInstFull;
   // only print when in list mode
-  if (d_env->getOption(options::printInstMode) == options::PrintInstMode::LIST)
+  if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST)
   {
     std::map<Node, std::vector<Node>> sks;
     qe->getSkolemTermVectors(sks);
@@ -1583,14 +1583,14 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
       continue;
     }
     // must have a name
-    if (d_env->getOption(options::printInstMode) == options::PrintInstMode::NUM)
+    if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM)
     {
       out << "(num-instantiations " << name << " " << i.second.size() << ")"
           << std::endl;
     }
     else
     {
-      Assert(d_env->getOption(options::printInstMode)
+      Assert(d_env->getOptions().printer.printInstMode
              == options::PrintInstMode::LIST);
       InstantiationList ilist(name, i.second);
       out << ilist;
@@ -1602,7 +1602,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   {
     out << "No instantiations" << std::endl;
   }
-  if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS)
+  if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
   {
     out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
   }
@@ -1613,9 +1613,9 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (d_env->getOption(options::produceProofs)
-      && (!d_env->getOption(options::unsatCores)
-          || d_env->getOption(options::unsatCoresMode) == options::UnsatCoresMode::FULL_PROOF)
+  if (d_env->getOptions().smt.produceProofs
+      && (!d_env->getOptions().smt.unsatCores
+          || d_env->getOptions().smt.unsatCoresMode == options::UnsatCoresMode::FULL_PROOF)
       && getSmtMode() == SmtMode::UNSAT)
   {
     // minimize instantiations based on proof manager
@@ -1716,7 +1716,7 @@ std::vector<Node> SmtEngine::getAssertions()
     getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut());
   }
   Trace("smt") << "SMT getAssertions()" << endl;
-  if (!d_env->getOption(options::produceAssertions))
+  if (!d_env->getOptions().smt.produceAssertions)
   {
     const char* msg =
       "Cannot query the current assertion list when not in produce-assertions mode.";