[compare2] Add total time for problems solved by both provers

This patch adds the number of problems that are solved by both provers
(with identical results, barring soundness issues) in the `compare2`
view, as well as the time each prover took to solve only those shared
problems.  This provides a more meaningful way of comparing different
provers' runtime.

src/core/Test_compare.ml

@@ -23,6 +23,8 @@ let cmp2sql = function
       or
       (r1.res not in ('sat', 'unsat') and r2.res not in ('sat', 'unsat'))
     |}
+  | `Solved ->
+    {| (r1.res in ('sat', 'unsat') and r1.res = r2.res) |}
   | `Mismatch ->
     {|
       r1.res in ('sat', 'unsat') and
@@ -84,6 +86,9 @@ module Short = struct
     regressed: int;
     mismatch: int;
     same: int; (* same result *)
+    solved: int; (* same solved result *)
+    old_time: float; (* same solved result *)
+    new_time: float; (* same solved result *)
   }
 
   let to_printbox (self : t) =
@@ -93,9 +98,12 @@ module Short = struct
         "appeared", int self.appeared;
         "disappeared", int self.disappeared;
         "same", int self.same;
+        "solved", int self.solved;
         "mismatch", pb_int_color Style.(fg_color Red) self.mismatch;
         "improved", pb_int_color Style.(fg_color Green) self.improved;
         "regressed", pb_int_color Style.(fg_color Cyan) self.regressed;
+        "old time (solved)", text @@ Misc.human_duration self.old_time;
+        "new time (solved)", text @@ Misc.human_duration self.new_time;
       ]
 
   let make1 ?status db p1 p2 : t =
@@ -109,6 +117,12 @@ module Short = struct
           | Some x -> x)
       |> Misc.unwrap_db (fun () -> spf "while running\n%s" q)
     in
+    let get_flt q =
+      Db.exec db q p1 p2
+        ~ty:Db.Ty.(p2 text text, p1 (nullable float), CCOpt.get_or ~default:0.)
+        ~f:Db.Cursor.get_one_exn
+      |> Misc.unwrap_db (fun () -> spf "while running\n%s" q)
+    in
     let appeared =
       get_n
         {| select count(r2.file) from db2.prover_res r2
@@ -124,14 +138,18 @@ module Short = struct
                 db2.prover_res.prover=?
                 and file = r1.file); |}
     and same = get_n (unsafe_sql ?status ~filter:`Same [ "count(r1.file)" ])
+    and solved = get_n (unsafe_sql ?status ~filter:`Solved [ "count(r1.file)" ])
+    and old_time = get_flt (unsafe_sql ?status ~filter:`Solved [ "sum(r1.rtime)" ])
+    and new_time = get_flt (unsafe_sql ?status ~filter:`Solved [ "sum(r2.rtime)" ])
     and mismatch =
       get_n (unsafe_sql ?status ~filter:`Mismatch [ "count(r1.file)" ])
     and improved =
       get_n (unsafe_sql ?status ~filter:`Improved [ "count(r1.file)" ])
     and regressed =
       get_n (unsafe_sql ?status ~filter:`Regressed [ "count(r1.file)" ])
     in
-    { appeared; disappeared; same; mismatch; improved; regressed }
+    { appeared; disappeared; same; solved; mismatch; improved; regressed
+    ; old_time ; new_time }
 
   let make_provers ?status (f1, p1) (f2, p2) : t =
     Error.guard
@@ -159,7 +177,7 @@ module Short = struct
 end
 
 module Full = struct
-  type filter = [ `Improved | `Regressed | `Mismatch | `Same ]
+  type filter = [ `Improved | `Regressed | `Mismatch | `Same | `Solved ]
   type entry = string * Res.t * float * Res.t * float
 
   let make_filtered ?(page = 0) ?(page_size = 500) ?filter ?status (f1, p1)

src/core/Test_compare.mli

@@ -12,6 +12,9 @@ module Short : sig
     regressed: int;
     mismatch: int;
     same: int; (* same result *)
+    solved: int; (* same solved result *)
+    old_time: float; (* same solved result *)
+    new_time: float; (* same solved result *)
   }
 
   val to_printbox : t -> PrintBox.t
@@ -22,7 +25,7 @@ module Short : sig
 end
 
 module Full : sig
-  type filter = [ `Improved | `Regressed | `Mismatch | `Same ]
+  type filter = [ `Improved | `Regressed | `Mismatch | `Same | `Solved ]
   type entry = string * Res.t * float * Res.t * float
 
   val make_filtered :

src/server/benchpress_server.ml

@@ -1228,12 +1228,14 @@ let handle_compare2 self : unit =
         | `Regressed -> short.regressed
         | `Mismatch -> short.mismatch
         | `Same -> short.same
+        | `Solved -> short.solved
       in
       let filter_to_string = function
         | `Improved -> "Improved"
         | `Regressed -> "Regressed"
         | `Mismatch -> "Mismatch"
         | `Same -> "Same"
+        | `Solved -> "Solved"
       in
       let short = Test_compare.Short.make_provers ?status (ff1, p1) (ff2, p2) in
       let make filter =