From 1c9b9d40b8f74a7c235d6110d1ed9e0b5e74b362 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 21 Aug 2023 15:37:06 +0200 Subject: [PATCH] Update the worker --- src/bin/js/worker_example.ml | 14 ++++++------- src/bin/js/worker_interface.ml | 37 +++++++++++---------------------- src/bin/js/worker_interface.mli | 7 ++----- src/bin/js/worker_js.ml | 25 +++++++--------------- 4 files changed, 29 insertions(+), 54 deletions(-) diff --git a/src/bin/js/worker_example.ml b/src/bin/js/worker_example.ml index b2dde3c2a..4a06f6a61 100644 --- a/src/bin/js/worker_example.ml +++ b/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); diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index 0a3f3fcf0..b45459d9b 100644 --- a/src/bin/js/worker_interface.ml +++ b/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 diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index cdcf7b69f..ecb332104 100644 --- a/src/bin/js/worker_interface.mli +++ b/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} *) diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index 5b3d2939e..d6dd62276 100644 --- a/src/bin/js/worker_js.ml +++ b/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) *) @@ -240,13 +234,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 @@ -255,7 +246,7 @@ 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 -> @@ -263,7 +254,7 @@ let main worker_id content = { 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] } | _ ->