Fix model output channel (#635)

* Remove the model-output option

* Use the regular output for printing smtlib error messages

src/bin/common/parse_command.ml

@@ -582,10 +582,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 mdl_output =
+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);
-  Options.Output.(create_channel mdl_output |> set_mdl);
   `Ok()
 
 (* Custom sections *)
@@ -1254,17 +1253,7 @@ let parse_fmt_opt =
     Term.(const (merge_formatters "stderr") $ err_output $ err_formatter)
   in
 
-  let model_output =
-    let doc =
-      Format.sprintf
-        "Set the output used for the model generation. Possible values are %s."
-        (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
-    in
-    Arg.(value & opt string "stdout" & info ["model-output"] ~docv ~docs ~doc)
-  in
-
-  Term.(ret (const mk_output_channel_opt $ std_output $ err_output
-             $ model_output))
+  Term.(ret (const mk_output_channel_opt $ std_output $ err_output))
 
 let main =
 

src/bin/js/worker_example.ml

@@ -233,7 +233,7 @@ let onload _ =
              (* Update debug area *)
              print_debug  (process_results res.debugs);
              (* Update model *)
-             print_model  (process_results res.model);
+             print_model  (process_results res.results);
              (* Update unsat core *)
              print_unsat_core  (process_results res.unsat_core);
              (* Update statistics *)

src/bin/js/worker_interface.ml

@@ -961,7 +961,6 @@ type results = {
   warnings : string list option;
   debugs : string list option;
   statistics : statistics option;
-  model : string list option;
   unsat_core : string list option;
 }
 
@@ -973,29 +972,27 @@ let init_results () = {
   warnings = None;
   debugs = None;
   statistics = None;
-  model = None;
   unsat_core = None;
 }
 
 let results_encoding =
   conv
     (fun {worker_id; status; results; errors; warnings;
-          debugs; statistics; model; unsat_core } ->
+          debugs; statistics; unsat_core } ->
       (worker_id, status, results, errors, warnings,
-       debugs, statistics, model, unsat_core))
+       debugs, statistics, unsat_core))
     (fun (worker_id, status, results, errors, warnings,
-          debugs, statistics, model, unsat_core) ->
+          debugs, statistics, unsat_core) ->
       {worker_id; status; results; errors; warnings;
-       debugs; statistics; model; unsat_core })
-    (obj9
+       debugs; statistics; unsat_core })
+    (obj8
        (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 "model" (list string))
        (opt "unsat_core" (list string)))
 
 let results_to_json res =

src/bin/js/worker_interface.mli

@@ -200,7 +200,6 @@ type results = {
   warnings : string list option;
   debugs : string list option;
   statistics : statistics option;
-  model : string list option;
   unsat_core : string list option;
 }
 

src/bin/js/worker_js.ml

@@ -76,8 +76,6 @@ let main worker_id content =
     Options.Output.set_wrn (snd buf_wrn);
     let buf_dbg = create_buffer () in
     Options.Output.set_dbg (snd buf_dbg);
-    let buf_mdl = create_buffer () in
-    Options.Output.set_mdl (snd buf_mdl);
     let buf_usc = create_buffer () in
     Options.Output.set_usc (snd buf_usc);
 
@@ -248,7 +246,6 @@ let main worker_id content =
       Worker_interface.debugs = check_buffer_content buf_dbg;
       Worker_interface.statistics =
         check_context_content (compute_statistics ());
-      Worker_interface.model = check_buffer_content buf_mdl;
       Worker_interface.unsat_core = check_buffer_content buf_usc;
     }
 

src/lib/reasoners/fun_sat.ml

@@ -1164,18 +1164,18 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     begin
       match !latest_saved_env with
       | None ->
-        Printer.print_fmt (Options.Output.get_fmt_mdl ())
+        Printer.print_fmt (Options.Output.get_fmt_std ())
           "@[<v 0>[FunSat]@, \
            It seems that no model has been computed so far.@,\
            You may need to change your model generation strategy@,\
            or to increase your timeout.@]"
       | Some env ->
-        Printer.print_fmt (Options.Output.get_fmt_mdl ())
+        Printer.print_fmt (Options.Output.get_fmt_std ())
           "@[<v 0>[FunSat]@, \
            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_mdl ()) ~prop_model
+        Th.output_concrete_model (Options.Output.get_fmt_std ()) ~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_mdl ()) ~prop_model
+      Th.output_concrete_model (Options.Output.get_fmt_std ()) ~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_mdl ()) ~prop_model
+    Th.output_concrete_model (Options.Output.get_fmt_std ()) ~prop_model
       env.tbox;
     terminated_normally := true
 

src/lib/util/options.ml

@@ -57,7 +57,6 @@ module Output = struct
   let err_output = ref Stderr
   let wrn_output = ref Stderr
   let dbg_output = ref Stderr
-  let mdl_output = ref Stdout
   let usc_output = ref Stdout
 
   let close o =
@@ -78,12 +77,10 @@ module Output = struct
     set_output err_output Invalid;
     set_output wrn_output Invalid;
     set_output dbg_output Invalid;
-    set_output mdl_output Invalid;
     set_output usc_output Invalid
 
   let set_regular o =
     set_output std_output o;
-    set_output mdl_output o;
     set_output usc_output o
 
   let set_diagnostic o =
@@ -95,14 +92,12 @@ module Output = struct
   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_mdl () = to_formatter !mdl_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_mdl = set_output mdl_output
   let set_usc = set_output usc_output
 end
 

src/lib/util/options.mli

@@ -1132,11 +1132,6 @@ module Output : sig
 
       Default to [Format.err_formatter]. *)
 
-  val get_fmt_mdl : unit -> Format.formatter
-  (** Value specifying the formatter used to output models.
-
-      Default to [Format.std_formatter]. *)
-
   val get_fmt_usc : unit -> Format.formatter
   (** Value specifying the formatter used to output unsat cores.
 
@@ -1154,9 +1149,6 @@ module Output : sig
   val set_dbg : t -> unit
   (** Set [fmt_dbg] accessible with {!val:get_fmt_dbg} *)
 
-  val set_mdl : t -> unit
-  (** Set [fmt_mdl] accessible with {!val:get_fmt_mdl} *)
-
   val set_usc : t -> unit
   (** Set [fmt_usc] accessible with {!val:get_fmt_usc} *)
 end

src/lib/util/printer.ml

@@ -376,7 +376,8 @@ let print_status_preprocess ?(validity_mode=true)
     time steps None
 
 let print_smtlib_err ?(flushed=true) s =
-  let fmt = Options.Output.get_fmt_err () in
+  (* The smtlib error messages are printed on the regular output. *)
+  let fmt = Options.Output.get_fmt_std () in
   let k fmt =
     if flushed || Options.get_output_with_forced_flush () then
       Format.fprintf fmt "\")@."