Interleaving full imperative and partial imperative modes

src/bin/common/dune

@@ -21,7 +21,8 @@
    Parse_command
    Input_frontend
    Signals_profiling
-   Solving_loop)
+   Solving_loop
+   Solving_loop_imperative)
 )
 
 (generate_sites_module

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 =

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 () =

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 *)
 

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