SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
benchmax.cpp
Go to the documentation of this file.
1 /**
2  * @file benchmax.cpp
3  *
4  * @author Sebastian Junges
5  * @author Ulrich Loup
6  *
7  * @since 2012-02-01
8  * @version 2013-04-23
9  */
10 
11 #include <csignal>
12 #include <filesystem>
13 #include <iostream>
14 
15 #include "config.h"
16 #include "logging.h"
17 #include "backends/Backends.h"
18 #include "backends/Jobs.h"
19 #include "benchmarks/benchmarks.h"
20 #include "tools/Tools.h"
22 #include "settings/Settings.h"
23 #include "settings/SettingsParser.h"
24 
25 
26 using namespace benchmax;
27 
28 /**
29  * Initialized the application.
30  *
31  * Takes care of loading settings from the command line and a config file.
32  * Afterwards checks for all options that are handled easily like being verbose or showing the help.
33  * Might signal to stop execution by returning true.
34  * @param argc argc as passed to main()
35  * @param argv argv as passed to main()
36  * @return true if the application should stop.
37  */
38 bool init_application(int argc, char** argv) {
39 
41 
42  auto& parser = SettingsParser::getInstance();
48  parser.finalize();
49  parser.parse_options(argc, argv);
50 
51  if (settings_core().be_quiet) {
52  logging_quiet();
53  }
54  if (settings_core().be_verbose) {
56  }
57  if (settings_core().show_help) {
58  std::cout << parser.print_help() << std::endl;
59  return false;
60  }
61  if (settings_core().show_settings) {
62  std::cout << parser.print_options() << std::endl;
63  return false;
64  }
65 
66  if (settings_operation().convert_ods_filename != "") {
67  std::string filename = settings_operation().convert_ods_filename;
68  std::string filter = settings_operation().convert_ods_filter;
69  BENCHMAX_LOG_INFO("benchmax.convert", "Converting " << filename << " to ods using import filer " << filter);
70  std::stringstream ss;
71  ss << "libreoffice --headless --infilter=" << filter << " --convert-to ods " << filename;
72  system(ss.str().c_str());
73  return false;
74  }
75 
76  if (settings_benchmarks().output_dir != "") {
77  std::filesystem::path oloc = std::filesystem::path(settings_benchmarks().output_dir);
78  if(!std::filesystem::exists(oloc) ||!std::filesystem::is_directory(oloc))
79  {
80  BENCHMAX_LOG_FATAL("benchmax", "Output directory does not exist: " << oloc);
81  exit(0);
82  }
83  }
84 
85  return true;
86 }
87 
88 /**
89  * Handles the interrupt signal.
90  */
91 void handleSignal(int)
92 {
93  BENCHMAX_LOG_WARN("benchmax", "User abort!");
94  exit(-1);
95 }
96 
97 /**
98  * Main program.
99  */
100 int main(int argc, char** argv)
101 {
102  std::signal(SIGINT, &handleSignal);
103 
104  if (!init_application(argc, argv)) {
105  return 0;
106  }
107 
108  Tools tools = loadTools();
109  if (tools.empty()) {
110  BENCHMAX_LOG_ERROR("benchmax", "No usable tools were found.");
111  return 0;
112  }
113 
114  BenchmarkSet benchmarks = loadBenchmarks();
115  if(benchmarks.size() == 0) {
116  BENCHMAX_LOG_ERROR("benchmax", "No benchmarks were found. Specify a valid location with --directory.");
117  return 0;
118  }
119  run_backend(settings_operation().backend, Jobs(tools, benchmarks));
120 
121  return 0;
122 }
#define BENCHMAX_LOG_WARN(channel, msg)
Log warnings.
Definition: logging.h:51
#define BENCHMAX_LOG_FATAL(channel, msg)
Log fatal errors.
Definition: logging.h:47
#define BENCHMAX_LOG_INFO(channel, msg)
Log informational messages.
Definition: logging.h:53
#define BENCHMAX_LOG_ERROR(channel, msg)
Log errors.
Definition: logging.h:49
int main(int argc, char **argv)
Main program.
Definition: benchmax.cpp:100
bool init_application(int argc, char **argv)
Initialized the application.
Definition: benchmax.cpp:38
void handleSignal(int)
Handles the interrupt signal.
Definition: benchmax.cpp:91
A set of benchmarks from some common base directory.
Definition: BenchmarkSet.h:12
std::size_t size() const
Number of files.
Definition: BenchmarkSet.h:23
Represents a set of jobs, constructed as the cartesian product of a set of tools and a set of benchma...
Definition: Jobs.h:70
void registerSlurmBackendSettings(SettingsParser *parser)
Registers Slurm settings with the settings parser.
void registerBenchmarkSettings(SettingsParser *parser)
Registers benchmark settings with the settings parser.
Definition: benchmarks.cpp:30
void registerSSHBackendSettings(SettingsParser *parser)
Registers SSH settings with settings parser.
Definition: SSHSettings.cpp:9
void registerToolSettings(SettingsParser *parser)
Registers tool settings with the settings parser.
Definition: Tools.cpp:64
void registerPresetSettings(SettingsParser *parser)
Registers preset settings with the settings parser.
void logging_verbose()
Configure verbose logging for benchmax.
Definition: logging.h:38
BenchmarkSet loadBenchmarks()
Loads benchmark files from directory specified in settings.
Definition: benchmarks.cpp:8
const auto & settings_core()
Retrieved core settings.
Definition: Settings.h:81
const auto & settings_benchmarks()
Return the benchmark settings.
Definition: benchmarks.h:41
void run_backend(const std::string &backend, const Jobs &jobs)
Runs a given backend on a list of tools and benchmarks.
Definition: Backends.h:43
const auto & settings_operation()
Retrieved operation settings.
Definition: Settings.h:85
void logging_quiet()
Configure quiet logging for benchmax.
Definition: logging.h:29
void logging_configure()
Configure default logging for benchmax.
Definition: logging.h:18
Tools loadTools()
Load all tools from the tool settings.
Definition: Tools.cpp:39
std::vector< ToolPtr > Tools
A vector of ToolPtr.
Definition: Tools.h:17
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
Use your own judgement for the following log levels: TRACE Finer-grained informational events than th...