Compiling z3 on raspberries
Let me first apologize if the question is illogical, but I am very new to modifying compilers and cross-architecture designs.
To evaluate the performance on different platforms, I am trying to compile the Z3 SMT solver on a raspberry pi 2. However, the problem seems to be related to the architecture of the hand. My intention so far has been to use a config script supplied by Mircrosoft Research, which works neatly and gives the following output:
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 fix the problem first:
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 understand the meaning of this error correctly, these comma parameters refer to the smart tatika used to calculate math exercises and are not needed unless performance is an issue. (To put it simply, it should still work, even if it is slower). Removing flags from the corresponding config.mk allows building to a certain extent.
After successfully creating a large number of result files, the make process will exit 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
Now my question is whether it is possible to compile again without using emmintrin.h (simply copying the missing library in the Pi does not work due to architectural barriers). Has anyone ever done this?
Thanks in advance for all the helpful comments.
source to share
Both the unsupported options and the bug in hwf.cpp relate to floating point support in Z3. The parameters are trying to make sure the floating point block is configured correctly and the bug in hwf.cpp is that we are trying to jump to hardware functions for floating point operations. In fact, the implications of these changes are that some floating point operations may not be accurate if these parameters are removed; however, not many parts of the Z3 rely on this, so you are unlikely to see bugs later.
I have an RPi at home, so I'll see if we can use different options for this when I get home tonight. The RPi may not have a floating point unit, but in this case, I'll have to switch it to soft floats (for which we also have support, but that might be slower).
source to share