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.