No longer use direct access to options in driver (#7094)

This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().

5 files changed, 12 insertions, 26 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index bd0f56b2d..39b38be30 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -26,8 +26,6 @@
 #include "base/check.h"
 #include "base/output.h"
 #include "expr/kind.h"
-#include "options/base_options.h"
-#include "options/options.h"
 #include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "smt/command.h"
@@ -899,7 +897,7 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s)
 
 api::Term Parser::mkStringConstant(const std::string& s)
 {
-  if (language::isLangSmt2(d_solver->getOptions().base.inputLanguage))
+  if (d_solver->getOption("input-language") == "LANG_SMTLIB_V2_6")
   {
     return d_solver->mkString(s, true);
   }
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 665836402..b1bb9a432 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -21,9 +21,6 @@
 #include "api/cpp/cvc5.h"
 #include "base/check.h"
 #include "cvc/cvc.h"
-#include "options/base_options.h"
-#include "options/options.h"
-#include "options/parser_options.h"
 #include "parser/antlr_input.h"
 #include "parser/input.h"
 #include "parser/parser.h"
@@ -41,7 +38,7 @@ ParserBuilder::ParserBuilder(api::Solver* solver,
   init(solver, sm);
   if (useOptions)
   {
-    withOptions(solver->getOptions());
+    withOptions();
   }
 }
 
@@ -109,17 +106,18 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
   return *this;
 }
 
-ParserBuilder& ParserBuilder::withOptions(const Options& opts)
+ParserBuilder& ParserBuilder::withOptions()
 {
   ParserBuilder& retval = *this;
   retval = retval.withInputLanguage(d_solver->getOption("input-language"))
-               .withChecks(opts.parser.semanticChecks)
-               .withStrictMode(opts.parser.strictParsing)
-               .withParseOnly(opts.base.parseOnly)
-               .withIncludeFile(opts.parser.filesystemAccess);
-  if (opts.parser.forceLogicStringWasSetByUser)
+               .withChecks(d_solver->getOptionInfo("semantic-checks").boolValue())
+               .withStrictMode(d_solver->getOptionInfo("strict-parsing").boolValue())
+               .withParseOnly(d_solver->getOptionInfo("parse-only").boolValue())
+               .withIncludeFile(d_solver->getOptionInfo("filesystem-access").boolValue());
+  auto info = d_solver->getOptionInfo("force-logic");
+  if (info.setByUser)
   {
-    LogicInfo tmp(opts.parser.forceLogicString);
+    LogicInfo tmp(info.stringValue());
     retval = retval.withForcedLogic(tmp.getLogicString());
   }
   return retval;
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 23a9daae2..d148a538d 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -104,8 +104,8 @@ class CVC5_EXPORT ParserBuilder
    */
   ParserBuilder& withParseOnly(bool flag = true);
 
-  /** Derive settings from the given options. */
-  ParserBuilder& withOptions(const Options& opts);
+  /** Derive settings from the solver's options. */
+  ParserBuilder& withOptions();
 
   /**
    * Should the parser use strict mode?
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 1a0a3d52a..2fd4a5596 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -17,9 +17,6 @@
 #include <algorithm>
 
 #include "base/check.h"
-#include "options/base_options.h"
-#include "options/options.h"
-#include "options/options_public.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
 #include "parser/smt2/smt2_input.h"
@@ -843,11 +840,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name)
   return d_solver->mkAbstractValue(name.substr(1));
 }
 
-Language Smt2::getLanguage() const
-{
-  return d_solver->getOptions().base.inputLanguage;
-}
-
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
 {
   Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index c3f93708d..97eb95c00 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -413,8 +413,6 @@ class Smt2 : public Parser
 
   void addSepOperators();
 
-  Language getLanguage() const;
-
   /**
    * Utility function to create a conjunction of expressions.
    *