在 OS X 上编译 z3 4.1 以使用 Boogie

Question

我正在尝试在 Mac OS X 10.8 上安装 Boogie（2012 年 10 月 22 日版本）。我从here 下载了 Boogie，并安装了 Mono 3.4.0。没有验证选项的 Boogie 对我来说效果很好。

接下来，我需要安装 Z3。我尝试了夜间 OS X 构建，因为我认为这会最简单，但 Boogie 给出了很多错误：

Prover error: line 5 column 22: the parameter 'model_v2' was renamed to 'model.v2', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:model.v2' for the full description of the parameter

所以我尝试下载 Z3 4.1 版的源代码并编译它。我运行了autoconf，并且配置没有任何问题，但是make有很多错误：

$ autoconf
$ ./configure
checking for dos2unix... /usr/local/bin/dos2unix
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking whether make sets $(MAKE)... yes
clang: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated
checking how to run the C++ preprocessor... g++ -E
configure: creating ./config.status
config.status: creating Makefile

Z3 was configured with success.
Host platform: osx
Arithmetic:    internal

Type 'make' to compile Z3.
$ make
Makefile:271: obj/external/act_cache.d: No such file or directory
Makefile:271: obj/external/add_bounds.d: No such file or directory
Makefile:271: obj/external/add_bounds_tactic.d: No such file or directory
Makefile:271: obj/external/aig.d: No such file or directory
....
(many like this)
....
Makefile:273: obj-test/external/array_property_expander.d: No such file or directory
Makefile:273: obj-test/external/arith_rewriter.d: No such file or directory
Makefile:273: obj-test/external/arith_simplifier_plugin.d: No such file or directory
Makefile:273: obj-test/external/ast.d: No such file or directory
....
(and more like this)
....
Making dependency file 'obj-test/external/bits.d' ...
clang: warning: argument unused during compilation: '-fopenmp'
clang: warning: argument unused during compilation: '-mfpmath=sse'
In file included from test/bits.cpp:5:
In file included from lib/mpz.h:29:
lib/z3_omp.h:23:9: fatal error: 'omp.h' file not found
#include"omp.h"
        ^
1 error generated.

知道有什么问题吗？我的 g++ 版本是： Apple LLVM 5.0 版（clang-500.2.79）（基于 LLVM 3.3svn）

编辑：我按照 Christoph 的建议，可以成功开始构建，但在某些时候出现以下错误：

clang: warning: argument unused during compilation: '-mfpmath=sse'
lib/hwf.cpp:27:14: warning: pragma STDC FENV_ACCESS ON is not supported, ignoring pragma [-Wunknown-pragmas]
#pragma STDC FENV_ACCESS ON
             ^
In file included from lib/hwf.cpp:50:
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1388:22: error: expected expression
  return (__m128)__in;
                     ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1394:23: error: expected expression
  return (__m128i)__in;
                      ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1400:23: error: expected expression
  return (__m128d)__in;
                      ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1406:23: error: expected expression
  return (__m128i)__in;
                      ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1412:22: error: expected expression
  return (__m128)__in;
                     ^
/usr/bin/../lib/clang/5.0/include/emmintrin.h:1418:23: error: expected expression
  return (__m128d)__in;
                      ^
1 warning and 6 errors generated.

有什么想法吗？

Answer 1

这个有点棘手，因为 Boogie 不支持新的 Z3（另请参阅 here），但旧的 4.1.2 版本的 Z3 不支持 OSX 10.9 上的新编译器（clang）。这主要是因为 clang 缺乏对 OpenMP 的支持。我们可以在不支持 OpenMP 的情况下构建这个版本的 Z3，方法是在 Makefile 的 CPPFLAGS 行中添加 -D_NO_OMP_，或者运行

CPPFLAGS=-D_NO_OMP_ LDFLAGS=-stdlib=libstdc++ ./configure

在命令行上（LDFLAGS 设置是必需的，因为默认情况下 clang 选择了一个不合适的标准 C++ 库；有关详细信息，请参阅here）。然后我们需要替换 Makefile 中所有出现的-fopenmp，例如，通过运行

sed -i '' "s/-fopenmp//" Makefile

一旦完成，Z3 4.1.2 应该会成功构建。