2019-05-23 17:03:08 -05:00
|
|
|
#ifndef __STDC_FORMAT_MACROS
|
2018-11-30 22:14:43 -06:00
|
|
|
#define __STDC_FORMAT_MACROS
|
2019-05-23 17:03:08 -05:00
|
|
|
#endif
|
|
|
|
#ifndef __STDC_LIMIT_MACROS
|
2018-11-30 22:14:43 -06:00
|
|
|
#define __STDC_LIMIT_MACROS
|
2019-05-23 17:03:08 -05:00
|
|
|
#endif
|
2018-11-30 22:14:43 -06:00
|
|
|
/***************************************************************************************[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
|
|
|
|
}
|