projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86ca9f1) | patch
Properly parse arithmetic values (#7876)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 5 Jan 2022 18:58:10 +0000 (12:58 -0600)
committerGitHub <noreply@github.com>
Wed, 5 Jan 2022 18:58:10 +0000 (18:58 +0000)
commit686164654ebca8a85a63fdb0c593ed2c8a77f369
tree862a55f2ebd7123187f32229167adedfb12db0eftree
parent86ca9f1aafb83202508221efdd8d3b7b772c4b70commit | diff
Properly parse arithmetic values (#7876)

This makes our parser correct for arithmetic values e.g. (- n) is parsed as a value not UMINUS when n is a numeral, as indicated in SMT-LIB. Similarly for (/ m n) and (/ (- m) n) we parse as values and not DIVISION.

This subsumes a patch for constructing array constants where this led to issues.
src/parser/smt2/smt2.cpp diff | blob | history