Skip to content

Commit

Permalink
Use Dolmen in the JS worker (#1249)
Browse files Browse the repository at this point in the history 
* Add In_channel.input_all in Compat

* Use Dolmen in the Javascript Worker

This PR removes the dependency of the Javascript worker to the legacy
frontend in order to remove it completely. In order to avoid code
duplication as it was done with the legacy frontend, we reuse the
`Solving_loop` module in the worker. This requires some modifications:

- Add a new argument to the main function of `Solving_loop` to give
  different kind of sources instead of reading the file at the path
  `Options.get_file ()`. The worker used a raw string as input. I reused
  the type `Dolmen_loop.State.source`.

- Add a new argument to the main function of `Solving_loop` to pass the
  selector hook to the constructor of the environment of the SAT solver.
  This hook is not used by the worker to select instantiations but just to
  record them. I have no strong opinion to preserve this feature but I
  try to keep all the feature of the Javascript worker.

- Remove the unused `sat_env` argument of the constructor `init_env` in
  `Frontend`. This removal is mostly motivated by the fact the semantic
  of `init_env = Some env` + `selector_inst = Some f` is not clear at
  all.

- Monomophize the `status` type in `Frontend`. This status is only used
  for printting purposes but we kept the SAT environment in some of its
  constructors. Unfortunately, the type of the SAT can change at the
  very beginning of the main function of `Solving_loop`, which means it
  is not easy to add a new argument for the `hook_status`. This hook is
  required to print the result of AE in the worker.

* Fix input format in the JS example

* Simplify mk_files in `Solving_loop`

We do not need `In_channel.input_all` too ;)
  • Loading branch information
@Halbaroth
Halbaroth authored Oct 7, 2024
1 parent bbe2eaa commit bc49809
Show file tree
Hide file tree
Showing 10 changed files with 131 additions and 254 deletions.
143 changes: 66 additions & 77 deletions src/bin/common/solving_loop.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,10 +130,19 @@ type solve_res =

exception StopProcessDecl

let main () =
let process_source ?selector_inst ~print_status src =
let () = Dolmen_loop.Code.init [] in

let solve (module SAT : Sat_solver_sig.S) all_context (cnf, goal_name) =
let hook_on_status status i =
print_status status i;
match (status : Frontend.status) with
| Timeout _ when not (Options.get_timelimit_per_goal ()) ->
exit_as_timeout ()
| _ -> raise StopProcessDecl
in

let solve (module SAT : Sat_solver_sig.S)
all_context (cnf, goal_name) =
let module FE = Frontend.Make (SAT) in
if Options.get_debug_commands () then
Printer.print_dbg "@[<v 2>goal %s:@ %a@]@."
Expand All @@ -149,14 +158,7 @@ let main () =
Options.Time.set_timeout (Options.get_timelimit ());
end;
SAT.reset_refs ();
let ftdn_env = FE.init_env used_context in
let hook_on_status status i =
Frontend.print_status status i;
match status with
| Timeout _ when not (Options.get_timelimit_per_goal ()) ->
exit_as_timeout ()
| _ -> raise StopProcessDecl
in
let ftdn_env = FE.init_env ?selector_inst used_context in
let () =
try
List.iter
Expand Down Expand Up @@ -400,17 +402,6 @@ let main () =
| Some (bt, exn) -> handle_exn st bt exn
| _ -> st
in
let set_output_format fmt =
if Options.get_infer_output_format () then
match fmt with
| ".ae" -> Options.set_output_format Native
| ".smt2" -> Options.set_output_format (Smtlib2 `Latest)
| ".psmt2" -> Options.set_output_format (Smtlib2 `Poly)
| s ->
warning
"The output format %s is not supported by the Dolmen frontend."
s
in
let set_mode ?model mode st =
let st = DO.Mode.set mode st in
match mode with
Expand All @@ -429,21 +420,52 @@ let main () =
| Sat model ->
set_mode Sat ~model st
in
(* The function In_channel.input_all is not available before OCaml 4.14. *)
let read_all ch =
let b = Buffer.create 113 in
try
while true do
Buffer.add_channel b ch 30
done;
assert false
with End_of_file ->
Buffer.contents b
let set_output_format fmt =
match fmt with
| Dl.Logic.Alt_ergo ->
Options.set_output_format Native
| Dl.Logic.(Smtlib2 version) ->
Options.set_output_format (Smtlib2 version)
| _ -> ()
in
let infer_output_format src =
if Options.get_infer_output_format () then
match src with
| `File filename
| `Raw (filename, _) ->
begin match Filename.extension filename with
| ".ae" -> set_output_format Dl.Logic.Alt_ergo
| ".smt2" -> set_output_format Dl.Logic.(Smtlib2 `Latest)
| ".psmt2" -> set_output_format Dl.Logic.(Smtlib2 `Poly)
| ext ->
warning "cannot infer output format from the extension '%s'" ext
end
| `Stdin -> ()
in
(* Prepare the input source for Dolmen from an input source for Alt-Ergo. *)
let mk_files src =
let lang =
match Options.get_input_format () with
| Some Native -> Some Dl.Logic.Alt_ergo
| Some Smtlib2 version -> Some (Dl.Logic.Smtlib2 version)
| Some (Why3 | Unknown _) | None -> None
in
let src =
match src with
| `File path when Filename.check_suffix path ".zip" ->
let content = AltErgoLib.My_zip.extract_zip_file path in
`Raw (Filename.(chop_extension path |> basename), content)
| `File _ | `Raw _ | `Stdin -> src
in
infer_output_format src;
let input_file = State.mk_file ?lang "" src in
let response_file = State.mk_file "" (`Raw ("", "")) in
input_file, response_file
in
let mk_state ?(debug = false) ?(report_style = State.Contextual)
?(max_warn = max_int) ?(time_limit = Float.infinity)
?(size_limit = Float.infinity) ?(type_check = true)
?(solver_ctx = empty_solver_ctx) path =
?(solver_ctx = empty_solver_ctx) src =
let reports =
Dolmen_loop.Report.Conf.(
let disable m t =
Expand All @@ -458,45 +480,7 @@ let main () =
|> disable "shadowing"
)
in
let dir = Filename.dirname path in
let filename = Filename.basename path in
let lang =
match Options.get_input_format () with
| Some Native -> Some Dl.Logic.Alt_ergo
| Some Smtlib2 version -> Some (Dl.Logic.Smtlib2 version)
| Some (Why3 | Unknown _) | None -> None
in
let source =
if Filename.check_suffix path ".zip" then (
Filename.(chop_extension path |> extension) |> set_output_format;
let content = AltErgoLib.My_zip.extract_zip_file path in
`Raw (Filename.chop_extension filename, content))
else
let is_stdin = String.equal path "" in
let is_incremental =
match lang with
| Some (Dl.Logic.Smtlib2 _) | None -> true
| _ -> false
in
if is_stdin then (
if is_incremental then (
set_output_format ".smt2";
`Stdin
) else (
`Raw (filename, read_all stdin)
)
) else (
Filename.extension path |> set_output_format;
let cin = open_in path in
let content = read_all cin in
close_in cin;
`Raw (filename, content)
)
in
let logic_file =
State.mk_file ?lang ~loc:(Dolmen.Std.Loc.mk_file path) dir source
in
let response_file = State.mk_file dir (`Raw ("", "")) in
let logic_file, response_file = mk_files src in
logic_file,
State.empty
|> State.set solver_ctx_key solver_ctx
Expand Down Expand Up @@ -1003,8 +987,8 @@ let main () =
in
aux (State.get named_terms st) st l
in
let d_fe filename =
let logic_file, st = mk_state filename in
let d_fe src =
let logic_file, st = mk_state src in
let () = on_strict_mode (O.get_strict_mode ()) in
try
Options.with_timelimit_if (not (Options.get_timelimit_per_goal ()))
Expand Down Expand Up @@ -1046,8 +1030,13 @@ let main () =
let bt = Printexc.get_raw_backtrace () in
ignore (handle_exn st bt exn)
in

let filename = O.get_file () in
match O.get_frontend () with
| "dolmen" -> d_fe filename
| frontend -> ae_fe filename frontend
| "dolmen" -> d_fe src
| frontend -> ae_fe (O.get_file ()) frontend

let main () =
let path = Options.get_file () in
if String.equal path "" then
process_source ~print_status:Frontend.print_status `Stdin
else
process_source ~print_status:Frontend.print_status @@ (`File path)
12 changes: 11 additions & 1 deletion src/bin/common/solving_loop.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,5 +25,15 @@
(* *)
(**************************************************************************)

(** Main function solve the input problem *)
val main : unit -> unit
(** Main function solve the input problem. The processed source is given
by the file located at [Options.get_file ()]. *)

val process_source :
?selector_inst:(AltErgoLib.Expr.t -> bool) ->
print_status:(AltErgoLib.Frontend.status -> int -> unit) ->
Dolmen_loop.State.source ->
unit
(** [process_source ?selector_inst ~print_status src] processes the
input source [src] and call [print_status] on each answers.
The hook [selector_inst] allows to track generated instantiations. *)
8 changes: 8 additions & 0 deletions src/bin/js/main_text_js.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,15 @@ let parse_cmdline () =
with Parse_command.Exit_parse_command i -> exit i

let () =
(* Currently, the main function of [Solving_loop] calls the [exit] function in
case of recoverable error, which is not supported in Javascript. We
turn off this feature as we do not support it correctly. See issue
https://github.com/OCamlPro/alt-ergo/issues/1250 *)
AltErgoLib.Options.set_exit_on_error false;
register_input ();
parse_cmdline ();
AltErgoLib.Printer.init_colors ();
AltErgoLib.Printer.init_output_format ();
Signals_profiling.init_signals ();
Logs.set_reporter (AltErgoLib.Printer.reporter);
Solving_loop.main ()
7 changes: 5 additions & 2 deletions src/bin/js/worker_example.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ let exec worker file options =
let solve () =
let options =
{(Worker_interface.init_options ()) with
input_format=Some Native;
input_format = None;
file = Some "try-alt-ergo";
debug = Some true;
verbose = Some true;
Expand All @@ -82,7 +82,10 @@ let solve () =
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
let json_file =
Worker_interface.file_to_json
(Some ("dummy" ^ !extension)) (Some 42) file
in
Firebug.console##log json_file;
let json_options = Worker_interface.options_to_json options in
Firebug.console##log json_options;
Expand Down
Loading

0 comments on commit bc49809

Please sign in to comment.