CODEWITHSUNDEEP
macosocamlz3
denbuttigieg
denbuttigieg

Reputation: 185

Using Z3 on OSX with OCaml

I am trying to use the Z3 Solver on OSX using the OCaml binding. When attempting to build and run my solution using ocamlfind ocamlc -o testsat.byte -package Z3 -linkpkg testsat.ml I am getting an ocamlfind: Package Z3 not found.

I have also tried using ocamlbuild without the -package tag, however then I'm getting an Unbound Module Z3 error.

I am also having problems installing the z3Overlay library - https://github.com/termite-analyser/z3overlay when trying to install the z3 dev portion.

Does anyone know of any fixes, or a stable version that can be used on OSX? My assumptions are that I'm encountering these errors since the build is failing (as can be seen from the official documentation: https://github.com/Z3Prover/z3).

I am new to this, any help is greatly appreciated.

Upvotes: 1

Views: 1034

Answers (1)

ivg
ivg

Reputation: 35210

Library and package names are case sensitive, and the package name of the z3 bindings is z3 not Z3. You can always query for available packages using ocamlfind list. 

ocamlfind list | grep -i Z3
z3                  (version: 4.6.0.0)

So the following command will work as expected

ocamlfind ocamlc -o testsat.byte -package z3 -linkpkg testsat.ml

There is a small caveat, that Martin mentions in the comments, so you should get another error, that should look like this:

libz3.so: cannot open shared object file: No such file or directory

Indeed, the package installs libz3.soin a location that is not searched, thus you should tell the system linker where to search for the z3 shared object. In Mac OS X, this can be achieved by setting the DYLD_LIBRARY_PATH variable, e.g.,

export DYLD_LIBRARY_PATH=`opam config var z3:lib`

on GNU/Linux systems the same can be done via the LD_LIBRARY_PATH environment variable:

export LD_LIBRARY_PATH=`opam config var z3:lib`

Upvotes: 1

Related Questions