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