diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/kinds | 10 | ||||
-rw-r--r-- | src/theory/strings/regexp_elim.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/regexp_entail.cpp | 11 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 35 | ||||
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 6 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 38 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 11 |
7 files changed, 65 insertions, 56 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 9faa935e1..d23e44cee 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -48,7 +48,7 @@ sort STRING_TYPE \ sort REGEXP_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkNode(REGEXP_EMPTY)" \ + "NodeManager::currentNM()->mkNode(REGEXP_NONE)" \ "util/string.h" \ "RegExp type" @@ -103,8 +103,8 @@ operator REGEXP_OPT 1 "regexp ?" operator REGEXP_RANGE 2 "regexp range" operator REGEXP_COMPLEMENT 1 "regexp complement" -operator REGEXP_EMPTY 0 "regexp empty" -operator REGEXP_SIGMA 0 "regexp all characters" +operator REGEXP_NONE 0 "regexp empty" +operator REGEXP_ALLCHAR 0 "regexp all characters" constant REGEXP_REPEAT_OP \ struct \ @@ -143,8 +143,8 @@ typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_COMPLEMENT "SimpleTypeRule<RRegExp, ARegExp>" typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>" typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>" -typerule REGEXP_EMPTY "SimpleTypeRule<RRegExp>" -typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>" +typerule REGEXP_NONE "SimpleTypeRule<RRegExp>" +typerule REGEXP_ALLCHAR "SimpleTypeRule<RRegExp>" ### operators that apply to both strings and sequences diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index b3dc309d5..d5b7606f2 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -121,7 +121,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) if (fl.isNull()) { if (!hasPivotIndex && c.getKind() == REGEXP_STAR - && c[0].getKind() == REGEXP_SIGMA) + && c[0].getKind() == REGEXP_ALLCHAR) { hasPivotIndex = true; pivotIndex = i; @@ -167,7 +167,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // We do not need to include memberships of the form // (str.substr x n 1) in re.allchar // since we know that by construction, n < len( x ). - if (re[i].getKind() != REGEXP_SIGMA) + if (re[i].getKind() != REGEXP_ALLCHAR) { Node currMem = nm->mkNode(STRING_IN_REGEXP, curr, re[i]); conc.push_back(currMem); @@ -212,13 +212,13 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) gap_minsize.push_back(0); gap_exact.push_back(true); } - else if (c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_SIGMA) + else if (c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_ALLCHAR) { // found a gap of any size onlySigmasAndConsts = true; gap_exact[gap_exact.size() - 1] = false; } - else if (c.getKind() == REGEXP_SIGMA) + else if (c.getKind() == REGEXP_ALLCHAR) { // add one to the minimum size of the gap onlySigmasAndConsts = true; @@ -565,7 +565,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) for (const Node& r : disj) { Assert(r.getKind() != REGEXP_UNION); - Assert(r.getKind() != REGEXP_SIGMA); + Assert(r.getKind() != REGEXP_ALLCHAR); lenOnePeriod = false; // lenOnePeriod is true if this regular expression is a single character // regular expression diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index be1646403..530f34455 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -116,7 +116,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren, mchildren.pop_back(); do_next = true; } - else if (rc.getKind() == REGEXP_RANGE || rc.getKind() == REGEXP_SIGMA) + else if (rc.getKind() == REGEXP_RANGE + || rc.getKind() == REGEXP_ALLCHAR) { if (!isConstRegExp(rc)) { @@ -513,11 +514,11 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s, return true; } } - case REGEXP_EMPTY: + case REGEXP_NONE: { return false; } - case REGEXP_SIGMA: + case REGEXP_ALLCHAR: { if (s.size() == index_start + 1) { @@ -654,7 +655,7 @@ Node RegExpEntail::getFixedLengthForRegexp(Node n) return ret; } } - else if (n.getKind() == REGEXP_SIGMA || n.getKind() == REGEXP_RANGE) + else if (n.getKind() == REGEXP_ALLCHAR || n.getKind() == REGEXP_RANGE) { return nm->mkConst(Rational(1)); } @@ -710,7 +711,7 @@ bool RegExpEntail::regExpIncludes(Node r1, Node r2) return false; } NodeManager* nm = NodeManager::currentNM(); - Node sigma = nm->mkNode(REGEXP_SIGMA, std::vector<Node>{}); + Node sigma = nm->mkNode(REGEXP_ALLCHAR, std::vector<Node>{}); Node sigmaStar = nm->mkNode(REGEXP_STAR, sigma); std::vector<Node> v1, v2; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 81ac75c84..fff512f98 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -35,11 +35,11 @@ RegExpOpr::RegExpOpr(Env& env, SkolemCache* sc) : EnvObj(env), d_true(NodeManager::currentNM()->mkConst(true)), d_false(NodeManager::currentNM()->mkConst(false)), - d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_EMPTY, + d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_NONE, std::vector<Node>{})), d_zero(NodeManager::currentNM()->mkConst(::cvc5::Rational(0))), d_one(NodeManager::currentNM()->mkConst(::cvc5::Rational(1))), - d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, + d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_ALLCHAR, std::vector<Node>{})), d_sigma_star( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)), @@ -84,7 +84,7 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r) d_constCache[cur] = tmp.isConst() ? RE_C_CONRETE_CONSTANT : RE_C_VARIABLE; } - else if (ck == REGEXP_SIGMA || ck == REGEXP_RANGE) + else if (ck == REGEXP_ALLCHAR || ck == REGEXP_RANGE) { d_constCache[cur] = RE_C_CONSTANT; } @@ -136,8 +136,8 @@ int RegExpOpr::delta( Node r, Node &exp ) { Kind k = r.getKind(); switch (k) { - case REGEXP_EMPTY: - case REGEXP_SIGMA: + case REGEXP_NONE: + case REGEXP_ALLCHAR: case REGEXP_RANGE: { // does not contain empty string @@ -295,11 +295,13 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode) d_deriv_cache[dv] = p; } else { switch( r.getKind() ) { - case kind::REGEXP_EMPTY: { + case kind::REGEXP_NONE: + { ret = 2; break; } - case kind::REGEXP_SIGMA: { + case kind::REGEXP_ALLCHAR: + { retNode = d_emptySingleton; break; } @@ -550,11 +552,13 @@ Node RegExpOpr::derivativeSingle(Node r, cvc5::String c) } else { Kind k = r.getKind(); switch( k ) { - case kind::REGEXP_EMPTY: { + case kind::REGEXP_NONE: + { retNode = d_emptyRegexp; break; } - case kind::REGEXP_SIGMA: { + case kind::REGEXP_ALLCHAR: + { retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ); break; } @@ -719,7 +723,8 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) SetNodes vset; Kind k = r.getKind(); switch( k ) { - case kind::REGEXP_EMPTY: { + case kind::REGEXP_NONE: + { break; } case kind::REGEXP_RANGE: { @@ -792,7 +797,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) firstChars(r[0], cset, vset); break; } - case kind::REGEXP_SIGMA: + case kind::REGEXP_ALLCHAR: case kind::REGEXP_COMPLEMENT: default: { // we do not expect to call this function on regular expressions that @@ -1198,7 +1203,7 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr1); r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr2); } - else if (nk == STRING_TO_REGEXP || nk == REGEXP_SIGMA || nk == REGEXP_RANGE + else if (nk == STRING_TO_REGEXP || nk == REGEXP_ALLCHAR || nk == REGEXP_RANGE || nk == REGEXP_COMPLEMENT || nk == REGEXP_LOOP) { // this leaves n unchanged @@ -1466,11 +1471,13 @@ std::string RegExpOpr::mkString( Node r ) { } else { int k = r.getKind(); switch( k ) { - case kind::REGEXP_EMPTY: { + case kind::REGEXP_NONE: + { retStr += "\\E"; break; } - case kind::REGEXP_SIGMA: { + case kind::REGEXP_ALLCHAR: + { retStr += "."; break; } diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 050ec594a..04de0ea44 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -52,7 +52,7 @@ RegExpSolver::RegExpSolver(Env& env, d_regexp_opr(env, tr.getSkolemCache()) { d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::String("")); - d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY); + d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_NONE); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } @@ -656,8 +656,8 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp) Node ret = r; switch (r.getKind()) { - case REGEXP_EMPTY: - case REGEXP_SIGMA: + case REGEXP_NONE: + case REGEXP_ALLCHAR: case REGEXP_RANGE: break; case STRING_TO_REGEXP: { diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 783e258fa..babf260fc 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -789,10 +789,10 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node) changed = true; emptyRe = c; } - else if (c.getKind() == REGEXP_EMPTY) + else if (c.getKind() == REGEXP_NONE) { // re.++( ..., empty, ... ) ---> empty - Node ret = nm->mkNode(REGEXP_EMPTY); + Node ret = nm->mkNode(REGEXP_NONE); return returnRewrite(node, ret, Rewrite::RE_CONCAT_EMPTY); } else @@ -868,7 +868,7 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node) { curr = Node::null(); } - else if (curr[0].getKind() == REGEXP_SIGMA) + else if (curr[0].getKind() == REGEXP_ALLCHAR) { Assert(!lastAllStar); lastAllStar = true; @@ -932,7 +932,7 @@ Node SequencesRewriter::rewriteStarRegExp(TNode node) // ("")* ---> "" return returnRewrite(node, node[0], Rewrite::RE_STAR_EMPTY_STRING); } - else if (node[0].getKind() == REGEXP_EMPTY) + else if (node[0].getKind() == REGEXP_NONE) { // (empty)* ---> "" retNode = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))); @@ -992,7 +992,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) } } } - else if (ni.getKind() == REGEXP_EMPTY) + else if (ni.getKind() == REGEXP_NONE) { if (nk == REGEXP_INTER) { @@ -1000,7 +1000,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) } // otherwise, can ignore } - else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_SIGMA) + else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_ALLCHAR) { if (nk == REGEXP_UNION) { @@ -1032,11 +1032,11 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) Node retNode; if (nk == REGEXP_INTER) { - retNode = nm->mkNode(kind::REGEXP_EMPTY); + retNode = nm->mkNode(kind::REGEXP_NONE); } else { - retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA)); + retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR)); } return returnRewrite(node, retNode, Rewrite::RE_ANDOR_INC_CONFLICT); } @@ -1047,11 +1047,11 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) { if (nk == REGEXP_INTER) { - retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA)); + retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR)); } else { - retNode = nm->mkNode(kind::REGEXP_EMPTY); + retNode = nm->mkNode(kind::REGEXP_NONE); } } else @@ -1091,7 +1091,7 @@ Node SequencesRewriter::rewriteLoopRegExp(TNode node) if (u < l) { std::vector<Node> nvec; - retNode = nm->mkNode(REGEXP_EMPTY, nvec); + retNode = nm->mkNode(REGEXP_NONE, nvec); } else if (u == l) { @@ -1184,7 +1184,7 @@ Node SequencesRewriter::rewriteRangeRegExp(TNode node) if (ch[0] > ch[1]) { // re.range( "B", "A" ) ---> re.none - Node retNode = nm->mkNode(REGEXP_EMPTY); + Node retNode = nm->mkNode(REGEXP_NONE); return returnRewrite(node, retNode, Rewrite::RE_RANGE_EMPTY); } return node; @@ -1199,7 +1199,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) TypeNode stype = x.getType(); TypeNode rtype = r.getType(); - if(r.getKind() == kind::REGEXP_EMPTY) + if (r.getKind() == kind::REGEXP_NONE) { Node retNode = NodeManager::currentNM()->mkConst(false); return returnRewrite(node, retNode, Rewrite::RE_IN_EMPTY); @@ -1212,7 +1212,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) Node retNode = NodeManager::currentNM()->mkConst(test); return returnRewrite(node, retNode, Rewrite::RE_IN_EVAL); } - else if (r.getKind() == kind::REGEXP_SIGMA) + else if (r.getKind() == kind::REGEXP_ALLCHAR) { Node one = nm->mkConst(Rational(1)); Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x)); @@ -1260,7 +1260,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) } } } - if (r[0].getKind() == kind::REGEXP_SIGMA) + if (r[0].getKind() == kind::REGEXP_ALLCHAR) { Node retNode = NodeManager::currentNM()->mkConst(true); return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA_STAR); @@ -1277,12 +1277,12 @@ Node SequencesRewriter::rewriteMembership(TNode node) for (size_t i = 0; i < nchildren; i++) { Node rc = r[i]; - Assert(rc.getKind() != kind::REGEXP_EMPTY); - if (rc.getKind() == kind::REGEXP_SIGMA) + Assert(rc.getKind() != kind::REGEXP_NONE); + if (rc.getKind() == kind::REGEXP_ALLCHAR) { allSigmaMinSize++; } - else if (rc.getKind() == REGEXP_STAR && rc[0].getKind() == REGEXP_SIGMA) + else if (rc.getKind() == REGEXP_STAR && rc[0].getKind() == REGEXP_ALLCHAR) { allSigmaStrict = false; } @@ -3245,7 +3245,7 @@ std::pair<size_t, size_t> SequencesRewriter::firstMatch(Node n, Node r) Assert(r.getType().isRegExp()); NodeManager* nm = NodeManager::currentNM(); - Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA)); + Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR)); Node re = nm->mkNode(REGEXP_CONCAT, r, sigmaStar); String s = n.getConst<String>(); 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 |