Merge pull request #780 from Halbaroth/disable-preludes

Use --enable-theories fpa to active the FPA builtin theory

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 @@ precisely, Alt-Ergo implements the second and third layers from the paper "[A
 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

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

src/lib/util/options.ml

@@ -285,6 +285,7 @@ let set_input_format f = input_format := f
 let set_infer_input_format b = infer_input_format := b
 let set_parse_only b = parse_only := b
 let set_preludes p = preludes := p
+
 let set_theory_preludes t = theory_preludes := t
 let set_type_only b = type_only := b
 let set_type_smt2 b = type_smt2 := b

src/lib/util/theories.ml

@@ -43,9 +43,11 @@ let all_preludes = [ Fpa; Ria; Nra ]
 
 let all = ADT :: AC :: List.map (fun p -> Prelude p) all_preludes
 
-let default_preludes = all_preludes
+(* By default we disable Fpa, Ria and Nra preludes to prevent
+   regressions. *)
+let default_preludes = []
 
-let default = all
+let default = [ ADT; AC ]
 
 let preludes =
   List.filter_map (function | Prelude p -> Some p | _ -> None)