diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-04 16:51:35 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-04 16:51:35 +0200 |
| commit | 59620e0dcafd8224ce609785c37dd8350c33683f (patch) | |
| tree | 1bd882ba00e2716ace9f520bcfc32ac6374f9b38 /src/parser/smt2/Smt2.g | |
| parent | b539a167fa56deea34472a9725693f45ae325dd8 (diff) | |
Set default language to smt lib 2.6 (including as a base language for sygus), update regressions.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c7156635d..86c0b3126 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -3036,15 +3036,15 @@ AS_TOK : 'as'; CONST_TOK : 'const'; // extended commands -DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-codatatype'; -DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() }? 'declare-datatype'; -DECLARE_DATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-datatypes'; -DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-datatypes'; -DECLARE_CODATATYPES_2_5_TOK : { !PARSER_STATE->v2_6() }?'declare-codatatypes'; -DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() }?'declare-codatatypes'; +DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype'; +DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-datatype'; +DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-datatypes'; +DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes'; +DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes'; +DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes'; PAR_TOK : { PARSER_STATE->v2_6() }?'par'; -TESTER_TOK : { PARSER_STATE->v2_6() && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is'; -MATCH_TOK : { PARSER_STATE->v2_6() && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match'; +TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is'; +MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; |