Merge pull request #75 from bclement-ocp/bclement/comparesat

Add support for comparing results with a specific status

src/core/Test_compare.ml

@@ -2,6 +2,7 @@ open Common
 
 type filename = string
 type prover = filename * Prover.name
+type status = [ `Sat | `Unsat ]
 
 let pb_v_record = Test.pb_v_record
 let pb_int_color = Test.pb_int_color
@@ -35,6 +36,12 @@ let cmp2sql = function
 
 let pp_cmp = Fmt.of_to_string cmp2sql
 
+let status_to_sql = function
+  | `Sat -> {| (r1.res = 'sat' or r2.res = 'sat') |}
+  | `Unsat -> {| (r1.res = 'unsat' or r2.res = 'unsat') |}
+
+let pp_status_sql = Fmt.of_to_string status_to_sql
+
 let pp_opt ?(none = Fmt.const_string "") pp ppf = function
   | None -> none ppf ()
   | Some v -> pp ppf v
@@ -43,12 +50,13 @@ let pp_prefix prefix pp ppf v =
   Fmt.fprintf ppf "%s" prefix;
   pp ppf v
 
-let unsafe_sql ?order ?limit ?offset ?filter select =
+let unsafe_sql ?order ?limit ?offset ?filter ?status select =
   let pp_filter ppf filter =
     match filter with
     | None -> ()
     | Some filter -> Format.fprintf ppf "and (%a)" pp_cmp filter
   in
+  let pp_status = pp_opt (pp_prefix " and " pp_status_sql) in
   let pp_select =
     Fmt.list
       ~sep:(fun ppf () -> Fmt.fprintf ppf ",@,")
@@ -58,9 +66,9 @@ let unsafe_sql ?order ?limit ?offset ?filter select =
     {| select %a
         from db1.prover_res r1
         inner join db2.prover_res r2 on r2.file = r1.file
-        where r1.prover = ? and r2.prover = ? %a %a %a %a
+        where r1.prover = ? and r2.prover = ? %a %a %a %a %a
       |}
-    pp_select select pp_filter filter
+    pp_select select pp_filter filter pp_status status
     (pp_opt (pp_prefix " order by " Fmt.string))
     order
     (pp_opt (pp_prefix " limit " Fmt.int))
@@ -90,7 +98,7 @@ module Short = struct
         "regressed", pb_int_color Style.(fg_color Cyan) self.regressed;
       ]
 
-  let make1 db p1 p2 : t =
+  let make1 ?status db p1 p2 : t =
     (* Note: first ? is p1, second ? is p2 *)
     let get_n q =
       Db.exec db q p1 p2
@@ -115,20 +123,22 @@ module Short = struct
                 and not exists (select file from db2.prover_res where
                 db2.prover_res.prover=?
                 and file = r1.file); |}
-    and same = get_n (unsafe_sql ~filter:`Same [ "count(r1.file)" ])
-    and mismatch = get_n (unsafe_sql ~filter:`Mismatch [ "count(r1.file)" ])
-    and improved = get_n (unsafe_sql ~filter:`Improved [ "count(r1.file)" ])
+    and same = get_n (unsafe_sql ?status ~filter:`Same [ "count(r1.file)" ])
+    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 ~filter:`Regressed [ "count(r1.file)" ])
+      get_n (unsafe_sql ?status ~filter:`Regressed [ "count(r1.file)" ])
     in
     { appeared; disappeared; same; mismatch; improved; regressed }
 
-  let make_provers (f1, p1) (f2, p2) : t =
+  let make_provers ?status (f1, p1) (f2, p2) : t =
     Error.guard
       (Error.wrapf "short comparison of '%s/%s' and '%s/%s'" f1 p1 f2 p2)
-    @@ fun () -> make1 (make_db f1 f2) p1 p2
+    @@ fun () -> make1 ?status (make_db f1 f2) p1 p2
 
-  let make f1 f2 : (_ * t) list =
+  let make ?status f1 f2 : (_ * t) list =
     Error.guard (Error.wrapf "short comparison of '%s' and '%s'" f1 f2)
     @@ fun () ->
     let db = Sqlite3.db_open ":memory:" in
@@ -145,19 +155,20 @@ module Short = struct
       |> Misc.unwrap_db (fun () -> "listing all provers")
     in
     Logs.debug (fun k -> k "provers: [%s]" (String.concat ";" provers));
-    CCList.map (fun prover -> prover, make1 db prover prover) provers
+    CCList.map (fun prover -> prover, make1 ?status db prover prover) provers
 end
 
 module Full = struct
   type filter = [ `Improved | `Regressed | `Mismatch | `Same ]
   type entry = string * Res.t * float * Res.t * float
 
-  let make_filtered ?(page = 0) ?(page_size = 500) ?filter (f1, p1) (f2, p2) =
+  let make_filtered ?(page = 0) ?(page_size = 500) ?filter ?status (f1, p1)
+      (f2, p2) =
     let tags = [] (* TODO? *) in
     let offset = page * page_size in
     let limit = page_size + 1 in
     Db.exec (make_db f1 f2)
-      (unsafe_sql ~order:"r1.file desc" ~limit ~offset ?filter
+      (unsafe_sql ~order:"r1.file desc" ~limit ~offset ?filter ?status
          [ "r1.file"; "r1.res"; "r2.res"; "r1.rtime"; "r2.rtime" ])
       p1 p2
       ~ty:

src/core/Test_compare.mli

@@ -2,6 +2,7 @@
 
 type filename = string
 type prover = filename * Prover.name
+type status = [ `Sat | `Unsat ]
 
 module Short : sig
   type t = {
@@ -14,9 +15,9 @@ module Short : sig
   }
 
   val to_printbox : t -> PrintBox.t
-  val make : filename -> filename -> (Prover.name * t) list
+  val make : ?status:status -> filename -> filename -> (Prover.name * t) list
 
-  val make_provers : prover -> prover -> t
+  val make_provers : ?status:status -> prover -> prover -> t
   (** Make a single comparison between two provers in (possibly) different files *)
 end
 
@@ -28,6 +29,7 @@ module Full : sig
     ?page:int ->
     ?page_size:int ->
     ?filter:filter ->
+    ?status:status ->
     prover ->
     prover ->
     entry list

src/server/benchpress_server.ml

@@ -1154,6 +1154,14 @@ let handle_compare2 self : unit =
           None)
     @@ H.Request.query req
   in
+  let status =
+    match
+      String.lowercase_ascii @@ List.assoc "status" (H.Request.query req)
+    with
+    | "sat" -> Some `Sat
+    | "unsat" -> Some `Unsat
+    | _ | (exception Not_found) -> None
+  in
   (* H.Request.query reverses the query order, so we have to reverse it again *)
   let provers = List.rev provers in
   let prover1, prover2 =
@@ -1183,6 +1191,30 @@ let handle_compare2 self : unit =
   in
   let options1 = CCList.mapi (mk_entry ?selected:prover1) entries in
   let options2 = CCList.mapi (mk_entry ?selected:prover2) entries in
+  let status_opt_to_string = function
+    | Some `Sat -> "sat"
+    | Some `Unsat -> "unsat"
+    | None -> ""
+  in
+  let status_option ?current status =
+    let open Html in
+    let attrs =
+      A.value (status_opt_to_string status)
+      ::
+      (if current = Some status then
+        [ A.selected "selected" ]
+      else
+        [])
+    in
+    option attrs [ txt (status_opt_to_string status) ]
+  in
+  let ostatus =
+    [
+      status_option None;
+      status_option ~current:status (Some `Unsat);
+      status_option ~current:status (Some `Sat);
+    ]
+  in
   let prover_info =
     let file_link fname text =
       PrintBox.link ~uri:(uri_get_file fname) (PrintBox.text text)
@@ -1203,7 +1235,7 @@ let handle_compare2 self : unit =
         | `Mismatch -> "Mismatch"
         | `Same -> "Same"
       in
-      let short = Test_compare.Short.make_provers (ff1, p1) (ff2, p2) in
+      let short = Test_compare.Short.make_provers ?status (ff1, p1) (ff2, p2) in
       let make filter =
         let total = get short filter in
         let page_size = min total 500 in
@@ -1220,8 +1252,8 @@ let handle_compare2 self : unit =
                 [
                   summary []
                     [ txtf "%s (%s)" (filter_to_string filter) limit_info ];
-                  Test_compare.Full.make_filtered ~page_size ~filter (ff1, p1)
-                    (ff2, p2)
+                  Test_compare.Full.make_filtered ?status ~page_size ~filter
+                    (ff1, p1) (ff2, p2)
                   |> Test_compare.Full.to_printbox ~file_link
                   |> Html.pb_html;
                 ]);
@@ -1242,17 +1274,41 @@ let handle_compare2 self : unit =
         |> String.concat "," |> gnuplot_img;
       ]
   in
+  let plot_html =
+    if Option.is_none status then
+      plot_html
+    else
+      Html.(
+        strong []
+          [ txt "Warning: this plot includes BOTH sat and unsat results." ])
+      :: plot_html
+  in
   let html =
     let open Html in
     mk_page ~title:"compare2"
       ([
          mk_navigation [ "/compare2/", "compare", true ];
          h3 [] [ txt "compare" ];
-         form []
+         form
+           [ A.class_ "container" ]
            [
-             select [ A.name "prover[]" ] options1;
-             select [ A.name "prover[]" ] options2;
-             mk_button ~cls:"btn-primary btn-sm" [] [ txt "Compare" ];
+             div
+               [ A.class_ "row" ]
+               [
+                 div
+                   [ A.class_ "col-6" ]
+                   [
+                     select [ A.name "prover[]" ] options1;
+                     select [ A.name "prover[]" ] options2;
+                     mk_button ~cls:"btn-primary btn-sm" [] [ txt "Compare" ];
+                   ];
+                 div
+                   [ A.class_ "col-3" ]
+                   [
+                     Html.label [] [ Html.txt "Limit to:" ];
+                     select [ A.name "status" ] ostatus;
+                   ];
+               ];
            ];
        ]
       @ prover_info