diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-08 00:51:13 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-07 22:51:13 -0700 |
| commit | 95e9918607ed879347bb250ecbaa3c5c557d71b4 (patch) | |
| tree | b49a02d8e47a25ee52ecec5a36b782c956577e95 /src/options/didyoumean_test.cpp | |
| parent | da756247012b6934999e9e66b8797b3655a01764 (diff) | |
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.
Diffstat (limited to 'src/options/didyoumean_test.cpp')
0 files changed, 0 insertions, 0 deletions