search

prove-rs / z3.rs

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

Support for regular expression "mk_re_all" and "mk_re_allchar" #272

Closed pzhang101 closed 3 months ago

pzhang101 commented 9 months ago

Hi, I wonder is it possible to use the current RUST API to express the string "ab?c", where "" means any string, and "?" means any character? It seems to require the functions like "mk_re_all" and "mk_re_allchar", which are not supported by the current RUST API.

waywardmonkeys commented 9 months ago

I don't see a Z3_mk_re_all in current releases of Z3. I checked the API and we're missing bindings for Z3_mk_re_allchar, Z3_mk_re_diff, and Z3_mk_re_power which I'll land in a moment.

One thing to note is that these were added after 4.8.12 which is the most recent version in Ubuntu, so to use them, you'll have to be providing Z3 (like using the bundled or vcpkg features).

There will need to be additions for this to the higher level API in the z3 crate. PRs welcome!

waywardmonkeys commented 9 months ago

The z3-sys bindings for those 3 functions mentioned above are on master now.