SMT Solvers Plug-in

From Event-B
Revision as of 16:44, 17 February 2012 by imported>YGU (→‎Introduction: Added a warning about the inclusion of an SMT tactic profile)
Jump to navigationJump to search

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 fully integrated and distributed 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....


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


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


Review the item to be installed and click Next.


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


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


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 plug-in integrates the SMT-solver veriT. 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.
You must set off proof production in Makefile.config, because the SMT plug-in needs solvers to check satisfiability only: 

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.

SMT solvers configurations

In order to use the plug-in, you must set up some SMT Solvers configuration.
We call SMT Solver configuration a settled configuration of a solver, with ad-hoc properties such as its path, 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, the SMT plug-in integrates the SMT-solver veriT. A configuration of this solver is already available in the plug-in : it launches the veriT solver (without e-prover), using the translation to SMT-LIB 2.0 and with the unsat-core extraction activated. To use the plug-in right now with this configuration, see #Usage.

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


Go to the SMT-Solvers page.


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

  • Fill the Solver ID with the name you want to give to this configuration.
  • Select the solver you want to use in this configuration (if it does not appear in the list, select unknown).
  • Click Browse to fill the solver executable path.
  • 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.).
  • Click OK.

The selected solver configuration is the blue one. This shows which solver configuration will be used when the SMT tactic will be called.
If you want to use another solver configuration, click on the corresponding line in the SMT-Solvers configurations list, and click Select.


SMT-LIB translation settings

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 plug-in integrates the SMT-solver veriT, so change this only if you want to use another veriT binary to produce SMT-LIB.

The plug-in may use some temporary files to discharge a sequent.
You can choose 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.


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

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

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

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

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.

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:

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.


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


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

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 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
Retrieved from ‘https://wiki.event-b.org/index.php?title=SMT_Solvers_Plug-in&oldid=9176’