diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-06-02 14:11:05 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 12:11:05 +0000 |
| commit | 6d359817283f196034d8e36d0b9c1f10fb16d644 (patch) | |
| tree | cb7d17927671a3b059575a86b55676eec922cef8 /src/parser/smt2/smt2.cpp | |
| parent | 61b2694ac72d41aeff9c67e3631278e5a3bea5cb (diff) | |
Move public wrapper functions out of options class (#6600)
This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d32f149bf..4f5440944 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -18,6 +18,7 @@ #include "base/check.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" @@ -316,7 +317,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const bool Smt2::isHoEnabled() const { - return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo(); + return getLogic().isHigherOrder() && options::getUfHo(d_solver->getOptions()); } bool Smt2::logicIsSet() { @@ -842,7 +843,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name) InputLanguage Smt2::getLanguage() const { - return d_solver->getOptions().getInputLanguage(); + return options::getInputLanguage(d_solver->getOptions()); } void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) @@ -1094,7 +1095,8 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } else if (isBuiltinOperator) { - if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT)) + if (!options::getUfHo(opts) + && (kind == api::EQUAL || kind == api::DISTINCT)) { // need --uf-ho if these operators are applied over function args for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); @@ -1146,7 +1148,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { - if (!opts.getUfHo()) + if (!options::getUfHo(opts)) { parseError("Cannot partially apply functions unless --uf-ho is set."); } |