diff options
Diffstat (limited to 'src/theory/strings/regexp_entail.h')
| -rw-r--r-- | src/theory/strings/regexp_entail.h | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h index 0732a6770..ef3f2d34e 100644 --- a/src/theory/strings/regexp_entail.h +++ b/src/theory/strings/regexp_entail.h @@ -108,6 +108,21 @@ class RegExpEntail * x in n entails len( x ) = c. */ static Node getFixedLengthForRegexp(Node n); + + /** + * Returns true if we can show that the regular expression `r1` includes + * the regular expression `r2` (i.e. `r1` matches a superset of sequences + * that `r2` matches). This method only works on a fragment of regular + * expressions, specifically regular expressions that pass the + * `isSimpleRegExp` check. + * + * @param r1 The regular expression that may include `r2` (must be in + * rewritten form) + * @param r2 The regular expression that may be included by `r1` (must be + * in rewritten form) + * @return True if the inclusion can be shown, false otherwise + */ + static bool regExpIncludes(Node r1, Node r2); }; } // namespace strings |