Difference between revisions of "SMT Solvers Plug-in"
imported>Fages |
imported>YGU |
||
| Line 1: | Line 1: | ||
| − | == Introduction == | + | ==Introduction== |
| − | The SMT plug-in allows to use SMT solvers within Rodin. | + | The SMT plug-in allows users to use SMT solvers within Rodin. It is still in developpment (See sources [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/_exploratory/fages/]). |
| + | |||
| + | |||
| + | ==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 [http://wiki.eclipse.org/FAQ_Where_do_I_get_and_install_Eclipse%3F]. | ||
| + | |||
| + | |||
| + | === 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: | ||
| + | |||
| + | [[Image:Subclipse_selection.png]] | ||
| + | |||
| + | |||
| + | 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...'. | ||
| + | |||
| + | [[Image: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 == | == Usage == | ||
Revision as of 11:20, 6 December 2010
Contents
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:
