Difference between revisions of "SMT Solvers Plug-in"
imported>YGU m (SMT Plug-in moved to SMT Solvers Plug-in: Renamed with the name of the plug-in.) |
imported>YGU (Divided page between user support and developer support) |
||
| Line 1: | Line 1: | ||
| + | ''For developer support, see [[SMT Solvers Plug-in Developer Support]]'' | ||
{| align="right" | {| align="right" | ||
| __TOC__ | | __TOC__ | ||
| Line 72: | Line 73: | ||
Z3 solver can be downloaded at http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html. | Z3 solver can be downloaded at http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html. | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | + | == 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-Solvers''. | To use the plug-in, you must set up the SMT Solvers preferences by reaching the SMT solvers section: ''Windows > Preferences > SMT-Solvers''. | ||
| Line 206: | Line 126: | ||
== Releases Notes == | == Releases Notes == | ||
| − | |||
| − | |||
| − | |||
'''Version '''{{TODO|choose a version number for the coming release}} | '''Version '''{{TODO|choose a version number for the coming release}} | ||
| Line 224: | Line 141: | ||
* Full set theory support needs to be improved | * Full set theory support needs to be improved | ||
* No SMT-LIB 2.0 support in this release | * No SMT-LIB 2.0 support in this release | ||
| + | |||
| + | [[Category:Plugin]] | ||
| + | [[Category:User documentation]] | ||
Revision as of 08:25, 10 October 2011
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]).
Installation
You will need to:
- Install the Rodin Platform.
- Install the SMT Solvers Plug-in into Rodin.
- Install veriT if you want to use it (instead of ppTrans) to translate Event-B to SMT-LIB.
- Install the SMT solvers you want to use.
Installing the Rodin Platform
Download the Rodin Platform 2.3 (Core) (around 61MB) corresponding to your operating system and install it [2].
Installing the SMT Solvers Plug-in
Launch Rodin and go to Help > Install New Software....
Click the Add button and type:
TODO
Name it (ex: SMT Solvers Plug-in 0.1.0).
In order to make the plug-in item appear in the list, make sure that the option Group items by category is not checked.
Select item SMT Solvers Plug-in.
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.
TODO: is the security warning on unsigned content apprearing? Laurent: Yes it will always appear unless we sign the plug-in, which we don't do currently
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)
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 settings
To use the plug-in, you must set up the SMT Solvers preferences by reaching the SMT solvers section: Windows > Preferences > SMT-Solvers.
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 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 to SMT-LIB benchmarks, you need to fill the veriT path, by clicking the corresponding Browse button, and selecting the veriT binary.
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.
Usage
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:
For now, the proof tree doesn't contain any detail because SMT-LIB 1.2 doesn't implement a proof witnesses system.
Bugs and features request
- SMT-LIB 2.0 support in developpment
- Full set theory support in progress
Releases Notes
Version TODO: choose a version number for the coming release
- 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
