search

Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80 stars 17 forks source link

Incorrect parse of Alt-Ergo reals #145

Closed bclement-ocp closed 1 year ago

bclement-ocp commented 1 year ago

Consider the following:

$ cat real.ae
goal g: 0.0 < 0xFFFFFF.0p104

This is valid using Alt-Ergo's legacy parser:

$ alt-ergo --frontend legacy real.ae
File "real.ae", line 1, characters 9-29: Valid (0.0002) (0 steps) (goal g)

But dolmen barfs:

$ alt-ergo --frontend dolmen real.ae
File "real.ae", line 1, character 14-28:
1 | goal g: 0.0 < 0xFFFFFF.0p104
                  ^^^^^^^^^^^^^^
Error Unbound identifier: `0xFFFFFF.0p104`

(Note: 0xFFFFFF.0p104 is 0xFFFFFF x 2^104 = 340282346638528859811704183484516925440)