44 lines
1.6 KiB
Diff
44 lines
1.6 KiB
Diff
|
--- 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.
|
||
|
|
|