From 28819ec677c2e20d399acdf1de299b179187b069 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Tue, 20 Aug 2024 11:57:24 +0200 Subject: [PATCH] Deprecate debug flags (#1204) * Deprecate the debug flag 'sum' After merging sum theory into adt theory, this flag has no effect anymore. This commit deprecates it and now it has the same effect as the flag 'adt'. * Deprecate debug flag `typing` This flag is unused. * Deprecated warnings flag The debug flag `warnings` is only used by legacy parser. We deprecate it in `v2.6.0` and it will be removed with the legacy parser in `v2.7.0`. --- rsc/extra/worker_json_example.json | 4 ++-- src/bin/common/parse_command.ml | 18 +++++++++++++++--- src/bin/js/options_interface.ml | 2 -- src/bin/js/worker_interface.ml | 16 ++-------------- src/bin/js/worker_interface.mli | 2 -- src/lib/util/options.ml | 6 ------ src/lib/util/options.mli | 12 ------------ 7 files changed, 19 insertions(+), 41 deletions(-) diff --git a/rsc/extra/worker_json_example.json b/rsc/extra/worker_json_example.json index 7e62a2e95..5e8983f49 100644 --- a/rsc/extra/worker_json_example.json +++ b/rsc/extra/worker_json_example.json @@ -13,8 +13,8 @@ "debug_explanations": false, "debug_fm": false, "debug_fpa": 0, "debug_gc": false, "debug_interpretation": false, "debug_ite": false, "debug_matching": 0, "debug_sat": false, "debug_split": false, - "debug_sum": false, "debug_triggers": false, "debug_types": false, - "debug_typing": false, "debug_uf": false, "debug_unsat_core": false, + "debug_triggers": false, "debug_types": false, + "debug_uf": false, "debug_unsat_core": false, "debug_use": false, "debug_warnings": false, "rule": 0, "case_split_policy": "AfterTheoryAssume", "enable_adts_cs": false, "max_split": 0, "replay": false, "replay_all_used_context": false, diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 6085fd342..9702d7162 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -222,7 +222,12 @@ module Debug = struct | Arith -> Options.set_debug_arith true | Arrays -> Options.set_debug_arrays true | Bitv -> Options.set_debug_bitv true - | Sum -> Options.set_debug_sum true + | 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 | Ite -> Options.set_debug_ite true | Cc -> Options.set_debug_cc true | Combine -> Options.set_debug_combine true @@ -238,11 +243,18 @@ module Debug = struct | Split -> Options.set_debug_split true | Triggers -> Options.set_debug_triggers true | Types -> Options.set_debug_types true - | Typing -> Options.set_debug_typing true + | 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 | Unsat_core -> Options.set_debug_unsat_core true | Use -> Options.set_debug_use true - | Warnings -> Options.set_debug_warnings true + | 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 | Optimize -> Options.set_debug_optimize true ) diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml index 1b5ffc870..e27c0b044 100644 --- a/src/bin/js/options_interface.ml +++ b/src/bin/js/options_interface.ml @@ -115,10 +115,8 @@ let set_options r = set_options_opt Options.set_debug_matching r.debug_matching; set_options_opt Options.set_debug_sat r.debug_sat; set_options_opt Options.set_debug_split r.debug_split; - set_options_opt Options.set_debug_sum r.debug_sum; set_options_opt Options.set_debug_triggers r.debug_triggers; set_options_opt Options.set_debug_types r.debug_types; - set_options_opt Options.set_debug_typing r.debug_typing; 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; diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index 00cf8362b..a39bfd7f1 100644 --- a/src/bin/js/worker_interface.ml +++ b/src/bin/js/worker_interface.ml @@ -194,10 +194,8 @@ type options = { debug_matching : int option; debug_sat : bool option; debug_split : bool option; - debug_sum : bool option; debug_triggers : bool option; debug_types : bool option; - debug_typing : bool option; debug_uf : bool option; debug_unsat_core : bool option; debug_use : bool option; @@ -297,10 +295,8 @@ let init_options () = { debug_matching = None; debug_sat = None; debug_split = None; - debug_sum = None; debug_triggers = None; debug_types = None; - debug_typing = None; debug_uf = None; debug_unsat_core = None; debug_use = None; @@ -403,7 +399,7 @@ let opt_dbg2_encoding = conv (fun dbg2 -> dbg2) (fun dbg2 -> dbg2) - (obj10 + (obj9 (opt "debug_fm" bool) (opt "debug_fpa" int31) (opt "debug_gc" bool) @@ -412,7 +408,6 @@ let opt_dbg2_encoding = (opt "debug_matching" int31) (opt "debug_sat" bool) (opt "debug_split" bool) - (opt "debug_sum" bool) (opt "debug_triggers" bool) ) @@ -420,9 +415,8 @@ let opt_dbg3_encoding = conv (fun dbg3 -> dbg3) (fun dbg3 -> dbg3) - (obj6 + (obj5 (opt "debug_types" bool) - (opt "debug_typing" bool) (opt "debug_uf" bool) (opt "debug_unsat_core" bool) (opt "debug_use" bool) @@ -572,12 +566,10 @@ let options_to_json opt = opt.debug_matching, opt.debug_sat, opt.debug_split, - opt.debug_sum, opt.debug_triggers) in let dbg_opt3 = (opt.debug_types, - opt.debug_typing, opt.debug_uf, opt.debug_unsat_core, opt.debug_use, @@ -703,10 +695,8 @@ let options_from_json options = debug_matching, debug_sat, debug_split, - debug_sum, debug_triggers) = dbg_opt2 in let (debug_types, - debug_typing, debug_uf, debug_unsat_core, debug_use, @@ -790,10 +780,8 @@ let options_from_json options = debug_matching; debug_sat; debug_split; - debug_sum; debug_triggers; debug_types; - debug_typing; debug_uf; debug_unsat_core; debug_use; diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index 31cf87017..b52303ad1 100644 --- a/src/bin/js/worker_interface.mli +++ b/src/bin/js/worker_interface.mli @@ -77,10 +77,8 @@ type options = { debug_matching : int option; debug_sat : bool option; debug_split : bool option; - debug_sum : bool option; debug_triggers : bool option; debug_types : bool option; - debug_typing : bool option; debug_uf : bool option; debug_unsat_core : bool option; debug_use : bool option; diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index ff5400472..00b32305c 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -155,10 +155,8 @@ let debug_ite = ref false let debug_matching = ref 0 let debug_sat = ref false let debug_split = ref false -let debug_sum = ref false let debug_triggers = ref false let debug_types = ref false -let debug_typing = ref false let debug_uf = ref false let debug_unsat_core = ref false let debug_use = ref false @@ -186,10 +184,8 @@ let set_debug_ite b = debug_ite := b let set_debug_matching i = debug_matching := i let set_debug_sat b = debug_sat := b let set_debug_split b = debug_split := b -let set_debug_sum b = debug_sum := b let set_debug_triggers b = debug_triggers := b let set_debug_types b = debug_types := b -let set_debug_typing b = debug_typing := 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 @@ -217,10 +213,8 @@ let get_debug_ite () = !debug_ite let get_debug_matching () = !debug_matching let get_debug_sat () = !debug_sat let get_debug_split () = !debug_split -let get_debug_sum () = !debug_sum let get_debug_triggers () = !debug_triggers let get_debug_types () = !debug_types -let get_debug_typing () = !debug_typing let get_debug_uf () = !debug_uf let get_debug_unsat_core () = !debug_unsat_core let get_debug_use () = !debug_use diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index bd1017508..323febc69 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -158,18 +158,12 @@ val set_debug_sat : bool -> unit (** Set [debug_split] accessible with {!val:get_debug_split} *) val set_debug_split : bool -> unit -(** Set [debug_sum] accessible with {!val:get_debug_sum} *) -val set_debug_sum : bool -> unit - (** Set [debug_triggers] accessible with {!val:get_debug_triggers} *) val set_debug_triggers : bool -> unit (** Set [debug_types] accessible with {!val:get_debug_types} *) val set_debug_types : bool -> unit -(** Set [debug_typing] accessible with {!val:get_debug_typing} *) -val set_debug_typing : bool -> unit - (** Set [debug_uf] accessible with {!val:get_debug_uf} *) val set_debug_uf : bool -> unit @@ -514,9 +508,6 @@ val get_debug_intervals : unit -> bool val get_debug_fpa : unit -> int (** Default to [0]. *) -(** Get the debugging flag of Sum. *) -val get_debug_sum : unit -> bool - (** Get the debugging flag of ADTs. *) val get_debug_adt : unit -> bool @@ -532,9 +523,6 @@ val get_debug_ac : unit -> bool (** Get the debugging flag of SAT. *) val get_debug_sat : unit -> bool -(** Get the debugging flag of typing. *) -val get_debug_typing : unit -> bool - (** Get the debugging flag of constructors. *) val get_debug_constr : unit -> bool