summaryrefslogtreecommitdiff
path: root/libs/minisat
diff options
context:
space:
mode:
authorRuben Undheim <ruben.undheim@gmail.com>2018-08-30 20:46:20 +0200
committerRuben Undheim <ruben.undheim@gmail.com>2018-08-30 20:46:20 +0200
commit5033b51947a6ef02cb785b5622e993335efa750a (patch)
tree7bed18c526bd94917fa2f08e3df12209863698a1 /libs/minisat
parentfefe0fc0430f4f173a25e674708aa0f4f0854b31 (diff)
New upstream version 0.7+20180830git0b7a184
Diffstat (limited to 'libs/minisat')
-rw-r--r--libs/minisat/00_PATCH_no_fpu_control.patch43
-rw-r--r--libs/minisat/00_PATCH_remove_zlib.patch17
-rw-r--r--libs/minisat/00_PATCH_typofixes.patch20
-rwxr-xr-x[-rw-r--r--]libs/minisat/00_UPDATE.sh6
-rw-r--r--libs/minisat/Dimacs.h8
-rw-r--r--libs/minisat/Options.cc4
-rw-r--r--libs/minisat/SimpSolver.cc4
-rw-r--r--libs/minisat/Solver.cc4
-rw-r--r--libs/minisat/System.cc15
-rw-r--r--libs/minisat/System.h7
10 files changed, 104 insertions, 24 deletions
diff --git a/libs/minisat/00_PATCH_no_fpu_control.patch b/libs/minisat/00_PATCH_no_fpu_control.patch
new file mode 100644
index 00000000..6c754b1e
--- /dev/null
+++ b/libs/minisat/00_PATCH_no_fpu_control.patch
@@ -0,0 +1,43 @@
+--- System.cc
++++ System.cc
+@@ -97,17 +97,6 @@ double Minisat::memUsedPeak(bool) { return 0; }
+ #endif
+
+
+-void Minisat::setX86FPUPrecision()
+-{
+-#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
+- // Only correct FPU precision on Linux architectures that needs and supports it:
+- fpu_control_t oldcw, newcw;
+- _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+- printf("WARNING: for repeatability, setting FPU to use double precision\n");
+-#endif
+-}
+-
+-
+ #if !defined(_MSC_VER) && !defined(__MINGW32__)
+ void Minisat::limitMemory(uint64_t max_mem_mb)
+ {
+--- System.h
++++ System.h
+@@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
+ #ifndef Minisat_System_h
+ #define Minisat_System_h
+
+-#if defined(__linux__)
+-#include <fpu_control.h>
+-#endif
+-
+ #include "IntTypes.h"
+
+ //-------------------------------------------------------------------------------------------------
+@@ -36,9 +32,6 @@ static inline double cpuTime(void); // CPU-time in seconds.
+ extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures).
+ extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures).
+
+-extern void setX86FPUPrecision(); // Make sure double's are represented with the same precision
+- // in memory and registers.
+-
+ extern void limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact
+ // semantics varies depending on architecture.
+
diff --git a/libs/minisat/00_PATCH_remove_zlib.patch b/libs/minisat/00_PATCH_remove_zlib.patch
index 61a36f7e..068356b7 100644
--- a/libs/minisat/00_PATCH_remove_zlib.patch
+++ b/libs/minisat/00_PATCH_remove_zlib.patch
@@ -36,3 +36,20 @@
int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
void operator ++ () { pos++; assureLookahead(); }
+--- Dimacs.h
++++ Dimacs.h
+@@ -76,10 +76,10 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) {
+
+ // Inserts problem into solver.
+ //
+-template<class Solver>
+-static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+- StreamBuffer in(input_stream);
+- parse_DIMACS_main(in, S, strictp); }
++//template<class Solver>
++//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
++// StreamBuffer in(input_stream);
++// parse_DIMACS_main(in, S, strictp); }
+
+ //=================================================================================================
+ }
diff --git a/libs/minisat/00_PATCH_typofixes.patch b/libs/minisat/00_PATCH_typofixes.patch
new file mode 100644
index 00000000..175f483b
--- /dev/null
+++ b/libs/minisat/00_PATCH_typofixes.patch
@@ -0,0 +1,20 @@
+--- Solver.h
++++ Solver.h
+@@ -103,7 +103,7 @@ public:
+ int nFreeVars () const;
+ void printStats () const; // Print some current statistics to standard output.
+
+- // Resource contraints:
++ // Resource constraints:
+ //
+ void setConfBudget(int64_t x);
+ void setPropBudget(int64_t x);
+@@ -230,7 +230,7 @@ protected:
+ double learntsize_adjust_confl;
+ int learntsize_adjust_cnt;
+
+- // Resource contraints:
++ // Resource constraints:
+ //
+ int64_t conflict_budget; // -1 means no budget.
+ int64_t propagation_budget; // -1 means no budget.
diff --git a/libs/minisat/00_UPDATE.sh b/libs/minisat/00_UPDATE.sh
index 96a34ec9..ea26215a 100644..100755
--- a/libs/minisat/00_UPDATE.sh
+++ b/libs/minisat/00_UPDATE.sh
@@ -9,9 +9,11 @@ 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
+sed -i -e '1 i #ifndef __STDC_LIMIT_MACROS\n#define __STDC_LIMIT_MACROS\n#endif' *.cc
+sed -i -e '1 i #ifndef __STDC_FORMAT_MACROS\n#define __STDC_FORMAT_MACROS\n#endif' *.cc
patch -p0 < 00_PATCH_mkLit_default_arg.patch
patch -p0 < 00_PATCH_remove_zlib.patch
+patch -p0 < 00_PATCH_no_fpu_control.patch
+patch -p0 < 00_PATCH_typofixes.patch
diff --git a/libs/minisat/Dimacs.h b/libs/minisat/Dimacs.h
index ccfa1c01..61b9d3ca 100644
--- a/libs/minisat/Dimacs.h
+++ b/libs/minisat/Dimacs.h
@@ -76,10 +76,10 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) {
// Inserts problem into solver.
//
-template<class Solver>
-static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
- StreamBuffer in(input_stream);
- parse_DIMACS_main(in, S, strictp); }
+//template<class Solver>
+//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+// StreamBuffer in(input_stream);
+// parse_DIMACS_main(in, S, strictp); }
//=================================================================================================
}
diff --git a/libs/minisat/Options.cc b/libs/minisat/Options.cc
index 1aff3fab..5c45dd6a 100644
--- a/libs/minisat/Options.cc
+++ b/libs/minisat/Options.cc
@@ -1,5 +1,9 @@
+#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
#define __STDC_LIMIT_MACROS
+#endif
/**************************************************************************************[Options.cc]
Copyright (c) 2008-2010, Niklas Sorensson
diff --git a/libs/minisat/SimpSolver.cc b/libs/minisat/SimpSolver.cc
index fd5774e0..7348a905 100644
--- a/libs/minisat/SimpSolver.cc
+++ b/libs/minisat/SimpSolver.cc
@@ -1,5 +1,9 @@
+#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
#define __STDC_LIMIT_MACROS
+#endif
/***********************************************************************************[SimpSolver.cc]
Copyright (c) 2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
diff --git a/libs/minisat/Solver.cc b/libs/minisat/Solver.cc
index ab476853..f6d4fb5a 100644
--- a/libs/minisat/Solver.cc
+++ b/libs/minisat/Solver.cc
@@ -1,5 +1,9 @@
+#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
#define __STDC_LIMIT_MACROS
+#endif
/***************************************************************************************[Solver.cc]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc
index febe3b40..1921a1d7 100644
--- a/libs/minisat/System.cc
+++ b/libs/minisat/System.cc
@@ -1,5 +1,9 @@
+#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
#define __STDC_LIMIT_MACROS
+#endif
/***************************************************************************************[System.cc]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
@@ -97,17 +101,6 @@ double Minisat::memUsedPeak(bool) { return 0; }
#endif
-void Minisat::setX86FPUPrecision()
-{
-#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
- // Only correct FPU precision on Linux architectures that needs and supports it:
- fpu_control_t oldcw, newcw;
- _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
- printf("WARNING: for repeatability, setting FPU to use double precision\n");
-#endif
-}
-
-
#if !defined(_MSC_VER) && !defined(__MINGW32__)
void Minisat::limitMemory(uint64_t max_mem_mb)
{
diff --git a/libs/minisat/System.h b/libs/minisat/System.h
index ee92a6e0..cd9d020c 100644
--- a/libs/minisat/System.h
+++ b/libs/minisat/System.h
@@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef Minisat_System_h
#define Minisat_System_h
-#if defined(__linux__)
-#include <fpu_control.h>
-#endif
-
#include "IntTypes.h"
//-------------------------------------------------------------------------------------------------
@@ -36,9 +32,6 @@ static inline double cpuTime(void); // CPU-time in seconds.
extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures).
extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures).
-extern void setX86FPUPrecision(); // Make sure double's are represented with the same precision
- // in memory and registers.
-
extern void limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact
// semantics varies depending on architecture.