Event-B to SMT-LIB - Revision history

imported>YGU: /* Previous work */

2011-10-24T10:29:12Z

Previous work

← Older revision		Revision as of 10:29, 24 October 2011
Line 15:		Line 15:
	== Previous work ==		== Previous work ==

	A first version (~~See~~ its [[#ancre_2\|specification draft]]) was mainly focusing on lemmas based on unquantified integer linear arithmetic. Its implementation can be found under the following repositories:		A first version (see its [[#ancre_2\|specification draft]]) was mainly focusing on lemmas based on unquantified integer linear arithmetic. Its implementation can be found under the following repositories:
	* <tt>_exploratory/carinepascal/fr.systerel.decert</tt>		* <tt>_exploratory/carinepascal/fr.systerel.decert</tt>
	* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>		* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>

imported>YGU at 10:28, 24 October 2011

2011-10-24T10:28:37Z

← Older revision		Revision as of 10:28, 24 October 2011
Line 8:		Line 8:
	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.		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.		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 [[#deharbe \| article]] of David Deharbe, 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 with ppTrans ==
Line 37:		Line 37:

	== Bibliography ==		== Bibliography ==
			* D. Deharbe, <font id="deharbe">''Integration of Smt-solvers in B and Event-b Development environments''</font>.
	* M. Konrad and L. Voisin, <font id="ppTrans">''Translation from set-theory to predicate calculus''</font>, 2010.		* M. Konrad and L. Voisin, <font id="ppTrans">''Translation from set-theory to predicate calculus''</font>, 2010.
	* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.		* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.

	[[Category:Design]]		[[Category:Design]]

imported>YGU at 10:23, 24 October 2011

2011-10-24T10:23:35Z

← Older revision		Revision as of 10:23, 24 October 2011
Line 37:		Line 37:

	== Bibliography ==		== Bibliography ==
			* M. Konrad and L. Voisin, <font id="ppTrans">''Translation from set-theory to predicate calculus''</font>, 2010.
	* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.		* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.
	* M. Konrad and L. Voisin, <font id="ppTrans">''Translation from set-theory to predicate calculus''</font>, 2010.

	[[Category:Design]]		[[Category:Design]]

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.

2011-10-24T10:22:37Z

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.

← Older revision		Revision as of 10:22, 24 October 2011
Line 2:		Line 2:

	== Introduction ==		== Introduction ==
	~~The Event-B to [[#ancre_3\|SMT-LIB]] plug-in allows to translate mathematical lemmas that rely on the Event-B language to the SMT-LIB format.~~

	The ~~considered lemmas are those often encountered in practice, but not yet well supported~~ by ~~proving~~		The need for translating the Event-B language to the SMT-LIB language was introduced by the [http://decert.gforge.inria.fr/index.html DECERT] project, of which one task is to [[SMT_Solvers_Plug-in \| 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 [http://decert.gforge.inria.fr/deliverable/D1-RequirementAnalysis-2009.pdf Work Package 1] of the project. Using the [http://www.smtlib.org/ SMT-LIB] standard is a requirement for this project.
	~~tools such as those embedded in~~ the ~~Rodin platform~~. ~~The purpose~~ is ~~not here~~ to ~~entirely define the translation, but rather to give a mapping for this subset of Event-B formulas. These typical mathematical problems are entry points for the~~ [[~~#ancre_1~~\|~~DECERT~~]] ~~project~~, ~~and more precisely for~~ the Work Package 1. Using the SMT-LIB standard is ~~among the requirements~~ for this project.

	This ~~version mainly focuses on lemmas based on unquantified integer linear arithmetic~~.		== 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.

	~~== Specification ==~~		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.
	A first ~~[[#ancre_2\|specification draft]]~~ has ~~been written~~.

	== ~~Implementation~~ ==		== Another approach with ppTrans ==
	~~A first~~ plug-in ~~prototype is accessible~~ under the following ~~respositories~~:		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 [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp sources] of the Rodin platform) so as to [[#ppTrans \| 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 [[#ancre_2\|specification draft]]) was mainly focusing on lemmas based on unquantified integer linear arithmetic. Its implementation can be found under the following repositories:
	* <tt>_exploratory/carinepascal/fr.systerel.decert</tt>		* <tt>_exploratory/carinepascal/fr.systerel.decert</tt>
	* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>		* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>
			It partially supports the following theories: Linear Arithmetic, Linear Order and Integer.

	~~The following theories are currently supported: Linear Arithmetic, Linear Order and Integer. The lemmas referencing other theories will not be translated.~~		=== Instructions to use it ===

	== ~~How~~ to ~~perform the translation?~~ ==

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

Line 37:		Line 37:

	== Bibliography ==		== Bibliography ==
	* <font id="ancre_1">DECERT</font>, [http://decert.gforge.inria.fr/index.html ''DEduction and CERTification'']
	* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.		* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.
	* S. ~~Ranise~~ and C. ~~Tinelli~~, ~~[http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf~~ <font id="~~ancre_3~~">''~~The SMT~~-~~LIB standard~~''</font>~~], Version 1.2~~, ~~2006~~.		* M. Konrad and L. Voisin, <font id="ppTrans">''Translation from set-theory to predicate calculus''</font>, 2010.

	[[Category:Design]]		[[Category:Design]]

imported>Pascal: /* How to perform the translation? */

2009-09-14T08:06:54Z

How to perform the translation?

← Older revision		Revision as of 08:06, 14 September 2009
Line 33:		Line 33:
	* The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.		* The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.
	* If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> 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 [http://goedel.cs.uiowa.edu/smtlib SMT-LIB web page].		* If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> 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 [http://goedel.cs.uiowa.edu/smtlib SMT-LIB web page].
	* If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> 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 [http://research.microsoft.com/en-us/um/redmond/projects/z3 following address]~~; only~~ the ~~versions 1~~.~~x are currently~~ supported.		* If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> 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 [http://research.microsoft.com/en-us/um/redmond/projects/z3 following address] (Note that the 2.0 version is not supported because it does not support user-defined attributes).
	</ol>		</ol>

imported>Pascal: /* Bibliography */

2009-08-25T15:38:24Z

Bibliography

← Older revision		Revision as of 15:38, 25 August 2009
Line 39:		Line 39:
	* <font id="ancre_1">DECERT</font>, [http://decert.gforge.inria.fr/index.html ''DEduction and CERTification'']		* <font id="ancre_1">DECERT</font>, [http://decert.gforge.inria.fr/index.html ''DEduction and CERTification'']
	* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.		* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.
	* S. Ranise and C. Tinelli, [http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf <font id="ancre_3">''The SMT-LIB standard''</font>], Version 1.2~~, 2006~~, 2006.		* S. Ranise and C. Tinelli, [http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf <font id="ancre_3">''The SMT-LIB standard''</font>], Version 1.2, 2006.

	[[Category:Design]]		[[Category:Design]]

imported>Pascal: /* How to perform the translation? */

2009-08-25T15:37:59Z

How to perform the translation?

← Older revision		Revision as of 15:37, 25 August 2009
Line 23:		Line 23:
	The XML files containing the Event-B lemmas are assumed to be stored in the <tt>Lemmas</tt> folder. The SMT files containing the SMT-LIB benchmarks are assumed to be stored in the <tt>Benchmarks</tt> folder.		The XML files containing the Event-B lemmas are assumed to be stored in the <tt>Lemmas</tt> folder. The SMT files containing the SMT-LIB benchmarks are assumed to be stored in the <tt>Benchmarks</tt> folder.

	Follow the ~~following~~ steps in order to translate Event-B lemmas to SMT-LIB benchmarks:		Follow the steps below in order to translate Event-B lemmas to SMT-LIB benchmarks:
	<ol>		<ol>
	<li> Launch the <tt>fr.systerel.decert.tests.TypeCheckingTests</tt> JUnit test to type-check the lemmas (optional).		<li> Launch the <tt>fr.systerel.decert.tests.TypeCheckingTests</tt> JUnit test to type-check the lemmas (optional).
Line 33:		Line 33:
	* The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.		* The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.
	* If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> 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 [http://goedel.cs.uiowa.edu/smtlib SMT-LIB web page].		* If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> 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 [http://goedel.cs.uiowa.edu/smtlib SMT-LIB web page].
	* If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> 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 [http://research.microsoft.com/en-us/um/redmond/projects/z3 following address].		* If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> 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 [http://research.microsoft.com/en-us/um/redmond/projects/z3 following address]; only the versions 1.x are currently supported.
	</ol>		</ol>

imported>Pascal: /* Implementation */

2009-08-25T15:26:23Z

Implementation

← Older revision		Revision as of 15:26, 25 August 2009
Line 17:		Line 17:
	* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>		* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>

	The following theories are currently supported: Linear Arithmetic, Linear Order ~~Int~~ and Integer.		The following theories are currently supported: Linear Arithmetic, Linear Order and Integer. The lemmas referencing other theories will not be translated.

	== How to perform the translation? ==		== How to perform the translation? ==

imported>Pascal: /* How to perform the translation? */

2009-08-25T15:14:23Z

How to perform the translation?

← Older revision		Revision as of 15:14, 25 August 2009
Line 32:		Line 32:
	* The <tt>XMLFolder</tt> field shall contain the absolute path of the <tt>Lemmas</tt> folder.		* The <tt>XMLFolder</tt> field shall contain the absolute path of the <tt>Lemmas</tt> folder.
	* The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.		* The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.
	* If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> 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 [http://goedel.cs.uiowa.edu/smtlib~~\|The~~ SMT-LIB web page].		* If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> 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 [http://goedel.cs.uiowa.edu/smtlib SMT-LIB web page].
	* If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> 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 [http://research.microsoft.com/en-us/um/redmond/projects/z3~~\|the~~ following address].		* If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> 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 [http://research.microsoft.com/en-us/um/redmond/projects/z3 following address].
	</ol>		</ol>

imported>Pascal: /* How to perform the translation? */

2009-08-25T15:07:34Z

How to perform the translation?

← Older revision		Revision as of 15:07, 25 August 2009
Line 24:		Line 24:

	Follow the following steps in order to translate Event-B lemmas to SMT-LIB benchmarks:		Follow the following steps in order to translate Event-B lemmas to SMT-LIB benchmarks:
			<ol>
	* Launch the <tt>fr.systerel.decert.tests.TypeCheckingTests</tt> JUnit test to type-check the lemmas (optional).		<li> Launch the <tt>fr.systerel.decert.tests.TypeCheckingTests</tt> JUnit test to type-check the lemmas (optional).
	Note that it is previously necessary to set the <tt>XMLFolder</tt> field of the <tt>TypeCheckingTests</tt> class to specify the absolute path of the <tt>Lemmas</tt> folder.		Note that it is previously necessary to set the <tt>XMLFolder</tt> field of the <tt>TypeCheckingTests</tt> class to specify the absolute path of the <tt>Lemmas</tt> folder.

	* Launch the <tt>fr.systerel.decert.tests.smt.TranslationTests</tt> JUnit test to translate the lemmas (mandatory).		<li> Launch the <tt>fr.systerel.decert.tests.smt.TranslationTests</tt> JUnit test to translate the lemmas (mandatory).
	Note that it is necessary to previously configure the test:		Note that it is necessary to previously configure the test:
	** The <tt>XMLFolder</tt> field shall contain the absolute path of the <tt>Lemmas</tt> folder.		* The <tt>XMLFolder</tt> field shall contain the absolute path of the <tt>Lemmas</tt> folder.
	** The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.		* The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.
	** If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> field shall contain the absolute path of the directory where is installed the SMT-LIB parser. Otherwise, the option shall be turned off.		* If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> 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 [http://goedel.cs.uiowa.edu/smtlib\|The SMT-LIB web page].
	The SMT-LIB parser is available from [http://goedel.cs.uiowa.edu/smtlib\|The SMT-LIB web page].		* If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> 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 [http://research.microsoft.com/en-us/um/redmond/projects/z3\|the following address].
	** If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> field shall contain the absolute path of the directory where is installed the Z3 SMT solver. Otherwise, the option shall be turned off.		</ol>
	The Z3 SMT solver is available from [http://research.microsoft.com/en-us/um/redmond/projects/z3\|the following address].

	== Bibliography ==		== Bibliography ==