feat(checker): ability to read .drup.gz files

src/checker/main.ml

@@ -3,8 +3,9 @@ module BL = Sidekick_bin_lib
 
 let clause_of_int_l store atoms : Drup_check.clause =
   atoms
-  |> CCList.map Drup_check.Atom.of_int_dimacs
+  |> Iter.of_list
-  |> Drup_check.Clause.of_list store
+  |> Iter.map Drup_check.Atom.of_int_dimacs
+  |> Drup_check.Clause.of_iter store
 
 let check ?pb proof : bool =
   Profile.with_ "check" @@ fun() ->
@@ -28,12 +29,7 @@ let check ?pb proof : bool =
       Error.errorf "unknown problem file extension '%s'" (Filename.extension f)
   end;
 
-  (* add proof to trace *)
+  let add_proof_from_chan ic =
-  begin match proof with
-    | f when Filename.extension f = ".drup" ->
-      Profile.with_ "parse-proof.drup" @@ fun() ->
-      CCIO.with_in f
-        (fun ic ->
     let p = BL.Drup_parser.create_chan ic in
     BL.Drup_parser.iter p
       (function
@@ -45,9 +41,28 @@ let check ?pb proof : bool =
           Drup_check.Trace.add_clause trace c
         | BL.Drup_parser.Delete c ->
           let c = clause_of_int_l cstore c in
-                 Drup_check.Trace.del_clause trace c))
+          Drup_check.Trace.del_clause trace c)
+  in
+
+  (* add proof to trace *)
+  begin match proof with
+    | f when Filename.extension f = ".drup" ->
+      (* read file *)
+      Profile.with_ "parse-proof.drup" @@ fun() ->
+      CCIO.with_in f add_proof_from_chan
+
+    | f when Filename.extension f = ".gz" ->
+      (* read compressed proof *)
+      Profile.with_ "parse-proof.drup" @@ fun() ->
+      (* TODO: more graceful failure mode here *)
+      assert (Filename.extension @@ Filename.chop_extension f = ".drup");
+      let cmd = Printf.sprintf "gzip --keep -d -c \"%s\"" f in
+      Log.debugf 1 (fun k->k"command to open proof: %s" cmd);
+      let p = Unix.open_process_in cmd in
+      CCFun.finally ~h:(fun () -> ignore (Unix.close_process_in p))
+        ~f:(fun () -> add_proof_from_chan p)
+
     | f ->
-      (* TODO: handle .drup.gz *)
       Error.errorf "unknown proof file extension '%s'" (Filename.extension f)
   end;
 

src/drup/sidekick_drup.ml

@@ -49,6 +49,7 @@ module type S = sig
     val pp : t Fmt.printer
 
     val of_list : store -> atom list -> t
+    val of_iter : store -> atom Iter.t -> t
   end
   type clause = Clause.t
 
@@ -95,6 +96,7 @@ module Make() : S = struct
         not (is_true self a) && not (is_false self a)
       let set = Bitvec.set
     end
+    module Set = CCSet.Make(CCInt)
     module Map = struct
       type 'a t = 'a Vec.t
       let create () = Vec.create ()
@@ -125,6 +127,7 @@ module Make() : S = struct
     val set_watches : t -> atom * atom -> unit
     val pp : t Fmt.printer
     val of_list : store -> atom list -> t
+    val of_iter : store -> atom Iter.t -> t
     module Set : CCSet.S with type elt = t
     module Tbl : CCHashtbl.S with type key = t
   end = struct
@@ -153,13 +156,15 @@ module Make() : S = struct
         | (p,q) -> Fmt.fprintf out "@ :watches (%a,%a)" Atom.pp p Atom.pp q in
       Fmt.fprintf out "(@[cl[%d]@ %a%a])"
         self.id (Fmt.Dump.array Atom.pp) self.atoms pp_watches self.watches
-    let of_list self atoms : t =
+    let of_iter self (atoms:atom Iter.t) : t =
       (* normalize + find in table *)
-      let atoms = List.sort_uniq Atom.compare atoms |> Array.of_list in
+      let atoms = Atom.Set.of_iter atoms |> Atom.Set.to_iter |> Iter.to_array  in
       let id = self.n in
       self.n <- 1 + self.n;
       let c = {atoms; id; watches=Atom.dummy, Atom.dummy} in
       c
+    let of_list self atoms : t = of_iter self (Iter.of_list atoms)
+
     module As_key = struct
       type nonrec t=t
       let[@inline] hash a = CCHash.int a.id