feat: add simplex-sat-phase option to benchmarks

benchmark/BenchmarkProgram.cpp

@@ -15,6 +15,19 @@ using std::vector;
 
 namespace dlinear::benchmark {
 
+namespace {
+
+inline dlinear::Config GetConfig(const string &filename, const string &solver, const string &precision,
+                                 int simplex_phase) {
+  dlinear::Config config{filename};
+  config.mutable_lp_solver().set_from_command_line(InfoGatherer::GetLPSolver(solver));
+  config.mutable_precision().set_from_command_line(stod(precision));
+  config.mutable_simplex_sat_phase().set_from_command_line(simplex_phase);
+  return config;
+}
+
+}  // namespace
+
 BenchmarkProgram::BenchmarkProgram(int argc, const char *argv[]) : argc_{argc}, argv_{argv} {
   BenchArgParser arg_parser{};
   arg_parser.parse(argc, argv);
@@ -40,13 +53,15 @@ void BenchmarkProgram::StartBenchmarks() {
   ConfigFileReader config_file_reader{config_.config_file()};
   config_file_reader.read();
 
-  PrintRow("file,solver,assertions,precision,timeUnit,time,parserTime,smtTime,actualPrecision,result", true);
+  PrintRow("file,solver,assertions,precision,simplexPhase,timeUnit,time,parserTime,smtTime,actualPrecision,result",
+           true);
 
   std::cout << "Starting benchmarking" << std::endl;
   for (const string &filename : config_.files()) {
     for (const string &solver : config_file_reader.solvers()) {
       for (const string &precision : config_file_reader.precisions()) {
-        InfoGatherer info_gatherer{filename, solver, precision, config_.timeout()};
+        dlinear::Config dlinear_config{GetConfig(filename, solver, precision, config_.simplex_sat_phase())};
+        InfoGatherer info_gatherer{dlinear_config, config_.timeout()};
         if (config_.isDryRun()) continue;
         if (info_gatherer.run() && info_gatherer.nAssertions() > 0) {
           PrintRow((std::stringstream{} << info_gatherer).str());

benchmark/util/BenchArgParser.cpp

@@ -66,6 +66,10 @@ void BenchArgParser::addOptions() {
       .help("apply the verbosity level INFO when running dlinear")
       .default_value(false)
       .implicit_value(true);
+  parser_.add_argument("-s", "--simplex-sat-phase")
+      .help("what phase to use to verify the feasibility of the LP problem")
+      .default_value(1)
+      .scan<'i', int>();
 }
 
 ostream &operator<<(ostream &os, const BenchArgParser &parser) {
@@ -81,6 +85,7 @@ BenchConfig BenchArgParser::toConfig() const {
   config.setTimeout(parser_.get<uint>("timeout"));
   config.setExtension(parser_.get<string>("extension"));
   config.setOutputFile(parser_.get<string>("output"));
+  config.setSimplexSatPhase(parser_.get<int>("simplex-sat-phase"));
   config.setFiles(getFilesVector());
   if (parser_.get<bool>("info-verbosity"))
     DLINEAR_LOG_INIT_VERBOSITY(3);
@@ -98,6 +103,9 @@ void BenchArgParser::validateOptions() {
     DLINEAR_INVALID_ARGUMENT("--path", fmt::format("directory {} does not exist", parser_.get<string>("path")));
   if (!file_exists(parser_.get<string>("config")))
     DLINEAR_INVALID_ARGUMENT("--config", fmt::format("file {} does not exist", parser_.get<string>("config")));
+  if (parser_.get<int>("simplex-sat-phase") != 1 && parser_.get<int>("simplex-sat-phase") != 2)
+    DLINEAR_INVALID_ARGUMENT("--simplex-sat-phase", fmt::format("value must be either 1 or 2, received '{}'",
+                                                                parser_.get<int>("simplex-sat-phase")));
 }
 
 string BenchArgParser::version() const { return DLINEAR_VERSION_STRING; }

benchmark/util/BenchConfig.h

@@ -37,6 +37,7 @@ class BenchConfig {
   [[nodiscard]] const std::string &path() const { return path_; }
   [[nodiscard]] const std::string &extension() const { return extension_; }
   [[nodiscard]] const std::string &output_file() const { return output_file_; }
+  [[nodiscard]] int simplex_sat_phase() const { return simplex_sat_phase_; }
 
   void setDryRun(bool isDryRun) { isDryRun_ = isDryRun; }
   void setFiles(const std::vector<std::string> &files) { files_ = files; }
@@ -48,6 +49,7 @@ class BenchConfig {
   void setPath(std::string &&path) { path_ = std::move(path); }
   void setExtension(const std::string &extension) { extension_ = extension; }
   void setOutputFile(const std::string &outputFile) { output_file_ = outputFile; }
+  void setSimplexSatPhase(int simplexSatPhase) { simplex_sat_phase_ = simplexSatPhase; }
 
  private:
   std::string config_file_;
@@ -57,6 +59,7 @@ class BenchConfig {
   std::string output_file_;
   bool isDryRun_{};
   uint timeout_{};
+  int simplex_sat_phase_{};
 
   friend std::ostream &operator<<(std::ostream &os, const BenchConfig &config);
 };

benchmark/util/InfoGatherer.cpp

@@ -8,19 +8,20 @@ using std::string;
 namespace dlinear::benchmark {
 
 InfoGatherer::InfoGatherer(string filename, string lp_solver, const string &precision)
-    : config_{std::move(filename)}, timeout_{0} {
-  precision_ = stod(precision);
+    : config_{std::move(filename)}, precision_{stod(precision)}, timeout_{0} {
   config_.mutable_lp_solver().set_from_command_line(GetLPSolver(lp_solver));
   config_.mutable_precision().set_from_command_line(precision_);
 }
 
 InfoGatherer::InfoGatherer(string filename, string lp_solver, const string &precision, uint timeout)
-    : config_{std::move(filename)}, timeout_{timeout} {
-  precision_ = stod(precision);
+    : config_{std::move(filename)}, precision_{stod(precision)}, timeout_{timeout} {
   config_.mutable_lp_solver().set_from_command_line(GetLPSolver(lp_solver));
   config_.mutable_precision().set_from_command_line(precision_);
 }
 
+InfoGatherer::InfoGatherer(Config config, uint timeout)
+    : config_{config}, precision_{config.precision()}, timeout_{timeout} {}
+
 bool InfoGatherer::run() {
   std::cout << "Running " << config_.filename() << " with " << config_.lp_solver() << " and " << precision_
             << std::endl;
@@ -97,7 +98,7 @@ void InfoGatherer::ParseResults(shared_results *results) {
   parser_time_ = results->parser_time;
 }
 
-Config::LPSolver InfoGatherer::GetLPSolver(const string &solver) const {
+Config::LPSolver InfoGatherer::GetLPSolver(const string &solver) {
   if (solver == "soplex") {
     return Config::SOPLEX;
   } else if (solver == "qsoptex") {
@@ -122,12 +123,17 @@ void InfoGatherer::GatherInfo(shared_results *results) {
 }
 
 std::ostream &operator<<(std::ostream &os, const InfoGatherer &info_gatherer) {
-  return os << info_gatherer.filename() << "," << info_gatherer.solver() << "," << info_gatherer.nAssertions() << ","
-            << info_gatherer.precision() << ","
-            << "s"
-            << "," << info_gatherer.time() << "," << info_gatherer.parser_time() << ","
-            << info_gatherer.smt_solver_time() << "," << info_gatherer.actualPrecision() << ","
-            << info_gatherer.isSat();
+  return os << info_gatherer.filename() << ","         // Filename
+            << info_gatherer.solver() << ","           // Solver
+            << info_gatherer.nAssertions() << ","      // Number of assertions
+            << info_gatherer.precision() << ","        // Precision
+            << info_gatherer.simplex_phase() << ","    // Simplex Phase
+            << "s,"                                    // Time unit
+            << info_gatherer.time() << ","             // Time
+            << info_gatherer.parser_time() << ","      // Parser time
+            << info_gatherer.smt_solver_time() << ","  // SMT solver time
+            << info_gatherer.actualPrecision() << ","  // Actual precision
+            << info_gatherer.isSat();                  // Result
 }
 
 }  // namespace dlinear::benchmark

benchmark/util/InfoGatherer.h

@@ -27,6 +27,9 @@ class InfoGatherer {
   InfoGatherer() = delete;
   InfoGatherer(std::string filename, std::string solver, const std::string &precision);
   InfoGatherer(std::string filename, std::string solver, const std::string &precision, uint timeout);
+  InfoGatherer(Config config, uint timeout);
+
+  static Config::LPSolver GetLPSolver(const std::string &solver);
   bool run();
 
   [[nodiscard]] const std::string &filename() const { return config_.filename(); }
@@ -39,6 +42,7 @@ class InfoGatherer {
   [[nodiscard]] uint time() const { return time_; }
   [[nodiscard]] double smt_solver_time() const { return smt_solver_time_; }
   [[nodiscard]] double parser_time() const { return parser_time_; }
+  [[nodiscard]] int simplex_phase() const { return config_.simplex_sat_phase(); }
 
  private:
   Config config_;
@@ -52,7 +56,6 @@ class InfoGatherer {
   double smt_solver_time_{0.0};
   double parser_time_{0.0};
 
-  Config::LPSolver GetLPSolver(const std::string &solver) const;
   void GatherInfo(shared_results *results);
   void StartIntermediateProcess(shared_results *results);
   bool WaitChild();