diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 11:05:09 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:59:00 -0600 |
commit | acb79cbe43ddcd855db042b7c937fc2eacaa0ac3 (patch) | |
tree | e8af21bba458cbc2a00d3512519cea3e07af3b65 /src/theory/strings/kinds | |
parent | 76f497ef9444a81143ad35b2eda899e119b8e662 (diff) |
a new regular expression engine for solving both positive and negative membership constraints
Diffstat (limited to 'src/theory/strings/kinds')
-rw-r--r-- | src/theory/strings/kinds | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index f8f8b9555..2c9ba4b3f 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -71,7 +71,7 @@ typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule # equal equal / less than / output operator STRING_TO_REGEXP 1 "convert string to regexp" operator REGEXP_CONCAT 2: "regexp concat" -operator REGEXP_OR 2: "regexp or" +operator REGEXP_UNION 2: "regexp union" operator REGEXP_INTER 2: "regexp intersection" operator REGEXP_STAR 1 "regexp *" operator REGEXP_PLUS 1 "regexp +" @@ -97,7 +97,7 @@ constant REGEXP_SIGMA \ # "a regexp contains all strings" typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule -typerule REGEXP_OR ::CVC4::theory::strings::RegExpOrTypeRule +typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule |