使用 OCaml 绑定安装 Z3

Question

我正在尝试使用 OCaml 绑定安装 Z3 并收到以下错误。

cp ../src/api/ml/z3.mli api/ml/z3.mli
ocamlc  -I api/ml -o api/ml/z3.cmi -c api/ml/z3.mli
File "api/ml/z3.mli", line 1159, characters 35-50:
Error: Unbound module Big_int
make: *** [api/ml/z3.cmo] Error 2

我首先尝试通过安装

opam install z3

然后我尝试克隆 Z3 存储库并运行

 python scripts/mk_make.py --ml
 cd build
 make

之后我得到同样的错误。

任何帮助将不胜感激。谢谢！

Answer 1

Z3 安装需要较旧的 OCaml 环境。在最近的 OCaml 版本中，Big_int 位于 Num 模块中。

$ opam install num

对于它的价值，我不相信 Z3 有一个 OPAM 模块。如果您运行 Z3 安装，OCaml/Z3 接口将被安装就像它是一个 OPAM 模块（在 ~/.opam 中）。但事实并非如此。

我每天都在使用 Z3，所以我可以验证它是否可以工作（OCaml 4.03.0 和 OCaml 4.06.0。）

更新

我刚刚验证了这些天在 OPAM 中有一个 Z3 包，并且我能够在 OCaml 4.06.0 下将它安装在一个我碰巧方便的以前干净的系统上。系统是Ubuntu 14.04。

我需要进行以下初始安装：

sudo apt-get update
sudo apt-get install ocaml
sudo apt-get install m4
sudo apt-get install dev-libgmp
sudo apt-get install g++

然后我安装了 OPAM：

sudo add-apt-repository ppa:avsm/ppa
sudo apt-get update
sudo apt-get install opam

现在以我自己的身份运行：

$ opam init
$ eval `opam config env`
$ opam update
$ opam switch 4.06.0
$ eval `opam config env`
$ opam install z3
$ ls ~/.opam/4.06.0/lib/z3
dllz3ml.so   z3.cmi       z3enums.cmx  z3ml.cmxa     z3native.cmx
libz3ml.a    z3.cmo       z3enums.mli  z3ml.cmxs     z3native.mli
libz3.so     z3.cmx       z3enums.o    z3.mli        z3native.o
META         z3enums.cmi  z3ml.a       z3native.cmi  z3native_stubs.o
opam.config  z3enums.cmo  z3ml.cma     z3native.cmo  z3.o

这对我来说看起来不错。我不是 Z3 巫师；它主要是我正在从事的项目的依赖。但这些是我习惯看到的文件。