This virtual machine contains all the necessary packages and files for reproducing results from the paper. Namely, it has installed
- BenchExec for running the experiments,
- R for summarizing the results,
- TeX Live for generating the tables from the results,
- all the packages that were necessary to build the solvers (ANTLR, Java, CMake, newer gcc).
The artifact itself is located in the directory artifact. Its
subdirectory solvers contains binaries and source codes for all
four evaluated solvers Boolector, CVC4, Q3B, and Z3. The binaries
for CVC4 and Z3 were downloaded from the official repositories,
solvers Boolector and Q3B were built from the source codes.
Finally, the subdirectory benchmarks contains all quantified
bit-vector benchmarks from SMT-LIB.
If the reader is interested in details, the file PREPARATION.org
contains all the scripts that were used to produce this virtual
machine from the clean Ubuntu 16.04 image. The image you see is the
result of cloning the repository
https://github.com/martinjonas/q3b-artifact.git and running bash
/preparation/PREPARATION.sh from the directory artifact and then
sudo Rscript preparation/PREPARATION.R, which are both
generated from the mentioned file
artifact/preparation/PREPARATION.org. This org-mode file contains
also results of some of the commands we have obtained during
preparation of the artifact: for example versions of the used tools
and results of tests of Q3B.
For running the experiments, you need to set-up the virtual machine with at least 3 physical or virtual processors. The machine should also have at least 8 GiB of RAM. The experiments can be also executed with less RAM (see later), but this will probably fail to produce exactly the same results as in the paper.
To run the experiments with the timeout 20 minutes of CPU time, as
in the paper, go to the directory artifact and run the scripts
./runExperiments.sh. After it finishes, you should see the folder
experiments/results with CSV files for Boolector, CVC4, Q3B, and
Z3. If you run the script ./runExperiments.sh again, the folder
gets deleted and all the experiments are executed again.
Beware that the script ./runExperiments.sh with the default
timeout needs about a week of CPU time to finish. The script
tries to use all the available CPU cores and will run more
experiments in parallel, if you have more available cores and RAM.
Therefore, adding cores to the virtual machine will speed up the
computation significantly: in our experimental setup, all the
experiments took about five days on a 6-core machine and 24 GiB of
RAM.
If you want to run a simpler version of the experiments, the script
./runExperiments.sh takes an optional parameter for custom
timeout. Therefore ./runExperiments.sh 5 will run the experiments
with timeout of 5 seconds. This took about two hours on our
machine. The timeout can be any positive number, so you can for
example get results more similar to the ones in the paper by
running ./runExperiments.sh 60 or more.
If you want to run the experiments with smaller amount or RAM, you
can pass the desired amount to ./runExperiments.sh as the third
argument. For example ./runExperiments.sh 5 2 runs the
experiments with CPU timeout of 5 seconds and with 2 GiB of RAM.
After you have all the experimental data, regardless of the
timeout, you can again go to the directory artifact and run the
script ./processResults.sh to process the resulting data. The
script should output several tables with results, generate LaTeX
files with those tables in results/tables, and generate PDFs with
plots in results/figures. However, most importantly, after the
script finishes, you should see a file results/results.pdf, which
contains nicely type-set tables and plots. Table 1 and 4 in this
file correspond to the tables from the paper and should have
exactly the same formatting. Actually, the tables in the paper are
result of merely including LaTeX files results/tables/solved.tex
and results/tables/cross.tex in the TeX source of the paper. The
same two files are also included in the PDF produced by the script.
Again, if the reader is interested in details of processing the
results, the scripts used in ./processResults.sh are generated
from the literate-programming file results/PROCESSRESULTS.org,
which contains all the used commands, describes their purpose and
contains all the results of these commands that were produced
during our experiments.
Precomputed results from our experiments can be found in the directory
artifact/logs. In particular, the directory contains the
directory artifact/logs/results, which is a copy of the directory
artifact/experiments/results generated by artifact/runExperiments.sh.
The directory also contains directories artifact/logs/tables,
artifact/logs/figures, and file artifact/log/results.pdf, which
are the respective copies of results of artifact/processResults.sh.
Therefore, if you copy the directory artifact/logs/results to the
directory artifact/experiments, you should obtain exactly the same
results.pdf file after running artifact/processResults.sh.
The binary of Q3B is located at artifact/solvers/Q3B/Q3B/build/q3b.
To run Q3B with an input file input.smt2, run
artifact/solvers/Q3B/Q3B/build/q3b input.smt2. To get all the available
options, run artifact/solvers/Q3B/Q3B/build/q3b --help.
The source code of Q3B is located at artifact/solvers/Q3B/Q3B/.
This directory contains the following directories
app, which containsmain.cpp, which reads the input from the user and runs the solver itself,cmake, which contains CMake modules,lib, which contains all the components described in the paper,parser, which contains grammar for ANTLR parser of SMT-LIB,tests, which contains regression and functional tests.
Q3B can be built from the source codes by creating a new directory
build, if it does not already exist, and then calling
cd build cmake .. -DANTLR_EXECUTABLE=/usr/share/java/antlr-4.7.2-complete.jar make make test