Using ProB with Z3 - Revision history

Joshua Schmidt: /* More details */

2023-06-06T07:39:07Z

More details

← Older revision		Revision as of 07:39, 6 June 2023
Line 54:		Line 54:
	* [https://www3.hhu.de/stups/downloads/z3interface/rawdata raw data] from our benchmarks including the R scripts to generate the		* [https://www3.hhu.de/stups/downloads/z3interface/rawdata raw data] from our benchmarks including the R scripts to generate the
	* [https://www3.hhu.de/stups/downloads/z3interface/output resulting graphs].		* [https://www3.hhu.de/stups/downloads/z3interface/output resulting graphs].

			A [https://link.springer.com/article/10.1007/s10009-022-00682-y journal paper] describing an extended interface to Z3 and alternative translation from B to SMT-LIB using Lambda functions has been published in the International Journal on Software Tools for Technology Transfer in 2022.

Joshua Schmidt: /* Examples */

2023-06-06T07:36:47Z

Examples

← Older revision		Revision as of 07:36, 6 June 2023
Line 38:		Line 38:
	>>> :z3 X<Y & Y<X & X:INTEGER		>>> :z3 X<Y & Y<X & X:INTEGER
	PREDICATE is FALSE		PREDICATE is FALSE

	~~Now an example which can be solved by ProB’s own solver:~~
	~~>>> (2\|->4):{y\|#x.(y=(x\|->x+2))}~~
	~~PREDICATE is TRUE~~

	~~This one cannot be solved by earlier versions of Z3 and ProB (but can now be solved in the latest nightly release):~~
	~~>>> :z3 (2\|->4):{y\|#x.(y=(x\|->x+2))}~~
	~~PREDICATE is UNKNOWN: solver_answered_unknown~~

	Here an example that shows that Z3 can be used to solve constraints and obtain solutions for the open variables:		Here an example that shows that Z3 can be used to solve constraints and obtain solutions for the open variables:

Joshua Schmidt: /* What can be translated */

2023-06-06T07:34:44Z

What can be translated

← Older revision		Revision as of 07:34, 6 June 2023
Line 16:		Line 16:
	= What can be translated =		= What can be translated =
	Currently, the Z3 translation is unable to cope with the following constructs:		Currently, the Z3 translation is unable to cope with the following constructs:
	* Strings
	* Generalised union, generalised intersection
	* Generalised concatenation		* Generalised concatenation
	* Permutation		* Permutation
	* Iteration and Closure		* Iteration and Closure
	* Projection

	When using Z3 alone, the solver will report "unsupported_type_or_expression" if it can not handle parts of a constraint.		When using Z3 alone, the solver will report "unsupported_type_or_expression" if it can not handle parts of a constraint.

Joshua Schmidt: /* How to install Z3 for ProB */

2023-06-06T07:31:30Z

How to install Z3 for ProB

@@ Line 12: / Line 12: @@
 = How to install Z3 for ProB =
-First of all, download a nightly build of ProB from the [[Download|Downloads]] page. To connect Z3 to ProB you also need the proper extension.
+For Linux and Mac OS, the extension is built on our infrastructure and ships with the regular ProB download. You don't need to install Z3 on your system.
 = What can be translated =

Joshua Schmidt: /* How to use Z3 within ProB */

2023-06-06T07:24:54Z

How to use Z3 within ProB

← Older revision		Revision as of 07:24, 6 June 2023
Line 5:		Line 5:
	= How to use Z3 within ProB =		= How to use Z3 within ProB =

	One can start a REPL (Read-Eval-Print-Loop) by starting probcli with the '-repl' command line option. Any predicate preceded with :z3 will be solved by Z3. The full integration of Z3 and ProB’s kernel can be enabled by setting the corresponding preference by passing		One can start a REPL (Read-Eval-Print-Loop) by starting probcli with the '-repl' command line option. Any predicate preceded with :z3 will be solved by Z3 considering the current machine's state. The command :z3-free can be used to solve a constraint without considering the current machine's state. The full integration of Z3 and ProB’s kernel can be enabled by setting the corresponding preference by passing

	-p SMT SUPPORTED INTERPRETER TRUE		-p SMT SUPPORTED INTERPRETER TRUE

Michael Leuschel: /* How to install Z3 for ProB */

2020-10-29T14:12:48Z

How to install Z3 for ProB

← Older revision		Revision as of 14:12, 29 October 2020
Line 19:		Line 19:
	and place it in the "lib" folder of the ProB nightly build.		and place it in the "lib" folder of the ProB nightly build.

	In addition to ProB, you need to install Z3 by downloading it from [https://github.com/Z3Prover Z3's GitHub page]. Previously, ProB was linked against the stable release 4.4.1 of Z3. Current nightly builds of ProB work with version 4.8.7 of Z3.		In addition to ProB, you need to install Z3 by downloading it from [https://github.com/Z3Prover Z3's GitHub page]. Previously, ProB 1.6 was linked against the stable release 4.4.1 of Z3. Current nightly builds of ProB work with version 4.8.7 of Z3.
	Inside the zip file of Z3 you will find a folder called "bin" with the z3 binary and the belonging libraries inside.		Inside the zip file of Z3 you will find a folder called "bin" with the z3 binary and the belonging libraries inside.

Michael Leuschel: /* Examples */

2020-10-27T14:45:01Z

Examples

← Older revision		Revision as of 14:45, 27 October 2020
Line 60:		Line 60:
	PREDICATE is TRUE		PREDICATE is TRUE

	This one cannot be solved by Z3:		This one cannot be solved by earlier versions of Z3 and ProB (but can now be solved in the latest nightly release):
	>>> :z3 (2\|->4):{y\|#x.(y=(x\|->x+2))}		>>> :z3 (2\|->4):{y\|#x.(y=(x\|->x+2))}
	PREDICATE is UNKNOWN: solver_answered_unknown		PREDICATE is UNKNOWN: solver_answered_unknown

Michael Leuschel: /* Examples */

2020-10-27T10:36:17Z

Examples

← Older revision		Revision as of 10:36, 27 October 2020
Line 45:		Line 45:

	First an example which can be solved by Z3 and not by ProB:		First an example which can be solved by Z3 and not by ProB:
	>>> X<Y & Y<X		>>> X<Y & Y<X & X:INTEGER
	% Timeout when posting constraint:		% Timeout when posting constraint:
	% kernel_objects:(_981727#>0)		% kernel_objects:(_981727#>0)
Line 53:		Line 53:

	Using the Z3 translation it can be solved:		Using the Z3 translation it can be solved:
	>>> :z3 X<Y & Y<X		>>> :z3 X<Y & Y<X & X:INTEGER
	PREDICATE is FALSE		PREDICATE is FALSE

Michael Leuschel: /* How to install Z3 for ProB */

2020-10-27T10:30:26Z

How to install Z3 for ProB

Michael Leuschel: /* More details */

2020-09-21T15:09:51Z

More details

← Older revision		Revision as of 15:09, 21 September 2020
Line 76:		Line 76:
	= More details =		= More details =

	A paper describing the integration of ProB and Z3 has been ~~submitted to~~ iFM 2016. You can download the		A [https://doi.org/10.1007/978-3-319-33693-0_23 paper describing the integration of ProB and Z3] has been published at iFM 2016. You can download the
	* [https://www3.hhu.de/stups/downloads/z3interface/rawdata raw data] from our benchmarks including the R scripts to generate the		* [https://www3.hhu.de/stups/downloads/z3interface/rawdata raw data] from our benchmarks including the R scripts to generate the
	* [https://www3.hhu.de/stups/downloads/z3interface/output resulting graphs].		* [https://www3.hhu.de/stups/downloads/z3interface/output resulting graphs].

← Older revision		Revision as of 10:30, 27 October 2020
Line 13:		Line 13:
	= How to install Z3 for ProB =		= How to install Z3 for ProB =
	First of all, download a nightly build of ProB from the [[Download\|Downloads]] page. To connect Z3 to ProB you also need the proper extension.		First of all, download a nightly build of ProB from the [[Download\|Downloads]] page. To connect Z3 to ProB you also need the proper extension.
	For Linux and Mac OS, the extension is ~~build~~ by on our infrastructure and ships with the regular ProB download.		For Linux and Mac OS, the extension is built by on our infrastructure and ships with the regular ProB download.
	For Windows, you can download it from the following URLs:		For Windows, you can download it from the following URLs:
	* [https://www3.hhu.de/stups/downloads/z3interface/windows32/z3interface.dll 32bit]		* [https://www3.hhu.de/stups/downloads/z3interface/windows32/z3interface.dll 32bit]
Line 19:		Line 19:
	and place it in the "lib" folder of the ProB nightly build.		and place it in the "lib" folder of the ProB nightly build.

	In addition to ProB, you need to install Z3 by downloading it from [https://github.com/Z3Prover Z3's GitHub page]. ~~Currently~~, ProB is linked against the stable release 4.4.1 of Z3.		In addition to ProB, you need to install Z3 by downloading it from [https://github.com/Z3Prover Z3's GitHub page]. Previously, ProB was linked against the stable release 4.4.1 of Z3. Current nightly builds of ProB work with version 4.8.7 of Z3.
	Inside the zip file you will find a folder called "bin" with the z3 binary and the belonging libraries inside.		Inside the zip file of Z3 you will find a folder called "bin" with the z3 binary and the belonging libraries inside.

	These libraries have to be made available to ProB. On Linux or Mac, this can either be done by placing them in an appropriate folder (like /usr/lib or /usr/local/lib) or by setting an environmental variable (like LD_LIBRARY_PATH on Linux or DYLD_LIBRARY_PATH on Mac).		These Z3 libraries have to be made available to ProB. On Linux or Mac, this can either be done by placing them in an appropriate folder (like /usr/lib or /usr/local/lib) or by setting an environmental variable (like LD_LIBRARY_PATH on Linux or DYLD_LIBRARY_PATH on Mac).
	On Windows, you can place z3.dll in the main folder of the ProB distribution, i. e., on the same level as the lib directory, not inside it.		On Windows, you can place z3.dll in the main folder of the ProB distribution, i. e., on the same level as the lib directory, not inside it.
	If the libraries can not be loaded, ProB will answer with "solver_not_available" when Z3 is queried.		If the libraries can not be loaded, ProB will answer with "solver_not_available" when Z3 is queried.

	* ~~Version~~ 4.8.9 is currently not recommended for use with ProB. An [https://github.com/Z3Prover/z3/issues/4699 issue in the model extraction] can lead to erroneous models ~~and assertion violations on macOS Catalina (on macOS the issue is already present in version 4.8.8)~~.		* Versions 4.8.8 and 4.8.9 of Z3 are currently not recommended for use with ProB. An [https://github.com/Z3Prover/z3/issues/4699 issue in the model extraction] can lead to erroneous models.

	= What can be translated =		= What can be translated =