diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 13:04:33 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:59:00 -0600 |
| commit | fb4104e7c5a88741f9ffd55384198af31435df9e (patch) | |
| tree | 4b9cd33cbe4ebccd914e63ddb1ae412f2c101d8b /src/theory/strings/kinds | |
| parent | acb79cbe43ddcd855db042b7c937fc2eacaa0ac3 (diff) | |
minor clean-up, bring back derivatives
Diffstat (limited to 'src/theory/strings/kinds')
| -rw-r--r-- | src/theory/strings/kinds | 19 |
1 files changed, 2 insertions, 17 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 2c9ba4b3f..b28c2fd9d 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -78,23 +78,8 @@ operator REGEXP_PLUS 1 "regexp +" operator REGEXP_OPT 1 "regexp ?" operator REGEXP_RANGE 2 "regexp range" -constant REGEXP_EMPTY \ - ::CVC4::RegExpEmpty \ - ::CVC4::RegExpHashFunction \ - "util/regexp.h" \ - "a regexp contains nothing" - -constant REGEXP_SIGMA \ - ::CVC4::RegExpSigma \ - ::CVC4::RegExpHashFunction \ - "util/regexp.h" \ - "a regexp contains an arbitrary charactor" - -#constant REGEXP_ALL \ -# ::CVC4::RegExp \ -# ::CVC4::RegExpHashFunction \ -# "util/string.h" \ -# "a regexp contains all strings" +operator REGEXP_EMPTY 0 "regexp empty" +operator REGEXP_SIGMA 0 "regexp all charactors" typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule |