remove wrn, dbg and usc outputs

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 ());
          )
       )
 

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. *)

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;

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
 

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

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 *)

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 "@[<v 0>";
     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 "@[<v 0>%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 "@[<v 0>%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 "\")@."

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,""))