Remove My_zip module (#1264)

* Use similar test for zip feature in native and SMT format

We should use the same test as we only want to check that Alt-Ergo can
unzip correctly the input file if its name has the form:
name.format.zip.

* Remove My_zip

The module `My_Zip` contains only function which is called once in
`Solving_loop`. This commit cleans the code and move it in
`Solving_loop` directly. Technically, `Solving_loop` is a part of the
binary, but as everyone knows, most of the code of this module will be
push into the library after we design a good API.

* Force deflate compression in zip tests

Add a padding comment in both tests to ensure that zip won't choose
the store method while compressing them.

src/bin/common/solving_loop.ml

@@ -305,6 +305,15 @@ let process_source ?selector_inst ~print_status src =
         end
       | `Stdin -> ()
   in
+  let extract_zip_file f =
+    let cin = Zip.open_in f in
+    Fun.protect ~finally:(fun () -> Zip.close_in cin) @@ fun () ->
+    match Zip.entries cin with
+    | [e] when not @@ e.Zip.is_directory ->
+      Zip.read_entry cin e
+    | _ ->
+      fatal_error "the zip archive '%s' should contain exactly one file" f
+  in
   (* Prepare the input source for Dolmen from an input source for Alt-Ergo. *)
   let mk_files src =
     let lang =
@@ -316,7 +325,7 @@ let process_source ?selector_inst ~print_status src =
     let src =
       match src with
       | `File path when Filename.check_suffix path ".zip" ->
-        let content = AltErgoLib.My_zip.extract_zip_file path in
+        let content = extract_zip_file path in
         `Raw (Filename.(chop_extension path |> basename), content)
       | `File _ | `Raw _ | `Stdin -> src
     in

src/lib/dune

@@ -61,7 +61,7 @@
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer
-    My_zip My_list Theories Nest Compat
+    My_list Theories Nest Compat
   )
 
  (js_of_ocaml

tests/misc/unzip.ae.expected

@@ -1,2 +1,2 @@
 
-unknown
+unsat