Removed Minisat dependency on zlib

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 3f43f3ece25b30660f3391ac79adfac81c6836c3..dc4e5d28374283324157c7ce27e240f1ddd51411 100644 (file)
--- 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/00_PATCH_mkLit_default_arg.patch b/libs/minisat/00_PATCH_mkLit_default_arg.patch
new file mode 100644 (file)
index 0000000..e21683f
--- /dev/null
+++ b/libs/minisat/00_PATCH_mkLit_default_arg.patch
@@ -0,0 +1,20 @@
+--- SolverTypes.h
++++ SolverTypes.h
+@@ -52,7 +52,7 @@ struct Lit {
+     int     x;
+ 
+     // Use this as a constructor:
+-    friend Lit mkLit(Var var, bool sign = false);
++    friend Lit mkLit(Var var, bool sign);
+ 
+     bool operator == (Lit p) const { return x == p.x; }
+     bool operator != (Lit p) const { return x != p.x; }
+@@ -60,7 +60,7 @@ struct Lit {
+ };
+ 
+ 
+-inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
++inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
+ inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
+ inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
+ inline  bool sign      (Lit p)              { return p.x & 1; }

diff --git a/libs/minisat/00_PATCH_remove_zlib.patch b/libs/minisat/00_PATCH_remove_zlib.patch
new file mode 100644 (file)
index 0000000..61a36f7
--- /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/00_UPDATE.sh b/libs/minisat/00_UPDATE.sh
new file mode 100644 (file)
index 0000000..96a34ec
--- /dev/null
+++ b/libs/minisat/00_UPDATE.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+rm -f LICENSE *.cc *.h
+git clone --depth 1 https://github.com/niklasso/minisat minisat_upstream
+rm minisat_upstream/minisat/*/Main.cc
+mv minisat_upstream/LICENSE minisat_upstream/minisat/*/*.{h,cc} .
+rm -rf minisat_upstream
+
+sed -i -e 's,^#include *"minisat/[^/]\+/\?,#include ",' *.cc *.h
+sed -i -e 's/Minisat::memUsedPeak()/Minisat::memUsedPeak(bool)/' System.cc
+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 < 00_PATCH_mkLit_default_arg.patch
+patch -p0 < 00_PATCH_remove_zlib.patch
+

diff --git a/libs/minisat/PATCH_mkLit_default_arg.patch b/libs/minisat/PATCH_mkLit_default_arg.patch
deleted file mode 100644 (file)
index e21683f..0000000
--- a/libs/minisat/PATCH_mkLit_default_arg.patch
+++ /dev/null
@@ -1,20 +0,0 @@
---- SolverTypes.h
-+++ SolverTypes.h
-@@ -52,7 +52,7 @@ struct Lit {
-     int     x;
- 
-     // Use this as a constructor:
--    friend Lit mkLit(Var var, bool sign = false);
-+    friend Lit mkLit(Var var, bool sign);
- 
-     bool operator == (Lit p) const { return x == p.x; }
-     bool operator != (Lit p) const { return x != p.x; }
-@@ -60,7 +60,7 @@ struct Lit {
- };
- 
- 
--inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
-+inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
- inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
- inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
- inline  bool sign      (Lit p)              { return p.x & 1; }

diff --git a/libs/minisat/ParseUtils.h b/libs/minisat/ParseUtils.h
index 1c9e7bf7b886210a66a0e1020c1bc511ceb04238..04911c70a5173b4e2e8e226d23fa3b768ed8e8bc 100644 (file)
--- 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(); }

diff --git a/libs/minisat/UPDATE.sh b/libs/minisat/UPDATE.sh
deleted file mode 100644 (file)
index fa72ba2..0000000
--- a/libs/minisat/UPDATE.sh
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/bin/bash
-
-rm -f LICENSE *.cc *.h
-git clone --depth 1 https://github.com/niklasso/minisat minisat_upstream
-rm minisat_upstream/minisat/*/Main.cc
-mv minisat_upstream/LICENSE minisat_upstream/minisat/*/*.{h,cc} .
-rm -rf minisat_upstream
-
-sed -i -e 's,^#include *"minisat/[^/]\+/\?,#include ",' *.cc *.h
-sed -i -e 's/Minisat::memUsedPeak()/Minisat::memUsedPeak(bool)/' System.cc
-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
-