Simple API for timings
Inspired by what is done by SPARK, keep a global map of timings and allow to record to it from different places by providing a wrapper. The table can be printed by calling Util.print_timings
, which is called at the end of execution if the --print-timings
global option is passed to the main executable.