CODEWITHSUNDEEP
ocamlz3formal-verificationfirst-order-logicsatisfiability
Theo Deep
Theo Deep

Reputation: 766

Calling Z3 as black box from Ocaml

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.

Upvotes: 2

Views: 453

Answers (1)

alias
alias

Reputation: 30428

z3 already comes with OCaml bindings:

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

Upvotes: 3

Related Questions