2014-10-24 18:00:36 +01:00
|
|
|
A small example using the Z3 Java bindings.
|
2014-10-24 19:43:36 +01:00
|
|
|
|
2014-10-24 18:00:36 +01:00
|
|
|
To build the example, configure Z3 with the --java option to scripts/mk_make.py, build via
|
2012-11-27 23:06:35 +00:00
|
|
|
make examples
|
|
|
|
|
in the build directory.
|
|
|
|
|
|
|
|
|
|
It will create JavaExample.class in the build directory,
|
2012-11-29 09:13:24 -08:00
|
|
|
which can be run on Windows via
|
|
|
|
|
java -cp com.microsoft.z3.jar;. JavaExample
|
|
|
|
|
|
|
|
|
|
On Linux and FreeBSD, we must use
|
|
|
|
|
LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample
|
2018-10-02 17:38:09 +07:00
|
|
|
On macOS, the corresponding option is DYLD_LIBRARY_PATH:
|
2014-10-24 18:00:36 +01:00
|
|
|
DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample
|
2021-08-13 23:54:02 +02:00
|
|
|
|
|
|
|
|
By default, Z3 Java bindings are automatically loading the required native library for Z3 from the default library path.
|
|
|
|
|
In certain environments, depending on the developing process, the Z3 library is not available in the given library path.
|
|
|
|
|
To disable the automated loading process, the user can set the environment variable "z3.skipLibraryLoad=true".
|
|
|
|
|
In that case, the calling application should directly load the corresponding libraries before any interaction with Z3.
|
|
|
|
|
|