z3 - 编译 Z3 测试示例会出现构建错误

Question

我从 codeplex 的源代码编译了 Z3。配置详情:

• 操作系统Debian 5.0 (Lenny)
• GLIBC 2.7
• 海湾合作委员会 4.4.3
• OpenMP 4.3.4(打包版)

当我尝试构建 c 示例时，我得到:

../../lib/libz3.so: undefined reference to `std::ctype<char>::_M_widen_init() const@GLIBCXX_3.4.11'

当我尝试构建 C++ 示例时，我得到:

../../lib/libz3.so: undefined reference to `omp_init_nest_lock@OMP_3.0'
../../lib/libz3.so: undefined reference to `omp_unset_nest_lock@OMP_3.0'
../../lib/libz3.so: undefined reference to `omp_set_nest_lock@OMP_3.0'
../../lib/libz3.so: undefined reference to `omp_destroy_nest_lock@OMP_3.0'.

提到的例子是以前从 Z3 网站下载的。当我构建随源代码一起提供的 test_capi 示例时，我得到了上面错误消息的并集。

问题的本质是什么？使用Z3对系统有什么要求吗？

在另一台 Debian 6.0 机器上一切顺利。 提前致谢。

Answer 1

我假设您使用的是官方 src 版本或 master 分支。如果是这种情况，您可以尝试在 test_capi 目录中编译 test_capi 吗？

gcc -o test_capi -I ../lib test_capi.c -L ../bin/external -lz3 -lstdc++ -lgomp

在上面的命令中，我们明确告诉 gcc 链接到 C++ 标准和 OMP 库。 对于 c++ 示例，您只需要包含 -lgomp，因为默认情况下 g++ 将链接到 C++ 标准库。您可以使用 ldd 找到其他缺少的依赖项:

ldd ../bin/external/libz3.o

也就是说，我正在为 Z3 开发一个新的构建系统，您可以通过从 codeplex 获取 unstable 分支来尝试它。你能试一试吗？很高兴收到您的反馈，让构建在更多平台上顺利进行。