This is amazing. I wanted to do something similar for a web-based optimization. I ended up just putting a C++ Lambda up to serve the requests.
I wonder how the performance compares? I feel like optimization frameworks make use of a lot of CPU-based heuristics.
Specifically, I haven't been able to find a reasonable set of parameters that cause the optimization to take longer than ~20 seconds on the slowest device I tried.
To get things to be smooth, though, I had to do debouncing and also run optimization in a web worker (separate, non-blocking thread) so the UI doesn't hang. Doing that was its own challenge since web workers don't use the HTTP cache for security reasons (they're supposed to be an isolated context), and it was re-requesting the ~5MB WASM files every time any of the numbers was adjusted. To solve this I used a service worker with a local cache.
Slow performance of web-based Z3 for optimization was one of the main reasons I switched to SCIP. I originally had a version working using a WASM port of Z3, but it just wasn't fast enough to be usable.
Did you do some local-vs-phone tests? I'm really curious how 20s on android compares to laptop.
If you end up wanting to use the version of SCIP compiled to WASM, I have it pre-compiled in the repo here: https://github.com/jstrieb/poker-chipper/tree/fab41bbe8821d0...
To interact with WASM SCIP, I use the CLI with an Emscripten virtual filesystem (as opposed to the C API/FFI): https://github.com/jstrieb/poker-chipper/blob/fab41bbe8821d0...
If you want to compile it yourself, the code and compiler flags I used to do that are documented in a Dockerfile in the repo: https://github.com/jstrieb/poker-chipper/blob/fab41bbe8821d0...