Event-B to SMT-LIB

From Event-B
Revision as of 10:22, 24 October 2011 by imported>YGU (Updated this page with last theorical approaches of translation used in the the SMT Solvers Plug-in. A link to a recent DECERT report is still missing.)
Jump to navigationJump to search

Introduction

The need for translating the Event-B language to the SMT-LIB language was introduced by the DECERT project, of which one task is to integrate the SMT solvers into the Rodin platform. Such an integration would increase the proving performances of the platform among a set of lemmas often encountered in practice, defined in the Work Package 1 of the project. Using the SMT-LIB standard is a requirement for this project.

A first approach with veriT

A first approach for running the translation is to use veriT to produce the SMT-LIB benchmarks which we intend to give as input to the SMT solvers. The idea is to take advantage of the capability of veriT to translate benchmarks expressed with its slightly extended version of the SMT-LIB language into standard SMT-LIB benchmarks. This way, we just need to implement the translation of Event-B language into the veriT extensions of the SMT-LIB language. It comes down to running a direct syntactic translation when the formula does not contain any set construction, or using a veriT macro otherwise.

At first, following on from the choice of using its macros, veriT was integrated into Rodin and responsible for translating them. All the translation rules used in this approach were originally extracted from the article of David Deharbe, Integration of Smt-solvers in B and Event-b Development environments, but some of them were fixed and some additional ones added. Unfortunately, veriT has one restriction: it does not handle proof obligations which contain sets of sets.

Another approach with ppTrans

Another approach is to use the translator ppTrans provided by the Predicate Prover available in Rodin (see project trunk/RodinCore/org.eventb.pptrans, among the sources of the Rodin platform) so as to obtain predicate expressions which are almost free of set-theoretic elements. More precisely, ppTrans removes most set-theoretic constructs of a predicate, separates arithmetic and set-theoretic constructs from each other and simplifies predicates. Once this is done, the Event-B Abstract Syntax Tree to be translated in SMT-LIB is restricted to the abstract syntax of ppTrans. This approach doesn’t only make the plug-in independent from veriT, but also resolves relations and functions problems.

Previous work

A first version (See its specification draft) was mainly focusing on lemmas based on unquantified integer linear arithmetic. Its implementation can be found under the following repositories:

  • _exploratory/carinepascal/fr.systerel.decert
  • _exploratory/carinepascal/fr.systerel.decert.tests

It partially supports the following theories: Linear Arithmetic, Linear Order and Integer.

Instructions to use it

The XML files containing the Event-B lemmas are assumed to be stored in the Lemmas folder. The SMT files containing the SMT-LIB benchmarks are assumed to be stored in the Benchmarks folder.

Follow the steps below in order to translate Event-B lemmas to SMT-LIB benchmarks:

  1. Launch the fr.systerel.decert.tests.TypeCheckingTests JUnit test to type-check the lemmas (optional). Note that it is previously necessary to set the XMLFolder field of the TypeCheckingTests class to specify the absolute path of the Lemmas folder.
  2. Launch the fr.systerel.decert.tests.smt.TranslationTests JUnit test to translate the lemmas (mandatory). Note that it is necessary to previously configure the test:
    • The XMLFolder field shall contain the absolute path of the Lemmas folder.
    • The SMTFolder field shall contain the absolute path of the Benchmarks folder.
    • If the format of the generated SMT files is to be checked, the CHECK_FORMAT option shall be set and the SMTParserFolder field shall contain the absolute path of the directory where is installed the SMT-LIB parser. Otherwise, the option shall be turned off. The SMT-LIB parser is available from the SMT-LIB web page.
    • If the generated benchmarks are to be checked for satisfiability, the CHECK_SAT option shall be set and the SMTSolverFolder field shall contain the absolute path of the directory where is installed the Z3 SMT solver. Otherwise, the option shall be turned off. The Z3 SMT solver is available from the following address (Note that the 2.0 version is not supported because it does not support user-defined attributes).

Bibliography

Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_to_SMT-LIB&oldid=4344’