SMT Solvers Plug-in

Introduction

The SMT plug-in allows to use SMT solvers within Rodin.

For the moment, it can handle some basic arithmetic proof obligations but still needs to be improved to be much more efficient.

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: