c++ - 在 Raspberry 上编译 z3

Question

如果这个问题是不必要的，首先让我道歉，但我对修改编译器和跨架构设计还很陌生。

为了评估各种平台上的性能，我一直在尝试在树莓派 2 上编译 Z3 SMT 求解器。但是由于 arm 架构似乎存在问题。到目前为止，我的意图是使用 Mircrosoft Research 提供的配置脚本，它运行良好并产生以下结果:

Testing ar...
Testing g++...
Testing gcc...
Testing OpenMP...
Host platform:  Linux
C++ Compiler:   g++
C Compiler  :   gcc
Arithmetic:     internal
OpenMP:         True
Prefix:         /usr
64-bit:         False
Python version: 2.7
Writing build/Makefile
Copied Z3Py example 'example.py' to 'build'
Makefile was successfully generated.
  python packages dir: /usr/lib/python2.7/dist-packages
  compilation mode: Release
Type 'cd build; make' to build Z3

在搭建的时候我首先遇到的问题是:

src/shell/install_tactic.cpp
cc1plus: error: unrecognized command line option '-mfpmath=sse'
cc1plus: error: unrecognized command line option 'u2018-msse'
cc1plus: error: unrecognized command line option 'u2018-msse2'
Makefile:3159: recipe for target 'shell/install_tactic.o' failed
make: *** [shell/install_tactic.o] Error 1

如果我正确理解此错误的含义，这些命令行选项指的是用于计算数学练习的巧妙策略，如果性能不是问题，则不需要这些选项。 (简单地说，它应该仍然可以工作，即使速度较慢)。从相应的 config.mk 中删除标志，允许构建到一定程度。

在成功生成大量结果文件后，make 过程因以下错误而终止:

src/util/hwf.cpp
../src/util/hwf.cpp:55:23: fatal error: emmintrin.h: Datei oder Verzeichnis nicht gefunden
compilation terminated.
Makefile:163: recipe for target 'util/hwf.o' failed
make: *** [util/hwf.o] Error 1

我现在的问题是，是否可以在不使用 emmintrin.h 的情况下再次编译(由于架构障碍，简单地将丢失的库复制到 Pi 是行不通的)。有人做过吗？

提前感谢您提供的所有有用评论。

Answer 1

不支持的选项和hwf.cpp 中的错误都指的是Z3 中对浮点运算的支持。这些选项试图确保浮点单元设置正确，而 hwf.cpp 中的错误是因为我们试图获取浮点运算的硬件内在函数。从本质上讲，这些更改的后果是，如果删除这些选项，某些浮点运算可能会不精确；然而，没有多少 Z3 依赖于它，所以你以后不太可能看到错误。

我家里确实有一个 RPi，所以我会在今晚回家时看看我们是否可以使用不同的选项。可能是 RPi 根本没有浮点单元，在这种情况下，我必须将其切换为软 float (我们也支持，但速度可能较慢)。