Skip to content

Latest commit

 

History

History

ml

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
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).