Adding Z3 to android or ios devices

[francos3]

Dear all,

I am considering using Z3 as a solver for a constraint problem in a mobile app. Is anybody aware of z3 being compiled for IOS or Android? If so, any advice or links would be very welcomed.

Thanks,

[aytey]

There's this:

• https://www.cs.utexas.edu/~bornholt/post/z3-iphone.html
• https://github.com/jamesbornholt/z3-ios

Given Z3 runs on my M1 (and the above), then I assume getting it to work on iOS is fine.

[francos3]

Great, thanks! I am now only missing how to compile Z3 for android devices but I can get started with iOS. I have been a Linux developer all my life so this is very new to me ;-)

[NikolajBjorner]

@jamesbornholt's instructions indicate that some patches are needed to z3. Some tests are disabled directly and an include of some architecture specific include is omitted instead of using an if-def block.

If it helps , you can submit a suitable update directly to Z3 and also update the Azure build pipelines.
These pipelines should be able to dry-run ios/android either nightly or on every push.