Here's a stupid app that runs Z3 on an iOS device. It's incredibly buggy and untested. It definitely won't work in the Xcode simulator. You'll need Xcode and an Apple developer account.
Preparing Z3 for iOS
Clone the Z3 repo, which is a submodule here:
git submodule update --init
cd z3
The repo includes a Z3 shared library
that's already compiled for ARM (src/app/libz3.dylib).
Compiling the app
You probably(?) need to change the signing settings in the project inspector in Xcode to use your certificate. Then you should just be able to compile the Z3 target against a real device scheme (not one of the simulator options).
Changing the SMT file
The app loads an SMT file from src/sat.smt2 into the editor initially.
You can load a new SMT file from the iOS file picker using the "Load SMT" button.
Recompiling the Z3 library
If you need to recompile libz3.dylib...
First, patch some files in Z3 to make cross-compilation work:
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 97e2b65f2..5765ae4b0 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -291,6 +291,8 @@ def test_fpmath(cc):
global FPMATH_FLAGS
if is_verbose():
print("Testing floating point support...")
+ FPMATH_FLAGS=""
+ return "UNKNOWN"
t = TempFile('tstsse.cpp')
t.add('int main() { return 42; }\n')
t.commit()
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index 4434cb19f..975656e83 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -97,7 +97,7 @@ void invoke_gdb() {
case 'g':
sprintf(buffer, "gdb -nw /proc/%d/exe %d", getpid(), getpid());
std::cerr << "invoking GDB...\n";
- if (system(buffer) == 0) {
+ if (1 /*system(buffer)*/ == 0) {
std::cerr << "continuing the execution...\n";
}
else {
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 32a074eb3..80b937458 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -30,7 +30,6 @@ Revision History:
#else
#error No multi-precision library selected.
#endif
-#include <immintrin.h>
// Available GCD algorithms
// #define EUCLID_GCD
Prepare to cross-compile Z3 with the right flags:
env CPPFLAGS="-arch arm64 -mios-version-min=12.0 -isysroot /Applications/Xcode.app/Contents/Developer/Platforms/iPhoneOS.platform/Developer/SDKs/iPhoneOS12.1.sdk" LDFLAGS="-arch arm64 -mios-version-min=12.0 -isysroot /Applications/Xcode.app/Contents/Developer/Platforms/iPhoneOS.platform/Developer/SDKs/iPhoneOS12.1.sdk" python scripts/mk_make.py
We need to manually edit the generated Makefile in one place.
In build/config.mk, change the line that starts with SLINK_EXTRA_FLAGS
to read:
SLINK_EXTRA_FLAGS=-arch arm64 -mios-version-min=12.0 -isysroot /Applications/Xcode.app/Contents/Developer/Platforms/iPhoneOS.platform/Developer/SDKs/iPhoneOS12.1.sdk
Then run:
cd build
make -j8
Now there's a libz3.dylib in the build directory.
We need to modify it to cooperate with the linker:
install_name_tool -id "@executable_path/Frameworks/libz3.dylib" libz3.dylib
Now you can copy libz3.dylib to src/app.