SMT Solvers Plug-in: Difference between revisions
imported>YGU |
imported>YGU |
||
| Line 43: | Line 43: | ||
=== Download Rodin Sources === | === Download Rodin Sources === | ||
Open the ''SVN Repository Exploring | 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 | 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 | ||
| Line 54: | Line 54: | ||
The downloading might be long (might take around 15min), do not interrupt. | The downloading 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'. | |||
=== Download SMT Plug-in Sources === | === Download SMT Plug-in Sources === | ||
Revision as of 13:21, 6 December 2010
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.
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'.
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:
