summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/kinds10
-rw-r--r--src/theory/strings/regexp_elim.cpp10
-rw-r--r--src/theory/strings/regexp_entail.cpp11
-rw-r--r--src/theory/strings/regexp_operation.cpp35
-rw-r--r--src/theory/strings/regexp_solver.cpp6
-rw-r--r--src/theory/strings/sequences_rewriter.cpp38
-rw-r--r--src/theory/strings/theory_strings_utils.cpp11
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback