From 525ac25289f214b45eb696f737947c8d0dc99fa6 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 12 Aug 2024 14:13:31 +0200 Subject: [PATCH 1/3] 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'. --- rsc/extra/worker_json_example.json | 2 +- src/bin/common/parse_command.ml | 7 ++++++- src/bin/js/options_interface.ml | 1 - src/bin/js/worker_interface.ml | 8 +------- src/bin/js/worker_interface.mli | 1 - src/lib/util/options.ml | 3 --- src/lib/util/options.mli | 6 ------ 7 files changed, 8 insertions(+), 20 deletions(-) diff --git a/rsc/extra/worker_json_example.json b/rsc/extra/worker_json_example.json index 7e62a2e95..a7bad8277 100644 --- a/rsc/extra/worker_json_example.json +++ b/rsc/extra/worker_json_example.json @@ -13,7 +13,7 @@ "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_triggers": false, "debug_types": false, "debug_typing": false, "debug_uf": false, "debug_unsat_core": false, "debug_use": false, "debug_warnings": false, "rule": 0, "case_split_policy": "AfterTheoryAssume", "enable_adts_cs": false, diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 6085fd342..74fd5d591 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 diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml index 1b5ffc870..a34472f8a 100644 --- a/src/bin/js/options_interface.ml +++ b/src/bin/js/options_interface.ml @@ -115,7 +115,6 @@ 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; diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index 00cf8362b..1efb8c027 100644 --- a/src/bin/js/worker_interface.ml +++ b/src/bin/js/worker_interface.ml @@ -194,7 +194,6 @@ 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; @@ -297,7 +296,6 @@ let init_options () = { debug_matching = None; debug_sat = None; debug_split = None; - debug_sum = None; debug_triggers = None; debug_types = None; debug_typing = None; @@ -403,7 +401,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 +410,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) ) @@ -572,7 +569,6 @@ let options_to_json opt = opt.debug_matching, opt.debug_sat, opt.debug_split, - opt.debug_sum, opt.debug_triggers) in let dbg_opt3 = @@ -703,7 +699,6 @@ let options_from_json options = debug_matching, debug_sat, debug_split, - debug_sum, debug_triggers) = dbg_opt2 in let (debug_types, debug_typing, @@ -790,7 +785,6 @@ let options_from_json options = debug_matching; debug_sat; debug_split; - debug_sum; debug_triggers; debug_types; debug_typing; diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index 31cf87017..3483805a1 100644 --- a/src/bin/js/worker_interface.mli +++ b/src/bin/js/worker_interface.mli @@ -77,7 +77,6 @@ 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; diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index ff5400472..05f5bcd34 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -155,7 +155,6 @@ 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 @@ -186,7 +185,6 @@ 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 @@ -217,7 +215,6 @@ 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 diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index bd1017508..36642006b 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -158,9 +158,6 @@ 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 @@ -514,9 +511,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 From 5ec05809876ea83f11027099a7851fee3a814231 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 12 Aug 2024 14:54:45 +0200 Subject: [PATCH 2/3] Deprecate debug flag `typing` This flag is unused. --- rsc/extra/worker_json_example.json | 2 +- src/bin/common/parse_command.ml | 5 ++++- src/bin/js/options_interface.ml | 1 - src/bin/js/worker_interface.ml | 8 +------- src/bin/js/worker_interface.mli | 1 - src/lib/util/options.ml | 3 --- src/lib/util/options.mli | 6 ------ 7 files changed, 6 insertions(+), 20 deletions(-) diff --git a/rsc/extra/worker_json_example.json b/rsc/extra/worker_json_example.json index a7bad8277..5e8983f49 100644 --- a/rsc/extra/worker_json_example.json +++ b/rsc/extra/worker_json_example.json @@ -14,7 +14,7 @@ "debug_gc": false, "debug_interpretation": false, "debug_ite": false, "debug_matching": 0, "debug_sat": false, "debug_split": false, "debug_triggers": false, "debug_types": false, - "debug_typing": false, "debug_uf": false, "debug_unsat_core": 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 74fd5d591..e1c1a48dd 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -243,7 +243,10 @@ 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 diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml index a34472f8a..e27c0b044 100644 --- a/src/bin/js/options_interface.ml +++ b/src/bin/js/options_interface.ml @@ -117,7 +117,6 @@ let set_options r = set_options_opt Options.set_debug_split r.debug_split; 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 1efb8c027..a39bfd7f1 100644 --- a/src/bin/js/worker_interface.ml +++ b/src/bin/js/worker_interface.ml @@ -196,7 +196,6 @@ type options = { debug_split : 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; @@ -298,7 +297,6 @@ let init_options () = { debug_split = None; debug_triggers = None; debug_types = None; - debug_typing = None; debug_uf = None; debug_unsat_core = None; debug_use = None; @@ -417,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) @@ -573,7 +570,6 @@ let options_to_json opt = in let dbg_opt3 = (opt.debug_types, - opt.debug_typing, opt.debug_uf, opt.debug_unsat_core, opt.debug_use, @@ -701,7 +697,6 @@ let options_from_json options = debug_split, debug_triggers) = dbg_opt2 in let (debug_types, - debug_typing, debug_uf, debug_unsat_core, debug_use, @@ -787,7 +782,6 @@ let options_from_json options = debug_split; 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 3483805a1..b52303ad1 100644 --- a/src/bin/js/worker_interface.mli +++ b/src/bin/js/worker_interface.mli @@ -79,7 +79,6 @@ type options = { debug_split : 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 05f5bcd34..00b32305c 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -157,7 +157,6 @@ let debug_sat = ref false let debug_split = 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 @@ -187,7 +186,6 @@ let set_debug_sat b = debug_sat := b let set_debug_split b = debug_split := 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,7 +215,6 @@ let get_debug_sat () = !debug_sat let get_debug_split () = !debug_split 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 36642006b..323febc69 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -164,9 +164,6 @@ 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 @@ -526,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 From 87f7fe118674b8bd27ee7e0579f0c25aa17749fd Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 12 Aug 2024 14:57:55 +0200 Subject: [PATCH 3/3] 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`. --- src/bin/common/parse_command.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index e1c1a48dd..9702d7162 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -250,7 +250,11 @@ module Debug = struct | 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 )