在 OSX 上使用 Z3 和 OCaml答案

【问题标题】：Using Z3 on OSX with OCaml在 OSX 上使用 Z3 和 OCaml
【发布时间】：2018-10-01 14:38:41
【问题描述】：

我正在尝试使用 OCaml 绑定在 OSX 上使用 Z3 Solver。尝试使用构建和运行我的解决方案时 ocamlfind ocamlc -o testsat.byte -package Z3 -linkpkg testsat.ml 我收到了ocamlfind: Package Z3 not found。

我也尝试过使用不带-package 标签的ocamlbuild，但是我收到Unbound Module Z3 错误。

在尝试安装 z3 dev 部分时，我在安装 z3Overlay 库时也遇到了问题 - https://github.com/termite-analyser/z3overlay。

有没有人知道可以在 OSX 上使用的任何修复程序或稳定版本？我的假设是我遇到了这些错误，因为构建失败（从官方文档可以看出：https://github.com/Z3Prover/z3）。

我是新手，非常感谢任何帮助。

【问题讨论】：

我认为你应该告诉我们你是如何安装 z3 的。现在有一个适用于 z3 4.6 的 opam 包，它适用于我们（需要注意的是 libz3.so 最终在 ~/.opam 下）。
@MartinJambon 我使用了opam install z3，并安装了所有必需的依赖项，我的安装成功（我猜）。当我运行opam list z3 时，我可以在 opam 的库列表中看到 z3。我现在要做的是克隆和构建存储库本身。（我不确定我是否在做所有正确的步骤）。另外，当我执行命令ocamlfind list z3 时没有出现。会不会是这个问题？
在直接运行 ocamlfind 或其他非 opam 命令之前忘记在 shell 中运行 eval $(opam config env) 是很常见的。它设置环境变量，包括OCAMLPATH，它告诉 ocamlfind 在哪里可以找到 opam 放置它们的库。
其实我刚查了一下，eval $(opam config env) 没有用 opam 2 设置OCAMLPATH。也许 opam 1.2 就是这种情况。不确定了。

标签： macos ocaml z3

【解决方案1】：

库和包名区分大小写，z3 绑定的包名是z3 而不是Z3。您始终可以使用ocamlfind list 查询可用的包。

ocamlfind list | grep -i Z3
z3                  (version: 4.6.0.0)

所以下面的命令会按预期工作

ocamlfind ocamlc -o testsat.byte -package z3 -linkpkg testsat.ml

Martin 在 cmets 中提到了一个小警告，因此您应该得到另一个错误，应该如下所示：

libz3.so: cannot open shared object file: No such file or directory

确实，该软件包将libz3.so 安装在未搜索到的位置，因此您应该告诉系统链接器在哪里搜索z3 共享对象。在 Mac OS X 中，这可以通过设置 DYLD_LIBRARY_PATH 变量来实现，例如，

export DYLD_LIBRARY_PATH=`opam config var z3:lib`

在 GNU/Linux 系统上，同样可以通过 LD_LIBRARY_PATH 环境变量完成：

export LD_LIBRARY_PATH=`opam config var z3:lib`

【讨论】：