ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
System2.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/glucose2/System.h"
22
23#if defined(__linux__)
24
25#include <stdio.h>
26#include <stdlib.h>
27
29
30using namespace Gluco2;
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 Gluco2::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
73double Gluco2::memUsedPeak() {
74 double peak = memReadPeak() / 1024;
75 return peak == 0 ? memUsed() : peak; }
76
78
79#elif defined(__FreeBSD__)
80
82
83using namespace Gluco2;
84
85double Gluco2::memUsed(void) {
86 struct rusage ru;
87 getrusage(RUSAGE_SELF, &ru);
88 return (double)ru.ru_maxrss / 1024; }
89double Gluco2::memUsedPeak(void) { return memUsed(); }
90
92
93#elif defined(__APPLE__)
94
95#include <malloc/malloc.h>
96
98
99double Gluco2::memUsed(void) {
100 malloc_statistics_t t;
101 malloc_zone_statistics(NULL, &t);
102 return (double)t.max_size_in_use / (1024*1024); }
103
105
106#else
107
109
111 return 0; }
112
114
115#endif
116
#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 memUsedPeak()
double memUsed()
Definition System2.cpp:110
char * sprintf()
VOID_HACK exit()