Removed Minisat dependency on zlib

5 files changed, 43 insertions, 13 deletions

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 3f43f3ece..dc4e5d283 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -27,6 +27,7 @@
 #include <stdint.h>
 #include <csignal>
 #include <cinttypes>
+#include <unistd.h>
 
 #include "../minisat/Solver.h"
 #include "../minisat/SimpSolver.h"
diff --git a/libs/minisat/PATCH_mkLit_default_arg.patch b/libs/minisat/00_PATCH_mkLit_default_arg.patch
index e21683f98..e21683f98 100644
--- a/libs/minisat/PATCH_mkLit_default_arg.patch
+++ b/libs/minisat/00_PATCH_mkLit_default_arg.patch
diff --git a/libs/minisat/00_PATCH_remove_zlib.patch b/libs/minisat/00_PATCH_remove_zlib.patch
new file mode 100644
index 000000000..61a36f7e5
--- /dev/null
+++ b/libs/minisat/00_PATCH_remove_zlib.patch
@@ -0,0 +1,38 @@
+--- ParseUtils.h
++++ ParseUtils.h
+@@ -24,8 +24,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
+ #include <stdlib.h>
+ #include <stdio.h>
+ 
+-#include <zlib.h>
+-
+ #include "XAlloc.h"
+ 
+ namespace Minisat {
+@@ -36,24 +34,16 @@ namespace Minisat {
+ 
+ 
+ class StreamBuffer {
+-    gzFile         in;
+     unsigned char* buf;
+     int            pos;
+     int            size;
+ 
+     enum { buffer_size = 64*1024 };
+ 
+-    void assureLookahead() {
+-        if (pos >= size) {
+-            pos  = 0;
+-            size = gzread(in, buf, buffer_size); } }
++    virtual void assureLookahead() = 0;
+ 
+ public:
+-    explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0){
+-        buf = (unsigned char*)xrealloc(NULL, buffer_size);
+-        assureLookahead();
+-    }
+-    ~StreamBuffer() { free(buf); }
++    virtual ~StreamBuffer() { }
+ 
+     int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
+     void operator ++ ()       { pos++; assureLookahead(); }
diff --git a/libs/minisat/UPDATE.sh b/libs/minisat/00_UPDATE.sh
index fa72ba213..96a34ec93 100644
--- a/libs/minisat/UPDATE.sh
+++ b/libs/minisat/00_UPDATE.sh
@@ -12,5 +12,6 @@ sed -i -e 's/PRI[iu]64/ & /' Options.h Solver.cc
 sed -i -e '1 i #define __STDC_LIMIT_MACROS' *.cc
 sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc
 
-patch -p0 < PATCH_mkLit_default_arg.patch
+patch -p0 < 00_PATCH_mkLit_default_arg.patch
+patch -p0 < 00_PATCH_remove_zlib.patch
 
diff --git a/libs/minisat/ParseUtils.h b/libs/minisat/ParseUtils.h
index 1c9e7bf7b..04911c70a 100644
--- a/libs/minisat/ParseUtils.h
+++ b/libs/minisat/ParseUtils.h
@@ -24,8 +24,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdlib.h>
 #include <stdio.h>
 
-#include <zlib.h>
-
 #include "XAlloc.h"
 
 namespace Minisat {
@@ -36,24 +34,16 @@ namespace Minisat {
 
 
 class StreamBuffer {
-    gzFile         in;
     unsigned char* buf;
     int            pos;
     int            size;
 
     enum { buffer_size = 64*1024 };
 
-    void assureLookahead() {
-        if (pos >= size) {
-            pos  = 0;
-            size = gzread(in, buf, buffer_size); } }
+    virtual void assureLookahead() = 0;
 
 public:
-    explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0){
-        buf = (unsigned char*)xrealloc(NULL, buffer_size);
-        assureLookahead();
-    }
-    ~StreamBuffer() { free(buf); }
+    virtual ~StreamBuffer() { }
 
     int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
     void operator ++ ()       { pos++; assureLookahead(); }