SMT Solvers Plug-in: Difference between revisions

Revision as of 15:18, 24 September 2010

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.

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:

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.

The user must then select the solver that will be used:

To launch the SMT solver on the selected Proof Obligation, the user must press the SMT button:

If the SMT solver suceeds, the status will be updated in the proof tree:

@@ Line 5: / Line 5: @@
 == Usage  ==
+To use the plugin, the user must set up SMT preferences by reaching the Windows/Preferences Menu of Rodin
+[[Image:preferences.PNG]]
+[[Image:preferences2.PNG]]
+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:
+[[Image:preferences3.PNG]]
+=== 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:
+[[Image:preferences4.PNG]]
+=== Solver launching ===
+To launch the SMT solver on the selected Proof Obligation, the user must press the SMT button:
+[[Image:smt.PNG]]
+=== Solver result ===
+If the SMT solver suceeds, the status will be updated in the proof tree:
+[[Image:smt2.PNG]]