| #ifndef __STDC_FORMAT_MACROS | |
| #define __STDC_FORMAT_MACROS | |
| #endif | |
| #ifndef __STDC_LIMIT_MACROS | |
| #define __STDC_LIMIT_MACROS | |
| #endif | |
| /***************************************************************************************[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 "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(bool) { 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(bool) { return memUsed(); } | |
| #else | |
| double Minisat::memUsed() { return 0; } | |
| double Minisat::memUsedPeak(bool) { return 0; } | |
| #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 | |
| } |