mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
81b8f397b3
I can compile the OCaml example with `-thread` option at Linux. ``` $ ocaml --version The OCaml toplevel, version 4.05.0 ```
24 lines
813 B
Plaintext
24 lines
813 B
Plaintext
Small example using the Z3 ML bindings.
|
|
|
|
To build the example execute
|
|
make examples
|
|
in the build directory.
|
|
|
|
This will create ml_example and ml_example.byte in the build directory, which
|
|
can be run in the build directory by calling
|
|
LD_LIBRARY_PATH=. ./ml_example
|
|
or
|
|
LD_LIBRARY_PATH=. ./ml_example.byte
|
|
for the byte-code version.
|
|
|
|
If Z3 was installed into the ocamlfind package repository (see
|
|
src/api/ml/README), then we can also compile this example as follows:
|
|
|
|
ocamlfind ocamlc -o ml_example.byte -thread -package Z3 -linkpkg ml_example.ml
|
|
or
|
|
ocamlfind ocamlopt -o ml_example -thread -package Z3 -linkpkg ml_example.ml
|
|
|
|
Note that the resulting binaries depend on the shared z3 library
|
|
(libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH
|
|
(Linux), or DYLD_LIBRARY_PATH (macOS).
|