1 #ifndef QUIET
2
3 #include "internal.hpp"
4
5 namespace CaDiCaL {
6
7 // Initialize all profile counters with constant name and profiling level.
8
Profiles(Internal * s)9 Profiles::Profiles (Internal * s)
10 :
11 internal (s)
12 #define PROFILE(NAME, LEVEL) \
13 , NAME (#NAME, LEVEL)
14 PROFILES
15 #undef PROFILE
16 {
17 }
18
start_profiling(Profile & profile,double s)19 void Internal::start_profiling (Profile & profile, double s) {
20 assert (profile.level <= opts.profile);
21 assert (!profile.active);
22 profile.started = s;
23 profile.active = true;
24 }
25
stop_profiling(Profile & profile,double s)26 void Internal::stop_profiling (Profile & profile, double s) {
27 assert (profile.level <= opts.profile);
28 assert (profile.active);
29 profile.value += s - profile.started;
30 profile.active = false;
31 }
32
update_profiles()33 double Internal::update_profiles () {
34 double now = time ();
35 # define PROFILE(NAME,LEVEL) \
36 do { \
37 Profile & profile = profiles.NAME; \
38 if (profile.active) { \
39 assert (profile.level <= opts.profile); \
40 profile.value += now - profile.started; \
41 profile.started = now; \
42 } \
43 } while (0);
44 PROFILES
45 # undef PROFILE
46 return now;
47 }
48
solve_time()49 double Internal::solve_time () {
50 (void) update_profiles ();
51 return profiles.solve.value;
52 }
53
54 #define PRT(S,T) \
55 MSG ("%s" S "%s", tout.magenta_code (), T, tout.normal_code ())
56
print_profile()57 void Internal::print_profile () {
58 double now = update_profiles ();
59 const char * time_type = opts.realtime ? "real" : "process";
60 SECTION ("run-time profiling");
61 PRT ("%s time taken by individual solving procedures", time_type);
62 PRT ("(percentage relative to %s time for solving)", time_type);
63 MSG ("");
64 const size_t size = sizeof profiles / sizeof (Profile);
65 struct Profile * profs[size];
66 size_t n = 0;
67 #define PROFILE(NAME,LEVEL) \
68 do { \
69 if (LEVEL > opts.profile) break; \
70 if (&profiles.NAME == &profiles.solve) break; \
71 if (!profiles.NAME.value && \
72 &profiles.NAME != &profiles.parse && \
73 &profiles.NAME != &profiles.search && \
74 &profiles.NAME != &profiles.simplify) break; \
75 profs[n++] = &profiles.NAME; \
76 } while (0);
77 PROFILES
78 #undef PROFILE
79
80 assert (n <= size);
81
82 // Explicit bubble sort to avoid heap allocation since 'print_profile'
83 // is also called during catching a signal after out of heap memory.
84 // This only makes sense if 'profs' is allocated on the stack, and
85 // not the heap, which should be the case.
86
87 double solve = profiles.solve.value;
88
89 for (size_t i = 0; i < n; i++) {
90 for (size_t j = i + 1; j < n; j++)
91 if (profs[j]->value > profs[i]->value)
92 swap (profs[i], profs[j]);
93 MSG ("%12.2f %7.2f%% %s",
94 profs[i]->value, percent (profs[i]->value, solve), profs[i]->name);
95 }
96
97 MSG (" =================================");
98 MSG ("%12.2f %7.2f%% solve", solve, percent (solve, now));
99
100 MSG ("");
101 PRT ("last line shows %s time for solving", time_type);
102 PRT ("(percentage relative to total %s time)", time_type);
103 }
104
105 }
106
107 #endif // ifndef QUIET
108