SMT Plug-in Performance

This page describes how to measure the performance of SMT solvers linked to the Rodin platform through the SMT Solvers plug-in.

Performance is measured by running the SMT solvers on a set of proof obligations coming from some Event-B projects. Each solver is run in the exact same conditions (input sequent, timeout, etc.) to avoid introducing any bias.

Moreover, the solvers are not run straight, but integrated within a more general tactic derived from the Default Auto Tactic packaged with the Rodin platform. This makes the tests closer to the end-user experience, and therefore more meaningful.

Finally, the SMT solvers are tested side-by-side with the Atelier B provers. This allows to compare their performance relative to the de facto standard automated provers that have always been available with Rodin.

Required Software

To start with, you need a Rodin platform with the Atelier B and SMT solvers plug-ins installed. Proceed as usual to install this software.

Then you need to install the testing application from the zipped update site http://sourceforge.net/projects/rodin-b-sharp/files/Plugin_SMT_Solvers/PerfApp/org.eventb.smt.core.perf.app-1.0.0.201404291022.zip/download.

Test Layout

The tests are organized in a directory as follows:

├─ preferences
├─ projects/
│   ├── ProjectOne/
│   ├── ProjectTwo/
├─ results/
├─ solvers/
├─ workspace/

where

preferences

text file describing the SMT configurations to run

projects

contains proof obligations to test, organized in Event-B projects

results

will contain the detailed results of the tests (that is all proof and proof status files created by the tests)

solvers

contains the SMT solvers to run

workspace

is a temporary directory used when running tests

Preparing tests

To prepare the tests, you need some proof obligations and some SMT solvers.

Preparing Proof Obligations

The easiest way to prepare your proof obligations is to fetch some Rodin project archives, for instance from the Advance/Deploy Repository.

If you want to be sure to start from a clean project, you can import the archive in a running Rodin platform, remove all proof files of the project, clean the project and rebuild it with the automated prover disabled.

In the end, you need to copy all projects containing proof obligations into the projects directory.

Preparing SMT solvers

Install the binary files of your SMT solver into the solvers directory and for each define at least one configuration in the preferences file. A model for the preferences file is available from https://sourceforge.net/p/rodin-b-sharp/smt/ci/master/tree/PerformanceApp/org.eventb.smt.core.perf.app/preferences.model.

Running Tests

To run the tests, you need to start Rodin from a command line, specifying the test application

   rodin -application org.eventb.smt.core.perf.app.main \
         -data /path/to/workspace \
         -nosplash -consoleLog /path/to/preferences-file

This will test each solver configured in the given preferences file on every projects. The proof and proof status files will be copied into the results directory.

Caution: The contents of the workspace and results directories will be wiped clean before running the tests.

If you want more details on the interaction with the SMT solvers, you can turn on tracing. For this create a file called `options` in the current directory with the contents

   org.eventb.smt.core/debug = true
   org.eventb.smt.core/debug/translator = true
   org.eventb.smt.core/debug/translator_details = true

and add the two arguments -debug `pwd`/options to the command line.

Exploiting Test Results

While the tests are run, some global statistics are displayed on the console. If you want more detailed statistics you can use this script or even tailor it to you specific needs.