diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-23 18:15:28 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-23 16:15:28 -0700 |
| commit | 64cef995a521ac7211b9e3ed95c85deb186ff352 (patch) | |
| tree | 927d14ff521127f37192afcfe8b737f15d54e061 /src/theory/strings/regexp_operation.h | |
| parent | 0d4d9bf3f31687d9cf48b0c45ab420b06ff099f7 (diff) | |
Fixes for SyGuS + regular expressions (#3313)
This commit fixes numerous issues involving the combination of SyGuS and regular expressions.
Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior.
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
| -rw-r--r-- | src/theory/strings/regexp_operation.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 117449d35..c7464760d 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -119,6 +119,8 @@ class RegExpOpr { bool checkConstRegExp( Node r ); /** get the constant type for regular expression r */ RegExpConstType getRegExpConstType(Node r); + /** is k a native operator whose return type is a regular expression? */ + static bool isRegExpKind(Kind k); void simplify(Node t, std::vector< Node > &new_nodes, bool polarity); int delta( Node r, Node &exp ); int derivativeS( Node r, CVC4::String c, Node &retNode ); |