Parse 'is', 'match' differently for non-DT input
authorAndres Noetzli <noetzli@stanford.edu>
Fri, 16 Jun 2017 15:47:35 +0000 (08:47 -0700)
committerAndres Noetzli <noetzli@stanford.edu>
Fri, 16 Jun 2017 15:57:19 +0000 (08:57 -0700)
commitbb908d1df39b3064294e5da4813fbfbcb301646b
tree5d9ec283717e86102e6722936ef71ca4056ab433
parent209b08887bc55349880b9ed6d858e23637267dee
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
test/regress/regress0/Makefile.am
test/regress/regress0/declare-fun-is-match.smt2 [new file with mode: 0644]