Compute elapsed time for verifying a goal (in seconds).

engine.ml

@@ -25,7 +25,14 @@ type task = {
   formula: string;
   (* Verification result.
      [None] means no verification yet. *)
-  result: (Solver.Result.t, string) Result.t option;
+  result: (task_result, string) Result.t option;
+}
+(* Result of a well-terminated task. *)
+and task_result = {
+  (* Solver result. *)
+  solver_result: Solver.Result.t;
+  (* Time elapsed to compute the result. *)
+  elapsed_time: float;
 }
 
 let check_availability solver config =
@@ -137,7 +144,7 @@ let build_command ~raw_options solver config model task =
   with Failure e ->
     Error (Format.sprintf "Unexpected failure:@ %s." e)
 
-let extract_result solver ~log ~output =
+let extract_solver_result solver ~log ~output =
   let module S = (val solver: Solver.S) in
   Logs.info (fun m -> m "Extracting result of verification.");
   let output =
@@ -192,26 +199,33 @@ let exec_tasks ~raw_options solver config model tasks_htbl =
                        ~f:(fun subgoal ->
                            Format.sprintf ", subgoal %d (%s)"
                              subgoal task.id)));
-              let res_exec_task =
+              let task_result =
                 (* Build the required command-line. *)
                 build_command ~raw_options solver config model task
                 >>= fun (cmd, prop, log, output) ->
                 (* Execute the command. *)
                 Logs.info (fun m -> m "Executing command `%s'." cmd);
                 try
+                  let start_time = Unix.gettimeofday () in
                   let retcode = Sys.command cmd in
+                  let elapsed_time = Unix.gettimeofday () -. start_time in
                   (* We extract the solver result first before looking at
                      [retcode] as the solver may crash after having produced a
                      result. *)
-                  let result = extract_result solver ~log ~output in
+                  let solver_result =
+                    extract_solver_result solver ~log ~output
+                  in
                   if retcode <> 0
-                     && Solver.Result.equal result Solver.Result.Failure
+                     && Solver.Result.equal solver_result Solver.Result.Failure
                   then
                     Error (Format.sprintf "Command `%s' has failed." cmd)
                   else begin
-                    Logs.app (fun m -> m "Result of `%s': %a."
-                                 task.id Solver.Result.pretty result);
-                    if Solver.Result.equal result Solver.Result.Failure
+                    Logs.app
+                      (fun m -> m "Result of `%s': %a (%.3fs)."
+                          task.id
+                          Solver.Result.pretty solver_result
+                          elapsed_time);
+                    if Solver.Result.equal solver_result Solver.Result.Failure
                     then
                       Logs.app (fun m ->
                           m "See error messages in `%s' for more information."
@@ -221,12 +235,12 @@ let exec_tasks ~raw_options solver config model tasks_htbl =
                       Utils.remove_on_normal_mode prop;
                       Utils.remove_on_normal_mode output;
                     end;
-                    Ok result
+                    Ok { solver_result; elapsed_time; }
                   end
                 with _ ->
                   Error "Unexpected failure."
               in
-              { task with result = Some res_exec_task; }));
+              { task with result = Some task_result; }));
   tasks_htbl
 
 let consolidate_task_results solver tasks_htbl =
@@ -234,29 +248,41 @@ let consolidate_task_results solver tasks_htbl =
   Hashtbl.map
     tasks_htbl
     ~f:(fun tasks ->
-        let consolidated_result =
-          List.fold tasks ~init:None
+        let consolidated_task_result =
+          List.fold
+            ~init:None
             ~f:(fun accum { result; _ } ->
-                let result =
+                let task_result =
                   match result with
-                  | None -> None
-                  | Some Ok result -> Some result
-                  | Some Error _ -> Some Failure
+                  | None ->
+                    None
+                  | Some Ok result ->
+                    Some (result.solver_result, result.elapsed_time)
+                  | Some Error _ ->
+                    Some (Failure, 0.)
                 in
-                match accum, result with
-                | _, None -> accum
-                | None, result -> result
-                | Some r1, Some r2 -> Some (S.consolidate r1 r2))
+                match accum, task_result with
+                | _, None ->
+                  accum
+                | None, result ->
+                  result
+                | Some (r1, t1), Some (r2, t2) ->
+                  Some (S.consolidate r1 r2, t1 +. t2))
+            tasks
         in
-        consolidated_result, tasks)
+        consolidated_task_result, tasks)
 
 let pretty_summary tasks_htbl =
   let pretty_task_status fmt { id; result; _ } =
     let result = Option.value_exn result in
     let result_string =
       match result with
-      | Ok r -> Format.asprintf "%a" Solver.Result.pretty r
-      | Error msg -> msg
+      | Ok r ->
+        Format.asprintf "%a (%.3fs)"
+          Solver.Result.pretty r.solver_result
+          r.elapsed_time
+      | Error msg ->
+        msg
     in
     Format.fprintf fmt "@[-- %s: @[<hov>%s@]@]" id result_string
   in
@@ -269,10 +295,14 @@ let pretty_summary tasks_htbl =
         (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_task_status)
         tasks
   in
-  let pretty_goal_tasks fmt (goalname, (consolidated_result, tasks)) =
-    Format.fprintf fmt "@[<v 2>- %s: @[%a@]%a@]"
+  let pretty_goal_tasks fmt (goalname, (consolidated_task_result, tasks)) =
+    let consolidated_result, consolidated_time =
+      Option.value_exn consolidated_task_result
+    in
+    Format.fprintf fmt "@[<v 2>- %s: @[%a (%.3fs)@]%a@]"
       goalname
-      Solver.Result.pretty (Option.value_exn consolidated_result)
+      Solver.Result.pretty consolidated_result
+      consolidated_time
       pretty_tasks tasks
   in
   Logs.app (fun m ->