3#ifndef TURBO_STATISTICS_HPP
4#define TURBO_STATISTICS_HPP
8#include "battery/utility.hpp"
9#include "battery/allocator.hpp"
10#include "lala/logic/ast.hpp"
29template <
class Allocator = battery::standard_allocator>
34 battery::vector<int64_t, allocator_type> timers_ns;
43 template <
class Alloc>
45 timers_ns(other.timers_ns)
49 return timers_ns[
static_cast<int>(timer)];
53 return timers_ns[
static_cast<int>(timer)];
56 template <
class Alloc>
58 for(
int i = 0; i < timers_ns.size(); i++) {
59 timers_ns[i] += other.timers_ns[i];
64 return timers_ns[
static_cast<int>(timer)] / 1000 / 1000;
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();
73 return cuda::std::chrono::system_clock::time_point{};
79 return std::chrono::steady_clock::now();
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>(
90 return cuda::std::chrono::system_clock::time_point{};
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>(
103 auto now = std::chrono::steady_clock::now();
104 time_of(timer) = std::chrono::duration_cast<std::chrono::nanoseconds>(
105 now - start).count();
109template <
class Allocator = battery::standard_allocator>
145 template <
class Alloc>
157 template <
class Alloc>
172 template <
class Alloc>
178 __device__ cuda::std::chrono::system_clock::time_point start_timer_device()
const {
179 return timers.start_timer_device();
184 return timers.start_timer_host();
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);
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);
199 timers.update_timer(timer, start);
203 return timers.time_ms_of(timer);
206 CUDA
void print_stat(
const char* name,
const char* value)
const {
208 printf(
"%%%%%%mzn-stat: %s=\"%s\"\n", name, value);
214 printf(
"%%%%%%mzn-stat: %s=%" PRIu64
"\n", name, value);
220 printf(
"%%%%%%mzn-stat: %s=%" PRIu64
"\n", name, value);
223 size_t M = 1000 * 1000;
224 if(value < M * 1000) {
225 printf(
"%.2fM",
static_cast<double>(value) / M);
227 else if(value < M * 1000 * 1000) {
228 printf(
"%.2fG",
static_cast<double>(value) / (M * 1000));
231 printf(
"%.2fT",
static_cast<double>(value) / (M * 1000 * 1000));
240 printf(
"%%%%%%mzn-stat: %s=%d\n", name, value);
246 printf(
"%%%%%%mzn-stat: %s_fp_iter_%" PRIu64
"=%" PRIu64
"\n", name, num_iterations, value);
252 printf(
"%%%%%%mzn-stat: %s=%lf\n", name, value);
260 if(bytes < 1000 * 1000) {
261 printf(
"%.2fKB",
static_cast<double>(bytes) / 1000);
263 else if(bytes < 1000 * 1000 * 1000) {
264 printf(
"%.2fMB",
static_cast<double>(bytes) / (1000 * 1000));
267 printf(
"%.2fGB",
static_cast<double>(bytes) / (1000 * 1000 * 1000));
274 CUDA
double to_sec(int64_t dur)
const {
275 return (
static_cast<double>(dur / 1000 / 1000) / 1000.);
320 printf(
"%%%%%%mzn-stat-end\n");
325 printf(
"%%%%%%mzn-stat: objective=");
326 if(is_minimization) {
327 obj.lb().template deinterpret<lala::TFormula<battery::standard_allocator>>().print(
false);
330 obj.ub().template deinterpret<lala::TFormula<battery::standard_allocator>>().print(
false);
336 printf(
"----------\n");
342 printf(
"==========\n");
348 printf(
"=====UNSATISFIABLE=====\n");
351 printf(
"=====UNBOUNDED=====\n");
354 printf(
"=====UNKNOWN=====\n");
Timer
Definition statistics.hpp:12
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