Support hexadecimal reals in Alt-Ergo syntax #148
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Gbury
approved these changes
May 2, 2023
|
I will add the changelog entry once #147 is merged and this is rebased onto it otherwise there will be conflicts |
Alt-Ergo allows specifying real literals using hexadecimal notation. For instance, [0x1.1p1] represents [(1 + 1/16) * 2^1 = 17/8]. Currently, dolmen parses such literals but does not typecheck them properly. This patch changes that. Note that such reals are stored in [Builtins.Decimal] using their raw representation. The documentation of [Builtins.Decimal] is updated to indicate that fact, and to suggest evaluating the string within using [Q.of_string] if canonicalization is required. Fixes Gbury#145
bclement-ocp
force-pushed
the
bclement/fix-145
branch
from
e280aaa
to
07bf316
Compare
Gbury
added a commit
to Gbury/opam-repository
that referenced
this pull request
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Alt-Ergo allows specifying real literals using hexadecimal notation. For instance, [0x1.1p1] represents [(1 + 1/16) * 2^1 = 17/8].
Currently, dolmen parses such literals but does not typecheck them properly. This patch changes that.
Note that such reals are stored in [Builtins.Decimal] using their raw representation. The documentation of [Builtins.Decimal] is updated to indicate that fact, and to suggest evaluating the string within using [Q.of_string] if canonicalization is required.
Fixes #145