From 30afd8b5626bb0f375685336b0bf0b343d1eceda Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Tue, 24 Sep 2024 13:27:01 +0200 Subject: [PATCH] [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) --- packages/alt-ergo-lib/alt-ergo-lib.2.6.0/opam | 70 +++++++++++++++++++ .../alt-ergo-parsers.2.6.0/opam | 56 +++++++++++++++ .../alt-ergo-plugin-ab-why3.2.6.0/opam | 51 ++++++++++++++ packages/alt-ergo/alt-ergo.2.6.0/opam | 55 +++++++++++++++ 4 files changed, 232 insertions(+) create mode 100644 packages/alt-ergo-lib/alt-ergo-lib.2.6.0/opam create mode 100644 packages/alt-ergo-parsers/alt-ergo-parsers.2.6.0/opam create mode 100644 packages/alt-ergo-plugin-ab-why3/alt-ergo-plugin-ab-why3.2.6.0/opam create mode 100644 packages/alt-ergo/alt-ergo.2.6.0/opam diff --git a/packages/alt-ergo-lib/alt-ergo-lib.2.6.0/opam b/packages/alt-ergo-lib/alt-ergo-lib.2.6.0/opam new file mode 100644 index 000000000000..9ee32cda575e --- /dev/null +++ b/packages/alt-ergo-lib/alt-ergo-lib.2.6.0/opam @@ -0,0 +1,70 @@ +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 "] +authors: ["Alt-Ergo developers "] +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" diff --git a/packages/alt-ergo-parsers/alt-ergo-parsers.2.6.0/opam b/packages/alt-ergo-parsers/alt-ergo-parsers.2.6.0/opam new file mode 100644 index 000000000000..e6509e7d5a45 --- /dev/null +++ b/packages/alt-ergo-parsers/alt-ergo-parsers.2.6.0/opam @@ -0,0 +1,56 @@ +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 "] +authors: ["Alt-Ergo developers "] +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" diff --git a/packages/alt-ergo-plugin-ab-why3/alt-ergo-plugin-ab-why3.2.6.0/opam b/packages/alt-ergo-plugin-ab-why3/alt-ergo-plugin-ab-why3.2.6.0/opam new file mode 100644 index 000000000000..d0b4b96a7d62 --- /dev/null +++ b/packages/alt-ergo-plugin-ab-why3/alt-ergo-plugin-ab-why3.2.6.0/opam @@ -0,0 +1,51 @@ +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 "] +authors: ["Alt-Ergo developers "] +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" diff --git a/packages/alt-ergo/alt-ergo.2.6.0/opam b/packages/alt-ergo/alt-ergo.2.6.0/opam new file mode 100644 index 000000000000..cb0c6444d0cb --- /dev/null +++ b/packages/alt-ergo/alt-ergo.2.6.0/opam @@ -0,0 +1,55 @@ +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 "] +authors: ["Alt-Ergo developers "] +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"