From 14c3818d5608256122eb22018192e9993e175abd Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 6 Dec 2023 16:43:39 +0100 Subject: [PATCH] Splitting legacy and dolmen frontend --- src/bin/common/solving_loop.ml | 210 ++++++++++++++++----------------- 1 file changed, 105 insertions(+), 105 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 150a40084c..45a9e15c05 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -179,9 +179,8 @@ let print_solve_res loc goal_name r = exception StopProcessDecl -let main () = - let () = Dolmen_loop.Code.init [] in - +let ae_main frontend = + let filename = O.get_file () 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 @@ -284,113 +283,113 @@ let main () = { solver_ctx with ctx = cnf } end in + let (module I : Input.S) = Input.find frontend in - let ae_fe filename frontend = - let (module I : Input.S) = Input.find frontend in - - let parsed () = - try - Options.Time.start (); - if not (Options.get_timelimit_per_goal()) then - Options.Time.set_timeout (Options.get_timelimit ()); + let parsed () = + try + Options.Time.start (); + if not (Options.get_timelimit_per_goal()) then + Options.Time.set_timeout (Options.get_timelimit ()); - Signals_profiling.init_profiling (); + Signals_profiling.init_profiling (); - let with_opt (get, set) v f = - let v' = get () in - set v; - Fun.protect - ~finally:(fun () -> set v') - f - in - let with_infer_output_format = - with_opt Options.(get_infer_output_format, set_infer_output_format) - in - let with_input_format = - with_opt Options.(get_input_format, set_input_format) - in - let theory_preludes = - Options.get_theory_preludes () - |> List.to_seq - |> Seq.flat_map (fun theory -> - let filename = Theories.filename theory in - let content = Theories.content theory in - with_input_format None @@ fun () -> - with_infer_output_format false @@ fun () -> - I.parse_file - ~content - ~format:(Some (Filename.extension filename))) - in - let preludes = Options.get_preludes () in - Stdcompat.Seq.append theory_preludes @@ - I.parse_files ~filename ~preludes - with - | Util.Timeout -> - Frontend.print_status (Timeout None) 0; - exit_as_timeout () - | Parsing.Parse_error -> - (* TODO(Steven): displaying a dummy value is a bad idea. - This should only be executed with the legacy frontend, which should - be deprecated in a near future, so this code will be removed (or at - least, its behavior unspecified). *) - fatal_error - "%a" - Errors.report - (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")) - | Errors.Error e -> - fatal_error "%a" Errors.report e - in - - let all_used_context = Frontend.init_all_used_context () in - if Options.get_timelimit_per_goal() then - Frontend.print_status Preprocess 0; - let assertion_stack = Stack.create () in - let typing_loop ((state, solver_ctx) as st) p = - if O.get_parse_only () then st else begin - try - let l, env = I.type_parsed state.env assertion_stack p in - let state = { state with env } in - let solver_ctx = - List.fold_left (typed_loop all_used_context state) solver_ctx l in - state, solver_ctx - with - | Errors.Error e -> - let () = - if e != Warning_as_error then - recoverable_error "%a" Errors.report e - else - recoverable_error "" - in - st - | Exit -> exit 0 - end - in - let sat_solver = - let module SatCont = - (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer) + let with_opt (get, set) v f = + let v' = get () in + set v; + Fun.protect + ~finally:(fun () -> set v') + f in - let module TH = (val Sat_solver.get_theory ~no_th:(O.get_no_theory ())) in - (module SatCont.Make(TH) : Sat_solver_sig.S) - in - let state = { - env = I.empty_env; - (* solver_ctx = empty_solver_ctx; *) - sat_solver; - } in - try - let parsed_seq = parsed () in - let _ : _ state * solver_ctx = - Seq.fold_left - typing_loop - (state, empty_solver_ctx) - parsed_seq + let with_infer_output_format = + with_opt Options.(get_infer_output_format, set_infer_output_format) in - Options.Time.unset_timeout (); - with Util.Timeout -> + let with_input_format = + with_opt Options.(get_input_format, set_input_format) + in + let theory_preludes = + Options.get_theory_preludes () + |> List.to_seq + |> Seq.flat_map (fun theory -> + let filename = Theories.filename theory in + let content = Theories.content theory in + with_input_format None @@ fun () -> + with_infer_output_format false @@ fun () -> + I.parse_file + ~content + ~format:(Some (Filename.extension filename))) + in + let preludes = Options.get_preludes () in + Stdcompat.Seq.append theory_preludes @@ + I.parse_files ~filename ~preludes + with + | Util.Timeout -> Frontend.print_status (Timeout None) 0; exit_as_timeout () + | Parsing.Parse_error -> + (* TODO(Steven): displaying a dummy value is a bad idea. + This should only be executed with the legacy frontend, which should + be deprecated in a near future, so this code will be removed (or at + least, its behavior unspecified). *) + fatal_error + "%a" + Errors.report + (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")) + | Errors.Error e -> + fatal_error "%a" Errors.report e in + let all_used_context = Frontend.init_all_used_context () in + if Options.get_timelimit_per_goal() then + Frontend.print_status Preprocess 0; + let assertion_stack = Stack.create () in + let typing_loop ((state, solver_ctx) as st) p = + if O.get_parse_only () then st else begin + try + let l, env = I.type_parsed state.env assertion_stack p in + let state = { state with env } in + let solver_ctx = + List.fold_left (typed_loop all_used_context state) solver_ctx l in + state, solver_ctx + with + | Errors.Error e -> + let () = + if e != Warning_as_error then + recoverable_error "%a" Errors.report e + else + recoverable_error "" + in + st + | Exit -> exit 0 + end + in + let sat_solver = + let module SatCont = + (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer) + in + let module TH = (val Sat_solver.get_theory ~no_th:(O.get_no_theory ())) in + (module SatCont.Make(TH) : Sat_solver_sig.S) + in + let state = { + env = I.empty_env; + (* solver_ctx = empty_solver_ctx; *) + sat_solver; + } in + try + let parsed_seq = parsed () in + let _ : _ state * solver_ctx = + Seq.fold_left + typing_loop + (state, empty_solver_ctx) + parsed_seq + in + Options.Time.unset_timeout (); + with Util.Timeout -> + Frontend.print_status (Timeout None) 0; + exit_as_timeout () + +let dolmen_main () = + let () = Dolmen_loop.Code.init [] in + let solver_ctx_key: solver_ctx State.key = State.create_key ~pipe:"" "solving_state" in @@ -1146,7 +1145,7 @@ let main () = D_cnf.cache_decls l; st - (* When the next statement is a goal, the solver is called and provided + (* When the next statement is a goal, the solver is called and provided the goal and the current context *) | { id; contents = (`Solve _ as contents); loc ; attrs; implicit=_ } -> cmd_on_modes st [Assert; Unsat; Sat] "check-sat"; @@ -1315,8 +1314,9 @@ let main () = let bt = Printexc.get_raw_backtrace () in ignore (handle_exn st bt exn) in + d_fe (O.get_file ()) - let filename = O.get_file () in +let main () = match O.get_frontend () with - | "dolmen" -> d_fe filename - | frontend -> ae_fe filename frontend + | "dolmen" -> dolmen_main () + | frontend -> ae_main frontend