CODEWITHSUNDEEP
c++compilationz3
user3661732
user3661732

Reputation: 51

Compile z3 on Raspberry

Let me first of all apologize in case the question is unnecassary, but I am very new to modifiying compilers and cross architectural designs.

In order to evaluate the performance on various platforms I have been trying to compile the Z3 SMT solver on a raspberry pi 2. However there seems to be a problem due to the arm architecture. My intention so far was to use the configure script supplied by Mircrosoft Research, which works neatly and produces the following outcome:

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

When building I first of all encouter the problem:

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

If I understood the meaning of this error correctly, these commad line options refer to clever tatics used to compute mathematical exercises and are not necessary if performance is not an issue. (Simply speaking, it should still work, even if it is slower).Removing the flags from the respective config.mk, allows building to a certain extend.

After sucessfully producing a lot of outcome files, the make process terminates with the following error:

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

My question now is, whether it is again possible to compile without using emmintrin.h (simply copying the missing library to the Pi does not work, due to architectural hurdles). Has anyone ever done this?

Thank you in advance for all you helpful comments.

Upvotes: 3

Views: 652

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

Both, the unsupported options and the error in hwf.cpp refer to the support for floating-point operations in Z3. The options are trying to make sure that the floating-point unit is set up correctly, and the error in hwf.cpp is because we're trying to get to hardware intrinsics for floating point operations. Essentially, the consequences of those changes are that some floating-point operations may be imprecise if those options are removed; however, not many pieces of Z3 rely on that, so it's unlikely you'll see errors later.

I do have a RPi at home, so I'll see whether we can use different options for that when I get home tonight. It may be that the RPi doesn't have a floating point unit at all though, in that case I'll have to switch it to soft floats (which we also have support for, but it may be slower).

Upvotes: 1

Related Questions