Turbo Constraint Solver
Loading...
Searching...
No Matches
statistics.hpp
Go to the documentation of this file.
1// Copyright 2021 Pierre Talbot
2
3#ifndef TURBO_STATISTICS_HPP
4#define TURBO_STATISTICS_HPP
5
6#include <chrono>
7#include <algorithm>
8#include "battery/utility.hpp"
9#include "battery/allocator.hpp"
10#include "lala/logic/ast.hpp"
11
12enum class Timer {
13 OVERALL,
15 SOLVE,
16 SEARCH,
17 // SPLIT,
18 // PUSH,
19 // POP,
25 DIVE,
27};
28
29template <class Allocator = battery::standard_allocator>
31 using allocator_type = Allocator;
32 template <class Alloc> friend struct TimingStatistics;
33private:
34 battery::vector<int64_t, allocator_type> timers_ns;
35
36public:
37
40 timers_ns(static_cast<int>(Timer::NUM_TIMERS), 0)
41 {}
42
43 template <class Alloc>
45 timers_ns(other.timers_ns)
46 {}
47
48 CUDA int64_t& time_of(Timer timer) {
49 return timers_ns[static_cast<int>(timer)];
50 }
51
52 CUDA int64_t time_of(Timer timer) const {
53 return timers_ns[static_cast<int>(timer)];
54 }
55
56 template <class Alloc>
57 CUDA void meet(const TimingStatistics<Alloc>& other) {
58 for(int i = 0; i < timers_ns.size(); i++) {
59 timers_ns[i] += other.timers_ns[i];
60 }
61 }
62
63 CUDA int64_t time_ms_of(Timer timer) const {
64 return timers_ns[static_cast<int>(timer)] / 1000 / 1000;
65 }
66
67#ifdef __CUDACC__
68 __device__ cuda::std::chrono::system_clock::time_point start_timer_device() const {
69 if(threadIdx.x == 0) {
70 return cuda::std::chrono::system_clock::now();
71 }
72 else {
73 return cuda::std::chrono::system_clock::time_point{};
74 }
75 }
76#endif
77
78 std::chrono::steady_clock::time_point start_timer_host() const {
79 return std::chrono::steady_clock::now();
80 }
81
82#ifdef __CUDACC__
83 __device__ cuda::std::chrono::system_clock::time_point stop_timer(Timer timer, cuda::std::chrono::system_clock::time_point start) {
84 if(threadIdx.x == 0) {
85 auto now = cuda::std::chrono::system_clock::now();
86 time_of(timer) += cuda::std::chrono::duration_cast<cuda::std::chrono::nanoseconds>(
87 now - start).count();
88 return now;
89 }
90 return cuda::std::chrono::system_clock::time_point{};
91 }
92#endif
93
94 std::chrono::steady_clock::time_point stop_timer(Timer timer, std::chrono::steady_clock::time_point start) {
95 auto now = std::chrono::steady_clock::now();
96 time_of(timer) += std::chrono::duration_cast<std::chrono::nanoseconds>(
97 now - start).count();
98 return now;
99 }
100
101 /** Replace the value of the timer with `now - start`. */
102 void update_timer(Timer timer, std::chrono::steady_clock::time_point start) {
103 auto now = std::chrono::steady_clock::now();
104 time_of(timer) = std::chrono::duration_cast<std::chrono::nanoseconds>(
105 now - start).count();
106 }
107};
108
109template <class Allocator = battery::standard_allocator>
111 template <class Alloc> friend struct Statistics;
112 using allocator_type = Allocator;
113 bool print_statistics; // from config.print_statistics
114 size_t variables;
117 int num_blocks; // The real count of config.or_nodes on GPU.
118 size_t nodes;
119 size_t fails;
120 size_t solutions;
130
140
141 CUDA Statistics(): Statistics(0,0,false,false) {}
142 Statistics(const Statistics&) = default;
143 Statistics(Statistics&&) = default;
144
145 template <class Alloc>
156
157 template <class Alloc>
158 CUDA void meet(const Statistics<Alloc>& other) {
159 nodes += other.nodes;
160 fails += other.fails;
161 solutions += other.solutions;
162 depth_max = battery::max(depth_max, other.depth_max);
169 timers.meet(other.timers);
170 }
171
172 template <class Alloc>
173 CUDA void meet(const TimingStatistics<Alloc>& other) {
174 timers.meet(other);
175 }
176
177#ifdef __CUDACC__
178 __device__ cuda::std::chrono::system_clock::time_point start_timer_device() const {
179 return timers.start_timer_device();
180 }
181#endif
182
183 std::chrono::steady_clock::time_point start_timer_host() const {
184 return timers.start_timer_host();
185 }
186
187#ifdef __CUDACC__
188 __device__ cuda::std::chrono::system_clock::time_point stop_timer(Timer timer, cuda::std::chrono::system_clock::time_point start) {
189 return timers.stop_timer(timer, start);
190 }
191#endif
192
193 std::chrono::steady_clock::time_point stop_timer(Timer timer, std::chrono::steady_clock::time_point start) {
194 return timers.stop_timer(timer, start);
195 }
196
197 /** Replace the value of the timer with `now - start`. */
198 void update_timer(Timer timer, std::chrono::steady_clock::time_point start) {
199 timers.update_timer(timer, start);
200 }
201
202 CUDA int64_t time_ms_of(Timer timer) const {
203 return timers.time_ms_of(timer);
204 }
205
206 CUDA void print_stat(const char* name, const char* value) const {
207 if(print_statistics) {
208 printf("%%%%%%mzn-stat: %s=\"%s\"\n", name, value);
209 }
210 }
211
212 CUDA void print_stat(const char* name, size_t value) const {
213 if(print_statistics) {
214 printf("%%%%%%mzn-stat: %s=%" PRIu64 "\n", name, value);
215 }
216 }
217
218 CUDA void print_human_stat(int verbose, const char* name, size_t value) const {
219 if(print_statistics) {
220 printf("%%%%%%mzn-stat: %s=%" PRIu64 "\n", name, value);
221 if(verbose) {
222 printf("%% [");
223 size_t M = 1000 * 1000;
224 if(value < M * 1000) {
225 printf("%.2fM", static_cast<double>(value) / M);
226 }
227 else if(value < M * 1000 * 1000) {
228 printf("%.2fG", static_cast<double>(value) / (M * 1000));
229 }
230 else {
231 printf("%.2fT", static_cast<double>(value) / (M * 1000 * 1000));
232 }
233 printf("]\n");
234 }
235 }
236 }
237
238 CUDA void print_stat(const char* name, int value) const {
239 if(print_statistics) {
240 printf("%%%%%%mzn-stat: %s=%d\n", name, value);
241 }
242 }
243
244 CUDA void print_stat_fp_iter(const char* name, size_t num_iterations, size_t value) const {
245 if(print_statistics) {
246 printf("%%%%%%mzn-stat: %s_fp_iter_%" PRIu64 "=%" PRIu64 "\n", name, num_iterations, value);
247 }
248 }
249
250 CUDA void print_stat(const char* name, double value) const {
251 if(print_statistics) {
252 printf("%%%%%%mzn-stat: %s=%lf\n", name, value);
253 }
254 }
255
256 CUDA void print_memory_statistics(int verbose, const char* key, size_t bytes) const {
257 print_stat(key, bytes);
258 if(verbose) {
259 printf("%% [");
260 if(bytes < 1000 * 1000) {
261 printf("%.2fKB", static_cast<double>(bytes) / 1000);
262 }
263 else if(bytes < 1000 * 1000 * 1000) {
264 printf("%.2fMB", static_cast<double>(bytes) / (1000 * 1000));
265 }
266 else {
267 printf("%.2fGB", static_cast<double>(bytes) / (1000 * 1000 * 1000));
268 }
269 printf("]\n");
270 }
271 }
272
273private:
274 CUDA double to_sec(int64_t dur) const {
275 return (static_cast<double>(dur / 1000 / 1000) / 1000.);
276 }
277
278public:
279 CUDA void print_block_timing_stat(const char* name, Timer timer) const {
280 print_stat(name, to_sec(timers.time_of(timer) / num_blocks));
281 }
282
283 CUDA void print_timing_stat(const char* name, Timer timer) const {
284 print_stat(name, to_sec(timers.time_of(timer)));
285 }
286
287 CUDA void print_mzn_statistics(int verbose = 0) const {
288 print_stat("num_blocks", num_blocks);
289 print_human_stat(verbose, "nodes", nodes);
290 print_stat("failures", fails);
291 print_stat("variables", variables);
292 print_stat("propagators", constraints);
293 print_stat("peakDepth", depth_max);
295 print_timing_stat("solveTime", Timer::OVERALL);
296 print_stat("num_solutions", solutions);
297 print_stat("eps_num_subproblems", eps_num_subproblems);
298 print_stat("eps_solved_subproblems", eps_solved_subproblems);
299 print_stat("eps_skipped_subproblems", eps_skipped_subproblems);
300 print_stat("num_blocks_done", num_blocks_done);
301 print_human_stat(verbose, "fixpoint_iterations", fixpoint_iterations);
302 print_human_stat(verbose, "num_deductions", num_deductions);
303
304 // Timing statistics
307 // print_block_timing_stat("split_time", Timer::SPLIT);
308 // print_block_timing_stat("push_time", Timer::PUSH);
309 // print_block_timing_stat("pop_time", Timer::POP);
311 print_block_timing_stat("transfer_cpu2gpu_time", Timer::TRANSFER_CPU2GPU);
312 print_block_timing_stat("transfer_gpu2cpu_time", Timer::TRANSFER_GPU2CPU);
313 print_block_timing_stat("select_fp_functions_time", Timer::SELECT_FP_FUNCTIONS);
316 }
317
318 CUDA void print_mzn_end_stats() const {
319 if(!print_statistics) { return; }
320 printf("%%%%%%mzn-stat-end\n");
321 }
322
323 CUDA void print_mzn_objective(const auto& obj, bool is_minimization) const {
324 if(!print_statistics) { return; }
325 printf("%%%%%%mzn-stat: objective=");
326 if(is_minimization) {
327 obj.lb().template deinterpret<lala::TFormula<battery::standard_allocator>>().print(false);
328 }
329 else {
330 obj.ub().template deinterpret<lala::TFormula<battery::standard_allocator>>().print(false);
331 }
332 printf("\n");
333 }
334
335 CUDA void print_mzn_separator() const {
336 printf("----------\n");
337 }
338
339 CUDA void print_mzn_final_separator() const {
340 if(solutions > 0) {
341 if(exhaustive) {
342 printf("==========\n");
343 }
344 }
345 else {
346 assert(solutions == 0);
347 if(exhaustive) {
348 printf("=====UNSATISFIABLE=====\n");
349 }
350 else if(optimization) {
351 printf("=====UNBOUNDED=====\n");
352 }
353 else {
354 printf("=====UNKNOWN=====\n");
355 }
356 }
357 }
358};
359
360#endif
Timer
Definition statistics.hpp:12
@ TRANSFER_CPU2GPU
@ WAIT_CPU
@ PREPROCESSING
@ TRANSFER_GPU2CPU
@ FIXPOINT
@ NUM_TIMERS
@ SELECT_FP_FUNCTIONS
Definition statistics.hpp:110
size_t eps_skipped_subproblems
Definition statistics.hpp:125
size_t fixpoint_iterations
Definition statistics.hpp:127
CUDA void print_timing_stat(const char *name, Timer timer) const
Definition statistics.hpp:283
size_t eps_solved_subproblems
Definition statistics.hpp:124
Allocator allocator_type
Definition statistics.hpp:112
TimingStatistics< Allocator > timers
Definition statistics.hpp:129
Statistics(const Statistics &)=default
size_t nodes
Definition statistics.hpp:118
CUDA void print_mzn_end_stats() const
Definition statistics.hpp:318
CUDA void print_block_timing_stat(const char *name, Timer timer) const
Definition statistics.hpp:279
CUDA void print_stat_fp_iter(const char *name, size_t num_iterations, size_t value) const
Definition statistics.hpp:244
CUDA void print_mzn_statistics(int verbose=0) const
Definition statistics.hpp:287
size_t constraints
Definition statistics.hpp:115
CUDA Statistics()
Definition statistics.hpp:141
int depth_max
Definition statistics.hpp:121
CUDA void print_mzn_final_separator() const
Definition statistics.hpp:339
bool optimization
Definition statistics.hpp:116
CUDA Statistics(size_t variables, size_t constraints, bool optimization, bool print_statistics)
Definition statistics.hpp:131
size_t num_blocks_done
Definition statistics.hpp:126
size_t fails
Definition statistics.hpp:119
CUDA int64_t time_ms_of(Timer timer) const
Definition statistics.hpp:202
std::chrono::steady_clock::time_point start_timer_host() const
Definition statistics.hpp:183
void update_timer(Timer timer, std::chrono::steady_clock::time_point start)
Definition statistics.hpp:198
bool exhaustive
Definition statistics.hpp:122
std::chrono::steady_clock::time_point stop_timer(Timer timer, std::chrono::steady_clock::time_point start)
Definition statistics.hpp:193
size_t variables
Definition statistics.hpp:114
size_t solutions
Definition statistics.hpp:120
CUDA void meet(const TimingStatistics< Alloc > &other)
Definition statistics.hpp:173
CUDA void print_stat(const char *name, size_t value) const
Definition statistics.hpp:212
size_t eps_num_subproblems
Definition statistics.hpp:123
CUDA void meet(const Statistics< Alloc > &other)
Definition statistics.hpp:158
CUDA void print_stat(const char *name, double value) const
Definition statistics.hpp:250
size_t num_deductions
Definition statistics.hpp:128
CUDA void print_mzn_separator() const
Definition statistics.hpp:335
CUDA void print_stat(const char *name, const char *value) const
Definition statistics.hpp:206
int num_blocks
Definition statistics.hpp:117
bool print_statistics
Definition statistics.hpp:113
CUDA void print_stat(const char *name, int value) const
Definition statistics.hpp:238
CUDA Statistics(const Statistics< Alloc > &other)
Definition statistics.hpp:146
CUDA void print_human_stat(int verbose, const char *name, size_t value) const
Definition statistics.hpp:218
CUDA void print_mzn_objective(const auto &obj, bool is_minimization) const
Definition statistics.hpp:323
Statistics(Statistics &&)=default
CUDA void print_memory_statistics(int verbose, const char *key, size_t bytes) const
Definition statistics.hpp:256
Definition statistics.hpp:30
CUDA void meet(const TimingStatistics< Alloc > &other)
Definition statistics.hpp:57
TimingStatistics(const TimingStatistics &)=default
std::chrono::steady_clock::time_point stop_timer(Timer timer, std::chrono::steady_clock::time_point start)
Definition statistics.hpp:94
CUDA TimingStatistics(const TimingStatistics< Alloc > &other)
Definition statistics.hpp:44
CUDA int64_t time_of(Timer timer) const
Definition statistics.hpp:52
Allocator allocator_type
Definition statistics.hpp:31
CUDA TimingStatistics()
Definition statistics.hpp:39
void update_timer(Timer timer, std::chrono::steady_clock::time_point start)
Definition statistics.hpp:102
CUDA int64_t time_ms_of(Timer timer) const
Definition statistics.hpp:63
std::chrono::steady_clock::time_point start_timer_host() const
Definition statistics.hpp:78
CUDA int64_t & time_of(Timer timer)
Definition statistics.hpp:48