diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-12 09:02:43 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-12 15:02:43 +0000 |
| commit | 99e830f0dd0beb00f93ea04b819294cab5e35b9a (patch) | |
| tree | b92f1ea4182fb0c0a04d504f36c45fe1685ceecf /src/theory/strings/rewrites.h | |
| parent | ad340126a7adbb9840cca1d082c57b43995987a4 (diff) | |
Add some basic rewrites for regular expression intersection (#7629)
Adds some basic rewrites for re.inter and re.union involving children of the form (str.to_re c) for constants c.
This is towards addressing bottlenecks for Zelkova benchmarks.
Diffstat (limited to 'src/theory/strings/rewrites.h')
| -rw-r--r-- | src/theory/strings/rewrites.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index 5e63c55c8..684ee0e8a 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -81,6 +81,8 @@ enum class Rewrite : uint32_t RE_AND_EMPTY, RE_ANDOR_FLATTEN, RE_ANDOR_INC_CONFLICT, + RE_INTER_CONST_CONST_CONFLICT, + RE_INTER_CONST_RE_CONFLICT, RE_CHAR_IN_STR_STAR, RE_CONCAT, RE_CONCAT_FLATTEN, |