Backporting 2.5.0 bis

.github/workflows/build.yml

@@ -48,9 +48,6 @@ jobs:
       - name: Build alt-ergo with opam
         run: opam exec -- opam reinstall .
 
-      - name: Generate tests
-        run: opam exec -- make gentest
-
       - name: Run tests
         run: opam exec -- make runtest-ci
 

Makefile

@@ -118,7 +118,7 @@ packages:
 # Generate new Dune tests from the problems in
 # the directory tests/.
 gentest: $(wildcard tests/**/*)
-	dune exec -- tools/gentest.exe tests/
+	dune build @tests/gentest --auto-promote
 
 # Run non-regression tests.
 runtest: gentest bin
@@ -234,6 +234,12 @@ archi: $(EXTRA_DIR)/ocamldot/ocamldot
 	echo "}" >> archi.dot
 	dot -Tpdf archi.dot > archi.pdf
 
+lock:
+	dune build ./alt-ergo-lib.opam
+	opam lock ./alt-ergo-lib.opam -w
+	# Remove OCaml compiler constraints
+	sed -i '/"ocaml"\|"ocaml-base-compiler"\|"ocaml-system"\|"ocaml-config"/d' ./alt-ergo-lib.opam.locked
+
 dev-switch:
 	opam switch create -y . --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers
 
@@ -250,7 +256,7 @@ test-deps:
 dune-deps:
 	dune-deps . | dot -Tpng -o docs/deps.png
 
-.PHONY: archi deps test-deps dune-deps dev-switch
+.PHONY: archi deps test-deps dune-deps dev-switch lock
 
 # ===============
 # PUBLIC RELEASES

alt-ergo-lib.opam.locked

@@ -0,0 +1,81 @@
+opam-version: "2.0"
+name: "alt-ergo-lib"
+version: "dev"
+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"
+license: ["LicenseRef-OCamlpro-Non-Commercial" "Apache-2.0"]
+tags: "org:OCamlPro"
+homepage: "https://alt-ergo.ocamlpro.com/"
+doc: "https://ocamlpro.github.io/alt-ergo"
+bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
+depends: [
+  "base-bigarray" {= "base"}
+  "base-bytes" {= "base"}
+  "base-threads" {= "base"}
+  "base-unix" {= "base"}
+  "camlzip" {= "1.11"}
+  "cmdliner" {= "1.2.0"}
+  "conf-gmp" {= "4"}
+  "conf-pkg-config" {= "3"}
+  "conf-zlib" {= "1"}
+  "cppo" {= "1.6.9"}
+  "csexp" {= "1.5.2"}
+  "dolmen" {= "0.9"}
+  "dolmen_loop" {= "0.9"}
+  "dolmen_type" {= "0.9"}
+  "dune" {= "3.10.0"}
+  "dune-build-info" {= "3.10.0"}
+  "dune-configurator" {= "3.10.0"}
+  "fmt" {= "0.9.0"}
+  "gen" {= "1.1"}
+  "js_of_ocaml" {= "5.4.0"}
+  "js_of_ocaml-compiler" {= "5.4.0"}
+  "logs" {= "0.7.0"}
+  "lwt" {= "5.6.1"}
+  "menhir" {= "20230608"}
+  "menhirLib" {= "20230608"}
+  "menhirSdk" {= "20230608"}
+  "num" {= "1.4"}
+  "ocaml-compiler-libs" {= "v0.12.4"}
+  "ocamlbuild" {= "0.14.2"}
+  "ocamlfind" {= "1.9.6"}
+  "ocplib-endian" {= "1.2"}
+  "ocplib-simplex" {= "0.5"}
+  "pp_loc" {= "2.1.0"}
+  "ppx_blob" {= "0.7.2"}
+  "ppx_derivers" {= "1.2.1"}
+  "ppxlib" {= "0.30.0"}
+  "sedlex" {= "3.2"}
+  "seq" {= "base"}
+  "sexplib0" {= "v0.15.1"}
+  "spelll" {= "0.4"}
+  "stdlib-shims" {= "0.3.0"}
+  "topkg" {= "1.0.7"}
+  "uutf" {= "1.0.3"}
+  "yojson" {= "2.1.0"}
+  "zarith" {= "1.13"}
+]
+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"

docs/sphinx_docs/Input_file_formats/Native/05_theories.md

@@ -1,4 +1,4 @@
- 
+
 # Theories
 
 Alt-Ergo has built-in support for many different theories.
@@ -44,10 +44,11 @@
 Three-tier Strategy for Reasoning about Floating-Point Numbers in
 SMT](https://inria.hal.science/hal-01522770)" by Conchon et al.
 
-*Note*: Support for floating-point arithmetic is enabled by default in
-Alt-Ergo since version 2.5.0.  Previous versions required the use of command
-line flags `--use-fpa` and `--prelude fpa-theory-2019-10-08-19h00.ae` to enable
-it.
+*Note*: Support for floating-point arithmetic is available as a built-in theory
+since version 2.5.0. It is enabled using flag `--enable-theory fpa`, which will
+become the default in a future release. Previous versions used the external
+prelude mechanism and required command line flags `--use-fpa` and
+`--prelude fpa-theory-2019-10-08-19h00.ae`.
 
 This means that Alt-Ergo doesn't actually support a floating-point type (that
 may come in a future release); instead, it supports a rounding function, as
@@ -63,7 +64,7 @@
 
 The rounding function is available as a builtin function called `float`:
 
 ```alt-ergo
 type fpa_rounding_mode =
   | NearestTiesToEven
     (** To nearest, tie breaking to even mantissa *)
@@ -92,7 +93,7 @@
 Alt-Ergo also exposes convenience functions specialized for standard
 floating-point types:
 
 ```alt-ergo
 function float32(m: fpa_rounding_mode, x: real): real = float(24, 149, m, x)
 function float32d(x: real): real = float32(NearestTiesToEven, x)
 function float64(m: fpa_rounding_mode, x: real): real = float(53, 1074, m, x)
@@ -105,13 +106,13 @@
 Finally, the `integer_round` function allows rounding a real to an integer
 using the aforementioned rounding modes:
 
 ```alt-ergo
 logic integer_round : fpa_rounding_mode, real -> int
 ```
 
 Here is an example:
 
 ```alt-ergo
 goal g: integer_round(ToZero, 2.1) = 2
 ```
 

examples/dune

@@ -0,0 +1,16 @@
+(executable
+ (name Lib_usage)
+ (libraries AltErgoLib)
+ (modules Lib_usage)
+)
+
+(rule
+ (alias runtest)
+ (action
+  (ignore-stdout
+   (ignore-stderr
+    (run ./Lib_usage.exe)
+   )
+  )
+ )
+)

examples/lib_usage.ml

@@ -65,7 +65,7 @@ open AltErgoLib
 
 module PA = Parsed_interface
 
-let x = PA.mk_var_type Loc.dummy "'a"
+let _x = PA.mk_var_type Loc.dummy "'a"
 
 let one = PA.mk_int_const Loc.dummy "1"
 let two = PA.mk_int_const Loc.dummy "2"
@@ -80,7 +80,7 @@ let goal_3 = PA.mk_goal Loc.dummy "toy_3" (PA.mk_not Loc.dummy eq1)
 
 let parsed = [goal_1; goal_2; goal_3]
 
-let typed, env = Typechecker.type_file parsed
+let typed, _env = Typechecker.type_file parsed
 
 let pbs = Typechecker.split_goals_and_cnf typed
 
@@ -89,16 +89,19 @@ module FE = Frontend.Make(SAT)
 
 let () =
   List.iter
-    (fun (pb, goal_name) ->
+    (fun (pb, _goal_name) ->
        let ctxt = FE.init_all_used_context () in
-       let acc0 = SAT.empty (), true, Explanation.empty in
+       let acc0 = SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty in
        let s = Stack.create () in
-       let _, consistent, ex =
+       let _env, consistent, _ex =
          List.fold_left
            (fun acc d ->
               FE.process_decl (fun _ _ -> ()) ctxt s acc d
-           )acc0 pb
+           ) acc0 pb
        in
-       Format.printf "%s@."
-         (if consistent then "unknown" else "unsat")
+       match consistent with
+       | `Sat _ | `Unknown _ ->
+         Format.printf "unknown"
+       | `Unsat ->
+         Format.printf "unsat"
     )pbs

src/bin/common/parse_command.ml

@@ -673,8 +673,9 @@ let parse_execution_opt =
             else if Compat.String.starts_with ~prefix:"fpa-theory" p then
               Printer.print_wrn ~header:true
                 "@[Support for the FPA theory has been integrated as a builtin \
-                 theory prelude in version 2.5.0 and is enabled by default. \
-                 This option is no longer needed, and the '%s'@ prelude will \
+                 theory prelude in version 2.5.0. Please use \
+                 `--enable-theories fpa` to enable it. \
+                 This option and the '%s'@ prelude will \
                  be removed in a later version.@]" p
           end;
 
@@ -1326,7 +1327,7 @@ let parse_theory_opt =
 
   let use_fpa =
     let doc = "Floating-point builtins are always enabled and this option has
-    no effect anymore. It will be removed in a future version." in
+      no effect anymore. It will be removed in a future version." in
     let deprecated = "this option is always enabled" in
     Arg.(value & flag & info ["use-fpa"] ~docs ~doc ~deprecated) in
 
@@ -1388,14 +1389,27 @@ let parse_theory_opt =
     let preludes enable_theories disable_theories =
       let theories = Theories.default in
       let rec aux th en dis =
-        match en, dis with
-        | _ :: _, [] -> aux (List.rev_append en th) [] []
-        | e :: _, d :: _ when e = d ->
-          Fmt.error_msg "theory prelude '%a' cannot be both enabled and
-          disabled" Theories.pp e
-        | e :: en, d :: _ when e < d -> aux (e :: th) en dis
-        | _ , d :: dis -> aux (List.filter ((<>) d) th) en dis
-        | [], [] -> Ok th
+        let theories =
+          match en, dis with
+          | _ :: _, [] -> aux (List.rev_append en th) [] []
+          | e :: _, d :: _ when e = d ->
+            Fmt.error_msg "theory prelude '%a' cannot be both enabled and
+            disabled" Theories.pp e
+          | e :: en, d :: _ when e < d -> aux (e :: th) en dis
+          | _ , d :: dis -> aux (List.filter ((<>) d) th) en dis
+          | [], [] -> Ok th
+        in
+        Result.bind theories @@ fun theories ->
+        if List.mem Theories.(Prelude Fpa) en then
+          if List.for_all (fun th ->
+              match (th : Theories.t) with
+              | Prelude Nra | Prelude Ria -> false
+              | _ -> true
+            ) dis then
+            Ok Theories.(Prelude Nra :: Prelude Ria :: theories)
+          else
+            Fmt.error_msg "theory prelude fpa requires both ria and nra"
+        else Ok th
       in
       aux
         theories
@@ -1436,16 +1450,18 @@ let parse_fmt_opt =
           models and unsat cores. Possible values are %s."
         (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
     in
-    let deprecated = "this option is deprecated. Please use --std-output." in
-    let std_output =
-      Arg.(value & opt (some' string) None & info ["std-output"] ~docs
+    let deprecated =
+      "this option is deprecated. Please use --regular-output."
+    in
+    let regular_output =
+      Arg.(value & opt (some' string) None & info ["regular-output"] ~docs
              ~doc ~docv)
     in
     let std_formatter =
       Arg.(value & opt (some' string) None  & info ["std-formatter"]
              ~deprecated ~docs ~docv)
     in
-    Term.(const (merge_formatters "stdout") $ std_output $ std_formatter)
+    Term.(const (merge_formatters "stdout") $ regular_output $ std_formatter)
   in
 
   let err_output =
@@ -1455,16 +1471,18 @@ let parse_fmt_opt =
          warning informations. Possible values are %s."
         (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
     in
-    let deprecated = "this option is deprecated. Please use --err-output." in
-    let err_output =
-      Arg.(value & opt (some' string) None & info ["err-output"] ~docs
+    let deprecated =
+      "this option is deprecated. Please use --diagnostic-output."
+    in
+    let diagnostic_output =
+      Arg.(value & opt (some' string) None & info ["diagnostic-output"] ~docs
              ~doc ~docv)
     in
     let err_formatter =
       Arg.(value & opt (some' string) None & info ["err-formatter"]
              ~deprecated ~docs ~docv)
     in
-    Term.(const (merge_formatters "stderr") $ err_output $ err_formatter)
+    Term.(const (merge_formatters "stderr") $ diagnostic_output $ err_formatter)
   in
 
   Term.(ret (const mk_output_channel_opt $ std_output $ err_output))

src/bin/common/solving_loop.ml

@@ -81,10 +81,10 @@ let main () =
           Options.Time.set_timeout (Options.get_timelimit ());
         end;
       SAT.reset_refs ();
-      let partial_model, consistent, _ =
+      let _, consistent, _ =
         List.fold_left
           (FE.process_decl FE.print_status used_context consistent_dep_stack)
-          (SAT.empty (), true, Explanation.empty) cnf
+          (SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty) cnf
       in
       if Options.get_timelimit_per_goal() then
         Options.Time.unset_timeout ();
@@ -96,9 +96,10 @@ let main () =
       (* If the status of the SAT environment is inconsistent,
          we have to drop the partial model in order to prevent
          printing wrong model. *)
-      if consistent then
+      match consistent with
+      | `Sat partial_model | `Unknown partial_model ->
         Some partial_model
-      else None
+      | `Unsat -> None
     with Util.Timeout ->
       if not (Options.get_timelimit_per_goal()) then exit 142;
       None

src/bin/js/worker_js.ml

@@ -130,11 +130,12 @@ let main worker_id content =
       let used_context = FE.choose_used_context all_context ~goal_name in
       let consistent_dep_stack = Stack.create () in
       SAT.reset_refs ();
+      let env = SAT.empty_with_inst add_inst in
       let _,_,dep =
         List.fold_left
           (FE.process_decl
              get_status_and_print used_context consistent_dep_stack)
-          (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in
+          (env, `Unknown env, Explanation.empty) cnf in
 
       if Options.get_unsat_core () then begin
         unsat_core := Explanation.get_unsat_core dep;