search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
338 stars 105 forks source link

Wasm build #215

Closed HKalbasi closed 1 year ago

HKalbasi commented 1 year ago

Hi, and thanks for this great library! Is it possible to use it with web assembly? Either wasm32-unknown-unknown or wasm32-wasi? My naive try failed with Can not find z3.h error, but I'm not sure if something is wrong on my side. It seems z3 itself supports webassembly so I wonder if there is a way to tweak this library and make it work with wasm.

waywardmonkeys commented 1 year ago

Great question. I assume you would want to build with static z3 … but not sure how best to tell cmake to build for WebAssmbky offhand. I am not home, so can’t try but feel free to experiment!

HKalbasi commented 1 year ago

Thanks for quick response! I tried to build with static link as well, but it failed to build with some wasm-ld error (can not find -lgcc or something like that). Unfortunately z3 itself uses emscripten so I think it wouldn't help much. I still have hope and will try more but I'm pretty unexperienced with c/c++ build systems so it would be great if you look at it as well when you find free time. Thanks!