Using ProB with Z3: Difference between revisions

 
(17 intermediate revisions by 3 users not shown)
Line 1: Line 1:
[[Category:User Manual]]
[[Category:User Manual]]
[[Category:Stubs]]


The current nightly versions of ProB can make use of [http://alloy.mit.edu/kodkod/ Z3] as an alternate way of solving constraints.
The current nightly versions of ProB can make use of [https://github.com/Z3Prover/z3 Z3] as an alternate way of solving constraints.


= 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
Line 13: Line 12:


= 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.
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.
Download the matching extension for your system:
* [https://www3.hhu.de/stups/downloads/z3interface/linux32/z3interface.so Linux, 32bit]
* [https://www3.hhu.de/stups/downloads/z3interface/linux64/z3interface.so Linux, 64bit]
* [https://www3.hhu.de/stups/downloads/z3interface/osx/z3interface.bundle OS X, 64bit]
* Currently, the Z3 extension is not build for Windows. You can build it yourself from source. Feel free to contact us for further support.
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.
Inside the zip file 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. 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.
If the libraries can not be loaded, ProB will answer with "solver_not_available" when Z3 is queried.


= 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.
Line 43: Line 28:


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 51: Line 36:


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
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 Z3:
>>> :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:
Line 69: Line 46:
       x = 1000000
       x = 1000000
       y = 1000000
       y = 1000000
As of version 1.10.0-beta4 you can also issue the <t>:z3-version</t> command in the REPL to obtain version information.


= More details =
= More details =


* A paper describing the integration of ProB and Z3 has been submitted to iFM 2016.
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/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.

Latest revision as of 07:39, 6 June 2023


The current nightly versions of ProB can make use of Z3 as an alternate way of solving constraints.

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 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

on the command line.

How to install Z3 for ProB

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

Currently, the Z3 translation is unable to cope with the following constructs:

  • Generalised concatenation
  • Permutation
  • Iteration and Closure

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

When used together with ProB, everything Z3 can not be coped with will be handled by ProB alone automatically.

Examples

Using the repl, one can try out different examples.

First an example which can be solved by Z3 and not by ProB:

>>> X<Y & Y<X & X:INTEGER
% Timeout when posting constraint:
% kernel_objects:(_981727#>0)
### Warning: enumerating X : INTEGER : inf:sup ---> -1:3
Existentially Quantified Predicate over X,Y is UNKNOWN
[FALSE with ** ENUMERATION WARNING **]

Using the Z3 translation it can be solved:

>>> :z3 X<Y & Y<X & X:INTEGER
PREDICATE is FALSE

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

>>> :z3 {x} /\ {y} /= {} & x:1000000..20000000 & y>=0 & y<2000000
PREDICATE is TRUE
Solution:
      x = 1000000
      y = 1000000

As of version 1.10.0-beta4 you can also issue the <t>:z3-version</t> command in the REPL to obtain version information.

More details

A paper describing the integration of ProB and Z3 has been published at iFM 2016. You can download the

A 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.