1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
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).
|
