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 plugin 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.

Install the Eclipse Platform

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

Install the Subclipse plugin

Launch Eclipse and go to the 'Help' Menu -> 'Install New Software...' entry.

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'.

Download 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 downloading might be long (might take around 15min), do not interrupt.

Download 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

Usage

To use the plugin, the user must set up SMT preferences by reaching the Windows/Preferences Menu of Rodin

The user must provide info on solvers just like if a preprocessing is used or not. Pushing the Create button leads to the following window:

Solver preference creation

The user must provide following info:

- An Id,
- A path,
- Arguments used to call the solver,
- On which SMT-LIB version the solver will be used.   

Solver selection

The user must then select the solver that will be used:

Solver launching

To launch the SMT solver on the selected Proof Obligation, the user must press the SMT button:

Solver result

If the SMT solver suceeds, the status will be updated in the proof tree: