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.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f01893a350f504ab284af50c31c31bebcc3e5ab6..e693f1d57c16437f8a94d9357f247a647e1139ee 100644 (file)
--- 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';

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 1d2cc9f451a860587f7922a7e9dcca3a33d9f76f..98be91454b7afbf3a67bcf808afd74332c136212 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -68,7 +68,8 @@ SMT2_TESTS = \
        hung10_itesdk_output2.smt2 \
        hung10_itesdk_output1.smt2 \
        hung13sdk_output2.smt2 \
-       declare-funs.smt2
+       declare-funs.smt2 \
+       declare-fun-is-match.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \

diff --git a/test/regress/regress0/declare-fun-is-match.smt2 b/test/regress/regress0/declare-fun-is-match.smt2
new file mode 100644 (file)
index 0000000..d938720
--- /dev/null
+++ b/test/regress/regress0/declare-fun-is-match.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic UFIDL)
+(set-info :status sat)
+(declare-fun match (Int Int) Int)
+(declare-fun is (Int Int) Int)
+(assert (= match is))
+(check-sat)
+(exit)