summaryrefslogtreecommitdiff
path: root/src/theory/strings/kinds
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-03-27 16:54:46 -0500
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-03-27 17:15:13 -0500
commit70a7ae4dc962e43c38cec19a5549673a46045d71 (patch)
tree92b0cd3ae9714db86d0833ad1bda9b2a406bd910 /src/theory/strings/kinds
parentabdb1691f287587f18801733e4ab7248167db1ca (diff)
adds new feature: re.loop
Diffstat (limited to 'src/theory/strings/kinds')
-rw-r--r--src/theory/strings/kinds2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index b28c2fd9d..67b60fdfe 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -77,6 +77,7 @@ operator REGEXP_STAR 1 "regexp *"
operator REGEXP_PLUS 1 "regexp +"
operator REGEXP_OPT 1 "regexp ?"
operator REGEXP_RANGE 2 "regexp range"
+operator REGEXP_LOOP 2:3 "regexp loop"
operator REGEXP_EMPTY 0 "regexp empty"
operator REGEXP_SIGMA 0 "regexp all charactors"
@@ -88,6 +89,7 @@ typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
+typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule
typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback