mirror of
https://github.com/Z3Prover/z3
synced 2025-10-26 01:14:36 +00:00
23 lines
797 B
Text
23 lines
797 B
Text
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 -package Z3 -linkpkg ml_example.ml
|
|
or
|
|
ocamlfind ocamlopt -o ml_example -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).
|