| #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 |
| } |