summaryrefslogtreecommitdiff
path: root/src/theory/strings/sequences_rewriter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/sequences_rewriter.cpp')
-rw-r--r--src/theory/strings/sequences_rewriter.cpp58
1 files changed, 29 insertions, 29 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 152f71019..d8b8765eb 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -99,20 +99,22 @@ Node SequencesRewriter::rewriteEquality(Node node)
{
unsigned index1 = r == 0 ? i : (c[0].size() - 1) - i;
unsigned index2 = r == 0 ? i : (c[1].size() - 1) - i;
- if (c[0][index1].isConst() && c[1][index2].isConst())
+ Node s = c[0][index1];
+ Node t = c[1][index2];
+ if (s.isConst() && t.isConst())
{
- CVC4::String s = c[0][index1].getConst<String>();
- CVC4::String t = c[1][index2].getConst<String>();
- unsigned len_short = s.size() <= t.size() ? s.size() : t.size();
- bool isSameFix =
- r == 1 ? s.rstrncmp(t, len_short) : s.strncmp(t, len_short);
+ size_t lenS = Word::getLength(s);
+ size_t lenT = Word::getLength(t);
+ size_t lenShort = lenS <= lenT ? lenS : lenT;
+ bool isSameFix = r == 1 ? Word::rstrncmp(s, t, lenShort)
+ : Word::strncmp(s, t, lenShort);
if (!isSameFix)
{
Node ret = NodeManager::currentNM()->mkConst(false);
return returnRewrite(node, ret, Rewrite::EQ_NFIX);
}
}
- if (c[0][index1] != c[1][index2])
+ if (s != t)
{
break;
}
@@ -280,7 +282,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
}
// ------- rewrites for (= "" _)
- Node empty = nm->mkConst(::CVC4::String(""));
+ Node empty = Word::mkEmptyWord(stype);
for (size_t i = 0; i < 2; i++)
{
if (node[i] == empty)
@@ -585,7 +587,6 @@ Node SequencesRewriter::rewriteConcat(Node node)
Assert(node.getKind() == kind::STRING_CONCAT);
Trace("strings-rewrite-debug")
<< "Strings::rewriteConcat start " << node << std::endl;
- NodeManager* nm = NodeManager::currentNM();
std::vector<Node> node_vec;
Node preNode = Node::null();
for (Node tmpNode : node)
@@ -598,8 +599,10 @@ Node SequencesRewriter::rewriteConcat(Node node)
{
if (tmpNode[0].isConst())
{
- preNode = nm->mkConst(
- preNode.getConst<String>().concat(tmpNode[0].getConst<String>()));
+ std::vector<Node> wvec;
+ wvec.push_back(preNode);
+ wvec.push_back(tmpNode[0]);
+ preNode = Word::mkWord(wvec);
node_vec.push_back(preNode);
}
else
@@ -1114,14 +1117,14 @@ Node SequencesRewriter::rewriteMembership(TNode node)
{
if (x.isConst())
{
- String s = x.getConst<String>();
- if (s.size() == 0)
+ size_t xlen = Word::getLength(x);
+ if (xlen == 0)
{
Node retNode = nm->mkConst(true);
// e.g. (str.in.re "" (re.* (str.to.re x))) ----> true
return returnRewrite(node, retNode, Rewrite::RE_EMPTY_IN_STR_STAR);
}
- else if (s.size() == 1)
+ else if (xlen == 1)
{
if (r[0].getKind() == STRING_TO_REGEXP)
{
@@ -1317,7 +1320,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
// above, we strip components to construct an equivalent membership:
// (str.++ xi .. xj) in (re.++ rk ... rl).
Node xn = utils::mkConcat(mchildren, stype);
- Node emptyStr = nm->mkConst(String(""));
+ Node emptyStr = Word::mkEmptyWord(stype);
if (children.empty())
{
// If we stripped all components on the right, then the left is
@@ -1913,7 +1916,7 @@ Node SequencesRewriter::rewriteContains(Node node)
Node ret;
if (nc2.size() > 1)
{
- Node emp = nm->mkConst(CVC4::String(""));
+ Node emp = Word::mkEmptyWord(stype);
NodeBuilder<> nb2(kind::AND);
for (const Node& n2 : nc2)
{
@@ -1969,7 +1972,7 @@ Node SequencesRewriter::rewriteContains(Node node)
{
if (node[1].isConst())
{
- CVC4::String t = node[1].getConst<String>();
+ Node t = node[1];
// Below, we are looking for a constant component of node[0]
// has no overlap with node[1], which means we can split.
// Notice that if the first or last components had no
@@ -1981,9 +1984,8 @@ Node SequencesRewriter::rewriteContains(Node node)
// constant contains
if (node[0][i].isConst())
{
- CVC4::String s = node[0][i].getConst<String>();
// if no overlap, we can split into disjunction
- if (s.noOverlapWith(t))
+ if (Word::noOverlapWith(node[0][i], node[1]))
{
std::vector<Node> nc0;
utils::getConcat(node[0], nc0);
@@ -2067,7 +2069,7 @@ Node SequencesRewriter::rewriteContains(Node node)
Node ctn = d_stringsEntail.checkContains(node[1], node[0][2]);
if (!ctn.isNull() && !ctn.getConst<bool>())
{
- Node empty = nm->mkConst(String(""));
+ Node empty = Word::mkEmptyWord(stype);
Node ret = nm->mkNode(
kind::STRING_STRCTN,
nm->mkNode(kind::STRING_STRREPL, node[0][0], node[0][1], empty),
@@ -2093,7 +2095,7 @@ Node SequencesRewriter::rewriteContains(Node node)
// Note: Length-based reasoning is not sufficient to get this rewrite. We
// can neither show that str.len(str.replace("", x, y)) - str.len(x) >= 0
// nor str.len(x) - str.len(str.replace("", x, y)) >= 0
- Node emp = nm->mkConst(CVC4::String(""));
+ Node emp = Word::mkEmptyWord(stype);
if (node[0] == node[1][1] && node[1][0] == emp)
{
Node ret = nm->mkNode(kind::EQUAL, emp, node[1]);
@@ -2169,7 +2171,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
Node negone = nm->mkConst(Rational(-1));
return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART);
}
- Node emp = nm->mkConst(CVC4::String(""));
+ Node emp = Word::mkEmptyWord(stype);
if (node[0] != emp)
{
// indexof( x, x, z ) ---> indexof( "", "", z )
@@ -2390,7 +2392,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
// if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "")
if (StringsEntail::checkLengthOne(node[0]))
{
- Node empty = nm->mkConst(String(""));
+ Node empty = Word::mkEmptyWord(stype);
Node rn1 = Rewriter::rewrite(
rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty)));
if (rn1 != node[1])
@@ -2480,7 +2482,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
// substitute y with "" in the third argument. Note that the third argument
// does not matter when the str.replace does not apply.
//
- Node empty = nm->mkConst(::CVC4::String(""));
+ Node empty = Word::mkEmptyWord(stype);
std::vector<Node> emptyNodes;
bool allEmptyEqs;
@@ -2890,9 +2892,8 @@ Node SequencesRewriter::rewriteStrReverse(Node node)
Node x = node[0];
if (x.isConst())
{
- std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
- std::reverse(nvec.begin(), nvec.end());
- Node retNode = nm->mkConst(String(nvec));
+ // reverse the characters in the constant
+ Node retNode = Word::reverse(x);
return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
}
else if (x.getKind() == STRING_CONCAT)
@@ -2928,8 +2929,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
}
if (n[0].isConst())
{
- CVC4::String t = n[0].getConst<String>();
- if (t.isEmptyString())
+ if (Word::isEmpty(n[0]))
{
Node ret = NodeManager::currentNM()->mkConst(true);
return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY_CONST);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback