Incorrect parse for Alt-Ergo language involving "and" token #144
Assignees
Labels
Comments
|
Solved by #147 |
Gbury
added a commit
to Gbury/opam-repository
that referenced
this issue
Jul 4, 2023
…men_bin and dolmen (0.9) CHANGES: ### Doc - Add examples in the doc and tuto for type-checking (including a minimal working example in the tutorial). ### UI - Make the unknown logic fatal by default, and simply enabled in non-strict mode (PR#158) - Add the `--check-flow` option to checks coherence of sequences of statements (PR#135) - Ensure stability of error codes for the `dolmen` binary ### Parsing - Add `attrs` fields for all declarations and definition types, and correctly attach predicate attribute to individual definitions (PR#130) - Restore support for toplevel "and" in non-recursive predicate/function definitions in Alt-Ergo syntax (PR Gbury/dolmen#147, fixes issue Gbury/dolmen#144) - Add support for hexadecimal floats in Alt-Ergo syntax (PR Gbury/dolmen#148, fixes issue Gbury/dolmen#145) - Add local goals to the `Prove` statement (PR#140) - Add a check-sat/prove-sat statement to ae's language (PR#140) ### Typing - Ignore arithmetic restrictions when typing model values. This particularly affects difference logic (PR#141) - Rename theory-specific configuration to `config` (instead of `arith`, `arrays`, etc..) (PR#142) - Add printing function for logics (PR#142) - Attach type definitions to type-defs (PR#157) - Add a proper reason for reserved builtins (PR#155) - Add bitvector builtins for alt-ergo's language (PR#136) ### Loop - Add possibility for users of the loop library to choose the exit/return code for a `Code.t` (PR#134) - Add the `Flow` module for flow checking (PR#135) - Add the `check` function in `typer.ml`/`typer_intf.ml` - Add `update` and `update_opt` in `State` (PR#156) - Print type definitions in the printer of typed statements (PR#157) - Prelude statements have been removed and replaced with prelude files (PR#160) - `Typer.additional_builtins` is now a `State.key` and takes the current state and language as arguments (PR#160) ### Model - Fix bug in bitvector implementation: negative inputs to `bvsmod` would raise an internal error (PR#138) - Remove the "error" keyword and statement from smtlib2 response (model) files (PR#139) - Correctly compare abstract array values (PR#143) - Accept extensions of functions/symbols with only partially defined semantics, for e.g. `fp.to_ubv`, `div`, etc.. (PR#151) - Error out on incremental problems (PR#169)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Consider the following:
Alt-Ergo's legacy frontend is happy with it:
But the dolmen parser barfs:
My guess is that some conflicts are not resolved in the right way.
The text was updated successfully, but these errors were encountered: