diff options
| author | Ruben Undheim <ruben.undheim@gmail.com> | 2018-08-30 20:46:20 +0200 |
|---|---|---|
| committer | Ruben Undheim <ruben.undheim@gmail.com> | 2018-08-30 20:46:20 +0200 |
| commit | 5033b51947a6ef02cb785b5622e993335efa750a (patch) | |
| tree | 7bed18c526bd94917fa2f08e3df12209863698a1 /libs/minisat/System.h | |
| parent | fefe0fc0430f4f173a25e674708aa0f4f0854b31 (diff) | |
New upstream version 0.7+20180830git0b7a184
Diffstat (limited to 'libs/minisat/System.h')
| -rw-r--r-- | libs/minisat/System.h | 7 |
1 files changed, 0 insertions, 7 deletions
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. |