Skip to content
Snippets Groups Projects
Commit fea75476 authored by Hague Matthew UXAC009's avatar Hague Matthew UXAC009
Browse files

bug(results): fix bugs in results compilation and graph output

The produced latex was not fully standalone.

The test solvers script needed to reindex its dataframes for tools that
only solved one instance.
parent 6f858833
Branches
No related tags found
No related merge requests found
......@@ -28,56 +28,56 @@ TIMES_DAT_SUFFIX = "_times.dat"
MARK_REPEAT = "10"
STYLES_DEFINITIONS = """
\tikzset{decoone/.style={
\\tikzset{decoone/.style={
orange,
decoration={
markings,
mark = between positions 0 and 1 step 5mm with {
\node[cross out,draw=orange,inner sep=0mm,minimum size=1mm]{};
\\node[cross out,draw=orange,inner sep=0mm,minimum size=1mm]{};
},
},
postaction={decorate}
}
}
\tikzset{decotwo/.style={
\\tikzset{decotwo/.style={
black,
decoration={
markings,
mark = between positions 0 and 1 step 4mm with {
\node[rectangle,fill=black,inner sep=0mm,minimum size=1mm]{};
\\node[rectangle,fill=black,inner sep=0mm,minimum size=1mm]{};
},
},
postaction={decorate}
}
}
\tikzset{decothree/.style={
\\tikzset{decothree/.style={
green,
decoration={
markings,
mark = between positions 0 and 1 step 4mm with {
\node[isosceles triangle,fill=green,inner sep=0mm,minimum size=1.5mm]{};
\\node[isosceles triangle,fill=green,inner sep=0mm,minimum size=1.5mm]{};
},
},
postaction={decorate}
}
}
\tikzset{decofour/.style={
\\tikzset{decofour/.style={
red,
decoration={
markings,
mark = between positions 0 and 1 step 4mm with {
\node[diamond,fill=red,inner sep=0mm,minimum size=1.5mm]{};
\\node[diamond,fill=red,inner sep=0mm,minimum size=1.5mm]{};
},
},
postaction={decorate}
}
}
\tikzset{decofive/.style={
\\tikzset{decofive/.style={
blue,
decoration={
markings,
mark = between positions 0 and 1 step 4mm with {
\node[circle,fill=blue,inner sep=0mm,minimum size=1mm]{};
\\node[circle,fill=blue,inner sep=0mm,minimum size=1mm]{};
},
},
postaction={decorate}
......@@ -165,6 +165,7 @@ def make_solver_time_data(df : pd.DataFrame, solver : str) -> pd.DataFrame:
time_series = df[df[time_col].apply(is_float)][time_col].astype(float)
time_series = time_series[time_series >= 0]
time_series = time_series.sort_values(ignore_index=True)
time_series = time_series.reset_index(drop=True)
time_df = pd.concat({
TIME: time_series,
COUNT: time_series.index.to_series().astype(int).add(1)
......@@ -255,6 +256,8 @@ def get_full_latex(
"\\usepackage{pgfplots}\n" +
"\\usepackage{subcaption}\n" +
"\\usepackage{booktabs}\n" +
"\\usepackage{tikz}\n" +
"\\usetikzlibrary{shapes,automata,positioning,decorations.markings}" +
"\\begin{document}\n" +
"\\begin{figure}\n" +
STYLES_DEFINITIONS + "\n"
......
......@@ -15,7 +15,7 @@ if len(sys.argv) < 2:
benchmark_directory = sys.argv[1]
SYM_PARIKH = "/path/to/sym_parikh"
SYM_PARIKH = "/home/matt/research/strings/symbolic-parikh/symparikh-release/build/sym_parikh"
@dataclass
class Solver:
......@@ -25,9 +25,9 @@ class Solver:
Z3 = Solver("z3", [])
SOLVERS = {
"z3": Z3,
"ostrich": Solver("/path/to/ostrich-client", []),
"ostrich": Solver("/home/matt/research/strings/ostrich/ostrich-client", []),
"ostrich-cea": Solver(
"/path/to/ostrich-cea",
"/home/matt/research/strings/ostrich/ostrich-cea",
["+parikh", "-portfolio=strings"]
),
"cvc5": Solver("cvc5", []),
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment