From 2fd830334a6c00c31be1532c223ba68b01e48718 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 22 Mar 2024 18:06:59 +0100 Subject: [PATCH] Interleaving full imperative and partial imperative modes --- src/bin/common/dune | 3 +- src/bin/common/parse_command.ml | 8 ++- src/bin/common/solving_loop.ml | 103 +++++++++++++++++++++++++++----- src/lib/util/options.ml | 3 + src/lib/util/options.mli | 7 +++ 5 files changed, 107 insertions(+), 17 deletions(-) diff --git a/src/bin/common/dune b/src/bin/common/dune index 307f982a5..8cc2a2b71 100644 --- a/src/bin/common/dune +++ b/src/bin/common/dune @@ -21,7 +21,8 @@ Parse_command Input_frontend Signals_profiling - Solving_loop) + Solving_loop + Solving_loop_imperative) ) (generate_sites_module diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 5e799b7df..1b5103aa7 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -303,7 +303,7 @@ let mk_context_opt replay replay_all_used_context replay_used_context let mk_execution_opt input_format parse_only () preludes no_locs_in_answers colors_in_output no_headers_in_output no_formatting_in_output no_forced_flush_in_output pretty_output - type_only type_smt2 + type_only type_smt2 imperative_mode = let answers_with_loc = not no_locs_in_answers in let output_with_colors = colors_in_output || pretty_output in @@ -321,6 +321,7 @@ let mk_execution_opt input_format parse_only () set_type_only type_only; set_type_smt2 type_smt2; set_preludes preludes; + set_imperative_mode imperative_mode; `Ok() let mk_internal_opt @@ -744,12 +745,15 @@ let parse_execution_opt = let doc = "Stop after SMT2 typing." in Arg.(value & flag & info ["type-smt2"] ~docs ~doc) in + let imperative_smt = + let doc = "Starts Alt-Ergo in incremental mode" in + Arg.(value & flag & info ["incremental-mode"] ~docs ~doc) in Term.(ret (const mk_execution_opt $ input_format $ parse_only $ parsers $ preludes $ no_locs_in_answers $ colors_in_output $ no_headers_in_output $ no_formatting_in_output $ no_forced_flush_in_output $ - pretty_output $ type_only $ type_smt2 + pretty_output $ type_only $ type_smt2 $ imperative_smt )) let parse_halt_opt = diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 5e6628189..cf3624835 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -121,6 +121,8 @@ let add_if_named names. *) acc +type stmt = Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt + (** Translates dolmen locs to Alt-Ergo's locs *) let dl_to_ael dloc_file (compact_loc: DStd.Loc.t) = DStd.Loc.(lexing_positions (loc dloc_file compact_loc)) @@ -1139,7 +1141,20 @@ let main () = set_partial_model_and_mode solve_res st in - let handle_stmt : + let handle_reset st = + let () = Steps.reset_steps () in + st + |> State.set partial_model_key None + |> State.set solver_ctx_key empty_solver_ctx + |> State.set is_decision_env false + |> DO.Mode.clear + |> DO.Optimize.clear + |> DO.ProduceAssignment.clear + |> DO.init + |> State.set named_terms Util.MS.empty + in + + let handle_stmt_full_incremental : Frontend.used_context -> State.t -> [< Typer_Pipe.typechecked | `Check of 'a ] D_loop.Typer_Pipe.stmt -> @@ -1248,17 +1263,7 @@ let main () = st end - | {contents = `Reset; _} -> - let () = Steps.reset_steps () in - st - |> State.set partial_model_key None - |> State.set solver_ctx_key empty_solver_ctx - |> State.set is_decision_env false - |> DO.Mode.clear - |> DO.Optimize.clear - |> DO.ProduceAssignment.clear - |> DO.init - |> State.set named_terms Util.MS.empty + | {contents = `Reset; _} -> handle_reset st | {contents = `Exit; _} -> raise Exit @@ -1319,16 +1324,86 @@ let main () = "Ignoring statement: %a" Typer_Pipe.print td; st in - let handle_stmts all_context st l = + + let handle_stmts_full_incremental all_context st l = let rec aux named_map st = function | [] -> State.set named_terms named_map st | stmt :: tl -> - let st = handle_stmt all_context st stmt in + let st = handle_stmt_full_incremental all_context st stmt in let named_map = add_if_named ~acc:named_map stmt in aux named_map st tl in aux (State.get named_terms st) st l in + + let current_path_key : stmt list State.key = + State.create_key ~pipe:"" "current_path" + in + let pushed_paths_key : stmt list Vec.t State.key = + State.create_key ~pipe:"" "pushed_paths" + in + let state_get key ~default st = + try State.get key st with State.Key_not_found _ -> default + in + let get_current_path = state_get current_path_key ~default:[] in + let get_pushed_paths = state_get pushed_paths_key ~default:(Vec.create ~dummy:(Obj.magic 0)) + in + let handle_stmt_pop_reinit all_context st l = + let rec aux named_map st = function + | [] -> State.set named_terms named_map st + | (stmt: stmt) :: tl -> + begin + let current_path = get_current_path st in + match stmt with + | {contents = `Push n; _} -> + let pushed_paths = get_pushed_paths st in + for _ = 0 to n - 1 do + Vec.push pushed_paths current_path + done; + aux named_map st tl + | {contents = `Pop n; _} -> + let pushed_paths = get_pushed_paths st in + Format.eprintf "Vec size: %i@." pushed_paths.sz; + let rec pop_until until res = + if until = 0 then res else pop_until (until - 1) (Vec.pop pushed_paths) + in + let prefix = pop_until (n - 1) (Vec.pop pushed_paths) in + let st = handle_reset st in + let whole_path = List.rev_append prefix tl in + Format.eprintf "Restarting with %i instructions@." (List.length whole_path); + aux (State.get named_terms st) st whole_path + | {contents; _ } -> + let st = + let new_current_path = + match contents with + | `Clause _ + | `Decls _ + | `Defs _ + | `Hyp _ + | `Other _ + | `Reset + | `Reset_assertions + | `Set_info _ + | `Set_logic _ + | `Set_option _ -> stmt :: current_path + | _ -> current_path + in + State.set current_path_key new_current_path st + in + let st = handle_stmt_full_incremental all_context st stmt in + let named_map = add_if_named ~acc:named_map stmt in + aux named_map st tl + end + in + aux (State.get named_terms st) st l + in + let handle_stmts all_context st l = + begin + if Options.get_imperative_mode () + then handle_stmts_full_incremental + else handle_stmt_pop_reinit + end all_context st l + in let d_fe filename = let logic_file, st = mk_state filename in let () = diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 9bb1764e9..16cbc2a97 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -272,6 +272,7 @@ let preludes = ref [] let theory_preludes = ref Theories.default_preludes let type_only = ref false let type_smt2 = ref false +let imperative_mode = ref false let set_answers_with_loc b = answers_with_loc := b let set_output_with_colors b = output_with_colors := b @@ -286,6 +287,7 @@ let set_preludes p = preludes := p let set_theory_preludes t = theory_preludes := t let set_type_only b = type_only := b let set_type_smt2 b = type_smt2 := b +let set_imperative_mode i = imperative_mode := i let get_answers_with_locs () = !answers_with_loc let get_output_with_colors () = !output_with_colors @@ -299,6 +301,7 @@ let get_preludes () = !preludes let get_theory_preludes () = !theory_preludes let get_type_only () = !type_only let get_type_smt2 () = !type_smt2 +let get_imperative_mode () = !imperative_mode (** Internal options *) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 9bbbf965c..c5cbcd3d7 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -298,6 +298,9 @@ val set_triggers_var : bool -> unit (** Set [type_smt2] accessible with {!val:get_type_smt2} *) val set_type_smt2 : bool -> unit +(** Set [type_smt2] accessible with {!val:get_type_smt2} *) +val set_imperative_mode : bool -> unit + (** Set [unsat_core] accessible with {!val:get_unsat_core} *) val set_unsat_core : bool -> unit @@ -660,6 +663,10 @@ val get_type_only : unit -> bool val get_type_smt2 : unit -> bool (** Default to [false] *) +(** [true] if the program shall stop after SMT2 typing. *) +val get_imperative_mode : unit -> bool +(** Default to [false] *) + (** {4 Internal options} *) (** [true] if the GC is prevented from collecting hashconsed data structrures