Merge pull request #231 from mgudemann/feature/remove_dependency_zlib

Remove dependency zlib

Author: tautschnig

.github/workflows/pull-request-checks.yaml

@@ -111,7 +111,7 @@ jobs:
       - name: Install Packages
         run: |
           sed -i -e "s|mirrorlist=|#mirrorlist=|g" -e "s|#baseurl=http://mirror.centos.org|baseurl=http://vault.centos.org|g" /etc/yum.repos.d/CentOS-Linux-*
-          yum -y install make gcc-c++ flex bison git rpmdevtools wget zlib-devel
+          yum -y install make gcc-c++ flex bison git rpmdevtools wget
           wget --no-verbose https://github.com/ccache/ccache/releases/download/v4.8.3/ccache-4.8.3-linux-x86_64.tar.xz
           tar xJf ccache-4.8.3-linux-x86_64.tar.xz
           cp ccache-4.8.3-linux-x86_64/ccache /usr/bin/

README.md

@@ -15,8 +15,6 @@ For full information see [cprover.org](http://www.cprover.org/ebmc/).
 Compiling
 =========
 
-- Install a package that provides `zlib.h`; e.g., on Debian/Ubuntu, do `sudo apt-get install
-  zlib1g-dev`
 - initialize and update the CBMC submodule: `$> git submodule init; git submodule update`
 - download minisat: `$> make -C lib/cbmc/src minisat2-download`
 - build EBMC: `$> make -C src` (this also builds the CBMC submodule)

src/ic3/minisat/CMakeLists.txt

@@ -26,10 +26,6 @@ set(MINISAT_SOVERSION ${MINISAT_SOMAJOR})
 #--------------------------------------------------------------------------------------------------
 # Dependencies:
 
-find_package(ZLIB)
-include_directories(${ZLIB_INCLUDE_DIR})
-include_directories(${minisat_SOURCE_DIR})
-
 #--------------------------------------------------------------------------------------------------
 # Compile flags:
 
@@ -47,9 +43,6 @@ set(MINISAT_LIB_SOURCES
 add_library(minisat-lib-static STATIC ${MINISAT_LIB_SOURCES})
 add_library(minisat-lib-shared SHARED ${MINISAT_LIB_SOURCES})
 
-target_link_libraries(minisat-lib-shared ${ZLIB_LIBRARY})
-target_link_libraries(minisat-lib-static ${ZLIB_LIBRARY})
-
 add_executable(minisat_core minisat/core/Main.cc)
 add_executable(minisat_simp minisat/simp/Main.cc)
 

src/ic3/minisat/minisat/core/Main.cc

@@ -19,7 +19,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 **************************************************************************************************/
 
 #include <errno.h>
-#include <zlib.h>
 
 #include "minisat/utils/System.h"
 #include "minisat/utils/ParseUtils.h"
@@ -84,7 +83,6 @@ int main(int argc, char** argv)
         if (argc == 1)
             printf("Reading from standard input... Use '--help' for help.\n");
 
-        gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
         if (in == NULL)
             printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
 
@@ -93,7 +91,6 @@ int main(int argc, char** argv)
             printf("|                                                                             |\n"); }
 
         parse_DIMACS(in, S, (bool)strictp);
-        gzclose(in);
         FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
 
         if (S.verbosity > 0){

src/ic3/minisat/minisat/simp/Main.cc

@@ -19,7 +19,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 **************************************************************************************************/
 
 #include <errno.h>
-#include <zlib.h>
 
 #include "minisat/utils/System.h"
 #include "minisat/utils/ParseUtils.h"
@@ -88,7 +87,6 @@ int main(int argc, char** argv)
         if (argc == 1)
             printf("Reading from standard input... Use '--help' for help.\n");
 
-        gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
         if (in == NULL)
             printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
 
@@ -97,7 +95,6 @@ int main(int argc, char** argv)
             printf("|                                                                             |\n"); }
 
         parse_DIMACS(in, S, (bool)strictp);
-        gzclose(in);
         FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
 
         if (S.verbosity > 0){

src/ic3/minisat/minisat/utils/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 "minisat/mtl/XAlloc.h"
 
 namespace IctMinisat {
@@ -36,7 +34,6 @@ namespace IctMinisat {
 
 
 class StreamBuffer {
-    gzFile         in;
     unsigned char* buf;
     int            pos;
     int            size;
@@ -46,13 +43,10 @@ class StreamBuffer {
     void assureLookahead() {
         if (pos >= size) {
             pos  = 0;
-            size = gzread(in, buf, buffer_size); } }
+        }
+    }
 
 public:
-    explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0){
-        buf = (unsigned char*)xrealloc(NULL, buffer_size);
-        assureLookahead();
-    }
     ~StreamBuffer() { free(buf); }
 
     int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }