The OCaml code in this repo reimplements the examples in this link: https://theory.stanford.edu/~nikolaj/programmingz3.html. There is no tutorial now on the internet for z3 OCaml bindings, so this repo might be a good study material.
First clone the z3 repo.
$ git clone https://github.com/Z3Prover/z3.git
Then on the root directory of the downloaded z3 folder, run these commands to build the source code.
$ sudo apt-get install ocaml opam libgmp-dev
$ opam init -y
$ eval `opam config env`; opam install zarith ocamlfind -y
$ python scripts/mk_make.py --ml --staticlib
$ set -e
$ cd build
$ eval `opam config env`
$ make -j3
Then change the Z3_SRC_ROOT in Makefile to the root directory of the downloaded z3 folder so that the z3 library can be found.
For example:
Z3_SRC_ROOT = ../z3
To rebuild my example code:
$ make all
To run my example code:
$ make run
To rebuild the official example code:
$ make ml_example
To run the official example code:
$ make run_ml_example
To clean the build:
$ make clean
- https://z3prover.github.io/api/html/ml/Z3.html
- https://github.com/Z3Prover/z3/tree/master/src/api/ml
- https://github.com/Z3Prover/z3/tree/master/src/api/python/z3 (You can study the OCaml bindings by reading its python counterpart)