diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-08-25 17:19:41 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-26 00:19:41 +0000 |
| commit | 71f025753f734ddade5da333dfe2d144fbc13221 (patch) | |
| tree | 271e0a03b5612652d5fdb040fa2d7f43e8644aea /src/parser/smt2/smt2.cpp | |
| parent | 78d29da02099762374adeb694ed96c496c7e1ffc (diff) | |
Consolidate language types (#7065)
This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2a39a6208..fe777fe27 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -711,16 +711,9 @@ api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars, return d_allocGrammars.back().get(); } -bool Smt2::sygus() const -{ - InputLanguage ilang = getLanguage(); - return ilang == language::input::LANG_SYGUS_V2; -} +bool Smt2::sygus() const { return language::isLangSygus(getLanguage()); } -bool Smt2::sygus_v2() const -{ - return getLanguage() == language::input::LANG_SYGUS_V2; -} +bool Smt2::sygus_v2() const { return getLanguage() == Language::LANG_SYGUS_V2; } void Smt2::checkThatLogicIsSet() { @@ -848,7 +841,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name) return d_solver->mkAbstractValue(name.substr(1)); } -InputLanguage Smt2::getLanguage() const +Language Smt2::getLanguage() const { return d_solver->getOptions().base.inputLanguage; } |