Simplify output channels (#782)

* remove deprecated options

* remove wrn, dbg and usc outputs

* change docv

* Update the worker

* Fix too long lines

src/bin/common/parse_command.ml

@@ -530,9 +530,9 @@ let mk_opts file () () debug_flags ddebug_flags dddebug_flags rule () halt_opt
     `Ok true
   end
 
-let mk_output_channel_opt std_output err_output =
-  Options.Output.(create_channel std_output |> set_std);
-  Options.Output.(create_channel err_output |> set_err);
+let mk_output_channel_opt regular_output diagnostic_output =
+  Options.Output.(create_channel regular_output |> set_regular);
+  Options.Output.(create_channel diagnostic_output |> set_diagnostic);
   `Ok()
 
 (* Custom sections *)
@@ -1438,58 +1438,29 @@ let parse_theory_opt =
 
 let parse_fmt_opt =
   let docs = s_fmt in
-  let docv = "CHANNEL" in
+  let docv = "OUTPUT" in
 
-  let merge_formatters default preferred deprecated =
-    match preferred, deprecated with
-    | Some fmt, _ -> fmt
-    | None, Some fmt -> fmt
-    | None, None -> default
-  in
-
-  let std_output =
+  let regular_output =
     let doc =
       Format.sprintf
-        "Set the standard output used by default to print the results,
+        "Set the regular output used by default to print the results,
           models and unsat cores. Possible values are %s."
         (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
     in
-    let deprecated =
-      "this option is deprecated. Please use --regular-output."
-    in
-    let regular_output =
-      Arg.(value & opt (some' string) None & info ["regular-output"] ~docs
-             ~doc ~docv)
-    in
-    let std_formatter =
-      Arg.(value & opt (some' string) None  & info ["std-formatter"]
-             ~deprecated ~docs ~docv)
-    in
-    Term.(const (merge_formatters "stdout") $ regular_output $ std_formatter)
+    Arg.(value & opt string "stdout" & info ["regular-output"] ~docs
+           ~doc ~docv)
   in
-
-  let err_output =
+  let diagnostic_output =
     let doc =
       Format.sprintf
-        "Set the error output used by default to print error, debug and
+        "Set the diagnostic output used by default to print error, debug and
          warning informations. Possible values are %s."
         (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
     in
-    let deprecated =
-      "this option is deprecated. Please use --diagnostic-output."
-    in
-    let diagnostic_output =
-      Arg.(value & opt (some' string) None & info ["diagnostic-output"] ~docs
-             ~doc ~docv)
-    in
-    let err_formatter =
-      Arg.(value & opt (some' string) None & info ["err-formatter"]
-             ~deprecated ~docs ~docv)
-    in
-    Term.(const (merge_formatters "stderr") $ diagnostic_output $ err_formatter)
+    Arg.(value & opt string "stderr" & info ["diagnostic-output"] ~docs
+           ~doc ~docv)
   in
-
-  Term.(ret (const mk_output_channel_opt $ std_output $ err_output))
+  Term.(ret (const mk_output_channel_opt $ regular_output $ diagnostic_output))
 
 let main =
 

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/bin/js/worker_example.ml

@@ -82,7 +82,7 @@ let solve () =
   (Lwt.pick [
       (let%lwt () = Lwt_js.sleep !timeout in
        Lwt.return {(Worker_interface.init_results ()) with
-                   debugs =Some ["Timeout"]});
+                   diagnostic = Some ["Timeout"]});
       (
         let file = String.split_on_char '\n' !file in
         let json_file = Worker_interface.file_to_json None (Some 42) file in
@@ -225,17 +225,17 @@ let onload _ =
              print_error (Some "");
              let%lwt res = solve () in
              (* Update results area *)
-             print_res (process_results res.results);
+             print_res (process_results res.regular);
              (* Update errors area if errors occurs at solving *)
-             print_error  (process_results res.errors);
+             print_error  (process_results res.diagnostic);
              (* Update warning area if warning occurs at solving *)
-             print_warning  (process_results res.warnings);
+             print_warning  (process_results res.diagnostic);
              (* Update debug area *)
-             print_debug  (process_results res.debugs);
+             print_debug  (process_results res.diagnostic);
              (* Update model *)
-             print_model  (process_results res.results);
+             print_model  (process_results res.regular);
              (* Update unsat core *)
-             print_unsat_core  (process_results res.unsat_core);
+             print_unsat_core  (process_results res.regular);
              (* Update statistics *)
              print_statistics res.statistics;
              Lwt.return_unit);

src/bin/js/worker_interface.ml

@@ -944,44 +944,31 @@ let status_encoding =
 type results = {
   worker_id : int option;
   status : status;
-  results : string list option;
-  errors : string list option;
-  warnings : string list option;
-  debugs : string list option;
+  regular : string list option;
+  diagnostic : string list option;
   statistics : statistics option;
-  unsat_core : string list option;
 }
 
 let init_results () = {
   worker_id = None;
   status = Unknown (-1);
-  results = None;
-  errors = None;
-  warnings = None;
-  debugs = None;
+  regular = None;
+  diagnostic = None;
   statistics = None;
-  unsat_core = None;
 }
 
 let results_encoding =
   conv
-    (fun {worker_id; status; results; errors; warnings;
-          debugs; statistics; unsat_core } ->
-      (worker_id, status, results, errors, warnings,
-       debugs, statistics, unsat_core))
-    (fun (worker_id, status, results, errors, warnings,
-          debugs, statistics, unsat_core) ->
-      {worker_id; status; results; errors; warnings;
-       debugs; statistics; unsat_core })
-    (obj8
+    (fun {worker_id; status; regular; diagnostic; statistics} ->
+       (worker_id, status, regular, diagnostic, statistics))
+    (fun (worker_id, status, regular, diagnostic, statistics) ->
+       {worker_id; status; regular; diagnostic; statistics })
+    (obj5
        (opt "worker_id" int31)
        (req "status" status_encoding)
-       (opt "results" (list string))
-       (opt "errors" (list string))
-       (opt "warnings" (list string))
-       (opt "debugs" (list string))
-       (opt "statistics" statistics_encoding)
-       (opt "unsat_core" (list string)))
+       (opt "regular" (list string))
+       (opt "diagnostic" (list string))
+       (opt "statistics" statistics_encoding))
 
 let results_to_json res =
   let json_results = Json.construct results_encoding res in

src/bin/js/worker_interface.mli

@@ -193,12 +193,9 @@ type status =
 type results = {
   worker_id : int option;
   status : status;
-  results : string list option;
-  errors : string list option;
-  warnings : string list option;
-  debugs : string list option;
+  regular : string list option;
+  diagnostic : string list option;
   statistics : statistics option;
-  unsat_core : string list option;
 }
 
 (** {2 Functions} *)

src/bin/js/worker_js.ml

@@ -68,16 +68,10 @@ let main worker_id content =
   try
     (* Create buffer for each formatter
        The content of this buffers are then retrieved and send as results *)
-    let buf_std = create_buffer () in
-    Options.Output.set_std (snd buf_std);
-    let buf_err = create_buffer () in
-    Options.Output.set_err (snd buf_err);
-    let buf_wrn = create_buffer () in
-    Options.Output.set_wrn (snd buf_wrn);
-    let buf_dbg = create_buffer () in
-    Options.Output.set_dbg (snd buf_dbg);
-    let buf_usc = create_buffer () in
-    Options.Output.set_usc (snd buf_usc);
+    let buf_regular = create_buffer () in
+    Options.Output.set_regular (snd buf_regular);
+    let buf_diagnostic = create_buffer () in
+    Options.Output.set_diagnostic (snd buf_diagnostic);
 
     (* Status updated regarding if AE succed or failed
        (error or steplimit reached) *)
@@ -241,13 +235,10 @@ let main worker_id content =
     {
       Worker_interface.worker_id = worker_id;
       Worker_interface.status = !returned_status;
-      Worker_interface.results = check_buffer_content buf_std;
-      Worker_interface.errors = check_buffer_content buf_err;
-      Worker_interface.warnings = check_buffer_content buf_wrn;
-      Worker_interface.debugs = check_buffer_content buf_dbg;
+      Worker_interface.regular = check_buffer_content buf_regular;
+      Worker_interface.diagnostic = check_buffer_content buf_diagnostic;
       Worker_interface.statistics =
         check_context_content (compute_statistics ());
-      Worker_interface.unsat_core = check_buffer_content buf_usc;
     }
 
   with
@@ -256,15 +247,15 @@ let main worker_id content =
     { res with
       Worker_interface.worker_id = worker_id;
       Worker_interface.status = Error "Assertion failure";
-      Worker_interface.errors =
+      Worker_interface.diagnostic =
         Some [Format.sprintf "assertion failed: %s line %d char %d" s l p];
     }
   | Errors.Error e ->
     let res = Worker_interface.init_results () in
     { res with
       Worker_interface.worker_id = worker_id;
       Worker_interface.status = Error "";
-      Worker_interface.errors =
+      Worker_interface.diagnostic =
         Some [Format.asprintf "%a" Errors.report e]
     }
   | _ ->

src/lib/frontend/frontend.ml

@@ -309,7 +309,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 *)
@@ -606,7 +585,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