diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 8 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 2 |
2 files changed, 9 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 81ddae6d6..04e8be64b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -330,7 +330,7 @@ api::Term Smt2::getExpressionForNameAndType(const std::string& name, bool Smt2::getTesterName(api::Term cons, std::string& name) { - if (v2_6() && strictModeEnabled()) + if ((v2_6() || sygus_v2()) && 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. @@ -744,11 +744,17 @@ bool Smt2::sygus() const return ilang == language::input::LANG_SYGUS || ilang == language::input::LANG_SYGUS_V2; } + bool Smt2::sygus_v1() const { return getLanguage() == language::input::LANG_SYGUS; } +bool Smt2::sygus_v2() const +{ + return getLanguage() == language::input::LANG_SYGUS_V2; +} + void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { // TODO: ??? } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 0400c680f..35d088601 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -277,6 +277,8 @@ class Smt2 : public Parser bool sygus() const; /** Are we using the sygus version 1.0 format? */ bool sygus_v1() const; + /** Are we using the sygus version 2.0 format? */ + bool sygus_v2() const; /** * Returns true if the language that we are parsing (SMT-LIB version >=2.5 |