issues
search
dreal
/
dreal4
Automated Reasoning in Nonlinear Theories of Reals
https://dreal.github.io
Apache License 2.0
150
stars
31
forks
source link
ToPrefix generates non-SMTLIB-compliant strings
#275
Closed
soonhokong
closed
2 years ago
soonhokong
commented
2 years ago
A negative constant
-c
should be formatted as
(- c)
.
https://github.com/dreal/dreal4/blob/db12dd0ff02c34701aec8f7061947c6706d217db/dreal/symbolic/prefix_printer.cc#L50-L58
-c
should be formatted as(- c)
. https://github.com/dreal/dreal4/blob/db12dd0ff02c34701aec8f7061947c6706d217db/dreal/symbolic/prefix_printer.cc#L50-L58