From 71cbe98a091ab05ef7bc678d8874db5ac9fb87ec Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 27 Mar 2017 14:32:43 +0200 Subject: Remove use of in minisat --- libs/minisat/00_PATCH_no_fpu_control.patch | 43 ++++++++++++++++++++++++++++++ libs/minisat/00_UPDATE.sh | 1 + libs/minisat/System.cc | 11 -------- libs/minisat/System.h | 7 ----- 4 files changed, 44 insertions(+), 18 deletions(-) create mode 100644 libs/minisat/00_PATCH_no_fpu_control.patch (limited to 'libs') 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 000000000..6c754b1ed --- /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 +-#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_UPDATE.sh b/libs/minisat/00_UPDATE.sh index 96a34ec93..eb278c307 100644 --- a/libs/minisat/00_UPDATE.sh +++ b/libs/minisat/00_UPDATE.sh @@ -14,4 +14,5 @@ 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 +patch -p0 < 00_PATCH_no_fpu_control.patch diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc index febe3b40f..ceef4292b 100644 --- a/libs/minisat/System.cc +++ b/libs/minisat/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) { diff --git a/libs/minisat/System.h b/libs/minisat/System.h index ee92a6e08..cd9d020c7 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 -#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. -- cgit v1.2.3