diff options
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 29 |
1 files changed, 10 insertions, 19 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index d104f3ade..0520ec88a 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -18,7 +18,7 @@ #include "expr/kind.h" #include "options/strings_options.h" -#include "theory/strings/sequences_rewriter.h" +#include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" @@ -83,7 +83,7 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r) { d_constCache[cur] = RE_C_CONSTANT; } - else if (!isRegExpKind(ck)) + else if (!utils::isRegExpKind(ck)) { // non-regular expression applications, e.g. function applications // with regular expression return type are treated as variables. @@ -115,15 +115,6 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r) return d_constCache[r]; } -bool RegExpOpr::isRegExpKind(Kind k) -{ - return k == REGEXP_EMPTY || k == REGEXP_SIGMA || 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 - || k == REGEXP_COMPLEMENT; -} - // 0-unknown, 1-yes, 2-no int RegExpOpr::delta( Node r, Node &exp ) { Trace("regexp-delta") << "RegExp-Delta starts with /" << mkString( r ) << "/" << std::endl; @@ -270,7 +261,7 @@ int RegExpOpr::delta( Node r, Node &exp ) { break; } default: { - Assert(!isRegExpKind(k)); + Assert(!utils::isRegExpKind(k)); break; } } @@ -521,7 +512,7 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { break; } default: { - Assert(!isRegExpKind(r.getKind())); + Assert(!utils::isRegExpKind(r.getKind())); return 0; break; } @@ -808,7 +799,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) // aren't a standard regular expression kind. However, if we do, then // the following code is conservative and says that the current // regular expression can begin with any character. - Assert(isRegExpKind(k)); + Assert(utils::isRegExpKind(k)); // can start with any character Assert(d_lastchar < std::numeric_limits<unsigned>::max()); for (unsigned i = 0; i <= d_lastchar; i++) @@ -908,12 +899,12 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes // all strings in the language of R1 have the same length, say n, // then the conclusion of the reduction is quantifier-free: // ~( substr(s,0,n) in R1 ) OR ~( substr(s,n,len(s)-n) in R2) - Node reLength = SequencesRewriter::getFixedLengthForRegexp(r[0]); + Node reLength = RegExpEntail::getFixedLengthForRegexp(r[0]); if (reLength.isNull()) { // try from the opposite end unsigned indexE = r.getNumChildren() - 1; - reLength = SequencesRewriter::getFixedLengthForRegexp(r[indexE]); + reLength = RegExpEntail::getFixedLengthForRegexp(r[indexE]); if (!reLength.isNull()) { indexRm = indexE; @@ -1068,7 +1059,7 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes break; } default: { - Assert(!isRegExpKind(k)); + Assert(!utils::isRegExpKind(k)); break; } } @@ -1267,7 +1258,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes break; } default: { - Assert(!isRegExpKind(k)); + Assert(!utils::isRegExpKind(k)); break; } } @@ -1744,7 +1735,7 @@ std::string RegExpOpr::mkString( Node r ) { std::stringstream ss; ss << r; retStr = ss.str(); - Assert(!isRegExpKind(r.getKind())); + Assert(!utils::isRegExpKind(r.getKind())); break; } } |