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 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 list of REPL commands is
You can stipulate the ProB should use Z3 to solver the PROPERTIES (aka axioms in Event-B) by setting the preference SOLVER_FOR_PROPERTIES to z3. You can do this either in the model via a definition SET_PREF_SOLVER_FOR_PROPERTIES == "z3" or when starting probcli via -p SOLVER_FOR_PROPERTIES z3. You can also use z3cns to just use the constructive translation, and z3axm for the axiomatic translation.
The tighter integration of Z3 and ProB’s kernel can be enabled by setting the SMT_SUPPORTED_INTERPRETER preference to TRUE. This will try and interleave ProB's solver with Z3.
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.
As of version 1.16.0, the libz3 library is no longer shipped within the lib folder of the ProB distributions (as it was quite large and not everybody needs the Z3 backend).
You can now install Z3 via
probcli --install z3
You can also first try
probcli --install-dry-run z3
Alternatively, you can download Z3 from https://github.com/Z3Prover/z3/releases.
For older versions of ProB you may have to set the DYLD_LIBRARY_PATH (macOS),or LD_LIBRARY_PATH (Linux) or PATH (Windows) environment variable. E.g., as follows when starting probcli from the terminal:
DYLD_LIBRARY_PATH=lib:$DYLD_LIBRARY_PATH probcli -repl
Newer versions of ProB should find Z3 automatically in ProB's lib folder.
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
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
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.