Merge pull request #20 from elsoroka/dev

new update, generate data files for plotting in tex

examples/paper_examples/graph_coloring_benchmark.jl

@@ -3,10 +3,9 @@ using Pkg;
 Pkg.add("BenchmarkTools")
 Pkg.add("Satisfiability")
 Pkg.add("StatsBase")
-Pkg.add("Plots")
 Pkg.add("ArgParse")
 using Satisfiability, BenchmarkTools
-using StatsBase, Random, Plots, ArgParse, InteractiveUtils # for versioninfo()
+using StatsBase, Random, ArgParse, InteractiveUtils # for versioninfo()
 Random.seed!(97)
 
 s = ArgParseSettings()
@@ -149,21 +148,13 @@ open("graph_execution_log_$(time()).txt", "w") do graph_execution_log
     end
 end
 
-##### PLOTTING #####
-# Note that the paper plots are generated using pgfplots but to simplify the Docker artifact we will generate the same plots in Julia Plots.jl.
-# They may look a bit different.
-
-ns = 2.0.^(4:nmax)
-p1 = plot(ns, satjl_timing[4:nmax], label="Satisfiability.jl", color=:green, marker=:square,
-          xaxis=:log, yaxis=:log,
-          xlabel="Benchmark size", ylabel="Time (seconds)", size=(400,400))
-p1 = plot!(p1, ns, z3_timing[4:nmax], label="Z3", color=:blue, marker=:o)
-p2 = plot(ns, 100.0 .* satjl_timing[4:nmax] ./ z3_timing[4:nmax], color=:blue, marker=:o,
-          xaxis=:log, primary=false,
-          xlabel="Benchmark size", ylabel="% of Z3 solve time", size=(400,400))
-
-p = plot(p1, p2, size=(800,400))
-savefig(p, "graph_coloring.pdf")
+##### EXPORT DATA #####
+outfile = open("graph_data.txt", "w")
+write(outfile, "n\tz3\tsat\n")
+for i=4:nmax
+    write(outfile, "$(2.0^i)\t$(z3_timing[i])\t$(satjl_timing[i])\n")
+end
+close(outfile)
 
 # save the time to write the files
 outfile = open("linecount_time_graph.txt", "w")

examples/paper_examples/merge_file_timing.jl

@@ -0,0 +1,19 @@
+# Run this file after the other two benchmarks. It reads saved data from them.
+
+using Pkg
+Pkg.add("CSV")
+using CSV
+
+graph_infile = CSV.File(open("linecount_time_graph.txt", "r"), header=true)
+pigeon_infile = CSV.File(open("linecount_time_pigeon.txt", "r"), header=true)
+lg = length(graph_infile[:seconds])
+lp = length(pigeon_infile[:seconds])
+
+outfile = open("filesize.txt", "w")
+write(outfile, "nlines_pigeon\ttime_pigeon\tnlines_graph\ttime_graph\n")
+for i=1:max(lg, lp)
+     pigeon_i = i > lp ? "\t" : "$(pigeon_infile[:linecount][i])\t$(pigeon_infile[:seconds][i])"
+     graph_i = i > lg ? "\t" : "$(graph_infile[:linecount][i])\t$(graph_infile[:seconds][i])"
+     write(outfile, "$pigeon_i\t$graph_i\n")
+end
+close(outfile)

examples/paper_examples/pigeons_benchmark.jl

@@ -2,9 +2,8 @@
 using Pkg
 Pkg.add("BenchmarkTools")
 Pkg.add("Satisfiability")
-Pkg.add("Plots")
 Pkg.add("ArgParse")
-using Satisfiability, BenchmarkTools, Plots, ArgParse, InteractiveUtils # for versioninfo()
+using Satisfiability, BenchmarkTools, ArgParse, InteractiveUtils # for versioninfo()
 
 s = ArgParseSettings()
 @add_arg_table! s begin
@@ -143,22 +142,13 @@ open("pigeons_execution_log_$(time()).txt", "w") do pigeons_execution_log
 
 end
 
-##### PLOTTING #####
-# Note that the paper plots are generated using pgfplots but to simplify the Docker artifact we will generate the same plots in Julia Plots.jl.
-# They may look a bit different.
-
-ns = collect(2:nmax)
-p1 = plot(ns, satjl_timing[2:nmax], label="Satisfiability.jl", color=:green, marker=:square,
-          yaxis=:log,
-          xlabel="Benchmark size", ylabel="Time (seconds)", size=(400,400))
-p1 = plot!(p1, ns, z3_timing[2:nmax], label="Z3", color=:blue, marker=:o)
-pct = 100.0 .* satjl_timing[2:nmax] ./ z3_timing[2:nmax]
-p2 = plot(ns, pct, color=:blue, marker=:o,
-          xaxis=:log, ylims=(min(50, minimum(pct)),max(150, maximum(pct))), primary=false,
-          xlabel="Benchmark size", ylabel="% of Z3 solve time", size=(400,400))
-
-p = plot(p1, p2, size=(800,400))
-savefig(p, "pigeons.pdf")
+##### EXPORT DATA #####
+outfile = open("pigeons_data.txt", "w")
+write(outfile, "n\tz3\tsat\n")
+for i=2:nmax
+    write(outfile, "$i\t$(z3_timing[i])\t$(satjl_timing[i])\n")
+end
+close(outfile)
 
 # save the time to write the files
 outfile = open("linecount_time_pigeon.txt", "w")

examples/paper_examples/plot_results/filesize.tex

@@ -0,0 +1,25 @@
+\begin{tikzpicture}
+\begin{loglogaxis} [
+width=0.49\textwidth,
+xlabel={Script length (\# SMT-LIB commands)},
+ylabel={Time to generate script (seconds)},
+%enlargelimits=false,
+legend pos=north west,
+%ymajorgrids=true,
+grid style=dashed,
+]
+\addplot+ [
+mark size=2pt,
+mark=*,
+]
+table [x=nlines_pigeon, y=time_pigeon,
+] {results/filesize.txt};
+\addplot+ [
+mark size=2pt,
+mark=square*,
+]
+table [x=nlines_graph, y=time_graph,
+] {results/filesize.txt};
+\legend{Pigeon benchmark,Graph benchmark}
+\end{loglogaxis}
+\end{tikzpicture}

examples/paper_examples/plot_results/graph.tex

@@ -0,0 +1,55 @@
+\pgfplotsset{
+	every mark/.append style={solid},
+}
+\begin{tikzpicture}
+\begin{loglogaxis}[
+width=0.45\textwidth,
+xlabel={Benchmark size},
+ylabel={Time (seconds)},
+%xmin=0, xmax=15,
+%ymin=0, ymax=1000,
+%xtick={0,20,40,60,80,100},
+%ytick={0,20,40,60,80,100,120},
+legend pos=north west,
+%ymajorgrids=true,
+grid style=dashed,
+]
+
+\addplot+[
+%mark=square*,
+mark size=2.5pt,
+color=blue,
+style=dashed,
+]
+table[x=n,y=z3] {results/graph_data.txt};
+
+\addplot+ [
+mark size=1.5pt,
+color=green!70!black,
+%mark=*,
+]
+table[x=n, y=sat] {results/graph_data.txt};
+\legend{Z3, Satisfiability.jl}
+\end{loglogaxis}
+\end{tikzpicture}
+%
+%
+\begin{tikzpicture}
+\begin{semilogxaxis} [
+width=0.45\textwidth,
+xlabel={Benchmark size},
+ylabel={\% of Z3 solve time},
+%enlargelimits=false,
+legend pos=north east,
+%ymajorgrids=true,
+grid style=dashed,
+]
+\addplot+ [
+mark size=2pt,
+mark=*,
+]
+table [x=n, y expr=(\thisrow{sat} / \thisrow{z3}) * 100,
+] {results/graph_data.txt};
+\legend{\% of Z3 solve time}
+\end{semilogxaxis}
+\end{tikzpicture}

examples/paper_examples/plot_results/pigeons.tex

@@ -0,0 +1,56 @@
+\pgfplotsset{
+	every mark/.append style={solid},
+}
+\begin{tikzpicture}
+\begin{semilogyaxis}[
+width=0.45\textwidth,
+xlabel={Benchmark size},
+ylabel={Time (seconds)},
+xmin=0, xmax=15,
+ymax=1000,
+%xtick={0,20,40,60,80,100},
+%ytick={0,20,40,60,80,100,120},
+legend pos=north west,
+%ymajorgrids=true,
+grid style=dashed,
+]
+
+\addplot+[
+%mark=square,
+mark size=2.5pt,
+color=blue,
+style=dashed,
+]
+table[x=n,y=z3] {results/pigeons_data.txt};
+
+\addplot+ [
+mark size=1.5pt,
+color=green!70!black,
+%mark=*,
+]
+table[x=n, y=sat] {results/pigeons_data.txt};
+
+\legend{Z3, Satisfiability.jl}
+\end{semilogyaxis}
+\end{tikzpicture}
+%
+\begin{tikzpicture}
+\begin{semilogxaxis} [
+width=0.45\textwidth,
+xlabel={Benchmark size},
+ylabel={\% of Z3 solve time},
+ymin=, ymax=150,
+%enlargelimits=false,
+legend pos=north east,
+%ymajorgrids=true,
+grid style=dashed,
+]
+\addplot+ [
+mark size=2pt,
+mark=*,
+]
+table [x=n, y expr=(\thisrow{sat} / \thisrow{z3}) * 100,
+] {results/pigeons_data.txt};
+\legend{\% of Z3 solve time}
+\end{semilogxaxis}
+\end{tikzpicture}

examples/paper_examples/plot_results/plotter.tex

@@ -0,0 +1,33 @@
+\documentclass{article}
+\usepackage[margin=1in]{geometry}
+\usepackage{pgfplots}
+%\usepgfplotslibrary{external}
+%\tikzexternalize
+\pgfplotsset{compat=1.15}
+
+\begin{document}
+\begin{figure}[h!]
+	\centering
+	%	\vspace{-0.5em}
+	\input{pigeons.tex}
+	\caption{Timing results for the pigeonhole benchmark.}
+	%	\vspace{-1.5em}
+	\label{fig:pigeons}
+\end{figure}
+%
+\begin{figure}[h!]
+	\centering
+	%	\vspace{-0.5em}
+	\input{graph.tex}
+	\caption{Timing results for interactive graph coloring.}
+	%	\vspace{-1em}
+	\label{fig:graph}
+\end{figure}
+\begin{figure}[h]
+	\centering
+	\input{filesize.tex}
+	\caption{Time to write SMT-LIB script files using Satisfiability.jl. Each command corresponds to one line in the script file.}
+	%	\vspace{-1em}
+	\label{fig:filesize}
+\end{figure}
+\end{document}

examples/paper_examples/readme/readme.tex

@@ -0,0 +1,44 @@
+\documentclass{article}
+\usepackage[margin=1in]{geometry}
+
+\begin{document}
+\title{README.pdf}
+
+\section*{Getting Started}
+
+A Dockerfile and a TeX script (\texttt{plotter.tex}) for displaying results is provided. In the directory containing the Dockerfile, issue two commands:
+\begin{enumerate}
+\item \texttt{docker build -t smt .}
+\item \texttt{docker run --name smt smt}
+\end{enumerate}
+Docker will run the package tests for \verb|Satisfiability.jl.| Some of these test error and warning behavior, so you will see 1 error and 3 warnings.
+
+\section*{Step-by-Step Instructions}
+These instructions generate the paper results, with an option to reduce the benchmark size.
+\begin{enumerate}
+	\item To run the examples: \texttt{docker run smt ./run\_examples.sh}
+\item To retrieve the results (note that this command stores them inside the \texttt{plot\_results} directory with the TeX files):
+\texttt{docker cp smt:/Satisfiability.jl/examples/paper\_examples/results plot\_results/}
+\item To display the results, compile \texttt{plot\_results/plotter.tex} in your LaTeX editor.
+\end{enumerate}
+Results will be provided in the form of execution logs, generated SMT files, and data files for plotting in TeX. Due to variations in computing hardware and environment, plots may not exactly match those in the submitted paper, especially the ``\% of Z3 solve time" plot for the pigeon benchmark which is sensitive to noise for small problem sizes. However, the plots should display the same trends.
+
+\subsection*{Machine Specs and Reducing Benchmark Size}
+The paper results were obtained on a Linux Mint machine with 16 GB RAM and an 8 core Intel i7-6820HQ CPU running at 2.70GHz. This is the output of Julia \verb|versioninfo()|.
+\begin{verbatim}
+Julia Version 1.9.0
+Commit 8e630552924 (2023-05-07 11:25 UTC)
+Platform Info:
+OS: Linux (x86_64-linux-gnu)
+CPU: 8 × Intel(R) Core(TM) i7-6820HQ CPU @ 2.70GHz
+WORD_SIZE: 64
+LIBM: libopenlibm
+LLVM: libLLVM-14.0.6 (ORCJIT, skylake)
+Threads: 1 on 8 virtual cores
+Environment:
+JULIA_REVISE = manual
+\end{verbatim}
+
+If running the benchmark takes too long, you may reduce the size by passing a negative number as an argument: for example, \texttt{docker run smt ./run\_examples.sh -2} reduces the size by 2. The number must be between 0 and -7 and will reduce the number of data points computed.
+
+\end{document}

examples/paper_examples/run_examples.sh

@@ -9,12 +9,10 @@ echo "Graph coloring benchmark of size $size2"
 julia graph_coloring_benchmark.jl -n $size2
 
 echo "File generation time plot"
-julia plot_file_generation_time.jl
+julia merge_file_timing.jl
 
 mkdir results
-mv graph*.txt results/
-mv pigeons*.txt results/
-mv *.pdf results/
+mv *.txt results/
 cp -r graph_genfiles results/graph_genfiles
 cp -r pigeons_genfiles results/pigeons_genfiles
 echo "Done, please run \"docker cp\" to retrieve the results."