summaryrefslogtreecommitdiff
path: root/src/theory/strings/strings_entail.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/strings_entail.cpp')
-rw-r--r--src/theory/strings/strings_entail.cpp77
1 files changed, 35 insertions, 42 deletions
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 311eda554..9f502e1f6 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
@@ -37,8 +37,6 @@ bool StringsEntail::canConstantContainConcat(Node c,
int& lastc)
{
Assert(c.isConst());
- CVC4::String t = c.getConst<String>();
- const std::vector<unsigned>& tvec = t.getVec();
Assert(n.getKind() == STRING_CONCAT);
// must find constant components in order
size_t pos = 0;
@@ -50,19 +48,20 @@ bool StringsEntail::canConstantContainConcat(Node c,
{
firstc = firstc == -1 ? i : firstc;
lastc = i;
- CVC4::String s = n[i].getConst<String>();
- size_t new_pos = t.find(s, pos);
+ size_t new_pos = Word::find(c, n[i], pos);
if (new_pos == std::string::npos)
{
return false;
}
else
{
- pos = new_pos + s.size();
+ pos = new_pos + Word::getLength(n[i]);
}
}
else if (n[i].getKind() == STRING_ITOS && ArithEntail::check(n[i][0]))
{
+ Assert(c.getType().isString());
+ const std::vector<unsigned>& tvec = c.getConst<String>().getVec();
// find the first occurrence of a digit starting at pos
while (pos < tvec.size() && !String::isDigit(tvec[pos]))
{
@@ -116,7 +115,8 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
{
Assert(dir == 1 || dir == -1);
Assert(nr.empty());
- Node zero = NodeManager::currentNM()->mkConst(CVC4::Rational(0));
+ NodeManager* nm = NodeManager::currentNM();
+ Node zero = nm->mkConst(CVC4::Rational(0));
bool ret = false;
bool success;
unsigned sindex = 0;
@@ -139,18 +139,16 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
if (lbr.sgn() > 0)
{
Assert(ArithEntail::check(curr, true));
- CVC4::String s = n1[sindex_use].getConst<String>();
- Node ncl =
- NodeManager::currentNM()->mkConst(CVC4::Rational(s.size()));
- Node next_s =
- NodeManager::currentNM()->mkNode(MINUS, lowerBound, ncl);
+ Node s = n1[sindex_use];
+ size_t slen = Word::getLength(s);
+ Node ncl = nm->mkConst(CVC4::Rational(slen));
+ Node next_s = nm->mkNode(MINUS, lowerBound, ncl);
next_s = Rewriter::rewrite(next_s);
Assert(next_s.isConst());
// we can remove the entire constant
if (next_s.getConst<Rational>().sgn() >= 0)
{
- curr = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(MINUS, curr, ncl));
+ curr = Rewriter::rewrite(nm->mkNode(MINUS, curr, ncl));
success = true;
sindex++;
}
@@ -160,25 +158,20 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
// lower bound minus the length of a concrete string is negative,
// hence lowerBound cannot be larger than long max
Assert(lbr < Rational(String::maxSize()));
- curr = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(MINUS, curr, lowerBound));
+ curr = Rewriter::rewrite(nm->mkNode(MINUS, curr, lowerBound));
uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
- Assert(lbsize < s.size());
+ Assert(lbsize < slen);
if (dir == 1)
{
// strip partially from the front
- nr.push_back(
- NodeManager::currentNM()->mkConst(s.prefix(lbsize)));
- n1[sindex_use] = NodeManager::currentNM()->mkConst(
- s.suffix(s.size() - lbsize));
+ nr.push_back(Word::prefix(s, lbsize));
+ n1[sindex_use] = Word::suffix(s, slen - lbsize);
}
else
{
// strip partially from the back
- nr.push_back(
- NodeManager::currentNM()->mkConst(s.suffix(lbsize)));
- n1[sindex_use] = NodeManager::currentNM()->mkConst(
- s.prefix(s.size() - lbsize));
+ nr.push_back(Word::suffix(s, lbsize));
+ n1[sindex_use] = Word::prefix(s, slen - lbsize);
}
ret = true;
}
@@ -496,8 +489,6 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
{
Assert(nb.empty());
Assert(ne.empty());
-
- NodeManager* nm = NodeManager::currentNM();
bool changed = false;
// for ( forwards, backwards ) direction
for (unsigned r = 0; r < 2; r++)
@@ -509,7 +500,7 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
bool removeComponent = false;
Node n1cmp = n1[index0];
- if (n1cmp.isConst() && n1cmp.getConst<String>().size() == 0)
+ if (n1cmp.isConst() && Word::isEmpty(n1cmp))
{
return false;
}
@@ -522,14 +513,15 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
<< ", dir = " << dir << std::endl;
if (n1cmp.isConst())
{
- CVC4::String s = n1cmp.getConst<String>();
+ Node s = n1cmp;
+ size_t slen = Word::getLength(s);
// overlap is an overapproximation of the number of characters
// n2[index1] can match in s
- unsigned overlap = s.size();
+ unsigned overlap = Word::getLength(s);
if (n2[index1].isConst())
{
- CVC4::String t = n2[index1].getConst<String>();
- std::size_t ret = r == 0 ? s.find(t) : s.rfind(t);
+ Node t = n2[index1];
+ std::size_t ret = r == 0 ? Word::find(s, t) : Word::rfind(s, t);
if (ret == std::string::npos)
{
if (n1.size() == 1)
@@ -545,7 +537,7 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
// This is used to partially strip off the endpoint
// e.g. str.contains( str.++( "abc", x ), str.++( "cd", y ) ) -->
// str.contains( str.++( "c", x ), str.++( "cd", y ) )
- overlap = r == 0 ? s.overlap(t) : t.overlap(s);
+ overlap = r == 0 ? Word::overlap(s, t) : Word::overlap(t, s);
}
else
{
@@ -553,19 +545,20 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
// if there is no overlap
// e.g. str.contains( str.++( str.substr( "c", i, j ), x), "a" )
// --> str.contains( x, "a" )
- removeComponent = ((r == 0 ? s.overlap(t) : t.overlap(s)) == 0);
+ removeComponent =
+ ((r == 0 ? Word::overlap(s, t) : Word::overlap(t, s)) == 0);
}
}
else if (sss.empty()) // only if not substr
{
- Assert(ret < s.size());
+ Assert(ret < slen);
// can strip off up to the find position, e.g.
// str.contains( str.++( "abc", x ), str.++( "b", y ) ) -->
// str.contains( str.++( "bc", x ), str.++( "b", y ) ),
// and
// str.contains( str.++( x, "abbd" ), str.++( y, "b" ) ) -->
// str.contains( str.++( x, "abb" ), str.++( y, "b" ) )
- overlap = s.size() - ret;
+ overlap = slen - ret;
}
}
else
@@ -573,7 +566,7 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
// inconclusive
}
// process the overlap
- if (overlap < s.size())
+ if (overlap < slen)
{
changed = true;
if (overlap == 0)
@@ -586,13 +579,13 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
// component
if (r == 0)
{
- nb.push_back(nm->mkConst(s.prefix(s.size() - overlap)));
- n1[index0] = nm->mkConst(s.suffix(overlap));
+ nb.push_back(Word::prefix(s, slen - overlap));
+ n1[index0] = Word::suffix(s, overlap);
}
else
{
- ne.push_back(nm->mkConst(s.suffix(s.size() - overlap)));
- n1[index0] = nm->mkConst(s.prefix(overlap));
+ ne.push_back(Word::suffix(s, slen - overlap));
+ n1[index0] = Word::prefix(s, overlap);
}
}
}
@@ -601,8 +594,8 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
{
if (n2[index1].isConst())
{
+ Assert(n2[index1].getType().isString());
CVC4::String t = n2[index1].getConst<String>();
-
if (n1.size() == 1)
{
// if n1.size()==1, then if n2[index1] is not a number, we can drop
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback