From: Clifford Wolf Date: Fri, 25 Jul 2014 01:31:16 +0000 (+0200) Subject: Removed Minisat dependency on zlib X-Git-Tag: yosys-0.4~439 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6789e3002aadb78623b9205492d14bbafb3e39eb;p=yosys.git Removed Minisat dependency on zlib --- 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 #include #include +#include #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 index 000000000..e21683f98 --- /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 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 + #include + +-#include +- + #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 index 000000000..96a34ec93 --- /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 index e21683f98..000000000 --- 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 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 #include -#include - #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 index fa72ba213..000000000 --- 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 -