Adding utils to steps for properly handling step errors

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

@@ -351,10 +351,26 @@ let main () =
     State.create_key ~pipe:"" "produce_assignment"
   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@]@."
@@ -491,6 +507,7 @@ let main () =
     |> State.set partial_model_key partial_model
     |> State.set optimize_key (O.get_optimize ())
     |> State.set produce_assignment false
+    |> set_steps_bound (O.get_steps_bound ())
     |> State.set named_terms Util.MS.empty
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
       ~size_limit ~response_file
@@ -651,6 +668,14 @@ let main () =
         | Some b ->
           set_optimize b st
       end
+    | ":steps-bound", Symbol { name = Simple n; _ } ->
+      begin
+        match int_of_string_opt n with
+        | None ->
+          print_wrn_opt ~name st_loc "integer" value;
+          st
+        | Some i -> set_steps_bound i st
+      end
     | _ ->
       unsupported_opt name; st
   in
@@ -890,6 +915,7 @@ let main () =
         |> State.set solver_ctx_key empty_solver_ctx
         |> State.set optimize_key (O.get_optimize ())
         |> State.set produce_assignment false
+        |> set_steps_bound (O.get_steps_bound ())
         |> State.set named_terms Util.MS.empty
 
       | {contents = `Exit; _} -> raise Exit

src/lib/reasoners/fun_sat.ml

@@ -1621,16 +1621,24 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         );
     Util.loop
       ~f:(fun _n () acc ->
-          let new_guard = E.fresh_name Ty.Tbool in
-          save_guard_and_refs acc new_guard;
-          let guards = ME.add new_guard
-              (mk_gf new_guard "" true true,Ex.empty)
-              acc.guards.guards in
-          {acc with guards =
-                      { acc.guards with
-                        current_guard = new_guard;
-                        guards = guards;
-                      }})
+          try
+            let new_guard = E.fresh_name Ty.Tbool in
+            save_guard_and_refs acc new_guard;
+            let guards = ME.add new_guard
+                (mk_gf new_guard "" true true,Ex.empty)
+                acc.guards.guards in
+            {acc with guards =
+                        { acc.guards with
+                          current_guard = new_guard;
+                          guards = guards;
+                        }}
+          with
+          | Util.Step_limit_reached _ ->
+            (* If we reached the step limit while pushing, we have to cancel the
+               push.
+               TODO: properly cancel the push. *)
+            env
+        )
       ~max:to_push
       ~elt:()
       ~init:env
@@ -1754,7 +1762,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 n -> i_dont_know env (Steps_limit n)
+    | 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/satml_frontend.ml

@@ -1270,13 +1270,20 @@ 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 _ ->
+          (* If we reached the step limit while pushing, we have to cancel the
+             push.
+             TODO: properly cancel the push. *)
+          env
       )
       ~max:to_push
       ~elt:()
@@ -1351,7 +1358,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 n -> i_dont_know env (Steps_limit n)
+         | 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/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,15 +106,14 @@ 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
       raise (Util.Step_limit_reached n)
     end
@@ -158,3 +159,9 @@ 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

src/lib/util/steps.mli

@@ -47,6 +47,12 @@ 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

tests/smtlib/testfile-steps-bound.dolmen.smt2

@@ -0,0 +1,22 @@
+(set-logic ALL)
+
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (* x x) 3))
+
+; Should answer 'unknown'
+(push 1)
+(set-option :steps-bound 2)
+(check-sat)
+(get-info :reason-unknown)
+(pop 1)
+
+(reset)
+
+; Should answer 'unsat'
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y Int)
+(set-option :steps-bound 100)
+(assert (= (* x x) 3))
+(check-sat)