SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
benchmarks.cpp
Go to the documentation of this file.
1 #include "benchmarks.h"
2 
3 #include <benchmax/logging.h>
5 
6 namespace benchmax {
7 
9  BenchmarkSet benchmarks;
10  for (const auto& p : settings_benchmarks().input_directories) {
11  std::filesystem::path path(p);
12  if (std::filesystem::exists(path)) {
13  BENCHMAX_LOG_INFO("benchmax.benchmarks", "Adding input directory " << path.native());
14  benchmarks.add_directory(path);
15  } else {
16  BENCHMAX_LOG_WARN("benchmax.benchmarks", "Benchmark path " << p << " does not exist.");
17  }
18  }
19  return benchmarks;
20 }
21 
22 namespace settings {
23 
24 /// Postprocess benchmark settings.
25 bool finalize_benchmark_settings(BenchmarkSettings& s, const boost::program_options::variables_map& /*values*/) {
27  return false;
28 }
29 
31  namespace po = boost::program_options;
32  auto& settings = settings::Settings::getInstance();
33  auto& s = settings.get<settings::BenchmarkSettings>("benchmarks");
34 
35  parser->add_finalizer([&s](const auto& values){
36  return finalize_benchmark_settings(s, values);
37  });
38  parser->add("Benchmark settings").add_options()
39  ("memory,M", po::value<carl::settings::binary_quantity>(&s.limit_memory)->default_value(carl::settings::binary_quantity(1024*1024*1024)), "memory limit")
40  ("timeout,T", po::value<carl::settings::duration>(&s.limit_time)->default_value(std::chrono::seconds(60))->value_name("time"), "timeout")
41  ("grace-time", po::value<carl::settings::duration>(&s.grace_time)->default_value(std::chrono::seconds(3))->value_name("time"), "grace time")
42  ("directory,D", po::value<std::vector<std::filesystem::path>>(&s.input_directories), "path to look for benchmarks")
43  ("output-dir", po::value<std::filesystem::path>(&s.output_dir), "output directory")
44  ("output-xml,X", po::value<std::filesystem::path>(&s.output_file_xml), "filename for xml output file")
45  ("output-csv,C", po::value<std::filesystem::path>(&s.output_file_csv), "filename for csv output file")
46  ;
47 }
48 }
49 
50 }
#define BENCHMAX_LOG_WARN(channel, msg)
Log warnings.
Definition: logging.h:51
#define BENCHMAX_LOG_INFO(channel, msg)
Log informational messages.
Definition: logging.h:53
A set of benchmarks from some common base directory.
Definition: BenchmarkSet.h:12
void add_directory(const std::filesystem::path &dir)
Recursively find all benchmarks from this directory.
Generic class to manage settings parsing using boost::program_options.
bool finalize_benchmark_settings(BenchmarkSettings &s, const boost::program_options::variables_map &)
Postprocess benchmark settings.
Definition: benchmarks.cpp:25
void registerBenchmarkSettings(SettingsParser *parser)
Registers benchmark settings with the settings parser.
Definition: benchmarks.cpp:30
BenchmarkSet loadBenchmarks()
Loads benchmark files from directory specified in settings.
Definition: benchmarks.cpp:8
const auto & settings_benchmarks()
Return the benchmark settings.
Definition: benchmarks.h:41
std::filesystem::path common_prefix(const std::filesystem::path &p1, const std::filesystem::path &p2)
Computes the common prefix of two paths.
Definition: filesystem.h:12
CoveringResult< typename op::PropertiesSet > exists(cadcells::datastructures::Projections &proj, FE &f, cadcells::Assignment ass, const VariableQuantification &quantification, bool characterize_sat, bool characterize_unsat)
Definition: Algorithm.h:139
Settings for benchmarks.
Definition: benchmarks.h:17
std::vector< std::filesystem::path > input_directories
Lift of input directories.
Definition: benchmarks.h:25
std::filesystem::path input_directories_common_prefix
Common prefix of input directories (to shorten filenames in output).
Definition: benchmarks.h:27