Merge pull request #18 from jbransen/master

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 <stdio.h>
 
 #include "minisat/utils/ParseUtils.h"
+#include "minisat/utils/StreamBuffer.h"
 #include "minisat/core/SolverTypes.h"
 
 namespace Minisat {

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 <math.h>
 
 #include "minisat/mtl/Alg.h"

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; }

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 <stdlib.h>
 #include <stdio.h>
 
-#include <zlib.h>
-
 #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'; }
 
 //-------------------------------------------------------------------------------------------------

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 <stdlib.h>
+#include <stdio.h>
+
+#include <zlib.h>
+
+#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

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(bool strictlyPeak) { (void) strictlyPeak; 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(bool strictlyPeak) { (void) strictlyPeak; return memUsed(); }
+double Minisat::memUsedPeak(bool) { return memUsed(); }
 
 #else
 double Minisat::memUsed()     { return 0; }
-double Minisat::memUsedPeak(bool strictlyPeak) { (void) strictlyPeak; return 0; }
+double Minisat::memUsedPeak(bool) { return 0; }
 #endif