From 753826aa97d9e80d7f16a98b9e2c44e1521dfb4e Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 18 Aug 2023 16:31:02 +0200 Subject: [PATCH] remove wrn, dbg and usc outputs --- src/bin/common/signals_profiling.ml | 6 ++-- src/bin/common/solving_loop.ml | 2 +- src/lib/frontend/frontend.ml | 2 +- src/lib/reasoners/fun_sat.ml | 6 ++-- src/lib/util/options.ml | 43 ++++++++--------------------- src/lib/util/options.mli | 40 ++++----------------------- src/lib/util/printer.ml | 33 ++++++++++------------ src/parsers/psmt2_to_alt_ergo.ml | 4 +-- 8 files changed, 41 insertions(+), 95 deletions(-) diff --git a/src/bin/common/signals_profiling.ml b/src/bin/common/signals_profiling.ml index 507c3a9e6..d99be885a 100644 --- a/src/bin/common/signals_profiling.ml +++ b/src/bin/common/signals_profiling.ml @@ -39,7 +39,7 @@ let init_sigterm_6 () = Sys.set_signal Sys.sigint(*-6*) (Sys.Signal_handle (fun _ -> if Options.get_profiling() then - Profiling.switch (Options.Output.get_fmt_err ()) + Profiling.switch (Options.Output.get_fmt_diagnostic ()) else begin Printer.print_wrn "User wants me to stop."; Printer.print_std "unknown"; @@ -58,7 +58,7 @@ let init_sigterm_11_9 () = (Sys.Signal_handle (fun _ -> Profiling.print true (Steps.get_steps ()) - timers (Options.Output.get_fmt_err ()); + timers (Options.Output.get_fmt_diagnostic ()); exit 1 ) ) @@ -72,7 +72,7 @@ let init_sigterm_21 () = (Sys.Signal_handle (fun _ -> Profiling.print false (Steps.get_steps ()) timers - (Options.Output.get_fmt_err ()); + (Options.Output.get_fmt_diagnostic ()); ) ) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 04445bb99..ce4f8ba34 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -92,7 +92,7 @@ let main () = Profiling.print true (Steps.get_steps ()) (Signals_profiling.get_timers ()) - (Options.Output.get_fmt_err ()); + (Options.Output.get_fmt_diagnostic ()); (* If the status of the SAT environment is inconsistent, we have to drop the partial model in order to prevent printing wrong model. *) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 5b7c4b02a..7c93e0030 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -291,7 +291,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct not (get_debug_unsat_core()) && not (get_save_used_context()) then - Printer.print_fmt (Options.Output.get_fmt_usc ()) + Printer.print_fmt (Options.Output.get_fmt_regular ()) "unsat-core:@,%a@." (Ex.print_unsat_core ~tab:true) dep; check_status_consistency status; diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 35ae79b0e..fb2cfb874 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1175,7 +1175,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct A model has been computed. However, I failed \ while computing it so may be incorrect.@]"; let prop_model = extract_prop_model ~complete_model:true env in - Th.output_concrete_model (Options.Output.get_fmt_std ()) ~prop_model + Th.output_concrete_model (Options.Output.get_fmt_regular ()) ~prop_model env.tbox; end; return_function () @@ -1193,7 +1193,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let prop_model = extract_prop_model ~complete_model:true env in if Options.(get_interpretation () && get_dump_models ()) then - Th.output_concrete_model (Options.Output.get_fmt_std ()) ~prop_model + Th.output_concrete_model (Options.Output.get_fmt_regular ()) ~prop_model env.tbox; terminated_normally := true; @@ -1926,7 +1926,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let env = compute_concrete_model env true in Options.Time.unset_timeout (); let prop_model = extract_prop_model ~complete_model:true env in - Th.output_concrete_model (Options.Output.get_fmt_std ()) ~prop_model + Th.output_concrete_model (Options.Output.get_fmt_regular ()) ~prop_model env.tbox; terminated_normally := true diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index bb8b78cc5..b7db512b3 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -53,11 +53,8 @@ module Output = struct let fmt = Format.formatter_of_out_channel cout in Channel (cout, fmt) - let std_output = ref Stdout - let err_output = ref Stderr - let wrn_output = ref Stderr - let dbg_output = ref Stderr - let usc_output = ref Stdout + let regular_output = ref Stdout + let diagnostic_output = ref Stderr let close o = match o with @@ -73,32 +70,14 @@ module Output = struct output := o let close_all () = - set_output std_output Invalid; - set_output err_output Invalid; - set_output wrn_output Invalid; - set_output dbg_output Invalid; - set_output usc_output Invalid - - let set_regular o = - set_output std_output o; - set_output usc_output o - - let set_diagnostic o = - set_output err_output o; - set_output wrn_output o; - set_output dbg_output o - - let get_fmt_std () = to_formatter !std_output - let get_fmt_err () = to_formatter !err_output - let get_fmt_wrn () = to_formatter !wrn_output - let get_fmt_dbg () = to_formatter !dbg_output - let get_fmt_usc () = to_formatter !usc_output - - let set_std = set_output std_output - let set_err = set_output err_output - let set_wrn = set_output wrn_output - let set_dbg = set_output dbg_output - let set_usc = set_output usc_output + set_output regular_output Invalid; + set_output diagnostic_output Invalid + + let set_regular o = set_output regular_output o + let set_diagnostic o = set_output diagnostic_output o + + let get_fmt_regular () = to_formatter !regular_output + let get_fmt_diagnostic () = to_formatter !diagnostic_output end (* Declaration of all the options as refs with default values *) @@ -605,7 +584,7 @@ let exec_timeout () = !timeout () let tool_req n msg = if get_rule () = n then - Format.fprintf (Output.get_fmt_dbg ()) "[rule] %s@." msg + Format.fprintf (Output.get_fmt_diagnostic ()) "[rule] %s@." msg (** Simple Timer module **) module Time = struct diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index cabbb1cbd..21d841bc7 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -1084,9 +1084,9 @@ module Output : sig val create_channel : string -> t (** [create_filename filename] create an out channel to the file [filename]. If the argument is "stdout", respectively "stderr", the channel is the - standard output, respectively the standard error. - If the file does not exist, the procedure creates it. An existant file - is truncated to zero length. *) + standard output, respectively the standard error. If the file does not + exist, the procedure creates it. An existant file is truncated to zero + length. *) val close_all : unit -> unit (** Flushing and closing all the remaining output channels. *) @@ -1103,45 +1103,15 @@ module Output : sig Default to [Format.err_formatter]. *) - val get_fmt_std : unit -> Format.formatter + val get_fmt_regular : unit -> Format.formatter (** Value specifying the formatter used to output results. Default to [Format.std_formatter]. *) - val get_fmt_err : unit -> Format.formatter + val get_fmt_diagnostic : unit -> Format.formatter (** Value specifying the formatter used to output errors. Default to [Format.err_formatter]. *) - - val get_fmt_wrn : unit -> Format.formatter - (** Value specifying the formatter used to output warnings. - - Default to [Format.err_formatter]. *) - - val get_fmt_dbg : unit -> Format.formatter - (** Value specifying the formatter used to output debug informations. - - Default to [Format.err_formatter]. *) - - val get_fmt_usc : unit -> Format.formatter - (** Value specifying the formatter used to output unsat cores. - - Default to [Format.std_formatter]. *) - - val set_std : t -> unit - (** Set [fmt_std] accessible with {!val:get_fmt_std} *) - - val set_err : t -> unit - (** Set [fmt_err] accessible with {!val:get_fmt_err} *) - - val set_wrn : t -> unit - (** Set [fmt_wrn] accessible with {!val:get_fmt_wrn} *) - - val set_dbg : t -> unit - (** Set [fmt_dbg] accessible with {!val:get_fmt_dbg} *) - - val set_usc : t -> unit - (** Set [fmt_usc] accessible with {!val:get_fmt_usc} *) end (** Print message as comment in the corresponding output format *) diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml index 7e125e349..c67e670b7 100644 --- a/src/lib/util/printer.ml +++ b/src/lib/util/printer.ml @@ -144,10 +144,8 @@ let add_colors formatter = let init_colors () = if Options.get_output_with_colors () then begin - add_colors (Options.Output.get_fmt_std ()); - add_colors (Options.Output.get_fmt_wrn ()); - add_colors (Options.Output.get_fmt_err ()); - add_colors (Options.Output.get_fmt_dbg ()) + add_colors (Options.Output.get_fmt_regular ()); + add_colors (Options.Output.get_fmt_diagnostic ()) end (************** Output Format *************) @@ -168,14 +166,14 @@ let pp_std_smt () = | true, true -> () | false, true -> clean_dbg_print := true; - Format.fprintf (Options.Output.get_fmt_std ()) "@," + Format.fprintf (Options.Output.get_fmt_regular ()) "@," | true, false -> clean_wrn_print := true; - Format.fprintf (Options.Output.get_fmt_std ()) "@," + Format.fprintf (Options.Output.get_fmt_regular ()) "@," | false, false -> clean_dbg_print := true; clean_wrn_print := true; - Format.fprintf (Options.Output.get_fmt_std ()) "@," + Format.fprintf (Options.Output.get_fmt_regular ()) "@," let add_smt formatter = let old_fs = Format.pp_get_formatter_out_functions formatter () in @@ -204,8 +202,7 @@ let force_new_line formatter = let init_output_format () = match Options.get_output_format () with | Smtlib2 -> - add_smt (Options.Output.get_fmt_wrn ()); - add_smt (Options.Output.get_fmt_dbg ()) + add_smt (Options.Output.get_fmt_diagnostic ()) | Native | Why3 | Unknown _ -> () @@ -214,14 +211,14 @@ let flush fmt = Format.fprintf fmt "@." let print_std ?(flushed=true) s = pp_std_smt (); - let fmt = Options.Output.get_fmt_std () in + let fmt = Options.Output.get_fmt_regular () in if flushed || Options.get_output_with_forced_flush () then Format.kfprintf flush fmt s else Format.fprintf fmt s let print_err ?(flushed=true) ?(header=(Options.get_output_with_headers ())) ?(error=true) s = if error then begin - let fmt = Options.Output.get_fmt_err () in + let fmt = Options.Output.get_fmt_diagnostic () in Format.fprintf fmt "@["; if header then if Options.get_output_with_colors () then @@ -239,7 +236,7 @@ let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) print_err ~flushed ~header ~error:warning s else if warning then begin - let fmt = Options.Output.get_fmt_wrn () in + let fmt = Options.Output.get_fmt_diagnostic () in Format.fprintf fmt "@[%s" (pp_smt clean_wrn_print); if header then if Options.get_output_with_colors () then @@ -253,7 +250,7 @@ let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) let print_dbg ?(flushed=true) ?(header=(Options.get_output_with_headers ())) ?(module_name="") ?(function_name="") s = - let fmt = Options.Output.get_fmt_dbg () in + let fmt = Options.Output.get_fmt_diagnostic () in Format.fprintf fmt "@[%s" (pp_smt clean_dbg_print); if header then begin let fname = @@ -327,12 +324,12 @@ let print_status_value fmt (v,color) = Format.fprintf fmt "%s" v let print_status ?(validity_mode=true) - ?(formatter=Options.Output.get_fmt_std ()) + ?(formatter=Options.Output.get_fmt_regular ()) (validity_status,unsat_status,color) loc time steps goal = pp_std_smt (); let native_output_fmt, comment_if_smt2 = if validity_mode then formatter, "" - else (Options.Output.get_fmt_dbg ()), (pp_smt clean_dbg_print) + else (Options.Output.get_fmt_diagnostic ()), (pp_smt clean_dbg_print) in (* print validity status. Commented and in debug fmt if in unsat mode *) Format.fprintf native_output_fmt @@ -362,7 +359,7 @@ let print_status_sat ?(validity_mode=true) loc let print_status_inconsistent ?(validity_mode=true) loc time steps goal = print_status ~validity_mode - ~formatter:(Options.Output.get_fmt_dbg ()) + ~formatter:(Options.Output.get_fmt_diagnostic ()) ("Inconsistent assumption","","fg_red") loc time steps goal @@ -381,13 +378,13 @@ let print_status_timeout ?(validity_mode=true) loc let print_status_preprocess ?(validity_mode=true) time steps = print_status ~validity_mode - ~formatter:(Options.Output.get_fmt_dbg ()) + ~formatter:(Options.Output.get_fmt_diagnostic ()) ("Preprocessing","","fg_magenta") None time steps None let print_smtlib_err ?(flushed=true) s = (* The smtlib error messages are printed on the regular output. *) - let fmt = Options.Output.get_fmt_std () in + let fmt = Options.Output.get_fmt_regular () in let k fmt = if flushed || Options.get_output_with_forced_flush () then Format.fprintf fmt "\")@." diff --git a/src/parsers/psmt2_to_alt_ergo.ml b/src/parsers/psmt2_to_alt_ergo.ml index 9112e0ffc..e334b4650 100644 --- a/src/parsers/psmt2_to_alt_ergo.ml +++ b/src/parsers/psmt2_to_alt_ergo.ml @@ -508,7 +508,7 @@ let aux aux_fun token lexbuf = let loc = (Lexing.lexeme_start_p lexbuf, Lexing.lexeme_end_p lexbuf) in let lex = Lexing.lexeme lexbuf in Parsing.clear_parser (); - Smtlib_error.print (Options.Output.get_fmt_err ()) (Options.get_file ()) + Smtlib_error.print (Options.Output.get_fmt_diagnostic ()) (Options.get_file ()) (Syntax_error (lex)) loc; Errors.error (Errors.Syntax_error (loc,"")) | Smtlib_error.Error (e , p) -> @@ -518,7 +518,7 @@ let aux aux_fun token lexbuf = Some loc -> loc | None -> Lexing.dummy_pos,Lexing.dummy_pos in - Smtlib_error.print (Options.Output.get_fmt_err ()) + Smtlib_error.print (Options.Output.get_fmt_diagnostic ()) (Options.get_file ()) e loc; Errors.error (Errors.Syntax_error (loc,""))