diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-08-31 18:17:24 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-01 01:17:24 +0000 |
commit | a6cdf2b085aaa9789f47757329a7803053ceb36a (patch) | |
tree | 98280ce376d9828241d850e6c9e1271c4024f0c2 /src/parser | |
parent | 068a0aa316f3760b401d900d39101955ba66b6c2 (diff) |
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().
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.cpp | 4 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 20 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 8 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 2 |
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. * |