diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-08-27 11:23:15 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-27 18:23:15 +0000 |
| commit | 3183ca6685f6b0dcca538efb72e6840a56479b60 (patch) | |
| tree | e6c51d6175d4a56c7849aa4f965ed49b743f0607 /src/parser/smt2/smt2.cpp | |
| parent | a698b522d619c800a3401c7294cf1c6c663d7acc (diff) | |
Handle languages as strings in driver (#7074)
This PR moves the first chunk of code in the driver to use the proper options API for the language options. It is now handled as a string.
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index fe777fe27..39492a98c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -334,7 +334,7 @@ api::Term Smt2::getExpressionForNameAndType(const std::string& name, bool Smt2::getTesterName(api::Term cons, std::string& name) { - if ((v2_6() || sygus_v2()) && strictModeEnabled()) + if ((v2_6() || sygus()) && strictModeEnabled()) { // 2.6 or above uses indexed tester symbols, if we are in strict mode, // we do not automatically define is-cons for constructor cons. @@ -711,9 +711,10 @@ api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars, return d_allocGrammars.back().get(); } -bool Smt2::sygus() const { return language::isLangSygus(getLanguage()); } - -bool Smt2::sygus_v2() const { return getLanguage() == Language::LANG_SYGUS_V2; } +bool Smt2::sygus() const +{ + return d_solver->getOption("input-language") == "LANG_SYGUS_V2"; +} void Smt2::checkThatLogicIsSet() { |