From 8b1942fccdf463cbaafa87bb23a815d7d71a392a Mon Sep 17 00:00:00 2001 From: Pierrot Date: Thu, 8 Jun 2023 14:11:34 +0200 Subject: [PATCH] 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 | 15 ++------------- src/bin/js/worker_example.ml | 2 +- src/bin/js/worker_interface.ml | 13 +++++-------- src/bin/js/worker_interface.mli | 1 - src/bin/js/worker_js.ml | 3 --- src/lib/reasoners/fun_sat.ml | 10 +++++----- src/lib/util/options.ml | 5 ----- src/lib/util/options.mli | 8 -------- src/lib/util/printer.ml | 3 ++- 9 files changed, 15 insertions(+), 45 deletions(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 9ff7a9aa9..7af2a901f 100644 --- a/src/bin/common/parse_command.ml +++ b/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"; ""]) - 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 = diff --git a/src/bin/js/worker_example.ml b/src/bin/js/worker_example.ml index 713f8408a..b2dde3c2a 100644 --- a/src/bin/js/worker_example.ml +++ b/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 *) diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index 25cc794af..a03890cb1 100644 --- a/src/bin/js/worker_interface.ml +++ b/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,21 +972,20 @@ 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)) @@ -995,7 +993,6 @@ let results_encoding = (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 = diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index 2c7685777..1139ac796 100644 --- a/src/bin/js/worker_interface.mli +++ b/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; } diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index 8d6f6b8eb..5b3d2939e 100644 --- a/src/bin/js/worker_js.ml +++ b/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; } diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 5493c2e68..586dff137 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/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 ()) "@[[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 ()) "@[[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 diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 53c8f253b..758bb7f93 100644 --- a/src/lib/util/options.ml +++ b/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 diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 564eb747a..dc6560c43 100644 --- a/src/lib/util/options.mli +++ b/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 diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml index 0edba2965..e2038328a 100644 --- a/src/lib/util/printer.ml +++ b/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 "\")@."