search

prove-rs / z3.rs

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

Support for more regular expression operations #275

Closed Pat-Lafon closed 3 months ago

Pat-Lafon commented 9 months ago

Fixes #272

(First two commits) My attempt at adding the new regular expression operations: power, allchar, and diff. I also noticed that option was exposed but not implemented so I've added that as well.

(Third commit) I was looking to test my inclusions to the code base but I realized that I'm not sure about the semantics of regular expressions in Z3? I ran into some weird behavior I don't understand so I just added a simple test from https://z3prover.github.io/api/html/z3py_8py_source.html#l11172 to get some advice. test_regex_union works as expected, checking that (a|b) matches with a and b but not c. However, I found that I get SatResult::Sat in more cases than I expect like in test_regex_union2 which just checks that c matches with (a|b). I would expect to get SatResult::Unsat but I don't?

waywardmonkeys commented 3 months ago

@Pat-Lafon Do you want to try rebasing this on top of current master and see if CI passes? We're preparing for a new release.