this repo has no description

[new release] alt-ergo (4 packages) (2.6.0)

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)

Changed files
+232
packages
alt-ergo
alt-ergo.2.6.0
alt-ergo-lib
alt-ergo-lib.2.6.0
alt-ergo-parsers
alt-ergo-parsers.2.6.0
alt-ergo-plugin-ab-why3
alt-ergo-plugin-ab-why3.2.6.0
+70
packages/alt-ergo-lib/alt-ergo-lib.2.6.0/opam
···
···
+
opam-version: "2.0"
+
synopsis: "The Alt-Ergo SMT prover library"
+
description: """
+
This is the core library used in the Alt-Ergo SMT solver.
+
+
Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
+
+
See more details on http://alt-ergo.ocamlpro.com/"""
+
maintainer: ["Alt-Ergo developers <alt-ergo@ocamlpro.com>"]
+
authors: ["Alt-Ergo developers <alt-ergo@ocamlpro.com>"]
+
homepage: "https://alt-ergo.ocamlpro.com/"
+
doc: "https://ocamlpro.github.io/alt-ergo"
+
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
+
depends: [
+
"ocaml" {>= "4.08.1"}
+
"dune" {>= "3.14"}
+
"dune-build-info"
+
"dolmen" {>= "0.10"}
+
"dolmen_type" {>= "0.10"}
+
"dolmen_loop" {>= "0.10"}
+
"ocplib-simplex" {>= "0.5.1"}
+
"zarith" {>= "1.11"}
+
"seq"
+
"fmt" {>= "0.9.0"}
+
"stdlib-shims"
+
"ppx_blob" {>= "0.7.2"}
+
"ppx_deriving"
+
"camlzip" {>= "1.07"}
+
"odoc" {with-doc}
+
"ppx_deriving"
+
"qcheck" {with-test}
+
]
+
conflicts: [
+
"ppxlib" {< "0.30.0"}
+
"result" {< "1.5"}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
+
# This part comes from the template. Please edit alt-ergo-lib.opam.template
+
# and not alt-ergo-lib.opam which is generated by dune
+
tags: "org:OCamlPro"
+
+
license: [
+
"LicenseRef-OCamlpro-Non-Commercial"
+
"Apache-2.0"
+
]
+
url {
+
src:
+
"https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.0/alt-ergo-2.6.0.tbz"
+
checksum: [
+
"sha256=1269311af25278a466892ba878cc888ba59f177f53dd03f12a2c623b03fcf37e"
+
"sha512=8a841e1f295e889fa9cb95aa4021bbb481d73279e99512c2afb3510e1f6c9d367113ee6bd3a90bc51111fa3e766a302633e9d5d18fde7660b139cd19a271eb23"
+
]
+
}
+
x-commit-hash: "af8193ed37e039010ed60486ac88bbbfbdec9614"
+56
packages/alt-ergo-parsers/alt-ergo-parsers.2.6.0/opam
···
···
+
opam-version: "2.0"
+
synopsis: "The Alt-Ergo SMT prover parser library"
+
description: """
+
This is the parser library used in the Alt-Ergo SMT solver.
+
+
Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
+
+
See more details on http://alt-ergo.ocamlpro.com/"""
+
maintainer: ["Alt-Ergo developers <alt-ergo@ocamlpro.com>"]
+
authors: ["Alt-Ergo developers <alt-ergo@ocamlpro.com>"]
+
homepage: "https://alt-ergo.ocamlpro.com/"
+
doc: "https://ocamlpro.github.io/alt-ergo"
+
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
+
depends: [
+
"ocaml" {>= "4.08.1"}
+
"dune" {>= "3.14"}
+
"alt-ergo-lib" {= version}
+
"psmt2-frontend" {>= "0.4"}
+
"menhir"
+
"stdlib-shims"
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
+
# This part comes from the template. Please edit alt-ergo-parsers.opam.template
+
# and not alt-ergo-parsers.opam which is generated by dune
+
tags: "org:OCamlPro"
+
+
license: [
+
"LicenseRef-OCamlpro-Non-Commercial"
+
"Apache-2.0"
+
]
+
url {
+
src:
+
"https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.0/alt-ergo-2.6.0.tbz"
+
checksum: [
+
"sha256=1269311af25278a466892ba878cc888ba59f177f53dd03f12a2c623b03fcf37e"
+
"sha512=8a841e1f295e889fa9cb95aa4021bbb481d73279e99512c2afb3510e1f6c9d367113ee6bd3a90bc51111fa3e766a302633e9d5d18fde7660b139cd19a271eb23"
+
]
+
}
+
x-commit-hash: "af8193ed37e039010ed60486ac88bbbfbdec9614"
+51
packages/alt-ergo-plugin-ab-why3/alt-ergo-plugin-ab-why3.2.6.0/opam
···
···
+
opam-version: "2.0"
+
synopsis: "An experimental Why3 frontend for Alt-Ergo"
+
description: """
+
An experimental front-end that parses a subset of Why3's logic. More
+
precisely, this front-end targets proof obligations generated by the
+
Atelier-B framework in Why3 format. It should be used with a prelude
+
defining the B Set theory."""
+
maintainer: ["Alt-Ergo developers <alt-ergo@ocamlpro.com>"]
+
authors: ["Alt-Ergo developers <alt-ergo@ocamlpro.com>"]
+
license: "LGPL-2.1-only"
+
homepage: "https://alt-ergo.ocamlpro.com/"
+
doc: "https://ocamlpro.github.io/alt-ergo"
+
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
+
depends: [
+
"dune" {>= "3.14"}
+
"alt-ergo" {= version}
+
"alt-ergo-lib" {= version}
+
"alt-ergo-parsers" {= version}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
+
# This part comes from the template. Please edit
+
# alt-ergo-plugin-ab-why3.opam.template and not alt-ergo-plugin-ab-why3.opam
+
# which is generated by dune
+
+
conflicts: [ "opam-option-bytecode-only" ]
+
url {
+
src:
+
"https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.0/alt-ergo-2.6.0.tbz"
+
checksum: [
+
"sha256=1269311af25278a466892ba878cc888ba59f177f53dd03f12a2c623b03fcf37e"
+
"sha512=8a841e1f295e889fa9cb95aa4021bbb481d73279e99512c2afb3510e1f6c9d367113ee6bd3a90bc51111fa3e766a302633e9d5d18fde7660b139cd19a271eb23"
+
]
+
}
+
x-commit-hash: "af8193ed37e039010ed60486ac88bbbfbdec9614"
+55
packages/alt-ergo/alt-ergo.2.6.0/opam
···
···
+
opam-version: "2.0"
+
synopsis: "The Alt-Ergo SMT prover"
+
description: """
+
Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
+
+
See more details on https://alt-ergo.ocamlpro.com/"""
+
maintainer: ["Alt-Ergo developers <alt-ergo@ocamlpro.com>"]
+
authors: ["Alt-Ergo developers <alt-ergo@ocamlpro.com>"]
+
homepage: "https://alt-ergo.ocamlpro.com/"
+
doc: "https://ocamlpro.github.io/alt-ergo"
+
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
+
depends: [
+
"ocaml" {>= "4.08.1"}
+
"dune" {>= "3.14"}
+
"alt-ergo-lib" {= version}
+
"alt-ergo-parsers" {= version}
+
"menhir"
+
"dune-site"
+
"cmdliner" {>= "1.1.0"}
+
"odoc" {with-doc}
+
]
+
build: [
+
["dune" "subst"] {dev}
+
[
+
"dune"
+
"build"
+
"-p"
+
name
+
"-j"
+
jobs
+
"--promote-install-files=false"
+
"@install"
+
"@runtest" {with-test}
+
"@doc" {with-doc}
+
]
+
["dune" "install" "-p" name "--create-install-files" name]
+
]
+
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
+
# This part comes from the template. Please edit alt-ergo.opam.template
+
# and not alt-ergo.opam which is generated by dune
+
tags: "org:OCamlPro"
+
+
license: [
+
"LicenseRef-OCamlpro-Non-Commercial"
+
"Apache-2.0"
+
]
+
url {
+
src:
+
"https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.0/alt-ergo-2.6.0.tbz"
+
checksum: [
+
"sha256=1269311af25278a466892ba878cc888ba59f177f53dd03f12a2c623b03fcf37e"
+
"sha512=8a841e1f295e889fa9cb95aa4021bbb481d73279e99512c2afb3510e1f6c9d367113ee6bd3a90bc51111fa3e766a302633e9d5d18fde7660b139cd19a271eb23"
+
]
+
}
+
x-commit-hash: "af8193ed37e039010ed60486ac88bbbfbdec9614"