diff options
Diffstat (limited to 'src/parser/smt2')
| -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."); } |