Tmp: steps handling

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

@@ -340,10 +340,19 @@ 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 =
+    Steps.set_steps_bound i;
+    State.set steps_bound i st
+  in
+
   let debug_parsed_pipe st c =
     if State.get State.debug st then
       Format.eprintf "[logic][parsed][%a] @[<hov>%a@]@."
@@ -457,6 +466,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
@@ -617,6 +627,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
@@ -866,6 +884,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

@@ -1301,10 +1301,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       let env = do_case_split env Util.AfterMatching in
       if ok1 || ok2 || ok3 || ok4 then env
       else
-        update_model_and_return_unknown
-          env (Options.get_last_interpretation ())
-          ~unknown_reason:Incomplete (* may becomes ModelGen *)
-
+        begin
+          update_model_and_return_unknown
+            env (Options.get_last_interpretation ())
+            ~unknown_reason:Incomplete (* may becomes ModelGen *)
+        end
   let normal_instantiation env try_greedy =
     Debug.print_nb_related env;
     let env = do_case_split env Util.BeforeMatching in
@@ -1621,16 +1622,19 @@ 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 _ -> acc)
       ~max:to_push
       ~elt:()
       ~init:env
@@ -1660,7 +1664,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
                       { acc.guards with
                         current_guard = new_current_guard;
                         guards = guards;
-                      }})
+                      }}
+        )
       ~max:to_pop
       ~elt:()
       ~init:env
@@ -1754,7 +1759,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,16 @@ 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 _ -> acc
       )
       ~max:to_push
       ~elt:()
@@ -1296,7 +1299,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           {acc with inst;
                     guards =
                       { acc.guards with
-                        current_guard = b;}})
+                        current_guard = b;}}
+        )
       ~max:to_pop
       ~elt:()
       ~init:env
@@ -1351,7 +1355,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
@@ -50,6 +52,9 @@ let mult_a = ref 0
 
 let all_steps = Stack.create ()
 
+let set_steps_bound i = steps_bound := i
+let get_steps_bound () = !steps_bound
+
 let push_steps () =
   Stack.push
     (!naive_steps,!steps,!mult_f,!mult_m,
@@ -104,15 +109,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

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,12 @@
+(set-logic ALL)
+
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (* x x) 4))
+
+; Should answer 'unknown'
+(push 1)
+(set-option :steps-bound 1)
+(check-sat)
+(get-info :reason-unknown)
+(pop 1)