diff options
Diffstat (limited to 'libs/minisat/System.cc')
| -rw-r--r-- | libs/minisat/System.cc | 171 |
1 files changed, 171 insertions, 0 deletions
diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc new file mode 100644 index 000000000..01d0dfe11 --- /dev/null +++ b/libs/minisat/System.cc @@ -0,0 +1,171 @@ +#define __STDC_FORMAT_MACROS +#define __STDC_LIMIT_MACROS +/***************************************************************************************[System.cc] +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include <signal.h> +#include <stdio.h> + +#include "libs/minisat/System.h" + +#if defined(__linux__) + +#include <stdlib.h> + +using namespace Minisat; + +static inline int memReadStat(int field) +{ + char name[256]; + pid_t pid = getpid(); + int value; + + sprintf(name, "/proc/%d/statm", pid); + FILE* in = fopen(name, "rb"); + if (in == NULL) return 0; + + for (; field >= 0; field--) + if (fscanf(in, "%d", &value) != 1) + printf("ERROR! Failed to parse memory statistics from \"/proc\".\n"), exit(1); + fclose(in); + return value; +} + + +static inline int memReadPeak(void) +{ + char name[256]; + pid_t pid = getpid(); + + sprintf(name, "/proc/%d/status", pid); + FILE* in = fopen(name, "rb"); + if (in == NULL) return 0; + + // Find the correct line, beginning with "VmPeak:": + int peak_kb = 0; + while (!feof(in) && fscanf(in, "VmPeak: %d kB", &peak_kb) != 1) + while (!feof(in) && fgetc(in) != '\n') + ; + fclose(in); + + return peak_kb; +} + +double Minisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); } +double Minisat::memUsedPeak(bool strictlyPeak) { + double peak = memReadPeak() / (double)1024; + return peak == 0 && !strictlyPeak ? memUsed() : peak; } + +#elif defined(__FreeBSD__) || defined(__FreeBSD_kernel__) || defined(__gnu_hurd__) + +double Minisat::memUsed() { + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return (double)ru.ru_maxrss / 1024; } +double Minisat::memUsedPeak() { return memUsed(); } + + +#elif defined(__APPLE__) +#include <malloc/malloc.h> + +double Minisat::memUsed() { + malloc_statistics_t t; + malloc_zone_statistics(NULL, &t); + return (double)t.max_size_in_use / (1024*1024); } +double Minisat::memUsedPeak() { return memUsed(); } + +#else +double Minisat::memUsed() { return 0; } +double Minisat::memUsedPeak() { 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) +{ +// FIXME: OpenBSD does not support RLIMIT_AS. Not sure how well RLIMIT_DATA works instead. +#if defined(__OpenBSD__) +#define RLIMIT_AS RLIMIT_DATA +#endif + + // Set limit on virtual memory: + if (max_mem_mb != 0){ + rlim_t new_mem_lim = (rlim_t)max_mem_mb * 1024*1024; + rlimit rl; + getrlimit(RLIMIT_AS, &rl); + if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){ + rl.rlim_cur = new_mem_lim; + if (setrlimit(RLIMIT_AS, &rl) == -1) + printf("WARNING! Could not set resource limit: Virtual memory.\n"); + } + } + +#if defined(__OpenBSD__) +#undef RLIMIT_AS +#endif +} +#else +void Minisat::limitMemory(uint64_t /*max_mem_mb*/) +{ + printf("WARNING! Memory limit not supported on this architecture.\n"); +} +#endif + + +#if !defined(_MSC_VER) && !defined(__MINGW32__) +void Minisat::limitTime(uint32_t max_cpu_time) +{ + if (max_cpu_time != 0){ + rlimit rl; + getrlimit(RLIMIT_CPU, &rl); + if (rl.rlim_max == RLIM_INFINITY || (rlim_t)max_cpu_time < rl.rlim_max){ + rl.rlim_cur = max_cpu_time; + if (setrlimit(RLIMIT_CPU, &rl) == -1) + printf("WARNING! Could not set resource limit: CPU-time.\n"); + } + } +} +#else +void Minisat::limitTime(uint32_t /*max_cpu_time*/) +{ + printf("WARNING! CPU-time limit not supported on this architecture.\n"); +} +#endif + + +void Minisat::sigTerm(void handler(int)) +{ + signal(SIGINT, handler); + signal(SIGTERM,handler); +#ifdef SIGXCPU + signal(SIGXCPU,handler); +#endif +} |