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

File:Exemple.jpg

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