From f199dd50a6aeece1f2aef3c83765989a7a8ea41b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 3 Apr 2019 16:55:39 -0500
Subject: [PATCH] feat: package for msat-bin, with gzip input

---
 dune             |  1 +
 msat-bin.opam    | 22 ++++++++++++++++++++++
 src/main/dune    |  5 +++--
 src/main/main.ml |  8 +++++++-
 tests/dune       |  4 ++++
 5 files changed, 37 insertions(+), 3 deletions(-)
 create mode 100644 msat-bin.opam

diff --git a/dune b/dune
index 79a54003..78c4bdf2 100644
--- a/dune
+++ b/dune
@@ -1,6 +1,7 @@
 
 (alias
  (name runtest)
+ (package msat)
  (deps README.md src/core/msat.cma src/sat/msat_sat.cma src/sudoku/sudoku_solve.exe)
  (locks test)
  (action (progn
diff --git a/msat-bin.opam b/msat-bin.opam
new file mode 100644
index 00000000..fd79290d
--- /dev/null
+++ b/msat-bin.opam
@@ -0,0 +1,22 @@
+opam-version: "2.0"
+name: "msat-bin"
+synopsis: "SAT solver binary based on the msat library"
+license: "Apache"
+version: "0.8"
+author: ["Simon Cruanes" "Guillaume Bury"]
+maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
+build: [
+  ["dune" "build" "@install" "-p" name "-j" jobs]
+  ["dune" "runtest" "-p" name "-j" jobs]
+]
+depends: [
+  "ocaml" { >= "4.03" }
+  "dune" {build}
+  "msat" { >= "0.8" < "0.9" }
+  "camlzip"
+]
+tags: [ "sat" ]
+homepage: "https://github.com/Gbury/mSAT"
+dev-repo: "git+https://github.com/Gbury/mSAT.git"
+bug-reports: "https://github.com/Gbury/mSAT/issues/"
+
diff --git a/src/main/dune b/src/main/dune
index bb0eb7d4..96d0cc4a 100644
--- a/src/main/dune
+++ b/src/main/dune
@@ -2,8 +2,9 @@
 ; main binary
 (executable
   (name main)
-  ;(package msat)
-  (libraries containers msat msat_sat msat.backend)
+  (public_name msat)
+  (package msat-bin)
+  (libraries containers camlzip msat msat.sat msat.backend)
   (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
   (ocamlopt_flags :standard -O3 -color always
                   -unbox-closures -unbox-closures-factor 20)
diff --git a/src/main/main.ml b/src/main/main.ml
index a8988f48..ddc1d856 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -73,7 +73,13 @@ let parse_file f =
   let module L = Lexing in
   CCIO.with_in f
     (fun ic ->
-       let buf = L.from_channel ic in
+       let buf =
+         if CCString.suffix ~suf:".gz" f
+         then (
+           let gic = Gzip.open_in_chan ic in
+           L.from_function (fun bytes len -> Gzip.input gic bytes 0 len)
+         ) else L.from_channel ic
+       in
        buf.L.lex_curr_p <- {buf.L.lex_curr_p with L.pos_fname=f;};
        Dimacs_parse.file Dimacs_lex.token buf)
 
diff --git a/tests/dune b/tests/dune
index 2dbfc6a6..0a32129d 100644
--- a/tests/dune
+++ b/tests/dune
@@ -9,24 +9,28 @@
 
 (alias
  (name    runtest)
+  (package msat)
  (deps    test_api.exe)
  (locks test)
  (action  (run %{deps})))
 
 (alias
  (name    runtest)
+  (package msat)
  (deps    ./icnf-solve/icnf_solve.exe Makefile (source_tree regression))
  (locks test)
  (action  (run make test-icnf)))
 
 (alias
  (name    runtest)
+  (package msat)
  (deps    ./../src/sudoku/sudoku_solve.exe Makefile (source_tree sudoku))
  (locks test)
  (action  (run make test-sudoku)))
 
 (alias
   (name runtest)
+  (package msat-bin)
   (deps   ./../src/main/main.exe ./run (source_tree .))
   (locks test)
   (action (run /usr/bin/time -f "%e" ./run sat)))