SMT Solvers Plug-in: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>YGU
imported>YGU
No edit summary
Line 6: Line 6:
You'll need to:
You'll need to:
* Install the Eclipse Platform.
* Install the Eclipse Platform.
* Install the Subclipse plugin to use SVN in Eclipse.
* Install the Subclipse plug-in to use SVN in Eclipse.
* Download Rodin sources into Eclipse.
* Download Rodin sources into Eclipse.
* Download SMT plug-in sources into Eclipse.
* Download SMT plug-in sources into Eclipse.
* Install the SMT solvers you want to use.
* Install the SMT solvers you want to use.


 
=== Installing the Eclipse Platform ===
=== 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].
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].


=== Installing the Subclipse plug-in ===
Launch Eclipse and go to ''Help > Install New Software...''.


=== Install the Subclipse plugin ===
Click the ''Add'' button and type:
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
http://subclipse.tigris.org/update_1.6.x


Name it (ex: SUBCLIPSE 1.6).
Name it (ex: SUBCLIPSE 1.6).


Then select the same items as in the following image:
Then select the same items as in the following image:


[[Image:Subclipse_selection.png]]
[[Image:Subclipse_selection.png|600px]]
 


Under Linux, in order to use JNI, you'll need to install the following packages:
Under Linux, in order to use JNI, you'll need to install the following packages:
Line 39: Line 35:
''-Djava.library.path=/usr/lib/jni''
''-Djava.library.path=/usr/lib/jni''


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


=== Download Rodin Sources ===
=== Downloading the Rodin Sources ===
Open the ''SVN Repository Exploring'' perspective.
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


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


[[Image:Rodin selection checkout.png]]
[[Image:Rodin selection checkout.png|400px]]


'Check out into the workspace as projects' must be selected. Then click 'Finish'.
''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.
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'.
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 ===
=== Downloading the SMT Plug-in Sources ===
Do the same as to dowload Rodin sources, with projects in 'trunk -> exploratory -> fages':
Do the same as to dowload Rodin sources, with projects in ''trunk > exploratory > fages'':
* fr.systerel.smt.provers.core
* fr.systerel.smt.provers.core
* fr.systerel.smt.provers.help
* fr.systerel.smt.provers.help
Line 64: Line 59:
* fr.systerel.smt.provers.ui
* 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. 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[http://eprover.org/] (''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''.
[[Image:Run As EclipseApp.png|450px]]


The Rodin platform is launched and ready.


== Usage  ==
=== 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''.
 
[[Image:Plug-ins to select.png|450px]]


To use the plugin, the user must set up SMT preferences by reaching the Windows/Preferences Menu of Rodin
Now, you can launch the Rodin platform extended with the SMT plug-in.


[[Image:preferences.PNG]]
=== 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''.


[[Image:preferences2.PNG]]
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''


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:
Then you must select which solver will be used when calling SMT tactic by selecting this solver's line and click ''Select'':


[[Image:preferences3.PNG]]
[[Image:Selected solver.png|450px]]


=== Solver preference creation ===
The selected solver is the blue one.


The user must provide following info:
=== SMT-LIB translation settings ===
- An Id,
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.
- 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:


[[Image:preferences4.PNG]]
== Usage  ==
{{TODO|Screenshots to be simplified. Must show Rules details and Proof Tree.}}


=== Solver launching ===
=== Solver launching ===

Revision as of 17:20, 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 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. 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

TODO: Screenshots to be simplified. Must show Rules details and Proof Tree.

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:

Retrieved from ‘https://wiki.event-b.org/index.php?title=SMT_Solvers_Plug-in&oldid=9134’