ocaml - 从 Ocaml 调用 Z3 作为黑盒

Question

我想访问 Ocaml 中 Z3 的量词消除策略，以避免实现我需要的所有有效性和量词消除方法。

为此，我想知道如何从 Ocaml 调用 Z3 API（例如，来自 Python 的 Z3 作为黑盒）。

任何人都可以帮忙吗？

PS：这个活动会被称为多范式编程吗？我问这个是为了在将来找到有关类似问题的更多信息。

Answer 1

z3 已经带有 OCaml 绑定：

• 接口：https ://z3prover.github.io/api/html/ml/Z3.html
• 示例：https ://github.com/Z3Prover/z3/tree/master/examples/ml

如果公开的 API 不足以做你想做的事，你真的应该要求他们通过 OCaml API 公开它。我认为通过 OCaml-Python-Z3 会非常有问题，因为您必须同时兼顾这两层。