Make :reproducible-resource-limit standards-compliant

CHANGES.md

@@ -1,5 +1,19 @@
 ## unreleased
 
+ - Added support for the `:reproducible-resource-limit` and
+   `--reproducible-resource-limit` options, following the SMT-LIB standard
+   (#1353)
+
+   The reproducible resource limit was previously using a time-based limit,
+   which does not respect the reproducibility criterion outlined in the SMT-LIB
+   standard. It now defines a per-goal step limit, which applies in addition to
+   the **global** step limit (defined with `--steps-bound`), if any.
+
+   We encourage users of the global step limit (`--steps-bound`) to switch to
+   the reproducible resource limit instead.
+
+## v2.6.3
+
  - Bump minimal cmdliner version to 2.0 (#1340)
 
 ## v2.6.2

src/bin/common/parse_command.ml

@@ -395,7 +395,7 @@ let mk_internal_opt
   `Ok(gc_policy)
 
 let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
-    steps_bound timelimit timelimit_per_goal
+    steps_bound reproducible_resource_limit timelimit timelimit_per_goal
   =
   let set_limit t d =
     match t with
@@ -421,7 +421,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
     Steps.set_steps_bound steps_bound;
     set_timelimit timelimit;
     set_timelimit_per_goal timelimit_per_goal;
-    `Ok()
+    `Ok Solving_loop.{ reproducible_resource_limit }
 
 let mk_output_opt
     produce_models objectives_in_interpretation unsat_core
@@ -563,7 +563,7 @@ let get_verbose_t =
   Arg.(value & flag & info ["v"; "verbose"] ~doc)
 
 let mk_opts file () () debug_flags ddebug_flags dddebug_flags backtrace
-    rule () halt_opt (gc) () () () () () () () () =
+    rule () halt_opt (gc) limits () () () () () () () =
   Debug.mk ~verbosity:1 debug_flags;
   Debug.mk ~verbosity:2 ddebug_flags;
   Debug.mk ~verbosity:3 dddebug_flags;
@@ -591,7 +591,7 @@ let mk_opts file () () debug_flags ddebug_flags dddebug_flags backtrace
     );
 
     Gc.set { (Gc.get()) with Gc.allocation_policy = gc };
-    `Ok (Some path)
+    `Ok (Some (Solving_loop.{ path; limits}))
   end
 
 let mk_output_channel_opt regular_output diagnostic_output =
@@ -886,6 +886,12 @@ let parse_limit_opt =
     Arg.(value & opt int (get_steps_bound ()) &
          info ["S"; "steps-bound"] ~docv ~doc) in
 
+  let reproducible_resource_limit =
+    let doc = "Set the reproducible resource limit." in
+    let docv = "LIMIT" in
+    Arg.(value & opt int 0 &
+         info ["reproducible-resource-limit"] ~docv ~doc) in
+
   let timelimit =
     let doc =
       "Set the time limit to $(docv) seconds (not supported on Windows)." in
@@ -902,7 +908,8 @@ let parse_limit_opt =
 
   Term.(ret (const mk_limit_opt $
              age_bound $ fm_cross_limit $ timelimit_interpretation $
-             steps_bound $ timelimit $ timelimit_per_goal
+             steps_bound $ reproducible_resource_limit $ timelimit $
+             timelimit_per_goal
             ))
 
 let parse_output_opt =
@@ -1568,7 +1575,7 @@ let parse_cmdline_arguments () =
   at_exit Options.Output.close_all;
   let r = Cmd.eval_value main in
   match r with
-  | Ok `Ok Some path -> Solving_loop.{ path }
+  | Ok `Ok Some result -> result
   | Ok `Ok None -> raise (Exit_parse_command 0)
   | Ok `Version | Ok `Help -> exit 0
   | Error `Parse -> exit Cmd.Exit.cli_error

src/bin/common/solving_loop.ml

@@ -32,8 +32,16 @@ module DO = D_state_option
 module Sy = Symbols
 module O = Options
 
+type limits =
+  { reproducible_resource_limit : int
+  }
+
+let empty_limits =
+  { reproducible_resource_limit = 0 }
+
 type parse_result = {
   path : [`Stdin | `File of string];
+  limits : limits;
 }
 
 exception Exit_with_code of int
@@ -172,7 +180,7 @@ let interactive_prompt st =
     Some "alt-ergo>"
   | _ -> None
 
-let process_source ?selector_inst ~print_status src =
+let process_source ?selector_inst ~print_status ?(limits = empty_limits) src =
   let () = Dolmen_loop.Code.init [] in
 
   let hook_on_status status i =
@@ -184,7 +192,7 @@ let process_source ?selector_inst ~print_status src =
   in
 
   let solve (module SAT : Sat_solver_sig.S)
-      all_context (cnf, goal_name) =
+      ~limit all_context (cnf, goal_name) =
     let module FE = Frontend.Make (SAT) in
     if Options.get_debug_commands () then
       Printer.print_dbg "@[<v 2>goal %s:@ %a@]@."
@@ -203,6 +211,11 @@ let process_source ?selector_inst ~print_status src =
       let ftdn_env = FE.init_env ?selector_inst used_context in
       let () =
         try
+          (* At the moment we ignore the [Error] case here: the unknown reason
+             should have already been set internally by the solver when the
+             [Util.Step_limit_reached] exception was raised. *)
+          let ( let& ) f scope = f ~scope in
+          let& () = Steps.with_step_limit limit in
           List.iter
             (FE.process_decl ~hook_on_status ftdn_env)
             cnf
@@ -262,6 +275,10 @@ let process_source ?selector_inst ~print_status src =
     State.create_key ~pipe:"" "named_terms"
   in
 
+  let reproducible_resource_limit : int State.key =
+    State.create_key ~pipe:"" ":reproducible-resource-limit"
+  in
+
   let set_steps_bound i st =
     try DO.Steps.set i st with
       Invalid_argument _ -> (* Raised by Steps.set_steps_bound *)
@@ -475,22 +492,14 @@ let process_source ?selector_inst ~print_status src =
       st
     | ":reproducible-resource-limit", Symbol { name = Simple level; _ } ->
       begin
-        if Sys.unix then
-          match int_of_string_opt level with
-          | Some i when i > 0 ->
-            Options.set_timelimit_per_goal true;
-            Options.set_timelimit (float_of_int i /. 1000.)
-          | Some 0 ->
-            Options.set_timelimit_per_goal false;
-            Options.set_timelimit 0.
-          | None | Some _ ->
-            print_wrn_opt ~loc ~name:":reproducible-resource-limit"
-              "nonnegative integer" value
-        else
-          warning ~loc
-            "reproducible-resource-limit is only supported on Unix"
-      end;
-      st
+        match int_of_string_opt level with
+        | Some i when i >= 0 ->
+          State.set reproducible_resource_limit i st
+        | None | Some _ ->
+          print_wrn_opt ~loc ~name:":reproducible-resource-limit"
+            "nonnegative integer" value;
+          st
+      end
     | ":sat-solver", Symbol { name = Simple solver; _ } -> (
         if not (is_solver_ctx_empty (State.get solver_ctx_key st)) then (
           recoverable_error ~loc
@@ -786,6 +795,9 @@ let process_source ?selector_inst ~print_status src =
         in
         let solve_res =
           solve
+            ~limit:(
+              State.get_or ~default:limits.reproducible_resource_limit
+                reproducible_resource_limit st)
             (DO.SatSolverModule.get st)
             all_context
             (cnf, name)
@@ -967,9 +979,9 @@ let process_source ?selector_inst ~print_status src =
   in
   d_fe src
 
-let main { path } =
+let main { path ; limits } =
   try
-    process_source
+    process_source ~limits
       ~print_status:Frontend.print_status
       (path :> D_loop.State.source)
   with Exit_with_code code -> exit code

src/bin/common/solving_loop.mli

@@ -29,9 +29,14 @@ exception Exit_with_code of int
 (** Exception raised to notify that [process_source] cannot continue.
     The integer corresponds to an error code. *)
 
+type limits =
+  { reproducible_resource_limit : int
+  }
+
 type parse_result = {
   path : [`Stdin | `File of string];
   (** Path to the input file. *)
+  limits : limits;
 }
 
 val main : parse_result -> unit
@@ -40,6 +45,7 @@ val main : parse_result -> unit
 val process_source :
   ?selector_inst:(AltErgoLib.Expr.t -> bool) ->
   print_status:(AltErgoLib.Frontend.status -> int -> unit) ->
+  ?limits:limits ->
   Dolmen_loop.State.source ->
   unit
 (** [process_source ?selector_inst ~print_status src] processes the

src/lib/util/steps.ml

@@ -72,6 +72,9 @@ let pop_steps () =
   mult_a := p_mult_a;
   mult_cp := p_mult_cp
 
+let step_limit_reached n =
+  raise (Util.Step_limit_reached n)
+
 (* Multipliers are here to homogeneize the global step counter *)
 let incr k =
   begin
@@ -118,7 +121,7 @@ let incr k =
       (* CR bclement: This is preserved legacy behavior, but figure out in
          which situation we can have [n <= 0]. *)
       let n = if n > 0 then n else !steps_bound in
-      raise (Util.Step_limit_reached n)
+      step_limit_reached n
     end
 
 let reset_steps () =
@@ -169,6 +172,45 @@ let set_steps_bound i =
   if get_steps () > i  && i >= 0 then invalid_arg "Steps.set_steps_bound";
   steps_bound := i
 
+let with_step_limit limit ~scope =
+  if limit < 0 then invalid_arg "with_step_limit: limit must be nonnegative";
+  (* Note that we may not guaranteed that calling [with_step_limit] with a
+      given value inside two distinct contexts will result in exactly the same
+      limit. What we do guarantee is that calling [with_step_limit] with the
+      same value and within the same context will result in the same limit.
+      This is consistent with the requirements of the
+      [:reproducible-resource-limit] SMT-LIB option:
+
+      > the returned result should depend deterministically on n; specifically,
+      > it should be the same every time the solver is run with the same
+      > sequence of previous commands on the same machine (and with an
+      > arbitrarily long external time out). *)
+  let old_steps_bound = !steps_bound in
+  let bound_for_limit =
+    (* SMT-LIB standard: 0 disables the limit *)
+    if limit = 0
+    then old_steps_bound
+    else get_steps () + limit
+  in
+  steps_bound :=
+    (* It is not allowed to bypass an existing limit. *)
+    if old_steps_bound < 0
+    then bound_for_limit
+    else min old_steps_bound bound_for_limit;
+  match scope () with
+  | result ->
+    steps_bound := old_steps_bound;
+    result
+  | exception e ->
+    match Printexc.get_raw_backtrace () with
+    | bt ->
+      steps_bound := old_steps_bound;
+      Printexc.raise_with_backtrace e bt
+    | exception Out_of_memory ->
+      steps_bound := old_steps_bound;
+      raise e
+
+
 let get_steps_bound () = !steps_bound
 
 let apply_without_step_limit cont =

src/lib/util/steps.mli

@@ -81,6 +81,19 @@ val incr_cs_steps : unit -> unit
 (** Disables the step limit during the execution of the continuation. *)
 val apply_without_step_limit : (unit -> 'a) -> 'a
 
+(** [with_step_limit limit ~scope] calls scope with the provided [limit]. The
+    [limit] is local: only steps performed during the call to [scope] are
+    counted towards the [limit] (in particular, any steps that have already been
+    recorded are *NOT* counted towards the [limit]).
+
+    [with_step_limit] is not guaranteed to raise if the limit is reached, as the
+    [Util.Step_limit_reached] exception might be caught by [scope].
+
+    [with_step_limit] respects any current limit enforced by [set_steps_bound]
+    or another call to [with_step_limit] higher in the call stack: if a parent
+    limit would be reached, then this limit is also considered as reached. *)
+val with_step_limit : int -> scope:(unit -> 'a) -> 'a
+
 (** {2 Incrementality} *)
 
 val push_steps : unit -> unit