Cleaner handling of step limit (#936)

* Treating step limit as an unknown reason and not a fatal error

* Update env when step limit is reached

* Also update env in fun_sat

* Rebase artifact

* Update frontend to handle query when unknown is already decided

* Steps as a dolmen option

* Adding missing file

* Poetry

* Poetry

* Rebase artifacts

src/bin/common/parse_command.ml

@@ -362,6 +362,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
     set_fm_cross_limit fm_cross_limit;
     set_timelimit_interpretation timelimit_interpretation;
     set_steps_bound steps_bound;
+    Steps.set_steps_bound steps_bound;
     set_timelimit timelimit;
     set_timelimit_per_goal timelimit_per_goal;
     `Ok()

src/bin/common/solving_loop.ml

@@ -316,6 +316,15 @@ let main () =
     State.create_key ~pipe:"" "named_terms"
   in
 
+  let set_steps_bound i st =
+    try DO.Steps.set i st with
+      Invalid_argument _ -> (* Raised by Steps.set_steps_bound *)
+      fatal_error
+        "Error while setting steps bound to %i: current step = %i."
+        i
+        (Steps.get_steps ())
+  in
+
   let debug_parsed_pipe st c =
     if State.get State.debug st then
       Format.eprintf "[logic][parsed][%a] @[<hov>%a@]@."
@@ -477,6 +486,7 @@ let main () =
         sat;
       st
     | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux ->
+      O.set_sat_solver sat;
       (* `make_sat` returns the sat solver corresponding to the new sat_solver
          option. *)
       DO.SatSolver.set sat st
@@ -608,6 +618,12 @@ let main () =
         | Some b ->
           set_optimize b st
       end
+    | ":steps-bound", Symbol { name = Simple level; _ } ->
+      begin
+        match int_of_string_opt level with
+        | None -> print_wrn_opt ~name st_loc "integer" value; st
+        | Some i -> set_steps_bound i st
+      end
     | _ ->
       unsupported_opt name; st
   in

src/bin/js/worker_js.ml

@@ -179,13 +179,8 @@ let main worker_id content =
         raise Exit
       | Errors.Error e ->
         begin match e with
-          | Errors.Run_error r -> begin
-              match r with
-              | Steps_limit _ ->
-                returned_status :=
-                  Worker_interface.LimitReached "Steps limit"
-              | _ -> returned_status := Worker_interface.Error "Run error"
-            end
+          | Errors.Run_error _ ->
+            returned_status := Worker_interface.Error "Run error"
           | _ -> returned_status := Worker_interface.Error "Error"
         end;
         Printer.print_err "%a" Errors.report e;

src/lib/frontend/d_state_option.ml

@@ -99,6 +99,12 @@ let msatsolver =
 
 module SatSolver = (val msatsolver)
 
+let msteps =
+  let on_update _ sat st = Steps.set_steps_bound sat; st in
+  (create_opt ~on_update "steps_bound" O.get_steps_bound)
+
+module Steps = (val msteps)
+
 (* Some options can be initialized to gain some performance. *)
 let options_requiring_initialization = [
   (module SatSolverModule : S);

src/lib/frontend/d_state_option.mli

@@ -64,5 +64,11 @@ module SatSolver : S with type t = Util.sat_solver
     on SatSolver: when SatSolver is updated, this one also is. *)
 module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S)
 
+(** Option for setting the max number of steps. Interfaces with the toplevel
+    Steps module.
+    The [set] function may raise Invalid_arg from the Steps.set_steps_bound call
+    if the new option value is lower than the current number of steps. *)
+module Steps : S with type t = int
+
 (** Initializes the state with options that requires some preprocessing. *)
 val init : D_loop.Typer.state -> D_loop.Typer.state

src/lib/frontend/frontend.ml

@@ -142,7 +142,7 @@ module type S = sig
     mutable expl : Explanation.t
   }
 
-  type 'a process = ?loc : Loc.t -> env -> 'a -> unit
+  type 'a process = ?loc : Loc.t -> 'a -> env -> unit
 
   val init_env : ?sat_env:sat_env -> used_context -> env
 
@@ -226,7 +226,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     mutable expl : Explanation.t
   }
 
-  type 'a process = ?loc : Loc.t -> env -> 'a -> unit
+  type 'a process = ?loc : Loc.t -> 'a -> env -> unit
 
   let init_env ?(sat_env=SAT.empty ()) used_context =
     {
@@ -300,13 +300,14 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
     else Ex.empty
 
-  let internal_push ?(loc = Loc.dummy) (env : env) (n : int) : unit =
+  let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;
     Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
       ~max:n ~elt:(env.res, env.expl) ~init:();
+    Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n);
     SAT.push env.sat_env n
 
-  let internal_pop ?(loc = Loc.dummy) (env : env) (n : int) : unit =
+  let internal_pop ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;
     let res, expl =
       Util.loop ~f:(fun _n () _env -> Stack.pop env.consistent_dep_stack)
@@ -318,8 +319,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   let internal_assume
       ?(loc = Loc.dummy)
-      (env : env)
-      ((name, f, mf) : string * E.t * bool) =
+      ((name, f, mf) : string * E.t * bool)
+      (env : env) =
     let is_hyp = try (Char.equal '@' name.[0]) with _ -> false in
     if is_hyp || not (unused_context name env.used_context) then
       let expl =
@@ -349,13 +350,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       | `Unsat ->
         env.expl <- expl
 
-  let internal_pred_def ?(loc = Loc.dummy) env (name, f) =
+  let internal_pred_def ?(loc = Loc.dummy) (name, f) env =
     if not (unused_context name env.used_context) then
       let expl = mk_root_dep name f loc in
       SAT.pred_def env.sat_env f name expl loc;
       env.expl <- expl
 
-  let internal_query ?(loc = Loc.dummy) env (n, f, sort) =
+  let internal_query ?(loc = Loc.dummy) (n, f, sort) env =
     ignore loc;
     let expl =
       match env.res with
@@ -385,8 +386,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   let internal_th_assume
       ?(loc = Loc.dummy)
-      env
-      ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) =
+      ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt)
+      env =
     if not (unused_context ax_name env.used_context) then
       match env.res with
       | `Sat | `Unknown ->
@@ -395,8 +396,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         env.expl <- expl
       | `Unsat -> ()
 
-  let handle_sat_exn f ?loc env x =
-    try f ?loc env x with
+  let check_step_limit f env =
+    match SAT.get_unknown_reason env.sat_env with
+    | Some (Step_limit _) -> ()
+    | _ -> f env
+
+  let handle_sat_exn f ?loc x env =
+    try f ?loc x env with
     | SAT.Sat -> env.res <- `Sat
     | SAT.Unsat expl ->
       env.res <- `Unsat;
@@ -405,35 +411,54 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       env.res <- `Unknown
   (* The SAT.Timeout exception is not catched. *)
 
-  let push = handle_sat_exn internal_push
+  (* Wraps the function f to check if the step limit is reached (in which case,
+     don't do anything), and then calls the function & catches the
+     exceptions. *)
+  let wrap_f f ?loc x env =
+    check_step_limit (handle_sat_exn f ?loc x) env
+
+  let push = wrap_f internal_push
 
-  let pop = handle_sat_exn internal_pop
+  let pop = wrap_f internal_pop
 
-  let assume = handle_sat_exn internal_assume
+  let assume = wrap_f internal_assume
 
-  let pred_def = handle_sat_exn internal_pred_def
+  let pred_def = wrap_f internal_pred_def
 
-  let query = handle_sat_exn internal_query
+  let query = wrap_f internal_query
 
-  let th_assume = handle_sat_exn internal_th_assume
+  let th_assume = wrap_f internal_th_assume
 
   let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
     try
       match d.st_decl with
-      | Push n -> internal_push ~loc:d.st_loc env n
-      | Pop n -> internal_pop ~loc:d.st_loc env n
-      | Assume (n, f, mf) -> internal_assume ~loc:d.st_loc env (n, f, mf)
-      | PredDef (f, name) -> internal_pred_def ~loc:d.st_loc env (name, f)
+      | Push n -> check_step_limit (internal_push ~loc:d.st_loc n) env
+      | Pop n -> check_step_limit (internal_pop ~loc:d.st_loc n) env
+      | Assume (n, f, mf) ->
+        check_step_limit (internal_assume ~loc:d.st_loc (n, f, mf)) env
+      | PredDef (f, name) ->
+        check_step_limit (internal_pred_def ~loc:d.st_loc (name, f)) env
       | RwtDef _ -> assert false
       | Query (n, f, sort) ->
         begin
-          internal_query ~loc:d.st_loc env (n, f, sort);
-          match env.res with
-          | `Unsat ->
-            hook_on_status (Unsat (d, env.expl)) (Steps.get_steps ())
-          | _ -> assert false
+          (* If we have reached an unknown state, we can return it right
+             away. *)
+          match SAT.get_unknown_reason env.sat_env with
+          | Some (Step_limit _) -> raise SAT.I_dont_know
+          | Some _ ->
+            (* For now, only the step limit is an unknown step reachable
+               here. We could raise SAT.I_dont_know as in the previous case,
+               but we have choosen a defensive strategy. *)
+            assert false
+          | None ->
+            internal_query ~loc:d.st_loc (n, f, sort) env;
+            match env.res with
+            | `Unsat ->
+              hook_on_status (Unsat (d, env.expl)) (Steps.get_steps ())
+            | _ -> assert false
         end
-      | ThAssume th_elt -> internal_th_assume ~loc:d.st_loc env th_elt
+      | ThAssume th_elt ->
+        check_step_limit (internal_th_assume ~loc:d.st_loc th_elt) env
     with
     | SAT.Sat ->
       (* This case should mainly occur when a query has a non-unsat result,

src/lib/frontend/frontend.mli

@@ -68,7 +68,7 @@ module type S = sig
       They catch the [Sat], [Unsat] and [I_dont_know] exceptions to update the
       frontend environment, but not the [Timeout] exception which is raised to
       the user. *)
-  type 'a process = ?loc:Loc.t -> env -> 'a -> unit
+  type 'a process = ?loc:Loc.t -> 'a -> env -> unit
 
   val push : int process
 

src/lib/reasoners/fun_sat.ml

@@ -1630,7 +1630,8 @@ module Make (Th : Theory.S) = struct
                       { acc.guards with
                         current_guard = new_guard;
                         guards = guards;
-                      }})
+                      }}
+        )
       ~max:to_push
       ~elt:()
       ~init:env
@@ -1735,6 +1736,7 @@ module Make (Th : Theory.S) = struct
       assert (Ex.has_no_bj dep);
       dep
     | Util.Timeout -> model_gen_on_timeout env
+    | Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
 
   let add_guard env gf =
     let current_guard = env.guards.current_guard in
@@ -1753,6 +1755,10 @@ module Make (Th : Theory.S) = struct
       (* don't attempt to compute a model if timeout before
          calling unsat function *)
       i_dont_know env (Timeout Assume)
+    | Util.Step_limit_reached n ->
+      (* When reaching the step limit on an assume, we do not want to answer
+         'unknown' right away. *)
+      {env with unknown_reason = Some (Step_limit n)}
 
   let pred_def env f name dep _loc =
     Debug.pred_def f;

src/lib/reasoners/sat_solver_sig.ml

@@ -40,11 +40,13 @@ type timeout_reason =
 type unknown_reason =
   | Incomplete
   | Memout
+  | Step_limit of int
   | Timeout of timeout_reason
 
 let pp_unknown_reason ppf = function
   | Incomplete -> Fmt.pf ppf "Incomplete"
   | Memout -> Fmt.pf ppf "Memout"
+  | Step_limit i -> Fmt.pf ppf "Step limit: %i" i
   | Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t
 
 let pp_unknown_reason_opt ppf = function

src/lib/reasoners/sat_solver_sig.mli

@@ -36,6 +36,7 @@ type timeout_reason =
 type unknown_reason =
   | Incomplete
   | Memout
+  | Step_limit of int
   | Timeout of timeout_reason
 
 val pp_unknown_reason: unknown_reason Fmt.t

src/lib/reasoners/satml_frontend.ml

@@ -1260,11 +1260,17 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let push env to_push =
     Util.loop ~f:(fun _n () () ->
-        let expr_guard, atom_guard = create_guard env in
-        SAT.push env.satml atom_guard;
-        Stack.push expr_guard env.guards.stack_guard;
-        Steps.push_steps ();
-        env.guards.current_guard <- expr_guard
+        try
+          let expr_guard, atom_guard = create_guard env in
+          SAT.push env.satml atom_guard;
+          Stack.push expr_guard env.guards.stack_guard;
+          Steps.push_steps ();
+          env.guards.current_guard <- expr_guard
+        with
+        | Util.Step_limit_reached _ ->
+          (* This function should be called without step limit
+             (see Steps.apply_without_step_limit) *)
+          assert false
       )
       ~max:to_push
       ~elt:()
@@ -1331,12 +1337,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     assert (SAT.decision_level env.satml == 0);
     try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf])
     with | IUnsat (_env, dep) -> raise (Unsat dep)
-  (* Timeout -> I_dont_know conversions temporarily disabled
-     https://github.com/OCamlPro/alt-ergo/issues/946 *)
-  (* | Util.Timeout ->
-     (* don't attempt to compute a model if timeout before
-       calling unsat function *)
-     i_dont_know env (Timeout Assume) *)
+         (* Timeout -> I_dont_know conversions temporarily disabled
+            https://github.com/OCamlPro/alt-ergo/issues/946 *)
+         (* | Util.Timeout ->
+            (* don't attempt to compute a model if timeout before
+              calling unsat function *)
+            i_dont_know env (Timeout Assume) *)
+         | Util.Step_limit_reached n ->
+           (* When reaching the step limit on an assume, we do not want to
+              answer 'unknown' right away. *)
+           env.unknown_reason <- Some (Step_limit n)
 
   (* instrumentation of relevant exported functions for profiling *)
   let assume t ff dep =

src/lib/structures/errors.ml

@@ -81,7 +81,6 @@ type typing_error =
 
 type run_error =
   | Invalid_steps_count of int
-  | Steps_limit of int
   | Failed_check_unsat_core
   | Unsupported_feature of string
   | Dynlink_error of string
@@ -229,8 +228,6 @@ let report_typing_error fmt = function
 let report_run_error fmt = function
   | Invalid_steps_count i ->
     fprintf fmt "%d is not a valid number of steps" i
-  | Steps_limit i ->
-    fprintf fmt "Steps limit reached: %d" i
   | Failed_check_unsat_core ->
     fprintf fmt "Checking produced unsat-core failed"
   | Unsupported_feature f ->

src/lib/structures/errors.mli

@@ -88,7 +88,6 @@ type typing_error =
 (** Errors that can be raised at solving*)
 type run_error =
   | Invalid_steps_count of int
-  | Steps_limit of int
   | Failed_check_unsat_core
   | Unsupported_feature of string
   | Dynlink_error of string