summaryrefslogtreecommitdiff
path: root/src/theory/strings/regexp_operation.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
-rw-r--r--src/theory/strings/regexp_operation.h2
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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback