Skip to content

Commit

Permalink
Splitting legacy and dolmen frontend
Browse files Browse the repository at this point in the history
  • Loading branch information
@Stevendeo
Stevendeo committed Dec 6, 2023
1 parent 5c3bb0d commit 14c3818
Showing 1 changed file with 105 additions and 105 deletions.
210 changes: 105 additions & 105 deletions src/bin/common/solving_loop.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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";
Expand Down Expand Up @@ -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

0 comments on commit 14c3818

Please sign in to comment.