Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix(CLI): Remove --optimize option in favor of --strict #1133

Merged
merged 4 commits into from
Jun 3, 2024
Merged

fix(CLI): Remove --optimize option in favor of --strict #1133

merged 4 commits into from
Jun 3, 2024

Conversation

bclement-ocp
Copy link
Collaborator

Following discussions at the Club's meeting last week, it was decided to enable optimization statements (maximize, minimize, and get-objectives) by default and to forbid their usage through a different option to enable strict mode with SMT-LIB spec compliance.

Currently, the --strict option only disables optimization. It should also disable extensions such as ae.round and bv2nat / int2bv.

This patch implements that change. Note that the --optimize option did not go into any release yet.

@bclement-ocp bclement-ocp mentioned this pull request May 27, 2024
Open
Halbaroth
Halbaroth requested changes Jun 3, 2024
View reviewed changes
Copy link
Collaborator

@Halbaroth Halbaroth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me.

tools/gentest.ml Outdated Show resolved Hide resolved
src/bin/common/solving_loop.ml
Comment on lines -555 to -549
| Util.Tableaux | Tableaux_CDCL when optim ->
warning
"Sat-solver %a is incompatible with optimization: ignoring command."
Util.pp_sat_solver
sat;
st
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a remainder. As we don't explore different SAT branches in FunSAT and we don't force the SAT solver to be SatML in presence of the MaxSMT extension, it means the feature is broken in presence of --sat-solver tableaux for instance. We should mention it at least in the documentation of AE for the next release.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The Tableaux solver errors out if it receives an optimization command (see implementation of Fun_sat_frontend.optimize).

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Uhm I'm not sure we should crash with an error here. We don't produce wrong model but we don't produce the best one (according to our definition of best one).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree that this is a bad error mechanism, but I'd argue that returning an error here is appropriate — the user is requesting an optimized model, but we can't satisfy that request. I'll change the mechanism when we encounter an optimize in the Tableaux solver.

@bclement-ocp
Copy link
Collaborator Author

bclement-ocp commented Jun 3, 2024 •
edited by Halbaroth
Loading

Looks good to me.

You marked the PR as "changes requested" so I am a bit confused by this comment.

@Halbaroth
Copy link
Collaborator

Looks good to me.

You marked the PR as "changes requested" so I am a bit confused by this comment.

:D my request changes weren't essential.

@bclement-ocp
Copy link
Collaborator Author

:D my request changes weren't essential.

In that case it is better to mark as "Approved" — marking as "Changes requested" prevents the PR from being merged until you (or someone else) later approve(s).

@bclement-ocp
fix(CLI): Remove --optimize option in favor of --strict
8a07ae2 
Following discussions at the Club's meeting last week, it was decided to
enable optimization statements (`maximize`, `minimize`, and
`get-objectives`) by default and to forbid their usage through a
different option to enable strict mode with SMT-LIB spec compliance.

Currently, the `--strict` option only disables optimization. It should
also disable extensions such as `ae.round` and `bv2nat` / `int2bv`.

This patch implements that change. Note that the `--optimize` option did
not go into any release yet.
@bclement-ocp
Remove optimize test suite
9478d0e
@bclement-ocp
Copy link
Collaborator Author

@Halbaroth Added a test to return an (error) reply when trying to use (maximize), (minimize), or (get-objectives) with a Tableaux-based solver. Whether or not we stop or ignore the corresponding statement depends on the --continue-on-error flag, as usual for errors per the SMT-LIB standard.

@bclement-ocp bclement-ocp merged commit 1a64e0f into OCamlPro:next Jun 3, 2024
14 checks passed
@bclement-ocp bclement-ocp deleted the strict-mode branch June 3, 2024 16:57
@bclement-ocp bclement-ocp added this to the 2.6.0 milestone Jul 11, 2024
@bclement-ocp bclement-ocp mentioned this pull request Sep 24, 2024
Merged
bclement-ocp added a commit to bclement-ocp/opam-repository that referenced this pull request Sep 24, 2024
@bclement-ocp
[new release] alt-ergo (4 packages) (2.6.0)
34f6b75 
CHANGES:

### Command-line interface

 - Enable FPA theory by default (OCamlPro/alt-ergo#1177)
 - Remove deprecated output channels (OCamlPro/alt-ergo#782)
 - Deprecate the --use-underscore since it produces models that are not SMT-LIB
   compliant (OCamlPro/alt-ergo#805)
 - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838)
 - Use consistent return codes (OCamlPro/alt-ergo#842)
 - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853)
 - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857)
 - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947)
 - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949)
 - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984)
 - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133)
 - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204)

### SMT-LIB support

 - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911,
   OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069)
 - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135)
 - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880)
 - Add support for the `:named` attribute (OCamlPro/alt-ergo#957)
 - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972)
 - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143)

### Model generation

 - Use post-solve SAT environment in model generation, fixing issues where
   incorrect models were generated (OCamlPro/alt-ergo#789)
 - Restore support for records in models (OCamlPro/alt-ergo#793)
 - Use abstract values instead of dummy values in models where the
   actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835)
 - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811)
 - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829)
 - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968)
 - Add support for optimization (MaxSMT / OptiSMT) with
   lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921)
 - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932)
 - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019)
 - Fix a rare soundness issue with integer constraints when model generation is
   enabled (OCamlPro/alt-ergo#1025)
 - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153)

### Theory reasoning

 - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010,
   OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144,
   OCamlPro/alt-ergo#1152)
 - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058,
   OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085)
 - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154)
 - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979)
 - Abstract more arguments of AC symbols to avoid infinite loops when
   they contain other AC symbols (OCamlPro/alt-ergo#990)
 - Do not make irrelevant decisions in CDCL solver, improving
   performance slightly (OCamlPro/alt-ergo#1041)
 - Rewrite the ADT theory to use domains and integrate the enum theory into the
   ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138)
 - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108)
 - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166)
 - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192)
 - Run cross-propagators to completion (OCamlPro/alt-ergo#1221)
 - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222)
 - Only perform optimization when building a model (OCamlPro/alt-ergo#1224)
 - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225)
 - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226)

### Internal/library changes

 - Rewrite the Vec module (OCamlPro/alt-ergo#607)
 - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808)
 - Mark proxy names as reserved (OCamlPro/alt-ergo#836)
 - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943)
 - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856)
 - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869)
 - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872)
 - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878)
 - Do not use existential variables for integer division (OCamlPro/alt-ergo#881)
 - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886)
 - Properly start timers (OCamlPro/alt-ergo#924)
 - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925)
 - Allow direct access to the SAT API in the Alt-Ergo library computations
   during printing (OCamlPro/alt-ergo#927)
 - Better handling for step limit (OCamlPro/alt-ergo#936)
 - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951)
 - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962)
 - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971)
 - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118)
 - Preserve trigger order when parsing quantifiers with multiple trigger
   (OCamlPro/alt-ergo#1046).
 - Store domains inside the union-find module (OCamlPro/alt-ergo#1119)
 - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219)

### Build and integration

 - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803)
 - Use dune-site for the inequalities plugins. External pluginsm ust now be
   registered through the dune-site plugin mechanism in the
   `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049).
 - Add a release workflow (OCamlPro/alt-ergo#827)
 - Add a Windows workflow (OCamlPro/alt-ergo#1203)
 - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830)
 - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882)
 - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887)
 - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888)
 - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918)
 - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912)
 - Fix the Makefile (OCamlPro/alt-ergo#914)
 - Add `Logs` dependency (OCamlPro/alt-ergo#1206)
 - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199)
 - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200)
 - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223)

### Testing

 - Use --enable-assertions in tests (OCamlPro/alt-ergo#809)
 - Add a test for push/pop (OCamlPro/alt-ergo#843)
 - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938)
 - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939)
 - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941)

### Documentation

 - Add a new example for model generation (OCamlPro/alt-ergo#826)
 - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862)
 - Update the current authors (OCamlPro/alt-ergo#865)
 - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871)
 - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915)
 - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995)
 - Document Windows support (OCamlPro/alt-ergo#1216)
 - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217)
 - Document optimization feature (OCamlPro/alt-ergo#1231)
tjammer pushed a commit to tjammer/opam-repository that referenced this pull request Sep 24, 2024
@bclement-ocp @tjammer
[new release] alt-ergo (4 packages) (2.6.0)
30afd8b 
CHANGES:

### Command-line interface

 - Enable FPA theory by default (OCamlPro/alt-ergo#1177)
 - Remove deprecated output channels (OCamlPro/alt-ergo#782)
 - Deprecate the --use-underscore since it produces models that are not SMT-LIB
   compliant (OCamlPro/alt-ergo#805)
 - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838)
 - Use consistent return codes (OCamlPro/alt-ergo#842)
 - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853)
 - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857)
 - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947)
 - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949)
 - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984)
 - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133)
 - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204)

### SMT-LIB support

 - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911,
   OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069)
 - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135)
 - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880)
 - Add support for the `:named` attribute (OCamlPro/alt-ergo#957)
 - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972)
 - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143)

### Model generation

 - Use post-solve SAT environment in model generation, fixing issues where
   incorrect models were generated (OCamlPro/alt-ergo#789)
 - Restore support for records in models (OCamlPro/alt-ergo#793)
 - Use abstract values instead of dummy values in models where the
   actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835)
 - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811)
 - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829)
 - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968)
 - Add support for optimization (MaxSMT / OptiSMT) with
   lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921)
 - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932)
 - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019)
 - Fix a rare soundness issue with integer constraints when model generation is
   enabled (OCamlPro/alt-ergo#1025)
 - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153)

### Theory reasoning

 - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010,
   OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144,
   OCamlPro/alt-ergo#1152)
 - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058,
   OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085)
 - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154)
 - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979)
 - Abstract more arguments of AC symbols to avoid infinite loops when
   they contain other AC symbols (OCamlPro/alt-ergo#990)
 - Do not make irrelevant decisions in CDCL solver, improving
   performance slightly (OCamlPro/alt-ergo#1041)
 - Rewrite the ADT theory to use domains and integrate the enum theory into the
   ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138)
 - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108)
 - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166)
 - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192)
 - Run cross-propagators to completion (OCamlPro/alt-ergo#1221)
 - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222)
 - Only perform optimization when building a model (OCamlPro/alt-ergo#1224)
 - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225)
 - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226)

### Internal/library changes

 - Rewrite the Vec module (OCamlPro/alt-ergo#607)
 - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808)
 - Mark proxy names as reserved (OCamlPro/alt-ergo#836)
 - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943)
 - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856)
 - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869)
 - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872)
 - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878)
 - Do not use existential variables for integer division (OCamlPro/alt-ergo#881)
 - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886)
 - Properly start timers (OCamlPro/alt-ergo#924)
 - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925)
 - Allow direct access to the SAT API in the Alt-Ergo library computations
   during printing (OCamlPro/alt-ergo#927)
 - Better handling for step limit (OCamlPro/alt-ergo#936)
 - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951)
 - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962)
 - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971)
 - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118)
 - Preserve trigger order when parsing quantifiers with multiple trigger
   (OCamlPro/alt-ergo#1046).
 - Store domains inside the union-find module (OCamlPro/alt-ergo#1119)
 - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219)

### Build and integration

 - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803)
 - Use dune-site for the inequalities plugins. External pluginsm ust now be
   registered through the dune-site plugin mechanism in the
   `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049).
 - Add a release workflow (OCamlPro/alt-ergo#827)
 - Add a Windows workflow (OCamlPro/alt-ergo#1203)
 - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830)
 - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882)
 - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887)
 - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888)
 - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918)
 - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912)
 - Fix the Makefile (OCamlPro/alt-ergo#914)
 - Add `Logs` dependency (OCamlPro/alt-ergo#1206)
 - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199)
 - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200)
 - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223)

### Testing

 - Use --enable-assertions in tests (OCamlPro/alt-ergo#809)
 - Add a test for push/pop (OCamlPro/alt-ergo#843)
 - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938)
 - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939)
 - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941)

### Documentation

 - Add a new example for model generation (OCamlPro/alt-ergo#826)
 - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862)
 - Update the current authors (OCamlPro/alt-ergo#865)
 - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871)
 - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915)
 - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995)
 - Document Windows support (OCamlPro/alt-ergo#1216)
 - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217)
 - Document optimization feature (OCamlPro/alt-ergo#1231)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Halbaroth Halbaroth Halbaroth approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
2.6.0
Development

Successfully merging this pull request may close these issues.
2 participants
@bclement-ocp @Halbaroth