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.
First of all, download a nightly build of ProB from the Downloads page. To connect Z3 to ProB you also need the proper extension. 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:
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 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.
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. 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:
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 & 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
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:
>>> :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.
A paper describing the integration of ProB and Z3 has been published at iFM 2016. You can download the