Fix spurious parse error for rational real array constants (#3554)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 17 Dec 2019 08:00:42 +0000 (02:00 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 17 Dec 2019 08:00:42 +0000 (00:00 -0800)
commit9b2914ed9f7b14ecf535ffe9e1328d0fa042e072
tree0c23031d07a12d84477885c155f10c6ba1c2b737
parente1074c87769d079936b52a8e8ea33cc03f8b4638
Fix spurious parse error for rational real array constants (#3554)

Currently we can't parse constant arrays that store real values that are given as rationals `(/ n m)`. We throw a spurious parse error for `((as const (Array Int Real)) (/ 1 3))`, indicating that the argument of the array is not constant. This is caused by the fact that `(/ 1 3)` is parsed as a *division* term not a rational value.

This adds a special case to constant array construction so that we compute the result of a constant division instead of using the division term `(/ n m)` when constructing an array constant.
src/parser/smt2/smt2.cpp
test/regress/CMakeLists.txt
test/regress/regress0/array-const-real-parse.smt2 [new file with mode: 0644]