diff options
Diffstat (limited to 'src/theory/strings/theory_strings_utils.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 9ab65f6ec..59bb0755c 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -285,7 +285,7 @@ bool isConstantLike(Node n) { return n.isConst() || n.getKind() == SEQ_UNIT; } bool isUnboundedWildcard(const std::vector<Node>& rs, size_t start) { size_t i = start; - while (i < rs.size() && rs[i].getKind() == REGEXP_SIGMA) + while (i < rs.size() && rs[i].getKind() == REGEXP_ALLCHAR) { i++; } @@ -295,7 +295,7 @@ bool isUnboundedWildcard(const std::vector<Node>& rs, size_t start) return false; } - return rs[i].getKind() == REGEXP_STAR && rs[i][0].getKind() == REGEXP_SIGMA; + return rs[i].getKind() == REGEXP_STAR && rs[i][0].getKind() == REGEXP_ALLCHAR; } bool isSimpleRegExp(Node r) @@ -313,8 +313,9 @@ bool isSimpleRegExp(Node r) return false; } } - else if (n.getKind() != REGEXP_SIGMA - && (n.getKind() != REGEXP_STAR || n[0].getKind() != REGEXP_SIGMA)) + else if (n.getKind() != REGEXP_ALLCHAR + && (n.getKind() != REGEXP_STAR + || n[0].getKind() != REGEXP_ALLCHAR)) { return false; } @@ -376,7 +377,7 @@ bool isStringKind(Kind k) bool isRegExpKind(Kind k) { - return k == REGEXP_EMPTY || k == REGEXP_SIGMA || k == STRING_TO_REGEXP + return k == REGEXP_NONE || k == REGEXP_ALLCHAR || k == STRING_TO_REGEXP || k == REGEXP_CONCAT || k == REGEXP_UNION || k == REGEXP_INTER || k == REGEXP_STAR || k == REGEXP_PLUS || k == REGEXP_OPT || k == REGEXP_RANGE || k == REGEXP_LOOP || k == REGEXP_RV |