We are pleased to announce a new release of Alt-Ergo!
Alt-Ergo 2.4.0 is now available from Alt-Ergo’s website. An associated opam package will be published in the next few days.
This release contains some major novelties:
- Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard.
- We switched command line parsing to use cmdliner. You will need to use – instead of -. Some options have also been renamed, see the manpage or the documentation.
- We improved the online documentation of your solver, available here.
This release also contains some minor novelties:
- .mlw and .why extension are depreciated, the use of .ae extension is advised.
- Add --input (resp --output) option to manually set the input (resp output) file format
- Add --pretty-output option to add better debug formatting and to add colors
- Add exponentiation operation, ** in native Alt-Ergo syntax. The operator is fully interpreted when applied to constants
- Fix --steps-count and improve the way steps are counted (AdaCore contribution)
- Add --instantiation-heuristic option that can enable lighter or heavier instantiation
- Reduce the instantiation context (considered foralls / exists) in CDCL-Tableaux to better mimic the Tableaux-like SAT solver
- Multiple bugfixes
The full list of changes is available here. As usual, do not hesitate to report bugs, to ask questions, or to give your feedback!
The Alt-Ergo team – OCamlPro