Remove deprecated cli options and preludes (#1265)

* Remove deprecated options and preludes

These features have been deprecated in v2.6.0.

src/bin/common/parse_command.ml

@@ -149,7 +149,6 @@ module Debug = struct
     | Arith
     | Arrays
     | Bitv
-    | Sum
     | Ite
     | Cc
     | Combine
@@ -165,20 +164,18 @@ module Debug = struct
     | Split
     | Triggers
     | Types
-    | Typing
     | Uf
     | Unsat_core
     | Use
-    | Warnings
     | Commands
     | Optimize
   [@@deriving eq]
 
   let all = [
-    Debug; Ac; Adt; Arith; Arrays; Bitv; Sum; Ite;
+    Debug; Ac; Adt; Arith; Arrays; Bitv; Ite;
     Cc; Combine; Constr; Explanations; Fm; Fpa; Gc;
     Interpretation; Intervals; Matching; Sat; Split; Triggers;
-    Types; Typing; Uf; Unsat_core; Use; Warnings;
+    Types; Uf; Unsat_core; Use;
     Commands; Optimize
   ]
 
@@ -189,7 +186,6 @@ module Debug = struct
     | Arith -> "arith"
     | Arrays -> "arrays"
     | Bitv -> "bitv"
-    | Sum -> "sum"
     | Ite -> "ite"
     | Cc -> "cc"
     | Combine -> "combine"
@@ -205,11 +201,9 @@ module Debug = struct
     | Split -> "split"
     | Triggers -> "triggers"
     | Types -> "types"
-    | Typing -> "typing"
     | Uf -> "uf"
     | Unsat_core -> "unsat-core"
     | Use -> "use"
-    | Warnings -> "warnings"
     | Commands -> "commands"
     | Optimize -> "optimize"
 
@@ -238,14 +232,6 @@ module Debug = struct
         | Bitv ->
           Options.set_debug_bitv true;
           set_level Bitv.src
-        | Sum ->
-          Printer.print_wrn
-            "The debug flag 'sum' is deprecated and is replaced by 'adt'. \
-             It has the same effect as 'adt' and will be removed in a future \
-             version.";
-          Options.set_debug_adt true;
-          set_level Adt.src;
-          set_level Adt_rel.src
         | Ite ->
           Options.set_debug_ite true;
           set_level Ite_rel.src
@@ -290,10 +276,6 @@ module Debug = struct
         | Types ->
           Options.set_debug_types true;
           set_level S.types
-        | Typing ->
-          Printer.print_wrn
-            "The debug flag 'typing' has no effect. It will be removed in a \
-             future version."
         | Uf ->
           Options.set_debug_uf true;
           set_level Uf.src
@@ -303,11 +285,6 @@ module Debug = struct
         | Use ->
           Options.set_debug_use true;
           set_level Use.src
-        | Warnings ->
-          Printer.print_wrn
-            "The debug flag 'warning' is deprecated and will be removed in a \
-             future version.";
-          Options.set_debug_warnings true
         | Commands ->
           Options.set_debug_commands true;
           set_level Commands.src
@@ -442,7 +419,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
     `Ok()
 
 let mk_output_opt
-    interpretation use_underscore objectives_in_interpretation unsat_core
+    interpretation objectives_in_interpretation unsat_core
     output_format model_type () () () ()
   =
   set_infer_output_format (Option.is_none output_format);
@@ -455,7 +432,6 @@ let mk_output_opt
     | Some v -> v
   in
   set_interpretation interpretation;
-  set_interpretation_use_underscore use_underscore;
   set_objectives_in_interpretation objectives_in_interpretation;
   set_unsat_core unsat_core;
   set_output_format output_format;
@@ -529,7 +505,7 @@ let mk_term_opt disable_ites inline_lets rewriting no_term_like_pp
 
 let mk_theory_opt () no_contracongru
     no_fm no_nla no_tcp no_theory restricted tighten_vars
-    _use_fpa (theories)
+    (theories)
   =
   set_no_ac (not (List.exists (Theories.equal Theories.AC) theories));
   set_no_fm no_fm;
@@ -750,25 +726,10 @@ let parse_execution_opt =
       else
         match Config.lookup_prelude p with
         | Some p' ->
-          begin if Compat.String.starts_with ~prefix:"b-set-theory" p then
-              Printer.print_wrn ~header:true
-                "Support for the B set theory is deprecated since version \
-                 2.5.0 and may be removed in a future version. If you are \
-                 actively using it, please make yourself known to the Alt-Ergo \
-                 developers by writing to <[email protected]>."
-            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 and the '%s'@ prelude will \ be removed in a \
-                 later version.@]" p
-          end;
-
           Ok p'
         | None ->
           Error (
-            Format.asprintf
+            Fmt.str
               "cannot load prelude '%s': no such file"
               p)
     in
@@ -1121,17 +1082,6 @@ let parse_output_opt =
     Term.term_result' term
   in
 
-  let use_underscore =
-    let doc = "Output \"_\" instead of fresh value in interpretation" in
-    let deprecated =
-      "this option will be removed as it does not produce a \
-       SMTLIB-compliant output."
-    in
-    let docv = "VAL" in
-    Arg.(value & flag & info
-           ["interpretation-use-underscore";"use-underscore"]
-           ~docv ~docs:s_models ~doc ~deprecated)
-  in
   let objectives_in_interpretation =
     let doc = " inline pretty-printing of optimized expressions in the \
                model instead of a dedicated section '(objectives \
@@ -1190,7 +1140,7 @@ let parse_output_opt =
   in
 
   Term.(ret (const mk_output_opt $
-             interpretation $ use_underscore $
+             interpretation $
              objectives_in_interpretation $ unsat_core $
              output_format $ model_type $
              set_dump_models $ set_dump_models_on $
@@ -1444,12 +1394,6 @@ let parse_theory_opt =
     let doc = "Compute the best bounds for arithmetic variables." in
     Arg.(value & flag & info ["tighten-vars"] ~docs ~doc) in
 
-  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
-    let deprecated = "this option is always enabled" in
-    Arg.(value & flag & info ["use-fpa"] ~docs ~doc ~deprecated) in
-
   let theories =
     let theory_enum =
       Theories.all
@@ -1476,34 +1420,12 @@ let parse_theory_opt =
           (Arg.doc_alts_enum theory_enum)
       in
       let docv = "THEORY" in
-      let disable_theories =
-        Term.(const List.concat $
-              Arg.(
-                value
-                & opt_all (list theory) []
-                & info ["disable-theory"; "disable-theories"] ~docs ~doc ~docv
-              ))
-      in
-      let disable_adts =
-        let doc = "Disable Algebraic Datatypes theory. Deprecated alias for
-        `--disable-theories adt`." in
-        let deprecated = "use `--disable-theories ac` instead." in
-        Arg.(value & flag & info ["disable-adts"] ~docs ~doc ~deprecated)
-      in
-      let no_ac =
-        let doc = "Disable the AC theory of Associative and \
-                   Commutative function symbols. Deprecated alias for
-                  `--disable-theories ac`." in
-        let deprecated = "use `--disable-theories ac` instead" in
-        Arg.(value & flag & info ["no-ac"] ~docs ~doc ~deprecated)
-      in
-      let mk_disable_theories disable_theories disable_adts no_ac =
-        let open Theories in
-        (if disable_adts then [ ADT ] else []) @
-        (if no_ac then [ AC ] else []) @
-        disable_theories
-      in
-      Term.(const mk_disable_theories $ disable_theories $ disable_adts $ no_ac)
+      Term.(const List.concat $
+            Arg.(
+              value
+              & opt_all (list theory) []
+              & info ["disable-theory"; "disable-theories"] ~docs ~doc ~docv
+            ))
     in
     let preludes enable_theories disable_theories =
       let theories = Theories.Set.of_list Theories.default in
@@ -1535,7 +1457,7 @@ let parse_theory_opt =
   Term.(ret (const mk_theory_opt $
              inequalities_plugin $ no_contracongru $
              no_fm $ no_nla $ no_tcp $ no_theory $ restricted $
-             tighten_vars $ use_fpa $ theories
+             tighten_vars $ theories
             )
        )
 

src/bin/js/options_interface.ml

@@ -113,7 +113,6 @@ let set_options r =
   set_options_opt Options.set_debug_uf r.debug_uf;
   set_options_opt Options.set_debug_unsat_core r.debug_unsat_core;
   set_options_opt Options.set_debug_use r.debug_use;
-  set_options_opt Options.set_debug_warnings r.debug_warnings;
   set_options_opt Options.set_rule r.rule;
 
   set_options_opt Options.set_case_split_policy

src/bin/js/worker_interface.ml

@@ -181,7 +181,6 @@ type options = {
   debug_uf : bool option;
   debug_unsat_core : bool option;
   debug_use : bool option;
-  debug_warnings : bool option;
   rule : int option;
 
   case_split_policy : case_split_policy option;
@@ -281,7 +280,6 @@ let init_options () = {
   debug_uf = None;
   debug_unsat_core = None;
   debug_use = None;
-  debug_warnings = None;
   rule = None;
 
   case_split_policy = None;
@@ -395,12 +393,11 @@ let opt_dbg3_encoding =
   conv
     (fun dbg3 -> dbg3)
     (fun dbg3 -> dbg3)
-    (obj5
+    (obj4
        (opt "debug_types" bool)
        (opt "debug_uf" bool)
        (opt "debug_unsat_core" bool)
        (opt "debug_use" bool)
-       (opt "debug_warnings" bool)
     )
 
 let opt1_encoding =
@@ -551,8 +548,7 @@ let options_to_json opt =
     (opt.debug_types,
      opt.debug_uf,
      opt.debug_unsat_core,
-     opt.debug_use,
-     opt.debug_warnings)
+     opt.debug_use)
   in
   let all_opt1 =
     (opt.rule,
@@ -677,8 +673,7 @@ let options_from_json options =
     let (debug_types,
          debug_uf,
          debug_unsat_core,
-         debug_use,
-         debug_warnings) = dbg_opt3 in
+         debug_use) = dbg_opt3 in
     let (rule,
          case_split_policy,
          enable_adts_cs,
@@ -762,7 +757,6 @@ let options_from_json options =
       debug_uf;
       debug_unsat_core;
       debug_use;
-      debug_warnings;
       rule;
       case_split_policy;
       enable_adts_cs;

src/bin/js/worker_interface.mli

@@ -78,7 +78,6 @@ type options = {
   debug_uf : bool option;
   debug_unsat_core : bool option;
   debug_use : bool option;
-  debug_warnings : bool option;
   rule : int option;
 
   case_split_policy : case_split_policy option;

src/lib/structures/expr.ml

@@ -1146,8 +1146,7 @@ let mk_forall_ter =
         let q = match form_view lem with Lemma q -> q | _ -> assert false in
         assert (equal q.main f (* should be true *));
         if compare_quant q new_q <> 0 then raise Exit;
-        Printer.print_wrn ~warning:(Options.get_debug_warnings ())
-          "(sub) axiom %s replaced with %s" name q.name;
+        Printer.print_wrn "(sub) axiom %s replaced with %s" name q.name;
         lem
       with Not_found | Exit ->
         let d = new_q.main.depth in (* + 1 ?? *)

src/lib/util/options.ml

@@ -175,7 +175,6 @@ let debug_types = ref false
 let debug_uf = ref false
 let debug_unsat_core = ref false
 let debug_use = ref false
-let debug_warnings = ref false
 let debug_commands = ref false
 let debug_optimize = ref false
 let rule = ref (-1)
@@ -204,7 +203,6 @@ let set_debug_types b = debug_types := b
 let set_debug_uf b = debug_uf := b
 let set_debug_unsat_core b = debug_unsat_core := b
 let set_debug_use b = debug_use := b
-let set_debug_warnings b = debug_warnings := b
 let set_debug_commands b = debug_commands := b
 let set_debug_optimize b = debug_optimize := b
 let set_rule b = rule := b
@@ -233,7 +231,6 @@ let get_debug_types () = !debug_types
 let get_debug_uf () = !debug_uf
 let get_debug_unsat_core () = !debug_unsat_core
 let get_debug_use () = !debug_use
-let get_debug_warnings () = !debug_warnings
 let get_debug_commands () = !debug_commands
 let get_debug_optimize () = !debug_optimize
 let get_rule () = !rule
@@ -361,7 +358,6 @@ let get_timelimit_per_goal () = !timelimit_per_goal
 let interpretation = ref INone
 let strict_mode = ref false
 let dump_models = ref false
-let interpretation_use_underscore = ref false
 let objectives_in_interpretation = ref false
 let output_format = ref Native
 let model_type = ref Value
@@ -371,7 +367,6 @@ let unsat_core = ref false
 let set_interpretation b = interpretation := b
 let set_strict_mode b = strict_mode := b
 let set_dump_models b = dump_models := b
-let set_interpretation_use_underscore b = interpretation_use_underscore := b
 let set_objectives_in_interpretation b = objectives_in_interpretation := b
 let set_output_format b = output_format := b
 let set_model_type t = model_type := t
@@ -400,7 +395,6 @@ let get_dump_models () = !dump_models
 let get_first_interpretation () = equal_mode !interpretation IFirst
 let get_every_interpretation () = equal_mode !interpretation IEvery
 let get_last_interpretation () = equal_mode !interpretation ILast
-let get_interpretation_use_underscore () = !interpretation_use_underscore
 let get_objectives_in_interpretation () = !objectives_in_interpretation
 let get_output_format () = !output_format
 let get_output_smtlib () =