diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-03-28 14:31:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-28 14:31:37 -0500 |
| commit | a7f4f4fcf4d42f2c5b60bd62d3fd914f31202f64 (patch) | |
| tree | eec8ff7d01a9465f2e3220cab41517053ba8f750 /src | |
| parent | 830c09d3cadc119845aff27684bd68c16e442692 (diff) | |
Change is-cons to (_ is cons) in Sygus benchmarks. (#4174)
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 |