From bb908d1df39b3064294e5da4813fbfbcb301646b Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 16 Jun 2017 08:47:35 -0700 Subject: Parse 'is', 'match' differently for non-DT input In SMT 2.6, Datatypes are being introduced and they come with testers (indexed identifier of the form (_ is c)) and match expressions. This lead to failures in UFIDL benchmarks in SMT-LIB because they declare the function 'is'. This commit changes the parser s.t. it does not consider 'is' and 'match' special tokens unless the theory of datatypes is enabled. --- src/parser/smt2/Smt2.g | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/parser/smt2/Smt2.g') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f01893a35..e693f1d57 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -3026,8 +3026,8 @@ 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'; PAR_TOK : { PARSER_STATE->v2_6() }?'par'; -TESTER_TOK : { PARSER_STATE->v2_6() }?'is'; -MATCH_TOK : { PARSER_STATE->v2_6() }?'match'; +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'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; -- cgit v1.2.3