diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-30 16:29:23 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-30 16:29:23 -0500 |
commit | 6838885b1250e0abbb1b8d56e6b400a5d7f3ca95 (patch) | |
tree | 3c1a7417d471aeea531a36024a460d605cb5d5f1 /src/theory/strings/regexp_operation.cpp | |
parent | 3ff70d61c111b70d5bf770669b0aa3f1d47a502e (diff) |
Support indexed operators re.loop and re.^ (#4167)
Towards support for the strings standard.
This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices).
This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions.
Also fixes #4161.
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 38 |
1 files changed, 16 insertions, 22 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 9a2091eac..6453e1909 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -93,15 +93,7 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r) { d_constCache[cur] = RE_C_UNKNOWN; visit.push_back(cur); - if (ck == REGEXP_LOOP) - { - // only add the first child of loop - visit.push_back(cur[0]); - } - else - { - visit.insert(visit.end(), cur.begin(), cur.end()); - } + visit.insert(visit.end(), cur.begin(), cur.end()); } } else if (it->second == RE_C_UNKNOWN) @@ -260,7 +252,9 @@ int RegExpOpr::delta( Node r, Node &exp ) { break; } case kind::REGEXP_LOOP: { - if(r[1] == d_zero) { + uint32_t lo = utils::getLoopMinOccurrences(r); + if (lo == 0) + { ret = 1; } else { ret = delta(r[0], exp); @@ -501,18 +495,18 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { break; } case kind::REGEXP_LOOP: { - if(r[1] == r[2] && r[1] == d_zero) { + uint32_t l = utils::getLoopMinOccurrences(r); + uint32_t u = utils::getLoopMaxOccurrences(r); + if (l == u && l == 0) + { ret = 2; //retNode = d_emptyRegexp; } else { Node dc; ret = derivativeS(r[0], c, dc); if(dc==d_emptyRegexp) { - unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt(); - unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); - Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], - NodeManager::currentNM()->mkConst(CVC4::Rational(l==0? 0 : (l-1))), - NodeManager::currentNM()->mkConst(CVC4::Rational(u-1))); + Node lop = nm->mkConst(RegExpLoop(l == 0 ? 0 : (l - 1), u - 1)); + Node r2 = nm->mkNode(REGEXP_LOOP, lop, r[0]); retNode = dc==d_emptySingleton? r2 : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r2 ); } else { retNode = d_emptyRegexp; @@ -686,16 +680,16 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { break; } case kind::REGEXP_LOOP: { - if(r[1] == r[2] && r[1] == d_zero) { + uint32_t l = utils::getLoopMinOccurrences(r); + uint32_t u = utils::getLoopMaxOccurrences(r); + if (l == u || l == 0) + { retNode = d_emptyRegexp; } else { Node dc = derivativeSingle(r[0], c); if(dc != d_emptyRegexp) { - unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt(); - unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); - Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], - NodeManager::currentNM()->mkConst(CVC4::Rational(l==0? 0 : (l-1))), - NodeManager::currentNM()->mkConst(CVC4::Rational(u-1))); + Node lop = nm->mkConst(RegExpLoop(l == 0 ? 0 : (l - 1), u - 1)); + Node r2 = nm->mkNode(REGEXP_LOOP, lop, r[0]); retNode = dc==d_emptySingleton? r2 : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r2 ); } else { retNode = d_emptyRegexp; |