From 0c07514ffbf59f9845d1e95d3bd4deb2d2138221 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 12 Nov 2024 10:43:24 +0100 Subject: [PATCH] Remove debug_warnings --- src/bin/js/options_interface.ml | 1 - src/bin/js/worker_interface.ml | 12 +++--------- src/bin/js/worker_interface.mli | 1 - src/lib/structures/expr.ml | 3 +-- src/lib/util/options.ml | 3 --- src/lib/util/options.mli | 6 ------ src/lib/util/printer.ml | 8 ++------ src/lib/util/printer.mli | 2 -- 8 files changed, 6 insertions(+), 30 deletions(-) diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml index 464e9c7a2..57479b2bb 100644 --- a/src/bin/js/options_interface.ml +++ b/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 diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index 21870d25e..907151e44 100644 --- a/src/bin/js/worker_interface.ml +++ b/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; diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index c3f1c2bd3..723e0a84e 100644 --- a/src/bin/js/worker_interface.mli +++ b/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; diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7945afddd..25b56dc07 100644 --- a/src/lib/structures/expr.ml +++ b/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 ?? *) diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index f99e83d46..930ff56f1 100644 --- a/src/lib/util/options.ml +++ b/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 diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 4a415ef5c..8946e2e84 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -173,9 +173,6 @@ val set_debug_unsat_core : bool -> unit (** Set [debug_use] accessible with {!val:get_debug_use} *) val set_debug_use : bool -> unit -(** Set [debug_warnings] accessible with {!val:get_debug_warnings} *) -val set_debug_warnings : bool -> unit - (** Set [debug_commands] accessible with {!val:get_debug_commands} *) val set_debug_commands : bool -> unit @@ -465,9 +462,6 @@ val set_used_context_file : string -> unit (** Get the debugging flag. *) val get_debug : unit -> bool -(** Get the debugging flag of warnings. *) -val get_debug_warnings : unit -> bool - (** Get the debugging flag of commands. If enabled, Alt-Ergo will display all the commands that are sent to the solver. *) val get_debug_commands : unit -> bool diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml index 5a76274e0..6386b193d 100644 --- a/src/lib/util/printer.ml +++ b/src/lib/util/printer.ml @@ -227,12 +227,10 @@ let print_err ?(flushed=true) ?(header=(Options.get_output_with_headers ())) end else Format.ifprintf Format.err_formatter s -let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) - ?(warning=true) s = +let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) s = if Options.get_warning_as_error () then - print_err ~flushed ~header ~error:warning s + print_err ~flushed ~header ~error:true s else - if warning then begin let fmt = Options.Output.get_fmt_diagnostic () in Format.fprintf fmt "@[%s" (pp_smt clean_wrn_print); if header then @@ -242,8 +240,6 @@ let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) Format.fprintf fmt "@[[Warning] " ; if flushed || Options.get_output_with_forced_flush () then Format.kfprintf flush fmt s else Format.fprintf fmt s - end - else Format.ifprintf Format.err_formatter s let print_dbg ?(flushed=true) ?(header=(Options.get_output_with_headers ())) ?(module_name="") ?(function_name="") s = diff --git a/src/lib/util/printer.mli b/src/lib/util/printer.mli index 55245c69c..98d1501e3 100644 --- a/src/lib/util/printer.mli +++ b/src/lib/util/printer.mli @@ -47,13 +47,11 @@ val print_err : (** Print warning message on the warning formatter accessible with {!val:Options.get_fmt_wrn} and set by default to stderr. - Prints only if warning (true by default) is true. If header is set, prints a header "[Warning]". The wrn formatter is flushed after the print if flushed is set *) val print_wrn : ?flushed:bool -> ?header:bool -> - ?warning:bool -> ('a, Format.formatter, unit) format -> 'a (** Print debug message on the debug formatter accessible with