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

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

@@ -334,10 +334,26 @@ let main () =
     State.create_key ~pipe:"" "sat_state"
   in
 
+  let steps_bound: int State.key =
+    State.create_key ~pipe:"" "steps-bound"
+  in
+
   let named_terms: DStd.Expr.term Util.MS.t State.key =
     State.create_key ~pipe:"" "named_terms"
   in
 
+  let set_steps_bound i st =
+    try
+      Steps.set_steps_bound i;
+      State.set steps_bound 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@]@."
@@ -471,6 +487,7 @@ let main () =
     State.empty
     |> State.set solver_ctx_key solver_ctx
     |> State.set partial_model_key partial_model
+    |> set_steps_bound (O.get_steps_bound ())
     |> State.set named_terms Util.MS.empty
     |> DO.init
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
@@ -496,6 +513,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

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/frontend.ml

@@ -302,7 +302,10 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     ignore loc;
     Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
       ~max:n ~elt:(env.res, env.expl) ~init:();
-    {env with sat_env = SAT.push env.sat_env n}
+    let sat_env =
+      Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n)
+    in
+    {env with sat_env}
 
   let internal_pop ?(loc = Loc.dummy) (env : env) (n : int) : env =
     ignore loc;
@@ -398,26 +401,37 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         {env with sat_env; expl}
       | `Unsat -> env
 
+  let check_step_limit f env =
+    match SAT.get_unknown_reason env.sat_env with
+    | Some (Step_limit _) -> env
+    | _ -> f env
+
   let handle_sat_exn f ?loc env x =
     try f ?loc env x with
     | SAT.Sat t -> {env with res = `Sat t}
     | SAT.Unsat expl -> {env with res = `Unsat; expl = Ex.union expl env.expl}
     | SAT.I_dont_know t -> {env with res = `Unknown t}
   (* 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 env x =
+    check_step_limit (fun env -> handle_sat_exn f ?loc env x) env
 
-  let pop = handle_sat_exn internal_pop
+  let push = wrap_f internal_push
 
-  let assume = handle_sat_exn internal_assume
+  let pop = wrap_f internal_pop
 
-  let pred_def = handle_sat_exn internal_pred_def
+  let assume = wrap_f internal_assume
 
-  let query = handle_sat_exn internal_query
+  let pred_def = wrap_f internal_pred_def
 
-  let th_assume = handle_sat_exn internal_th_assume
+  let query = wrap_f internal_query
 
-  let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
+  let th_assume = wrap_f internal_th_assume
+
+  let process_decl ~hook_on_status env d =
     try
       match d.st_decl with
       | Push n -> internal_push ~loc:d.st_loc env n
@@ -470,6 +484,9 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       hook_on_status (Timeout (Some d)) (Steps.get_steps ());
       raise e
 
+  let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
+    check_step_limit (fun env -> process_decl ~hook_on_status env d) env
+
   let print_model ppf env =
     match SAT.get_model env with
     | None ->

src/lib/reasoners/fun_sat.ml

@@ -1630,7 +1630,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.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) : Sat_solver_sig.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) : Sat_solver_sig.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 _ ->
+      (* When reaching the step limit on an assume, we do not want to answer
+         'unknown' right away. *)
+      env
 
   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

@@ -1278,13 +1278,19 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let push env to_push =
     Util.loop ~f:(fun _n () acc ->
-        let expr_guard, atom_guard = create_guard acc in
-        SAT.push acc.satml atom_guard;
-        Stack.push expr_guard acc.guards.stack_guard;
-        Steps.push_steps ();
-        {acc with guards =
-                    {acc.guards with
-                     current_guard = expr_guard;} }
+        try
+          let expr_guard, atom_guard = create_guard acc in
+          SAT.push acc.satml atom_guard;
+          Stack.push expr_guard acc.guards.stack_guard;
+          Steps.push_steps ();
+          {acc with guards =
+                      {acc.guards with
+                       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:()
@@ -1343,6 +1349,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       end;
       dep
     | (Util.Timeout | I_dont_know _ ) as e -> raise e
+    | Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
     | e ->
       Printer.print_dbg
         ~module_name:"Satml_frontend" ~function_name:"unsat"
@@ -1360,6 +1367,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.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 _ ->
+           (* When reaching the step limit on an assume, we do not want to
+              answer 'unknown' right away. *)
+           env
 
   (* 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

src/lib/util/steps.ml

@@ -39,6 +39,8 @@ type incr_kind =
   | Th_assumed of int  (* Increment the counter for each term assumed in the
                           theories environment *)
 
+let steps_bound = ref (Options.get_steps_bound ())
+
 let naive_steps = ref 0
 let steps = ref 0
 let mult_f = ref 0
@@ -104,17 +106,16 @@ let incr k =
         Errors.run_error (Invalid_steps_count n);
       naive_steps := !naive_steps + n;
   end;
-  let steps_bound = Options.get_steps_bound () in
-  if steps_bound <> -1
-  && ((Stdlib.compare !steps ((steps_bound)) > 0)
-      || (Stdlib.compare !naive_steps ((steps_bound)) > 0)) then
+  if !steps_bound <> -1
+  && ((Stdlib.compare !steps !steps_bound > 0)
+      || (Stdlib.compare !naive_steps !steps_bound > 0)) then
     begin
       let n =
         if !naive_steps > 0 then !naive_steps
         else if !steps > 0 then !steps
-        else steps_bound
+        else !steps_bound
       in
-      Errors.run_error (Steps_limit n)
+      raise (Util.Step_limit_reached n)
     end
 
 let reset_steps () =
@@ -158,3 +159,16 @@ let get_steps () =
 let cs_steps_cpt = ref 0
 let cs_steps () = !cs_steps_cpt
 let incr_cs_steps () = Stdlib.incr cs_steps_cpt
+
+let set_steps_bound i =
+  if get_steps () > i  && i >= 0 then invalid_arg "Steps.set_steps_bound";
+  steps_bound := i
+
+let get_steps_bound () = !steps_bound
+
+let apply_without_step_limit cont =
+  let bound = !steps_bound in
+  steps_bound := -1;
+  match cont () with
+  | res ->         steps_bound := bound; res
+  | exception e -> steps_bound := bound; raise e

src/lib/util/steps.mli

@@ -47,14 +47,20 @@ type incr_kind =
                           theories environment *)
 (** Define the type of increment *)
 
+(** Returns the max number of bounds *)
+val get_steps_bound : unit -> int
+
+(** Sets the max number of bounds *)
+val set_steps_bound : int -> unit
+
 val incr  : incr_kind -> unit
 (** Increment the number of steps depending of the incr_kind
     @raise Errors.Error.Invalid_steps_count if the number of steps is inbound
     by the --steps-bound option.
     @raise Run_error
     {!Errors.Invalid_steps_count} if the number of steps sent to the theories
      is invalid.
-    {!Errors.Steps_limit} if the number of steps is reached *)
+    @raise {!Util.Step_limit_reached} if the number of steps is reached *)
 
 val reset_steps : unit -> unit
 (** Reset the global steps counter *)
@@ -74,10 +80,13 @@ val cs_steps : unit -> int
 (** Increase the number of case-split steps *)
 val incr_cs_steps : unit -> unit
 
+(** Disables the step limit during the execution of the continuation. *)
+val apply_without_step_limit : (unit -> 'a) -> 'a
+
 (** {2 Incrementality} *)
 
 val push_steps : unit -> unit
 (** Save all the steps value in an internal stack for each push command *)
 
 val pop_steps : unit -> unit
-(** Pop the last steps value when a pop command is processed *)
+(** Pop the last steps value when a pop command is processed *)

src/lib/util/util.ml

@@ -29,6 +29,7 @@
 (**************************************************************************)
 
 exception Timeout
+exception Step_limit_reached of int
 exception Unsolvable
 
 exception Cmp of int

src/lib/util/util.mli

@@ -29,6 +29,7 @@
 (**************************************************************************)
 
 exception Timeout
+exception Step_limit_reached of int
 exception Unsolvable
 
 exception Cmp of int