Remove use of <fpu_control.h> in minisat

This commit is contained in:
Clifford Wolf 2017-03-27 14:32:43 +02:00
parent 106e44f406
commit 71cbe98a09
4 changed files with 44 additions and 18 deletions

View File

@ -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.

View File

@ -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

View File

@ -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)
{

View File

@ -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.