ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
System.cpp
Go to the documentation of this file.
1/***************************************************************************************[System.cc]
2Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3Copyright (c) 2007-2010, Niklas Sorensson
4
5Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6associated documentation files (the "Software"), to deal in the Software without restriction,
7including without limitation the rights to use, copy, modify, merge, publish, distribute,
8sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9furnished to do so, subject to the following conditions:
10
11The above copyright notice and this permission notice shall be included in all copies or
12substantial portions of the Software.
13
14THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19**************************************************************************************************/
20
21#include "sat/bsat2/System.h"
22
23#if defined(__linux__)
24
25#include <stdio.h>
26#include <stdlib.h>
27
29
30using namespace Minisat;
31
32// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
33// one for reading the current virtual memory size.
34
35static inline int memReadStat(int field)
36{
37 char name[256];
38 pid_t pid = getpid();
39 int value;
40
41 sprintf(name, "/proc/%d/statm", pid);
42 FILE* in = fopen(name, "rb");
43 if (in == NULL) return 0;
44
45 for (; field >= 0; field--)
46 if (fscanf(in, "%d", &value) != 1)
47 printf("ERROR! Failed to parse memory statistics from \"/proc\".\n"), exit(1);
48 fclose(in);
49 return value;
50}
51
52
53static inline int memReadPeak(void)
54{
55 char name[256];
56 pid_t pid = getpid();
57
58 sprintf(name, "/proc/%d/status", pid);
59 FILE* in = fopen(name, "rb");
60 if (in == NULL) return 0;
61
62 // Find the correct line, beginning with "VmPeak:":
63 int peak_kb = 0;
64 while (!feof(in) && fscanf(in, "VmPeak: %d kB", &peak_kb) != 1)
65 while (!feof(in) && fgetc(in) != '\n')
66 ;
67 fclose(in);
68
69 return peak_kb;
70}
71
72double Minisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
73double Minisat::memUsedPeak() {
74 double peak = memReadPeak() / 1024;
75 return peak == 0 ? memUsed() : peak; }
76
78
79#elif defined(__FreeBSD__)
80
82
83double Minisat::memUsed(void) {
84 struct rusage ru;
85 getrusage(RUSAGE_SELF, &ru);
86 return (double)ru.ru_maxrss / 1024; }
87double MiniSat::memUsedPeak(void) { return memUsed(); }
88
90
91#elif defined(__APPLE__)
92#include <malloc/malloc.h>
93
95
96double Minisat::memUsed(void) {
97 malloc_statistics_t t;
98 malloc_zone_statistics(NULL, &t);
99 return (double)t.max_size_in_use / (1024*1024); }
100
102
103#else
104
106
107double Minisat::memUsed() { return 0; }
108double Minisat::memUsedPeak() { return 0; }
109
111
112#endif
113
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START typedef signed char value
char * name
Definition main.h:24
Definition Alg.h:28
double memUsed()
Definition System.cpp:107
double memUsedPeak()
Definition System.cpp:108
char * sprintf()
VOID_HACK exit()