Skip to content

Commit

Permalink
Update the worker
Browse files Browse the repository at this point in the history
  • Loading branch information
Halbaroth committed Aug 21, 2023
1 parent 1196340 commit 1c9b9d4
Show file tree
Hide file tree
Showing 4 changed files with 29 additions and 54 deletions.
14 changes: 7 additions & 7 deletions src/bin/js/worker_example.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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);
Expand Down
37 changes: 12 additions & 25 deletions src/bin/js/worker_interface.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
7 changes: 2 additions & 5 deletions src/bin/js/worker_interface.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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} *)
Expand Down
25 changes: 8 additions & 17 deletions src/bin/js/worker_js.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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) *)
Expand Down Expand Up @@ -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
Expand All @@ -255,15 +246,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]
}
| _ ->
Expand Down

0 comments on commit 1c9b9d4

Please sign in to comment.