使用OPAM安装Z3的OCAML API

Installing ocaml API for Z3 using opam

本文关键字：OCAML API Z3 OPAM 安装 使用      更新时间：2023-10-16

我想在我的OCAML程序中使用Z3。使用OPAM，我做了

$ opam install z3
$ eval $(opam env)

然后尝试用

编译 
$ ocamlfind ocamlopt -o main -package z3 -linkpkg main.ml

我得到的是成千上万的In function foo undefined reference to bar的巨大转储，从

开始 
/home/andrepd/.opam/4.06.1+flambda/lib/z3/libz3-static.a(api_datatype.o): In function `mk_datatype_decl':
api_datatype.cpp:(.text+0x4bf): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x522): undefined reference to `__cxa_throw'
api_datatype.cpp:(.text+0x57b): undefined reference to `__cxa_free_exception'
api_datatype.cpp:(.text+0x58f): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x5f9): undefined reference to `__cxa_throw'
api_datatype.cpp:(.text+0x61f): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x68b): undefined reference to `__cxa_throw'
...

以

结尾 
binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x1ab): undefined reference to `__cxa_allocate_exception'
binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x205): undefined reference to `__cxa_throw'
binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x226): undefined reference to `__cxa_free_exception'
/home/andrepd/.opam/4.06.1+flambda/lib/z3/libz3-static.a(binary_heap_upair_queue.o): In function `_GLOBAL__sub_I_binary_heap_upair_queue.cpp':
binary_heap_upair_queue.cpp:(.text.startup+0xc): undefined reference to `std::ios_base::Init::Init()'
binary_heap_upair_queue.cpp:(.text.startup+0x13): undefined reference to `std::ios_base::Init::~Init()'
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
Command exited with code 2.

我在做什么错？为了记录，我正在使用

的ocamlbuild 
$ ocamlbuild -use-ocamlfind -cflag '-linkpkg' main.native

和 true: package(z3)在_tags文件中。但是，像上面的呼叫普通的ocamlfind可以提供相同的输出。

版本：编译器：4.06.1 W/Flambda，Opam：2.0.0，Z3：4.8.4。

tl; dr;包裹坏了。修复程序和几个解决方法如下，但是通常，这些问题应发布到相应的问题跟踪器。因此，请考虑打开问题报告或使用修复。

那些链接器错误表明C 标准库中的符号缺失。由于OCAML使用C链接器来链接最终产品，因此默认情况下不会传递C 标准库。当然，正确制作的软件包应该为我们做 1 ，但是我们仍然可以通过-cclib -lstdc++手动进行操作(如果您有libstdc ，否则请使用-lc++(。

ocamlfind ocamlopt -linkpkg -cclib -lstdc++ -package z3 example.ml -o exe

使用ocamlbuild，您可以使用cclib(x)参数化标签，例如

 <example.ml>: cclib(-lstdc++)

沙丘用户的注释

tl; dr;如果您使用的是dune，那么您仍然必须将(flags (-cclib -lstdc++))添加到您的库/可执行性stanza，因为Dune忽略了linkopts(以及Meta文件的许多其他字段(。

长篇小说。元文件规范由Findlib库定义和实现。沙丘构建系统没有使用Findlib，而是重新实现了一小部分Findlib，其中缺少许多功能，即linkopts和Predicates等字段。这就是为什么您仍然需要添加此字段的原因，尽管事实是Meta规定的。至少截至2019年10月。

1 提供的元文件包含一个伪造

linkopts = "-cclib -L/usr/lib"

(a(没有意义，因为-L不是链接器选项，而是编译器ONE，并且(b(是没有用的，因为/usr/lib通常在搜索路径中。

正确的选项应为：

linkopts = "-cclib -lstdc++"

您可以直接编辑文件，位于$(ocamlfind query z3)/META。

请考虑将修复程序提交给OPAM软件包或(理想情况下(Z3。

相关文章：