SMT Solvers Plug-in

Introduction

The SMT plug-in allows users to use SMT solvers within Rodin. It is still in developpment (See sources [1]).

Installation

You'll need to:

Install the Eclipse Platform.
Install the Subclipse plug-in to use SVN in Eclipse.
Download Rodin sources into Eclipse.
Download SMT plug-in sources into Eclipse.
Install the SMT solvers you want to use.

Installing the Eclipse Platform

Download Eclipse Classic (SDK) (169 MB) at http://www.eclipse.org/downloads/ . Install it [2].

Installing the Subclipse plug-in

Launch Eclipse and go to Help > Install New Software....

Click the Add button and type:

http://subclipse.tigris.org/update_1.6.x

Name it (ex: SUBCLIPSE 1.6).

Then select the same items as in the following image:

Under Linux, in order to use JNI, you'll need to install the following packages:

   * libsvn-java
   * subversion
   * libsvn1

and to link the installation directory in eclipse.ini, by adding:

-Djava.library.path=/usr/lib/jni

then restart Eclipse and select JavaHL in Window > Preferences > Team > SVN.

Downloading the Rodin Sources

Open the SVN Repository Exploring perspective.

Right-clic in the SVN Repositories view, then New > Repository Location. Enter the following URL : https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp

Select all projects in trunk > RodinCore then right-clic and Checkout....

Check out into the workspace as projects must be selected. Then click Finish.

The download might be long (might take around 15min), do not interrupt.

Once all the sources are downloaded, get back to the Java perspective. org.eventb.core.seqprover and org.eventb.core.seqprover.tests projects might need to be recompiled: select the former and press F5.

Downloading the SMT Plug-in Sources

Do the same as to dowload Rodin sources, with projects in trunk > exploratory > fages:

fr.systerel.smt.provers.core
fr.systerel.smt.provers.help
fr.systerel.smt.provers.tests
fr.systerel.smt.provers.ui

Installing the SMT solvers

Currently, the SMT plug-in has been tested with the following solvers:

veriT (Loria Nancy and UFRN)
Alt-Ergo (INRIA Saclay)
CVC3 (New York and Iowa Universities)
Z3 (Microsoft Research)

Installing veriT

veriT solver can be downloaded at http://www.verit-solver.org/veriT-download.php. Compilation and installation instructions are in the INSTALL file. You must set off proof production in Makefile.config, because the SMT plug-in needs solvers to check satisfiability only:

PROOF_PRODUCTION = NO
# PROOF_PRODUCTION = YES

The following tools are used in the installation process (Debian/Ubuntu platforms):

gcc, g++: compilers
make, ar, ranlib: build process
wget, tar, patch: to fetch GMP and Minisat
bison, flex, m4: build compilers and preprocessing

Do not forget to install the E-prover as well[3] (eprover package on Ubuntu platforms).

Installing Alt-Ergo

alt-ergo solver can be downloaded at http://alt-ergo.lri.fr/, or installed using the Ubuntu repository: alt-ergo package.

Installing CVC3

CVC3 solver can be downloaded at http://cs.nyu.edu/acsys/cvc3/download.html, or installed using the Ubuntu repository: cvc3 package.

Installing Z3

Z3 solver can be downloaded at http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html.

Configuration

You'll need to:

Launch the Rodin platform as to set the default Run Configuration.
Add the SMT plug-ins to this configuration.
Set the SMT solvers you want to use within Rodin.

Launching the Rodin Platform

Once we have downloaded the Rodin sources, and built it within Eclipse, we can launch the Rodin platform.

Enter the org.rodinp.platform project and right-clic Rodin.product file then choose Run As... > Eclipse Application.

The Rodin platform is launched and ready.

Adding the SMT plug-ins to the Run Configuration

Close the Rodin Platform. Back in the Eclipse Platform, go to the Run Configuration: Run > Run Configurations....

Select the Rodin.product configuration, and go to the Plug-ins tab. Check all the SMT Plug-ins except fr.systerel.smt.provers.tests.

Now, you can launch the Rodin platform extended with the SMT plug-in.

SMT solvers settings

To use the plug-in, you must set up the SMT Solvers preferences by reaching the SMT solvers section: Windows > Preferences > SMT Solver.

Add a new SMT solver configuration into Rodin by clicking the Add button:

Fill the Solver ID with the name of the solver
Click Browse to fill the solver path
Fill the Solver arguments if needed. For now, veriT, Alt-Ergo and Z3 do not need any argument. CVC3 must be used with -lang smt argument.
Select which version of SMT-LIB must be used by the plug-in (Currently, version 1.2 is the only one covered by the plug-in).
Click OK

Then you must select which solver will be used when calling SMT tactic by selecting this solver's line and click Select:

The selected solver is the blue one.

SMT-LIB translation settings

If you want to use veriT instead of ppTrans to translate Event-B sequents into SMT-LIB benchmarks, select prepro option, and click Browse to fill veriT's path.

Usage

We give an example of Event-B model of which proof obligation can be discharge using an SMT solver:

thm1 is a theorem which must be proved given axioms axm2..axm5.

Since we installed SMT Plug-in into the Rodin Platform, the SMT tactic button is now accessible in the Proof Control bar.

Clicking on this button will call the previously selected SMT solver, which will discharge the proof obligation if possible:

When the tactic is applied successfully, this means that the reasonner created the new proof rule:

For now, the proof tree doesn't contain any detail because SMT-LIB 1.2 doesn't implement a proof witnesses system.