Replies: 1 comment 2 replies
-
I am not sure what the issue of the question is. Instead of using integers and substring that have to deal with cases where g1_e - g1_s is negative InRe are z3 expressions so you can add them in nested formulas. |
Beta Was this translation helpful? Give feedback.
2 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
So I want to have regexes in z3 and have groups, but from what I can see right now that's not an option in z3, and I want to try to emulate groups. So the current approach is for every group, create a pair of ints that represents the start and end matching positions of the group, and assert that what's before, inside and after the group matches the string sliced by the pair of ints. Example:
However, this only works standalone, but if there needs to be a pre-condition, then there's a problem. How can I turn this into an actual z3 expression so that it can be used in other expressions? Thanks!
Beta Was this translation helpful? Give feedback.
All reactions