Simplify and improve the sygus parser (#2266)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 8 Aug 2018 05:51:13 +0000 (00:51 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 8 Aug 2018 05:51:13 +0000 (22:51 -0700)
commit95e9918607ed879347bb250ecbaa3c5c557d71b4
treeb49a02d8e47a25ee52ecec5a36b782c956577e95
parentda756247012b6934999e9e66b8797b3655a01764
Simplify and improve the sygus parser (#2266)

Currently, there is code duplication for parsing constants in sygus grammars, e.g.:
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L1048
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2304

This PR removes this duplication by introducing a new ANTLR grammar "termAtomic" in Smt2.g.

As a result of this PR, we now parse sygus grammars with any constant we otherwise parse. This addresses known issues where CVC4 rejects grammars with floating point constants.

It also removes some unnecessary code for converting builtin kinds to their total versions.

This is work towards #2197.  We still do not support sygus grammars with non-trivial *composite* terms, such as applications of indexed function symbols.
src/parser/smt2/Smt2.g