Merging v2.5.x on main #831
Closed
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
Unifying types in pattern matching
* Latest version of opam * Starting CI on branch 'fix-ci' * Adding depext
This makes it so that the configure step does not need to call opam.
* Avoid multiple rounding of intervals for polynomes * Fix style and indent * Review
This is required for compatibility with Menhir 20211215.
This allows removing the %type declarations for [clone_subst] and [use]. This is probably preferable (clearer) in the long run.
config file. Leaving it up to the user to install the deps.
* Add apt-get update step to workflows * Some more apt-get updates * Update to latest cmdliner * Update bounds for cmdliner version in opam files * Properly exit after --help/--version * Require --prefix in configure script if opam is not present * Try and remove superfluous printing * Restore prefix in Makefile.config * WIP * Restrict dune version to avoid bug in dune uninstall See ocaml/dune#5542
* Extended purify_form (access to ('a, bool) farray)
Added the purification of the operands when the operator is an access to an functional array storing booleans
* replaced evey "assert false" with a "failwith"
and made the lifting of let bindings be done at the top in farray access in purify_form
* Updating version of ocaml environment installer
The AltGr-Ergo package now depends on lablgtk3 and lablgtk3-sourcview3 packages. Since GtkFontChooserDialog is not supported in lalbgtk3, changing font in the editor is temporarily disabled.
Compatibility with dune 3 for release 2.4.2
CI: avsm/setup-ocaml@v2 -> ocaml/setup-ocaml@v2
from 'share' to 'lib'
Adding details on alt-ergo's output
The tests can be added or updated by the command: make gentests I modify also the Makefile in order to run tests as follow: make runtest
* Update the opam file for Dolmen 0.9 * Update the documentation * remove the pin for Dolmen
…764) Since --produce-models is intended to be used with `(get-model)` in the SMT-LIB format, it only makes sense to use a frontend that actually supports `(get-model)` when the option is provided. (Reported by @Halbaroth)
* Keep the default width of the rtd-theme * Improve conf.py * Clarify input file formats * Fix spelling * Review changes * Doublon * Revert removing _static directory
* Update the frontend documentation * Removing the `fully` adjective * Review changes
* Update model documentation * Review changes * Review changes bis * Review changes ter * Clarify the dolmen option
The dolmen frontend is adding declarations to the end of the command queue instead of to the front, causing the final command list to be all shuffled. This is the cause of at least some of the regressions with the dolmen frontend, since the solver now processes things in a different order. This patch ensures that the definitions are added with the correct ordering, so that the command queue should be the same with both frontends, barring additional bugs. This was tested with `-d commands` on a few benchmarks locally, where it produced the exact same output with both frontends. The patch also refactors slightly the [handle_smtt] method in the solving loop: as part of the debugging for this, I realized that we can never end up with `Hyp` constructors with local/global hypotheses names there, because one difference between the Dolmen and legacy frontend is that the legacy frontend extracts the hypotheses from the goal during typechecking (so prior to cnf-conversion) while the Dolmen frontend extracts the hypotheses from the goal during cnf-conversion (i.e. when we encounter a `Solve`).
Backporting 2.5.0
* Remove useless template * Add a lock file for the alt-ergo-lib * Remove the compiler in the lock file * Fix the lock file * Don't remove all packages matching ocaml * Make the lock target phony * fix * Use --enable-theories fpa to enable the fpa prelude * artefact * Use dune's include stanza for generated tests The current implementation of test generation is quite high friction: - When adding new tests, running tests directly with dune doesn't work, because the dune files must be generated by `make gentest` beforehand. There is `make runtest`, but that always runs all the tests, and does not allow specifying only some tests to run (which, given that our test suite is quite big, is sometimes needed for quick iterations). - The generated dune files are not commited to the repository, which means that it is easy to forget to run `make gentest` when switching branches -- which either causes some tests to silently not run, or errors because some files are missing. This patch solves both issues by integrating the test generation with dune, using the `include` stanza. More precisely: - The test generation script (gentest.ml) is modified to write all the test cases on the standard output as a single file, rather than creating the dune test files by itself. The generated file makes use of the `subdir` stanza to locate the targets appropriately. - There is a new `dune.inc` file that is included by the `dune` file in `tests`, and a `diff` rule that generates the content of that `dune.inc` file using the `gentest.ml` script. This is the way rules generation must work in dune, and it means that the `dune.inc` file must be commited to the repository --- which may not be such a bad thing, see above. The rule generation is added to the `gentest`, `runtest`, `runtest-quick` and `runtest-ci` aliases. The advantage of the new approach is that since the dependency is known to dune (and not only to make), running a command such as `dune build @tests/issues/XXX/runtest-quick` will always regenerate the tests, and also that we won't have to delete `dune` files manually when switching branches, since everything is in the file that gets re-generated. It means that running tests is slightly slower, because it always requires running the `gentest` script --- but that is probably fine, until we have many more tests than currently. * Review changes * Modify the warning for the fpa prelude * Fix spelling * Rebase artefacts * Promote tests * Rename output cli * Fix too long lines * Return the right environment * Promote tests * Use an adt to save the results of queries * Use an adt to save the results of queries (bis) * Fix lib_usage and worker_js --------- Co-authored-by: Basile Clément <basile.clement@ocamlpro.com>
* Add alt-ergo as a dependency for cram tests * Use ppx_blob 0.7.2 * Review changes * Prevent dune to compile examples
* Use fmt >= 0.9.0 * Removing useless line in the cram tests * Restoring trailing spaces
We have to use ppxlib >= 0.30.0 and prevent conflict with result < 1.5.
* Do not discard `bvnot` applied to uninterpreted terms In PR #745 we correctly handled the case where uninterpreted terms appear deep within a bit-vector terms, but we accidentally missed the case where the whole bit-vector is itself an uninterpreted term, leading to unsoundness (see the attached test). This patch fixes the code to properly deal with `bvnot` applied to an uninterpreted term. * Update the changes log for v2.5.1 * Review changes --------- Co-authored-by: Basile Clément <bc@ocamlpro.com>
|
Looks like there are conflicts here :( Should we revert the few commits for 2.3.3 that seems to be on |
|
We shouldn't remove the commit e0b89ab on main as the tag of the release |
|
Sorry, I meant revert the commits (as in |
When printing models, we can end up with class representatives that are not actually in the model. This can happen if a class representative is a defined constant, but also if it is an intermediate fresh constant introduced by the solver (!kXXX). This is because, in a class containing only uninterpreted terms, the representative will be the minimum term, independently of whether it is defined or fresh. This patch records and adds such terms to the `values` table as a (named) `Abstract` constant. This ensures that the same abstract value is used for all uses of a given constant. This is backported from a0575d2 for branch 2.5.x. Fixes #854
* Fix distinct unsoundness This PR quickly fixes the clash between the SMT-LIB specification of `distinct` and the implementation of this expression in AE. Basically, we expand the expression `distinct x_1 ... x_n` into a conjunction of binary disequalities. Notice that the model outputted for `uf2.models.smt2` changes because I don't preserve the old order used in `distinct`. * Fix the smart constructor of `mk_distinct` The smart construct `mk_distinct` produces an SMT-LIB compliant expression. * Clean up
We are not compatible with the development release of Dolmen due to the `implicit` field added in [1]. Further, we currently require that Dolmen move trigger annotations in SMT-LIB format from the body of the formula to the quantifier itself, but this was removed in [2]. Since both of these will be part of the next release of dolmen, let us pre-emptively ensure that release won't break Alt-Ergo. [1] : Gbury/dolmen#199 [2] : Gbury/dolmen#207
|
Merging |
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.
No description provided.