3

我从 codeplex 的源代码编译了 Z3。配置细节：

  • 操作系统 Debian 5.0 (Lenny)
  • GLIBC 2.7
  • GCC 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 机器上，一切顺利。提前致谢。

4

1 回答 1

4

我假设您使用的是官方 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 开发一个新的构建系统，您可以通过unstable从 codeplex 获取分支来尝试它。你能试一试吗？很高兴收到您的反馈，以使构建在更多平台上顺利进行。

于 2012-11-01T17:26:02.287 回答