blob: 46dcb55af0758755606c9d0e056500c3d37064ee [file] [edit]
/*
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Gabriel Ebner
*/
#include "library/profiling.h"
#include "util/option_declarations.h"
#ifndef LEAN_DEFAULT_PROFILER
#define LEAN_DEFAULT_PROFILER false
#endif
#ifndef LEAN_DEFAULT_PROFILER_THRESHOLD
#define LEAN_DEFAULT_PROFILER_THRESHOLD 100
#endif
namespace lean {
static name * g_profiler = nullptr;
static name * g_profiler_threshold = nullptr;
bool get_profiler(options const & opts) {
return opts.get_bool(*g_profiler, LEAN_DEFAULT_PROFILER);
}
second_duration get_profiling_threshold(options const & opts) {
return second_duration(static_cast<double>(opts.get_unsigned(*g_profiler_threshold, LEAN_DEFAULT_PROFILER_THRESHOLD))/1000.0);
}
void initialize_profiling() {
g_profiler = new name{"profiler"};
mark_persistent(g_profiler->raw());
g_profiler_threshold = new name{"profiler", "threshold"};
mark_persistent(g_profiler_threshold->raw());
register_bool_option(*g_profiler, LEAN_DEFAULT_PROFILER, "(profiler) profile tactics and vm_eval command");
register_unsigned_option(*g_profiler_threshold, LEAN_DEFAULT_PROFILER_THRESHOLD,
"(profiler) threshold in milliseconds, profiling times under threshold will not be reported");
}
void finalize_profiling() {
delete g_profiler;
delete g_profiler_threshold;
}
}