(Created page with "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....") |
No edit summary |
||

Line 4: | Line 4: | ||

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 [http://alloy.mit.edu/kodkod/ 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. 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 = | = How to install Z3 for ProB = | ||

For Linux and OS X, the nightly builds of ProB available from the [[Download|Downloads]] page already include the extension needed for ProB to communicate with Z3. | |||

In addition to ProB, you need to install Z3 by downloading it from [[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 = | |||

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

* Strings | |||

* Generalised union, generalised intersection | |||

* Generalised concatenation | |||

* Permutation | |||

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

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

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

>>> :z3 {x} /\ {y} /= {} & x:1000000..20000000 & y>=0 & y<2000000 | |||

PREDICATE is TRUE | |||

Solution: | |||

x = 1000000 | |||

y = 1000000 | |||

= More details = | = More details = | ||

* A paper describing the integration of ProB and Z3 has been submitted to iFM 2016. | * A paper describing the integration of ProB and Z3 has been submitted to iFM 2016. |

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

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

-p SMT SUPPORTED INTERPRETER TRUE

on the command line.

For Linux and OS X, the nightly builds of ProB available from the Downloads page already include the extension needed for ProB to communicate with Z3.

In addition to ProB, you need to install Z3 by downloading it from 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.

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

- Strings
- Generalised union, generalised intersection
- Generalised concatenation
- Permutation
- 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 used together with ProB, everything Z3 can not be coped with will be handled by ProB alone automatically.

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

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

- A paper describing the integration of ProB and Z3 has been submitted to iFM 2016.