I would like to get access to the quantifier elimination tactic of Z3 in Ocaml, in order to avoiding implementing all the validity and quantifier elimination methods I need.

To do so, I would like to know how to call a Z3 API (for instance, Z3 from Python as a black box) from Ocaml.

Can anyone help?

PS: Would this activity be called multi-paradigm programming? I ask this in order to find more info about similar issues in the future.

>Solution :

z3 already comes with O’Caml bindings:

• API: https://z3prover.github.io/api/html/ml/Z3.html
• Example: https://github.com/Z3Prover/z3/tree/master/examples/ml

If the API exposed isn’t enough to do what you want, you should really ask them to expose it through the O’Caml API. I think going through O’Caml-Python-Z3 would be really problematic as you’d have to juggle both layers.