diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-30 14:30:45 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-30 20:30:45 +0000 |
| commit | 23f134fa7309621be513ca3c728b7a3c03473a45 (patch) | |
| tree | 66e2040ec77f4c662971c20ac9b98b6aee61eb11 /docs/api/python/z3compat/bitvec.rst | |
| parent | 641c531bcb9df45ca6c19f3f9ccfad08afbe17de (diff) | |
Generalize eager length bound conflicts for regular expression memberships (#7633)
This generalizes eager length bound conflicts to take into account regular expression memberships.
For example:
If `(str.in_re x (re.++ (re.* re.allchar) (str.to_re "abc") (re.* re.allchar))` is asserted, then we know `(str.len x) >= 3`.
If e.g. equivalence class of `x` is merged with `(str.substr y 0 2)`, we get the conflict
`(and (str.in_re x (re.++ (re.* re.allchar) (str.to_re "abc") (re.* re.allchar)) (= x (str.substr y 0 2))`
since `(str.len (str.substr y 0 2)) <= 2`.
This also does some minor refactoring to eager prefix conflicts to make it more analogous to our implementation of length conflicts.
Diffstat (limited to 'docs/api/python/z3compat/bitvec.rst')
0 files changed, 0 insertions, 0 deletions