Skip to content

Commit

Permalink
bench: differentiate between parser time and smt solver time
Browse files Browse the repository at this point in the history
  • Loading branch information
@TendTo
TendTo committed Nov 1, 2023
1 parent e7b6dc4 commit 0249d3c
Show file tree
Hide file tree
Showing 8 changed files with 112 additions and 123 deletions.
2 changes: 1 addition & 1 deletion benchmark/BenchmarkProgram.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ void BenchmarkProgram::StartBenchmarks() {
ConfigFileReader config_file_reader{config_.config_file()};
config_file_reader.read();

PrintRow("file,solver,assertions,precision,timeUnit,time,actualPrecision,result", true);
PrintRow("file,solver,assertions,precision,timeUnit,time,parserTime,smtTime,actualPrecision,result", true);

std::cout << "Starting benchmarking" << std::endl;
for (const string &filename : config_.files()) {
Expand Down
71 changes: 71 additions & 0 deletions benchmark/parser/base_parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,19 @@
from typing import TypedDict, Literal

TimeUnit = Literal["ns", "us", "ms", "s", "m", "h"]
ProblemCategory = Literal["lp", "ss", "smt"]

class Benchmark(TypedDict):
file: str
solver: str
assertions: int
timeUnit: str
time: int
parserTime: int
smtTime: int
precision: float
actualPrecision: float
result: int

class SloaneStufken(TypedDict):
assertions: int
Expand All @@ -23,6 +36,10 @@ class SloaneStufken(TypedDict):
actualPrecisionQ: float
timeS: float
timeQ: float
parserTimeS: float
parserTimeQ: float
smtTimeS: float
smtTimeQ: float
resultS: str
resultQ: str

Expand All @@ -36,6 +53,10 @@ class LPProblem(TypedDict):
actualPrecisionQ: float
timeS: float
timeQ: float
parserTimeS: float
parserTimeQ: float
smtTimeS: float
smtTimeQ: float
resultS: str
resultQ: str

Expand All @@ -49,6 +70,10 @@ class SMTProblem(TypedDict):
actualPrecisionQ: float
timeS: float
timeQ: float
parserTimeS: float
parserTimeQ: float
smtTimeS: float
smtTimeQ: float
resultS: str
resultQ: str

Expand Down Expand Up @@ -79,6 +104,52 @@ def __init__(
self.min_time: "int" = min_time
self.time_unit: "TimeUnit" = time_unit

def add_row(self, file: "str", benchmark: "Benchmark", row_dict: "dict"):
solver = benchmark["solver"]
result = "delta-sat" if int(benchmark["result"]) == 1 else "unsat"
precision = float(benchmark["precision"])
assertions = int(benchmark["assertions"])
actual_precision = float(benchmark["actualPrecision"])
time = self.time_conversion(benchmark["time"], benchmark["timeUnit"])

default_row = {
"file": file,
"assertions": assertions,
"precision": precision,
"timeUnit": self.time_unit,
"iterations": 1,
"actualPrecisionS": -1,
"actualPrecisionQ": -1,
"timeS": -1,
"timeQ": -1,
"resultS": "/",
"resultQ": "/",
}
if row_dict is self.slone_stufken_rows:
s1, k1, s2, k2, t = (int(val) for val in file.split("-"))
default_row.update({
"s1": s1,
"k1": k1,
"s2": s2,
"k2": k2,
"t": t,
})

key = f"{file}/{precision}"
row: "LPProblem | SloaneStufken | SMTProblem" = row_dict.get(key, default_row)

identifier = "S" if solver == "soplex" else "Q"
row[f"actualPrecision{identifier}"] = actual_precision
row[f"time{identifier}"] = round(time, 3)
row[f"parserTime{identifier}"] = benchmark["parserTime"]
row[f"smtTime{identifier}"] = benchmark["smtTime"]
row["fest"] = "A"
row[f"result{identifier}"] = result

row_dict[key] = row



@abstractmethod
def load_benchmarks(self):
pass
Expand Down
127 changes: 6 additions & 121 deletions benchmark/parser/csv_parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,18 +5,8 @@
from .base_parser import BaseBenchmarkParser

if TYPE_CHECKING:
from typing import TypedDict
from base_parser import SloaneStufken, LPProblem, SMTProblem, TimeUnit

class Benchmark(TypedDict):
file: str
solver: str
assertions: int
timeUnit: str
time: int
precision: float
actualPrecision: float
result: int
from .base_parser import Benchmark


class BenchmarkCsvParser(BaseBenchmarkParser):
Expand All @@ -40,128 +30,23 @@ def load_benchmarks(self):

def parse_lp_problem(self, benchmark: "Benchmark"):
file = benchmark["file"].split("/")[-1].removeprefix("LP_").removesuffix(".smt2").removesuffix(".mps")
solver = benchmark["solver"]
result = "delta-sat" if int(benchmark["result"]) == 1 else "unsat"

precision = float(benchmark["precision"])
assertions = int(benchmark["assertions"])
actual_precision = float(benchmark["actualPrecision"])
time = self.time_conversion(benchmark["time"], benchmark["timeUnit"])

key = f"{file}/{precision}"
row: "LPProblem" = self.lp_problem_rows.get(
key,
{
"file": file,
"assertions": assertions,
"precision": precision,
"timeUnit": self.time_unit,
"iterations": 1,
"actualPrecisionS": -1,
"actualPrecisionQ": -1,
"timeS": -1,
"timeQ": -1,
"resultS": "/",
"resultQ": "/",
},
)
if solver == "soplex":
row["actualPrecisionS"] = actual_precision
row["timeS"] = round(time, 3)
row["resultS"] = result
elif solver == "qsoptex":
row["actualPrecisionQ"] = actual_precision
row["timeQ"] = round(time, 3)
row["resultQ"] = result
self.lp_problem_rows[key] = row
self.add_row(file, benchmark, self.lp_problem_rows)

def parse_sloane_stufken_problem(self, benchmark: "Benchmark"):
file = benchmark["file"].split("/")[-1].removesuffix(".smt2")
solver = benchmark["solver"]
result = "delta-sat" if int(benchmark["result"]) == 1 else "unsat"

precision = float(benchmark["precision"])
assertions = int(benchmark["assertions"])
actual_precision = float(benchmark["actualPrecision"])
time = self.time_conversion(benchmark["time"], benchmark["timeUnit"])
s1, k1, s2, k2, t = (int(val) for val in file.split("-"))

key = f"{file}/{precision}"
row: "SloaneStufken" = self.slone_stufken_rows.get(
key,
{
"assertions": assertions,
"precision": precision,
"timeUnit": self.time_unit,
"iterations": 1,
"s1": s1,
"k1": k1,
"s2": s2,
"k2": k2,
"t": t,
"actualPrecisionS": -1,
"actualPrecisionQ": -1,
"timeS": -1,
"timeQ": -1,
"resultS": "/",
"resultQ": "/",
},
)
if solver == "soplex":
row["actualPrecisionS"] = actual_precision
row["timeS"] = round(time, 3)
row["resultS"] = result
elif solver == "qsoptex":
row["actualPrecisionQ"] = actual_precision
row["timeQ"] = round(time, 3)
row["resultQ"] = result
self.slone_stufken_rows[key] = row
file = benchmark["file"].split("/")[-1].removeprefix("SMT_").removesuffix(".smt2")
self.add_row(file, benchmark, self.slone_stufken_rows)

def parse_smt_problem(self, benchmark: "Benchmark"):
file = benchmark["file"].split("/")[-1].removeprefix("SMT_").removesuffix(".smt2")
solver = benchmark["solver"]
result = "delta-sat" if int(benchmark["result"]) == 1 else "unsat"

precision = float(benchmark["precision"])
assertions = int(benchmark["assertions"])
actual_precision = float(benchmark["actualPrecision"])
time = self.time_conversion(benchmark["time"], benchmark["timeUnit"])

key = f"{file}/{precision}"
row: "SMTProblem" = self.smt_problem_rows.get(
key,
{
"file": file,
"assertions": assertions,
"precision": precision,
"timeUnit": self.time_unit,
"iterations": 1,
"actualPrecisionS": -1,
"actualPrecisionQ": -1,
"timeS": -1,
"timeQ": -1,
"resultS": "/",
"resultQ": "/",
},
)
if solver == "soplex":
row["actualPrecisionS"] = actual_precision
row["timeS"] = round(time, 3)
row["resultS"] = result
elif solver == "qsoptex":
row["actualPrecisionQ"] = actual_precision
row["timeQ"] = round(time, 3)
row["resultQ"] = result
self.add_row(file, benchmark, self.smt_problem_rows)

def _parse_benchmarks(self):
for benchmark in self.benchmarks:
file = benchmark["file"].split("/")[-1]
if file.startswith("LP"):
if file.startswith("LP") or file.endswith(".mps"):
self.parse_lp_problem(benchmark)
elif file.startswith("SMT"):
self.parse_smt_problem(benchmark)
elif file.endswith(".mps"):
self.parse_lp_problem(benchmark)
elif re.match(r"^(\d+-){4}\d+.smt2$", file):
self.parse_sloane_stufken_problem(benchmark)
else:
Expand Down
8 changes: 7 additions & 1 deletion benchmark/util/InfoGatherer.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,8 @@ void InfoGatherer::ParseResults(shared_results *results) {
isSat_ = results->isSat;
actualPrecision_ = results->actualPrecision;
time_ = results->time;
smt_solver_time_ = results->smt_solver_time;
parser_time_ = results->parser_time;
}

Config::LPSolver InfoGatherer::GetLPSolver(const string &solver) const {
Expand All @@ -112,6 +114,8 @@ void InfoGatherer::GatherInfo(shared_results *results) {
results->nAssertions = res.n_assertions();
results->isSat = res.is_sat();
results->actualPrecision = res.actual_precision().get_d();
results->parser_time = res.parser_time();
results->smt_solver_time = res.smt_solver_time();

auto end = std::chrono::high_resolution_clock::now();
results->time = std::chrono::duration_cast<std::chrono::seconds>(end - start).count();
Expand All @@ -121,7 +125,9 @@ 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.actualPrecision() << "," << info_gatherer.isSat();
<< "," << info_gatherer.time() << "," << info_gatherer.parser_time() << ","
<< info_gatherer.smt_solver_time() << "," << info_gatherer.actualPrecision() << ","
<< info_gatherer.isSat();
}

} // namespace dlinear::benchmark
6 changes: 6 additions & 0 deletions benchmark/util/InfoGatherer.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ struct shared_results {
bool isSat;
double actualPrecision;
uint time;
double smt_solver_time;
double parser_time;
};

class InfoGatherer {
Expand All @@ -35,6 +37,8 @@ class InfoGatherer {
[[nodiscard]] bool isSat() const { return isSat_; }
[[nodiscard]] uint timeout() const { return timeout_; }
[[nodiscard]] uint time() const { return time_; }
[[nodiscard]] double smt_solver_time() const { return smt_solver_time_; }
[[nodiscard]] double parser_time() const { return parser_time_; }

private:
Config config_;
Expand All @@ -45,6 +49,8 @@ class InfoGatherer {
pid_t intermediate_pid_{-1};
uint timeout_{0};
uint time_{0};
double smt_solver_time_{0.0};
double parser_time_{0.0};

Config::LPSolver GetLPSolver(const std::string &solver) const;
void GatherInfo(shared_results *results);
Expand Down
5 changes: 5 additions & 0 deletions dlinear/solver/Solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,12 @@
#include "dlinear/solver/SolverOutput.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Infinity.h"
#include "dlinear/util/Timer.h"
#include "dlinear/util/exception.h"
#include "dlinear/util/logging.h"

namespace dlinear {

Solver::Solver() : Solver{Config{true}} {}
Solver::Solver(const std::string &filename) : Solver{Config{filename}} {}
Solver::Solver(Config config)
Expand Down Expand Up @@ -53,6 +55,7 @@ SolverOutput Solver::CheckSat() {

bool Solver::ParseInput() {
DLINEAR_TRACE("Solver::ParseInput");
TimerGuard timer_guard{&output_.mutable_parser_timer(), true};
switch (config_.format()) {
case Config::Format::AUTO:
if (config_.read_from_stdin()) return ParseSmt2();
Expand Down Expand Up @@ -84,6 +87,7 @@ bool Solver::ParseMps() {

void Solver::CheckObjCore() {
DLINEAR_DEBUG("Solver::CheckObjCore");
TimerGuard timer_guard{&output_.mutable_smt_solver_timer(), true};
output_.mutable_model() = context_.box();
int status =
context_.CheckOpt(&output_.mutable_lower_bound(), &output_.mutable_upper_bound(), &output_.mutable_model());
Expand All @@ -100,6 +104,7 @@ void Solver::CheckObjCore() {

void Solver::CheckSatCore() {
DLINEAR_DEBUG("Solver::CheckSatCore");
TimerGuard timer_guard{&output_.mutable_smt_solver_timer(), true};
const std::optional<Box> model{context_.CheckSat(&output_.mutable_actual_precision())};
if (model) {
output_.mutable_model() = *model;
Expand Down
7 changes: 7 additions & 0 deletions dlinear/solver/SolverOutput.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@

#include "dlinear/libs/gmp.h"
#include "dlinear/util/Box.h"
#include "dlinear/util/Timer.h"

namespace dlinear {

Expand Down Expand Up @@ -53,6 +54,8 @@ class SolverOutput {
produce_models_{produce_models},
with_timings_{with_timings} {}

Timer &mutable_parser_timer() { return parser_timer_; }
Timer &mutable_smt_solver_timer() { return smt_solver_timer_; }
SolverResult &mutable_result() { return result_; }
mpq_class &mutable_actual_precision() { return actual_precision_; }
mpq_class &mutable_lower_bound() { return lower_bound_; }
Expand All @@ -62,6 +65,8 @@ class SolverOutput {
bool &mutable_produce_models() { return produce_models_; }
uint &mutable_n_assertions() { return n_assertions_; }

[[nodiscard]] double parser_time() const { return parser_timer_.seconds(); }
[[nodiscard]] double smt_solver_time() const { return smt_solver_timer_.seconds(); }
[[nodiscard]] SolverResult result() const { return result_; }
[[nodiscard]] const mpq_class &actual_precision() const { return actual_precision_; }
[[nodiscard]] double precision_upper_bound() const;
Expand All @@ -79,6 +84,8 @@ class SolverOutput {
[[nodiscard]] std::string ToString() const;

private:
Timer parser_timer_{};
Timer smt_solver_timer_{};
uint n_assertions_{0};
SolverResult result_{SolverResult::UNSOLVED};
mpq_class lower_bound_{0};
Expand Down
Loading

0 comments on commit 0249d3c

Please sign in to comment.