diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 2f0a5d0383..d8d9624ded 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -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 "@[goal %s:@ %a@]@." @@ -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 @@ -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 @@ -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 = @@ -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 @@ -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 ())) @@ -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) diff --git a/src/bin/common/solving_loop.mli b/src/bin/common/solving_loop.mli index cc4791656d..62c107add6 100644 --- a/src/bin/common/solving_loop.mli +++ b/src/bin/common/solving_loop.mli @@ -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. *) diff --git a/src/bin/js/main_text_js.ml b/src/bin/js/main_text_js.ml index dcd118cd35..ec82a032d9 100644 --- a/src/bin/js/main_text_js.ml +++ b/src/bin/js/main_text_js.ml @@ -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 () diff --git a/src/bin/js/worker_example.ml b/src/bin/js/worker_example.ml index 7690eb8396..2ee4bcef59 100644 --- a/src/bin/js/worker_example.ml +++ b/src/bin/js/worker_example.ml @@ -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; @@ -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; diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index 4d79920db2..e86915d99c 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -30,14 +30,6 @@ open Js_of_ocaml_lwt open Alt_ergo_common open AltErgoLib -(* Internal state while iterating over input statements *) -type 'a state = { - env : 'a; - ctx : Commands.sat_tdecl list; - local : Commands.sat_tdecl list; - global : Commands.sat_tdecl list; -} - (* If the buffer is not empty split the string in strings at each newline *) let check_buffer_content (buf, output) = Format.pp_print_flush (Options.Output.to_formatter output) (); @@ -61,7 +53,7 @@ let create_buffer () = in buf, output -let main worker_id content = +let main worker_id filename filecontent = try (* Create buffer for each formatter The content of this buffers are then retrieved and send as results *) @@ -78,24 +70,8 @@ let main worker_id content = let unsat_core = ref [] in let tbl = Hashtbl.create 53 in - - (* Initialisation *) - Input_frontend.register_legacy (); - - let module SatCont = - (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer) in - - let module TH = - (val - (if Options.get_no_theory() then (module Theory.Main_Empty : Theory.S) - else (module Theory.Main_Default : Theory.S)) : Theory.S ) in - - let module SAT = SatCont.Make(TH) in - - let module FE = Frontend.Make (SAT) in - (* Aux function used to record axioms used in instantiations *) - let add_inst orig = + let selector_inst orig = let id = Expr.uid orig in begin try incr (snd (Hashtbl.find tbl id)) @@ -104,7 +80,7 @@ let main worker_id content = true in - let get_status_and_print status n = + let print_status status n = returned_status := begin match status with | Frontend.Unsat _ -> Worker_interface.Unsat n @@ -117,95 +93,6 @@ let main worker_id content = Frontend.print_status status n in - let solve all_context (cnf, goal_name) = - let used_context = Frontend.choose_used_context all_context ~goal_name in - SAT.reset_refs (); - let sat_env = SAT.empty ~selector:add_inst () in - let ftnd_env = FE.init_env ~sat_env used_context in - List.iter - (FE.process_decl ~hook_on_status:get_status_and_print ftnd_env) - cnf; - if Options.get_unsat_core () then begin - unsat_core := Explanation.get_unsat_core ftnd_env.FE.expl; - end; - let () = - match ftnd_env.FE.res with - | `Sat | `Unknown -> - begin - if Options.(get_interpretation () && get_dump_models ()) then - FE.print_model - (Options.Output.get_fmt_models ()) - ftnd_env.sat_env; - end - | `Unsat -> () - in - () - in - - let typed_loop all_context state td = - match td.Typed.c with - | Typed.TGoal (_, kind, name, _) -> - let l = state.local @ state.global @ state.ctx in - let cnf = List.rev @@ Cnf.make l td in - let () = solve all_context (cnf, name) in - begin match kind with - | Ty.Check - | Ty.Cut -> { state with local = []; } - | Ty.Thm | Ty.Sat -> { state with global = []; local = []; } - end - | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s -> - let cnf = Cnf.make state.global td in - { state with global = cnf; } - | Typed.TAxiom (_, s, _, _) when Ty.is_local_hyp s -> - let cnf = Cnf.make state.local td in - { state with local = cnf; } - | _ -> - let cnf = Cnf.make state.ctx td in - { state with ctx = cnf; } - in - - let (module I : Input.S) = Input.find (Options.get_frontend ()) in - let parsed () = - try - Options.Time.start (); - I.parse_file ~content ~format:None - with - | Parsing.Parse_error -> - Printer.print_err "%a" Errors.report - (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")); - raise Exit - | Errors.Error e -> - begin match e with - | Errors.Run_error _ -> - returned_status := Worker_interface.Error "Run error" - | _ -> returned_status := Worker_interface.Error "Error" - end; - Printer.print_err "%a" Errors.report e; - raise Exit - in - let all_used_context = Frontend.init_all_used_context () in - let assertion_stack = Stack.create () in - let typing_loop state p = - try - let l, env = I.type_parsed state.env assertion_stack p in - List.fold_left (typed_loop all_used_context) { state with env; } l - with Errors.Error e -> - Printer.print_err "%a" Errors.report e; - raise Exit - in - - let state = { - env = I.empty_env; - ctx = []; - local = []; - global = []; - } in - - begin - try let _ : _ state = - Seq.fold_left typing_loop state (parsed ()) in () - with Exit -> () end; - let compute_statistics () = let used = List.fold_left (fun acc ({Explanation.f;_} as r) -> @@ -230,8 +117,8 @@ let main worker_id content = :: acc ) tbl [] in - - + Solving_loop.process_source + ~selector_inst ~print_status (`Raw (filename, filecontent)); (* returns a records with compatible worker_interface fields *) { Worker_interface.worker_id = worker_id; @@ -259,11 +146,12 @@ let main worker_id content = Worker_interface.diagnostic = Some [Format.asprintf "%a" Errors.report e] } - | _ -> + | exn -> let res = Worker_interface.init_results () in + let msg = Fmt.str "Unknown error: %s" (Printexc.to_string exn) in { res with Worker_interface.worker_id = worker_id; - Worker_interface.status = Error "Unknown error"; + Worker_interface.status = Error msg; } (** Worker initialisation @@ -272,24 +160,21 @@ let main worker_id content = Return a couple of list for status (one per goal) and errors *) let () = at_exit Options.Output.close_all; - Worker.set_onmessage (fun (json_file,json_options) -> + Worker.set_onmessage (fun (json_file, json_options) -> Lwt_js_events.async (fun () -> - let filename,worker_id,filecontent = - Worker_interface.file_from_json json_file in - begin match filename with - | Some fl -> Options.set_file_for_js fl - | None -> Options.set_file_for_js "" - end; + let filename_opt, worker_id, filecontent = + Worker_interface.file_from_json json_file + in let filecontent = String.concat "\n" filecontent in - (* Format.eprintf - "file content : @, %s @,@, end of file @." filecontent; *) (* Extract options and set them *) let options = Worker_interface.options_from_json json_options in Options_interface.set_options options; + Options.set_exit_on_error false; (* Run the worker on the input file (filecontent) *) - let results = main worker_id filecontent in + let filename = Option.get filename_opt in + let results = main worker_id filename filecontent in (* Convert results and returns them *) Worker.post_message (Worker_interface.results_to_json results); diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index c730a88d5f..34f858e656 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -39,11 +39,11 @@ let unused_context name context = | None -> false | Some s -> not (Util.SS.mem name s) -type 'a status = +type status = | Unsat of Commands.sat_tdecl * Ex.t | Inconsistent of Commands.sat_tdecl - | Sat of Commands.sat_tdecl * 'a - | Unknown of Commands.sat_tdecl * 'a + | Sat of Commands.sat_tdecl + | Unknown of Commands.sat_tdecl | Timeout of Commands.sat_tdecl option | Preprocess @@ -97,13 +97,13 @@ let print_status status steps = Printer.print_status_inconsistent ~validity_mode (Some loc) (Some time) (Some steps) (get_goal_name d); - | Sat (d, _) -> + | Sat d -> let loc = d.st_loc in Printer.print_status_sat ~validity_mode (Some loc) (Some time) (Some steps) (get_goal_name d); check_status_consistency status; - | Unknown (d, _) -> + | Unknown d -> let loc = d.st_loc in Printer.print_status_unknown ~validity_mode (Some loc) (Some time) (Some steps) (get_goal_name d); @@ -141,7 +141,7 @@ module type S = sig type 'a process = ?loc : Loc.t -> 'a -> env -> unit - val init_env : ?sat_env:sat_env -> used_context -> env + val init_env : ?selector_inst:(Expr.t -> bool) -> used_context -> env val push : int process @@ -158,7 +158,7 @@ module type S = sig val optimize : Objective.Function.t process val process_decl: - ?hook_on_status: (sat_env status -> int -> unit) -> + ?hook_on_status: (status -> int -> unit) -> env -> sat_tdecl -> unit @@ -227,23 +227,21 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct type 'a process = ?loc : Loc.t -> 'a -> env -> unit - let init_env ?(sat_env=SAT.empty ()) used_context = + let init_env ?selector_inst used_context = { used_context; consistent_dep_stack = Stack.create (); - sat_env; + sat_env = SAT.empty ?selector:selector_inst (); res = `Unknown; expl = Explanation.empty } let output_used_context g_name dep = - if not (Options.get_js_mode ()) then begin - let f = Options.get_used_context_file () in - let cout = open_out (sprintf "%s.%s.used" f g_name) in - let cfmt = Format.formatter_of_out_channel cout in - Ex.print_unsat_core cfmt dep; - close_out cout - end + let f = Options.get_used_context_file () in + let cout = open_out (sprintf "%s.%s.used" f g_name) in + let cfmt = Format.formatter_of_out_channel cout in + Ex.print_unsat_core cfmt dep; + close_out cout let check_produced_unsat_core dep = if get_verbose () then @@ -481,7 +479,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | SAT.Sat -> (* This case should mainly occur when a query has a non-unsat result, so we want to print the status in this case. *) - hook_on_status (Sat (d, env.sat_env)) (Steps.get_steps ()); + hook_on_status (Sat d) (Steps.get_steps ()); env.res <- `Sat | SAT.Unsat expl' -> @@ -500,7 +498,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let status = match ur with | Some (Sat_solver_sig.Timeout _) -> Timeout (Some d) - | _ -> Unknown (d, env.sat_env) + | _ -> Unknown d in hook_on_status status (Steps.get_steps ()); (* TODO: Is it an appropriate behaviour? *) diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index ec4401d027..9622bd4181 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -30,15 +30,15 @@ type used_context val init_all_used_context : unit -> used_context val choose_used_context : used_context -> goal_name:string -> used_context -type 'a status = +type status = | Unsat of Commands.sat_tdecl * Explanation.t | Inconsistent of Commands.sat_tdecl - | Sat of Commands.sat_tdecl * 'a - | Unknown of Commands.sat_tdecl * 'a + | Sat of Commands.sat_tdecl + | Unknown of Commands.sat_tdecl | Timeout of Commands.sat_tdecl option | Preprocess -val print_status : 'a status -> int -> unit +val print_status : status -> int -> unit module type S = sig @@ -59,7 +59,7 @@ module type S = sig mutable expl : Explanation.t } - val init_env : ?sat_env:sat_env -> used_context -> env + val init_env : ?selector_inst:(Expr.t -> bool) -> used_context -> env (** Process are wrappers of calls to the SAT solver. They catch the [Sat], [Unsat] and [I_dont_know] exceptions to update the @@ -82,7 +82,7 @@ module type S = sig val optimize : Objective.Function.t process val process_decl: - ?hook_on_status:(sat_env status -> int -> unit) -> + ?hook_on_status:(status -> int -> unit) -> env -> Commands.sat_tdecl -> unit diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 9f16dccb14..95916e9cb4 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -591,21 +591,18 @@ let file = ref "" let status = ref Status_Unknown let session_file = ref "" let used_context_file = ref "" -let js_mode = ref false let set_timers b = timers := b let set_status s = status := match_known_status s let set_file f = file := f let set_session_file f = session_file := f let set_used_context_file f = used_context_file := f -let set_js_mode b = js_mode := b let get_timers () = !timers || !profiling let get_file () = !file let get_status () = !status let get_session_file () = !session_file let get_used_context_file () = !used_context_file -let get_js_mode () = !js_mode (** particular getters : functions that are immediately executed **************) @@ -668,12 +665,6 @@ let with_timelimit_if cond f = (** globals **) -(* extra **) - -let set_file_for_js filename = - set_file filename; - set_js_mode true - (* Printer **) let pp_comment fmt msg = match get_output_format () with diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 892fb018c2..e33dd5bf10 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -316,9 +316,6 @@ val set_status : string -> unit (** Set [file] accessible with {!val:get_file} *) val set_file : string -> unit -(** Updates the filename to be parsed and sets a js_mode flag *) -val set_file_for_js : string -> unit - (** Setters used by parse_command *) (** Set [case_split_policy] accessible with {!val:get_case_split_policy} *) @@ -1032,10 +1029,6 @@ val get_rule : unit -> int val get_status : unit -> known_status (** Default to [Status_Unknown] *) -(** [true] if the JavaScript mode is activated *) -val get_js_mode : unit -> bool -(** Default to [false] *) - (** Value specifying the file given to Alt-Ergo *) val get_file : unit -> string (** Default to [""] *) diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 5872c9c453..ecaa42b09a 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -122,22 +122,22 @@ no errors expected. Now we check that we have a proper error message when optimizing with the Tableaux solver. - $ echo '(set-logic ALL) (maximize 1) (check-sat)' | alt-ergo --sat-solver Tableaux 2>/dev/null + $ echo '(set-logic ALL) (maximize 1) (check-sat)' | alt-ergo -i smtlib2 -o smtlib2 --sat-solver Tableaux 2>/dev/null (error "the selected solver does not support optimization") [1] - $ echo '(set-option :produce-models true) (set-logic ALL) (check-sat) (get-objectives)' | alt-ergo --sat-solver Tableaux 2>/dev/null + $ echo '(set-option :produce-models true) (set-logic ALL) (check-sat) (get-objectives)' | alt-ergo -i smtlib2 -o smtlib2 --sat-solver Tableaux 2>/dev/null unknown (error "the selected solver does not support optimization") [1] - $ echo '(set-logic ALL) (maximize 1) (check-sat)' | alt-ergo --continue-on-error --sat-solver Tableaux 2>/dev/null + $ echo '(set-logic ALL) (maximize 1) (check-sat)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error --sat-solver Tableaux 2>/dev/null (error "the selected solver does not support optimization") unknown - $ echo '(set-option :produce-models true) (set-logic ALL) (check-sat) (get-objectives)' | alt-ergo --continue-on-error --sat-solver Tableaux 2>/dev/null + $ echo '(set-option :produce-models true) (set-logic ALL) (check-sat) (get-objectives)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error --sat-solver Tableaux 2>/dev/null unknown (error "the selected solver does not support optimization")