Difference between pages "User:Tommy/Collections/ADVANCE Delivrable D3.2" and "User:YGU/SMT Solvers Plug-in"

From Event-B
< User:Tommy(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>YGU
 
Line 1: Line 1:
{{saved_book}}
+
''For developer support, see [[SMT Solvers Plug-in Developer Support]]''
 +
{| align="right"
 +
| __TOC__
 +
|}
  
== Introduction ==
+
==Introduction==
The purpose of this page is to give a common structure and guidelines to collaboratively build the ADVANCE Deliverable D3.2 (Methods and tools for model construction and proof I) which will be delivered to the European Commission at month 10 (31st July 2012).
+
The SMT plug-in allows users to use SMT solvers within Rodin. It is still in development (See sources [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/_exploratory/fages/]).
The deliverable will give to the project reviewers some insight on what happened in the work package 3, concerning its 3 main objectives:
 
#to provide the methodological and tooling means for modelling Systems-of-Systems.
 
#to provide expert formal proof support to the industrial partners;
 
#to improve the usability and productivity of the Rodin platform to support larger-scale developments;
 
  
== Schedule ==
+
'''Since version 0.8:'''<br />
*the template of the deliverable is released on 01-06-2012
+
* '''the SMT-Solver veriT is bundled within the plug-in. Therefore, it is not necessary (but still possible) to install another copy of the solver.'''
*the contents are contributed by 22-06-2012
+
* '''An Auto-Tactic with SMT profile is available. Thus, it is not necessary (but still possible) to create a new profile to use SMT solvers tactics (see [[#Selecting an SMT auto-tactic profile]] to use this profile).'''
*the draft for internal review is sent on 29-06-2012
 
*the final deliverable is produced for 31-07-2012
 
  
== Template ==
+
==Installation==
For each item covered in this document, a wiki page has been created (see [[#Contents | Contents]]) to give a brief description of the work that was carried on during the first 10 months of the project (Oct 2011-July 2012). The contents of each page should not go deeply into technical details, but should rather look like an executive summary. All details (papers, detailed wiki pages, etc.) should be made available as pointers.
+
You will need to:
'''Moreover, each contribution shall be quite short (ca. two printed pages).'''
+
* Install the Rodin Platform.
 +
* Install the SMT Solvers Plug-in into Rodin.
 +
* Install any additional SMT-solvers you want to use.
  
== Direct link with the DoW ==
+
=== Installing the Rodin Platform ===
To ease the reviewer's reading of the present deliverable, the structure of the document will follow the objectives mentioned in the DoW:
+
Download the Rodin Platform 2.4 (Core) (around 69MB) corresponding to your operating system and install it [http://www.event-b.org/install.html].
''
 
D3.2) Methods and tools for model construction and proof I: This deliverable describes the maintenance actions
 
carried through, together with a summary of progress on the improvement of automated proof and model
 
checking. A list of the scalability enhancements achieved so far in the project, together with their expected
 
impact on performance and capacity, is included and validated against the Tool Development Roadmap.
 
Progress of the planned improvements to the existing automated proof tools is described, stating clearly what
 
improvements have been delivered and how the development of longer-term improvements measures against
 
the original plan. Appropriate documentation and tutorials are delivered to describe the methods that will ensure
 
that these improvements can be best used to increase the proportion of automated proofs. Improvements to the
 
ProB model checking tool and associated methods are also described. [month 10]''
 
  
=== Overview ===
+
=== Installing the SMT Solvers Plug-in ===
This first paragraph shall identify the involved partners and give an overview of the contribution. In particular, it shall provide answers to the following questions:
+
Launch Rodin and go to ''Help > Install New Software...''.
* What are the common denominations?
 
* Is it a new feature or an improvement?
 
* What is the main purpose?
 
* Who was in charge?
 
* Who was involved?
 
  
=== Motivations ===
+
[[Image:Install_new_software.png|450px]]
This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements were addressed and what are the main benefits.
 
  
=== Choices / Decisions ===
 
This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.
 
  
=== Available Documentation ===
+
Select the Rodin Platform Update Site: http://rodin-b-sharp.sourceforge.net/updates.
This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:
 
* Requirements.
 
* Pre-studies (states of the art, proposals, discussions).
 
* Technical details (specifications).
 
* Teaching materials (tutorials).
 
* User's guides.
 
A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.
 
  
=== Planning ===
+
[[Image:Select_update_site.png|450px]]
This paragraph shall give an outlook on the current status and the plans for future work.
 
  
== Formatting rules ==
 
In order to homogeneize the contributions and to ensure consistent spelling the following formatting rules shall be enforced:
 
* See §4 of [http://wiki.event-b.org/images/Llncsdoc.pdf How to Edit Your Input File] for LLNCS formatting rules.
 
* ADVANCE and Rodin shall be typed this way.
 
* Contractions shall not be used (eg. write "does not" instead of "doesn't", "let us" instead of "let's", etc).
 
* British english spelling shall be retained.
 
* "plug-in" shall be preferred to "plugin".
 
* Remember that the document is dated 31st July 2012, use past, present and future accordingly.
 
* The dedicated category, <nowiki>[[Category:ADVANCE D3.2 Deliverable]]</nowiki>, shall be specified for wiki pages.
 
* If you intend to use the same reference multiple times, please use the Cite extension [http://www.mediawiki.org/wiki/Extension:Cite/Cite.php] that has been installed recently.
 
: By doing so, you will have to add the additional paragraph at the end of your page :
 
==References==
 
<nowiki><references/></nowiki>
 
: Note that you can add references using the normal wikimedia links as well as using references nevertheless only the latter ones will appear in the references section on the wiki (e.g. all references will appear in the final PDF document whatever their type).
 
  
== ADVANCE Deliverable ==
+
Unfold the ''Prover Extensions'' category, and select the ''SMT Solvers Integration'' feature. Click ''Next''.
=== D3.2 ===
 
  
:[[ADVANCE D3.2 Introduction|Introduction]] (Laurent Voisin/Thomas Muller)
+
[[Image:Select_smt_feature.png|449px]]
  
:[[ADVANCE D3.2 General Platform Maintenance|General Platform Maintenance]]
 
:* Core Rodin platform (Thomas Muller)
 
:* UML-B Improvements (Colin Snook, Vitaly Savicks)
 
:* Code generation (Andy Edmunds)
 
:* ProR (Michael Jastram/Lukas Ladenberger)
 
:* Camille (Ingo Weigelt)
 
  
:[[ADVANCE D3.2 Improvement of automated proof|Improvement of automated proof]]
+
Review the item to be installed and click ''Next''.
:* Integrated provers (Laurent Voisin/Thomas Muller)
 
:* SMT Provers (Laurent Voisin)
 
  
:[[ADVANCE D3.2 Language extension|Language extension]](Issam Maamria)
+
[[Image:Review_install_details.png|449px]]
  
:[[ADVANCE D3.2 Model Checking|Model Checking]](Michael Leuschel & al.)
 
  
:[[ADVANCE D3.2 Model Composition and Decomposition|Model Composition and Decomposition]] (Renato Silva)
+
Read and accept the terms of the license agreement to install the plug-in. Then click ''Finish''.
  
[[Category:ADVANCE D3.2 Deliverable]]
+
[[Image:Review_licenses.png|449px]]
[[Category:Books]]
+
 
 +
 
 +
A security warning appears because the feature content is unsigned. Click ''Ok''.
 +
 
 +
[[Image:Security_warning.png|450px]]
 +
 
 +
 
 +
Click ''Restart Now''.
 +
 
 +
The SMT Solvers Plug-in is now installed.
 +
 
 +
=== Installing the SMT solvers ===
 +
Currently, the SMT plug-in has been tested with the following solvers:
 +
* Alt-Ergo (INRIA Saclay)
 +
* CVC3 (New York and Iowa Universities)
 +
* veriT (Loria Nancy and UFRN)
 +
* Z3 (Microsoft Research)
 +
 
 +
Since version 0.8.0, the SMT-solver veriT is bundled within the plug-in. To use the plug-in right now with this solver, see [[#Usage]].
 +
 
 +
==== 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.<br>
 +
If you want the plug-in to extract unsatisfiability cores from veriT proofs, make sure that the proof production is on in ''Makefile.config'' :
 +
# PROOF_PRODUCTION = NO
 +
PROOF_PRODUCTION = YES
 +
 
 +
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.
 +
 
 +
== Connecting SMT Solvers to the Rodin Platform ==
 +
In order to use the plug-in, you must connect some SMT solvers to the platform.<br>
 +
Such a connection is done by adding a new SMT solver in the plug-in user interface, and setting its path and kind.<br>
 +
 
 +
Since version 0.8.0, some SMT solvers are bundled within the plug-in, and some ad-hoc configurations are already available. To use the plug-in right now with these solvers, see [[#Usage]].
 +
 
 +
As to reach the SMT solvers page, open the ''Preferences'' window: ''Window > Preferences''.
 +
 
 +
[[Image:Preferences_menu.png|450px]]
 +
 
 +
 
 +
Unfold the SMT section and go to the Solvers page.
 +
 
 +
[[Image:SMT_solvers.png|500px]]
 +
 
 +
=== Adding a new SMT solver connection ===
 +
Add a new SMT solver into Rodin by clicking the ''Add'' button.
 +
 
 +
[[Image:Solver.png]]
 +
 
 +
* Fill the ''Name'' field with the name you want to give to this solver.
 +
* Select the kind of the solver if it appears in the combo box. In this case, this will let the plug-in use some specific options of the solver to make its integration possible. If it does not appear in the list, select ''unknown''.
 +
* Click ''Browse'' to fill the solver executable path.
 +
* Click ''OK''.
 +
 
 +
=== Editing an SMT solver connection ===
 +
You can edit all the informations given when adding a connection by clicking the ''Edit'' button. The bundled solvers connections cannot be edited.
 +
 
 +
=== Removing an SMT solver connection ===
 +
You can remove the connection with the ''selected'' solver by clicking the ''Remove'' button. The bundled solvers connections cannot be removed.
 +
 
 +
=== Restoring default solvers ===
 +
The default solvers are the bundled ones. A click on the ''Restore default'' button will remove all the solvers which are not bundled within the plugin.
 +
 
 +
== Customizing SMT solvers configurations ==
 +
In order to use the plug-in, you must set up some SMT Solvers configurations.<br>
 +
We call ''SMT Solver configuration'' a settled configuration of a solver, with ad-hoc properties such as its parameters and the SMT-LIB version of the benchmarks it will execute.<br>
 +
For example, such configurations can execute the same solver with different options, or different versions of the same solver, or different solvers.<br>
 +
 
 +
Since version 0.8.0, some SMT solvers are bundled within the plug-in. Some configurations of these solvers is already available in the plug-in : for example, the bundled veriT configuration launches the veriT solver (without e-prover), using the translation to SMT-LIB 2.0 and with the unsat-core extraction enabled. To use the plug-in right now with these configurations, see [[#Usage]].
 +
 
 +
As to reach the SMT solvers configurations page, open the ''Preferences'' window: ''Window > Preferences''.
 +
 
 +
[[Image:Preferences_menu.png|450px]]
 +
 
 +
 
 +
Go to the ''Configurations'' page.
 +
 
 +
[[Image:SMT_configurations.png|500px]]
 +
 
 +
 
 +
Add a new SMT solver configuration into Rodin by clicking the ''Add'' button.
 +
 
 +
[[Image:Solver_configuration.png|402px]]
 +
 
 +
* Fill the ''Name'' with the name you want to give to this configuration.
 +
* Choose whether this configuration shall be run or not when calling the SMT tactic by checking the ''Enable'' checkbox. This value can be changed directly in the ''Configurations'' page too.
 +
* Select the solver you want to use in this configuration. A solver to choose among the connected solvers of the ''Solvers'' page.
 +
* Fill the ''Solver arguments'' if needed. For example, you must enter here the solver option which sets the version of SMT-LIB to be used by the solver.
 +
* Select which version of SMT-LIB must be used by the plug-in.
 +
* Enter the value of the time out delay, which is, the time (in milliseconds) before which the platform will terminate the solver if it has not returned itself.
 +
 
 +
* Click ''OK''.
 +
 
 +
== Setting the SMT translation ==
 +
If you want to use veriT instead of ppTrans to translate Event-B sequents to SMT-LIB benchmarks, you need to fill the veriT path, by clicking the corresponding ''Browse'' button, and selecting the veriT binary. Since version 0.8.0, the SMT solver veriT is bundled within the plug-in and its path used by default, so change this only if you want to use another veriT binary to produce SMT-LIB benchmarks.
 +
 
 +
The plug-in may use some temporary files to discharge a sequent.<br>
 +
You can change the directory to use for this purpose, by clicking the corresponding ''Browse'' button, and selecting the target directory.
 +
 
 +
== SMT Auto-Tactic profile ==
 +
One might want to set-up one or several configurations of SMT solver to be used automatically to discharge Event-b sequents in the Rodin platform.<br>
 +
Since version 2.3 of Rodin, it is possible to create new ''tactic combinations'' called ''profiles'' to be applied automatically (See ''Advanced Profile Customisation'' in [[Rodin_Platform_2.3_Release_Notes]] and ''3.1.8.4 Sequent Prover / Auto/Post Tactic'' in [http://handbook.event-b.org/current/html/preferences.html the preference page of the Rodin User’s Handbook v.2.4]).<br>
 +
Since version 0.8.0 of the plug-in, an Auto-Tactic profile using SMT solvers is available in the plug-in. To use this profile, see [[#Selecting an SMT auto-tactic profile]].
 +
 
 +
=== Creating a new SMT auto-tactic profile ===
 +
 
 +
A reasonable combination using the SMT tactic is an SMT tactic queued to the default auto tactic combination. We show here how to create such a ''profile''.
 +
 
 +
First, open the ''Preferences'' window of the Rodin platform: ''Window > Preferences''.
 +
 
 +
[[Image:Preferences_menu.png|450px]]
 +
 
 +
 
 +
Open the ''Auto/Post Tactic'' preferences page: ''Event-B > Sequent Prover > Auto/Post Tactic''. Go to the ''Profiles'' tab.
 +
 
 +
[[Image:Duplicating_auto_tactic_profile.png|450px]]
 +
 
 +
Select the default auto tactic profile, and click ''Duplicate'' to duplicate it.
 +
 
 +
Then, select the duplicated profile, and click ''Edit'' to edit it.
 +
 
 +
[[Image:Auto_tactic_profile_duplicated.png|450px]]
 +
 
 +
In the tactic profile window, rename the profile, and drag and drop the chosen SMT tactic from the tactics list (in the first column) to the end of the combined tactics (in the second column).
 +
 
 +
[[Image:Adding_smt_tactic_in_profile.png|450px]]
 +
 
 +
Then click ''Finish''.
 +
 
 +
Now a new profile combining the SMT tactic with other tactics is created.
 +
 
 +
 
 +
=== Selecting an SMT auto-tactic profile ===
 +
 
 +
One may want to use the new SMT auto-tactic profile (available since version 0.8.0 of the plug-in), or a user-defined profile using SMT solvers.
 +
 
 +
To set it on, go to the ''Auto/Post Tactic'' tab.
 +
 
 +
[[Image:Smt auto tactic profile selected.png|450px]]
 +
 
 +
Set the tactic profile to be used for auto-tactics up to the one combining the SMT tactic, by using the drop-down menu.
 +
 
 +
Then click ''Ok''.
 +
 
 +
Now, the combined tactics of your new profile, including the SMT tactic, will be automatically launched when auto-provers are called.
 +
 
 +
== Usage ==
 +
 
 +
=== Discharging a sequent ===
 +
We give an example of Event-B model of which proof obligation can be discharge using an SMT solver:
 +
 
 +
[[Image:PrettyPrinted context.png|225px]]
 +
[[Image:Hypothesis and goal.png|225px]]
 +
 
 +
''thm1'' is a theorem which must be proved given axioms ''axm2..axm5''.
 +
 
 +
 
 +
Since we installed SMT Plug-in into the Rodin Platform, the SMT tactic button is now accessible in the ''Proof Control'' bar.
 +
 
 +
[[Image:SMT button.png|450px]]
 +
 
 +
 
 +
Clicking on this button will call the previously selected SMT solver, which will discharge the proof obligation if possible:
 +
 
 +
[[Image:Tactic applied successfully.png|450px]]
 +
 
 +
 
 +
When the tactic is applied successfully, this means that the reasonner created the new proof rule:
 +
 
 +
[[Image:Proof Tree and Rule Details.png|450px]]
 +
 
 +
If the solver used to discharge the sequent is able to extract an unsatisfiability core, the proof rule will be produced using it. This is the case for veriT.
 +
 
 +
== Bugs and features request ==
 +
* SMT-LIB 2.0 support with the veriT translation approach in developpment
 +
* Full set theory support in progress
 +
 
 +
== Releases Notes ==
 +
 
 +
'''Version 1.0.0'''
 +
* Cvc3 SMT solver bundled with the plug-in
 +
* User Interface entirely refactored for more intuitive experience
 +
 
 +
'''Version 0.8.0'''
 +
* Support of SMT-LIB 2.0 in the PP translation approach
 +
* Inclusion of the SMT-Solver veriT in the plug-in
 +
* Addition of an SMT auto-tactic
 +
* Auto-Tactic profile containing the SMT auto-tactic
 +
* Possibility to parameterize a new SMT tactic
 +
* Integration of solvers successfully tested with:
 +
** Alt-Ergo 0.93
 +
** Cvc3 2011-11-21
 +
** veriT (included in the plug-in)
 +
** z3 3.2
 +
** Cvc4 2011-12-11 (but few theories are available for now)
 +
* Good results in the field of linear integer arithmetic with uninterpreted sort and function symbols
 +
* Good support of basic set theory
 +
* Full set theory support needs to be improved
 +
* Results showed the SMT-Solvers Plug-in was a good alternative to the Atelier-B provers
 +
 
 +
'''Version 0.1.0'''
 +
* Initial beta-release.
 +
* Two approaches for translating Event-B to SMT-LIB 1.2:
 +
** with ppTrans (included in Rodin official releases)
 +
** with veriT (must be installed)
 +
* Integration of solvers successfully tested with: ''(notice that no solver will be included in the plug-in at all)''
 +
** Alt-Ergo 0.93
 +
** Cvc3 2011-07-14
 +
** veriT 201107
 +
** z3 2.19
 +
* Good results in the field of linear integer arithmetic with uninterpreted sort and function symbols
 +
* Good support of basic set theory
 +
* Full set theory support needs to be improved
 +
* No SMT-LIB 2.0 support in this release
 +
 
 +
[[Category:Plugin]]
 +
[[Category:User documentation]]

Revision as of 14:36, 4 April 2012

For developer support, see SMT Solvers Plug-in Developer Support

Introduction

The SMT plug-in allows users to use SMT solvers within Rodin. It is still in development (See sources [1]).

Since version 0.8:

  • the SMT-Solver veriT is bundled within the plug-in. Therefore, it is not necessary (but still possible) to install another copy of the solver.
  • An Auto-Tactic with SMT profile is available. Thus, it is not necessary (but still possible) to create a new profile to use SMT solvers tactics (see #Selecting an SMT auto-tactic profile to use this profile).

Installation

You will need to:

  • Install the Rodin Platform.
  • Install the SMT Solvers Plug-in into Rodin.
  • Install any additional SMT-solvers you want to use.

Installing the Rodin Platform

Download the Rodin Platform 2.4 (Core) (around 69MB) corresponding to your operating system and install it [2].

Installing the SMT Solvers Plug-in

Launch Rodin and go to Help > Install New Software....

Install new software.png


Select the Rodin Platform Update Site: http://rodin-b-sharp.sourceforge.net/updates.

Select update site.png


Unfold the Prover Extensions category, and select the SMT Solvers Integration feature. Click Next.

Select smt feature.png


Review the item to be installed and click Next.

Review install details.png


Read and accept the terms of the license agreement to install the plug-in. Then click Finish.

Review licenses.png


A security warning appears because the feature content is unsigned. Click Ok.

Security warning.png


Click Restart Now.

The SMT Solvers Plug-in is now installed.

Installing the SMT solvers

Currently, the SMT plug-in has been tested with the following solvers:

  • Alt-Ergo (INRIA Saclay)
  • CVC3 (New York and Iowa Universities)
  • veriT (Loria Nancy and UFRN)
  • Z3 (Microsoft Research)

Since version 0.8.0, the SMT-solver veriT is bundled within the plug-in. To use the plug-in right now with this solver, see #Usage.

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.
If you want the plug-in to extract unsatisfiability cores from veriT proofs, make sure that the proof production is on in Makefile.config :

# PROOF_PRODUCTION = NO
PROOF_PRODUCTION = YES

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.

Connecting SMT Solvers to the Rodin Platform

In order to use the plug-in, you must connect some SMT solvers to the platform.
Such a connection is done by adding a new SMT solver in the plug-in user interface, and setting its path and kind.

Since version 0.8.0, some SMT solvers are bundled within the plug-in, and some ad-hoc configurations are already available. To use the plug-in right now with these solvers, see #Usage.

As to reach the SMT solvers page, open the Preferences window: Window > Preferences.

Preferences menu.png


Unfold the SMT section and go to the Solvers page.

SMT solvers.png

Adding a new SMT solver connection

Add a new SMT solver into Rodin by clicking the Add button.

Solver.png

  • Fill the Name field with the name you want to give to this solver.
  • Select the kind of the solver if it appears in the combo box. In this case, this will let the plug-in use some specific options of the solver to make its integration possible. If it does not appear in the list, select unknown.
  • Click Browse to fill the solver executable path.
  • Click OK.

Editing an SMT solver connection

You can edit all the informations given when adding a connection by clicking the Edit button. The bundled solvers connections cannot be edited.

Removing an SMT solver connection

You can remove the connection with the selected solver by clicking the Remove button. The bundled solvers connections cannot be removed.

Restoring default solvers

The default solvers are the bundled ones. A click on the Restore default button will remove all the solvers which are not bundled within the plugin.

Customizing SMT solvers configurations

In order to use the plug-in, you must set up some SMT Solvers configurations.
We call SMT Solver configuration a settled configuration of a solver, with ad-hoc properties such as its parameters and the SMT-LIB version of the benchmarks it will execute.
For example, such configurations can execute the same solver with different options, or different versions of the same solver, or different solvers.

Since version 0.8.0, some SMT solvers are bundled within the plug-in. Some configurations of these solvers is already available in the plug-in : for example, the bundled veriT configuration launches the veriT solver (without e-prover), using the translation to SMT-LIB 2.0 and with the unsat-core extraction enabled. To use the plug-in right now with these configurations, see #Usage.

As to reach the SMT solvers configurations page, open the Preferences window: Window > Preferences.

Preferences menu.png


Go to the Configurations page.

SMT configurations.png


Add a new SMT solver configuration into Rodin by clicking the Add button.

Solver configuration.png

  • Fill the Name with the name you want to give to this configuration.
  • Choose whether this configuration shall be run or not when calling the SMT tactic by checking the Enable checkbox. This value can be changed directly in the Configurations page too.
  • Select the solver you want to use in this configuration. A solver to choose among the connected solvers of the Solvers page.
  • Fill the Solver arguments if needed. For example, you must enter here the solver option which sets the version of SMT-LIB to be used by the solver.
  • Select which version of SMT-LIB must be used by the plug-in.
  • Enter the value of the time out delay, which is, the time (in milliseconds) before which the platform will terminate the solver if it has not returned itself.
  • Click OK.

Setting the SMT translation

If you want to use veriT instead of ppTrans to translate Event-B sequents to SMT-LIB benchmarks, you need to fill the veriT path, by clicking the corresponding Browse button, and selecting the veriT binary. Since version 0.8.0, the SMT solver veriT is bundled within the plug-in and its path used by default, so change this only if you want to use another veriT binary to produce SMT-LIB benchmarks.

The plug-in may use some temporary files to discharge a sequent.
You can change the directory to use for this purpose, by clicking the corresponding Browse button, and selecting the target directory.

SMT Auto-Tactic profile

One might want to set-up one or several configurations of SMT solver to be used automatically to discharge Event-b sequents in the Rodin platform.
Since version 2.3 of Rodin, it is possible to create new tactic combinations called profiles to be applied automatically (See Advanced Profile Customisation in Rodin_Platform_2.3_Release_Notes and 3.1.8.4 Sequent Prover / Auto/Post Tactic in the preference page of the Rodin User’s Handbook v.2.4).
Since version 0.8.0 of the plug-in, an Auto-Tactic profile using SMT solvers is available in the plug-in. To use this profile, see #Selecting an SMT auto-tactic profile.

Creating a new SMT auto-tactic profile

A reasonable combination using the SMT tactic is an SMT tactic queued to the default auto tactic combination. We show here how to create such a profile.

First, open the Preferences window of the Rodin platform: Window > Preferences.

Preferences menu.png


Open the Auto/Post Tactic preferences page: Event-B > Sequent Prover > Auto/Post Tactic. Go to the Profiles tab.

Duplicating auto tactic profile.png

Select the default auto tactic profile, and click Duplicate to duplicate it.

Then, select the duplicated profile, and click Edit to edit it.

Auto tactic profile duplicated.png

In the tactic profile window, rename the profile, and drag and drop the chosen SMT tactic from the tactics list (in the first column) to the end of the combined tactics (in the second column).

Adding smt tactic in profile.png

Then click Finish.

Now a new profile combining the SMT tactic with other tactics is created.


Selecting an SMT auto-tactic profile

One may want to use the new SMT auto-tactic profile (available since version 0.8.0 of the plug-in), or a user-defined profile using SMT solvers.

To set it on, go to the Auto/Post Tactic tab.

Smt auto tactic profile selected.png

Set the tactic profile to be used for auto-tactics up to the one combining the SMT tactic, by using the drop-down menu.

Then click Ok.

Now, the combined tactics of your new profile, including the SMT tactic, will be automatically launched when auto-provers are called.

Usage

Discharging a sequent

We give an example of Event-B model of which proof obligation can be discharge using an SMT solver:

PrettyPrinted context.png Hypothesis and goal.png

thm1 is a theorem which must be proved given axioms axm2..axm5.


Since we installed SMT Plug-in into the Rodin Platform, the SMT tactic button is now accessible in the Proof Control bar.

SMT button.png


Clicking on this button will call the previously selected SMT solver, which will discharge the proof obligation if possible:

Tactic applied successfully.png


When the tactic is applied successfully, this means that the reasonner created the new proof rule:

Proof Tree and Rule Details.png

If the solver used to discharge the sequent is able to extract an unsatisfiability core, the proof rule will be produced using it. This is the case for veriT.

Bugs and features request

  • SMT-LIB 2.0 support with the veriT translation approach in developpment
  • Full set theory support in progress

Releases Notes

Version 1.0.0

  • Cvc3 SMT solver bundled with the plug-in
  • User Interface entirely refactored for more intuitive experience

Version 0.8.0

  • Support of SMT-LIB 2.0 in the PP translation approach
  • Inclusion of the SMT-Solver veriT in the plug-in
  • Addition of an SMT auto-tactic
  • Auto-Tactic profile containing the SMT auto-tactic
  • Possibility to parameterize a new SMT tactic
  • Integration of solvers successfully tested with:
    • Alt-Ergo 0.93
    • Cvc3 2011-11-21
    • veriT (included in the plug-in)
    • z3 3.2
    • Cvc4 2011-12-11 (but few theories are available for now)
  • Good results in the field of linear integer arithmetic with uninterpreted sort and function symbols
  • Good support of basic set theory
  • Full set theory support needs to be improved
  • Results showed the SMT-Solvers Plug-in was a good alternative to the Atelier-B provers

Version 0.1.0

  • Initial beta-release.
  • Two approaches for translating Event-B to SMT-LIB 1.2:
    • with ppTrans (included in Rodin official releases)
    • with veriT (must be installed)
  • Integration of solvers successfully tested with: (notice that no solver will be included in the plug-in at all)
    • Alt-Ergo 0.93
    • Cvc3 2011-07-14
    • veriT 201107
    • z3 2.19
  • Good results in the field of linear integer arithmetic with uninterpreted sort and function symbols
  • Good support of basic set theory
  • Full set theory support needs to be improved
  • No SMT-LIB 2.0 support in this release