From f071e0b786ea4804526f9ba98913b7509d8f59be Mon Sep 17 00:00:00 2001 From: Jeroen Bransen Date: Thu, 8 May 2014 19:21:47 +0200 Subject: [PATCH 1/4] Fix compilation for non-linux OS's --- minisat/utils/System.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc index 21aa4ff4..46faf09a 100644 --- a/minisat/utils/System.cc +++ b/minisat/utils/System.cc @@ -77,7 +77,7 @@ double Minisat::memUsed() { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_maxrss / 1024; } -double Minisat::memUsedPeak() { return memUsed(); } +double Minisat::memUsedPeak(bool) { return memUsed(); } #elif defined(__APPLE__) @@ -87,11 +87,11 @@ double Minisat::memUsed() { malloc_statistics_t t; malloc_zone_statistics(NULL, &t); return (double)t.max_size_in_use / (1024*1024); } -double Minisat::memUsedPeak() { return memUsed(); } +double Minisat::memUsedPeak(bool) { return memUsed(); } #else double Minisat::memUsed() { return 0; } -double Minisat::memUsedPeak() { return 0; } +double Minisat::memUsedPeak(bool) { return 0; } #endif From d9f3c41381ed8508746eed147dea86d9b4946590 Mon Sep 17 00:00:00 2001 From: Jeroen Bransen Date: Thu, 19 Jun 2014 09:45:33 +0200 Subject: [PATCH 2/4] Remove illigal (and not neccesary) friend definition to fix compilation on Mac OS --- minisat/core/SolverTypes.h | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h index 89986d1e..5f387d84 100644 --- a/minisat/core/SolverTypes.h +++ b/minisat/core/SolverTypes.h @@ -51,16 +51,13 @@ typedef int Var; struct Lit { int x; - // Use this as a constructor: - friend Lit mkLit(Var var, bool sign = false); - bool operator == (Lit p) const { return x == p.x; } bool operator != (Lit p) const { return x != p.x; } bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering. }; -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; } From 1258c9b2df34b0143a3d673f52fce7510396cbf8 Mon Sep 17 00:00:00 2001 From: Jeroen Bransen Date: Thu, 19 Jun 2014 10:37:20 +0200 Subject: [PATCH 3/4] Turn off compiler optimisations for MinGW because it triggers a compiler-bug --- minisat/core/Solver.cc | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 0b4f77ad..059a8889 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -18,6 +18,12 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +// It seems that we trigger a compiler bug in MinGW in the code below, so +// turn off the optimisations for now +#if defined(__MINGW32__) +#pragma GCC optimize "O0" +#endif + #include #include "minisat/mtl/Alg.h" From 4c1923b1272f9a095bff1e96cb2d7ff3894087ba Mon Sep 17 00:00:00 2001 From: Jeroen Bransen Date: Fri, 3 Jul 2015 12:08:32 +0200 Subject: [PATCH 4/4] Move StreamBuffer to separate file (such that only main depends on zlib) --- minisat/core/Dimacs.h | 1 + minisat/utils/ParseUtils.h | 36 +------------------ minisat/utils/StreamBuffer.h | 69 ++++++++++++++++++++++++++++++++++++ 3 files changed, 71 insertions(+), 35 deletions(-) create mode 100644 minisat/utils/StreamBuffer.h diff --git a/minisat/core/Dimacs.h b/minisat/core/Dimacs.h index d5db4139..a1173eb6 100644 --- a/minisat/core/Dimacs.h +++ b/minisat/core/Dimacs.h @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include "minisat/utils/ParseUtils.h" +#include "minisat/utils/StreamBuffer.h" #include "minisat/core/SolverTypes.h" namespace Minisat { diff --git a/minisat/utils/ParseUtils.h b/minisat/utils/ParseUtils.h index f31fb9ec..20673167 100644 --- a/minisat/utils/ParseUtils.h +++ b/minisat/utils/ParseUtils.h @@ -24,48 +24,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include - #include "minisat/mtl/XAlloc.h" namespace Minisat { -//------------------------------------------------------------------------------------------------- -// A simple buffered character stream class: - - - -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); } } - -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]; } - void operator ++ () { pos++; assureLookahead(); } - int position () const { return pos; } -}; - //------------------------------------------------------------------------------------------------- -// End-of-file detection functions for StreamBuffer and char*: - +// End-of-file detection functions for char*: -static inline bool isEof(StreamBuffer& in) { return *in == EOF; } static inline bool isEof(const char* in) { return *in == '\0'; } //------------------------------------------------------------------------------------------------- diff --git a/minisat/utils/StreamBuffer.h b/minisat/utils/StreamBuffer.h new file mode 100644 index 00000000..77ae5cad --- /dev/null +++ b/minisat/utils/StreamBuffer.h @@ -0,0 +1,69 @@ +/**********************************************************************************[StreamBuffer.h] +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Minisat_StreamBuffer_h +#define Minisat_StreamBuffer_h + +#include +#include + +#include + +#include "minisat/mtl/XAlloc.h" + +namespace Minisat { + +//------------------------------------------------------------------------------------------------- +// A simple buffered character stream class: + +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); } } + +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]; } + void operator ++ () { pos++; assureLookahead(); } + int position () const { return pos; } +}; + +//------------------------------------------------------------------------------------------------- +// End-of-file detection functions for StreamBuffer: + +static inline bool isEof(StreamBuffer& in) { return *in == EOF; } + +//================================================================================================= +} + +#endif