{
Assert(cn.isConst());
Assert(Word::getLength(cn) == 1);
- unsigned hchar = cn.getConst<String>().front();
// The operands of the concat on each side of the equality without
// constant strings
std::vector<Node> trimmed[2];
- // Counts the number of `hchar`s on each side
- size_t numHChars[2] = {0, 0};
+ // Counts the number of `cn`s on each side
+ size_t numCns[2] = {0, 0};
for (size_t j = 0; j < 2; j++)
{
// Sort the operands of the concats on both sides of the equality
{
if (cc.isConst())
{
- // Count the number of `hchar`s in the string constant and make
- // sure that all chars are `hchar`s
- std::vector<unsigned> veccc = cc.getConst<String>().getVec();
- for (size_t k = 0, size = veccc.size(); k < size; k++)
+ // Count the number of `cn`s in the string constant and make
+ // sure that all chars are `cn`s
+ std::vector<Node> veccc = Word::getChars(cc);
+ for (const Node& cv : veccc)
{
- if (veccc[k] != hchar)
+ if (cv != cn)
{
// This conflict case should mostly should be taken care of by
// multiset reasoning in the strings rewriter, but we recognize
return returnRewrite(
node, new_ret, Rewrite::STR_EQ_CONST_NHOMOG);
}
- numHChars[j]++;
+ numCns[j]++;
}
}
else
}
}
- // We have to remove the same number of `hchar`s from both sides, so the
- // side with less `hchar`s determines how many we can remove
- size_t trimmedConst = std::min(numHChars[0], numHChars[1]);
+ // We have to remove the same number of `cn`s from both sides, so the
+ // side with less `cn`s determines how many we can remove
+ size_t trimmedConst = std::min(numCns[0], numCns[1]);
for (size_t j = 0; j < 2; j++)
{
- size_t diff = numHChars[j] - trimmedConst;
+ size_t diff = numCns[j] - trimmedConst;
if (diff != 0)
{
- // Add a constant string to the side with more `hchar`s to restore
- // the difference in number of `hchar`s
- std::vector<unsigned> vec(diff, hchar);
- trimmed[j].push_back(nm->mkConst(String(vec)));
+ // Add a constant string to the side with more `cn`s to restore
+ // the difference in number of `cn`s
+ std::vector<Node> vec(diff, cn);
+ trimmed[j].push_back(Word::mkWord(vec));
}
}
}
if (node[0].isConst())
{
- CVC4::String s = node[0].getConst<String>();
if (node[1].isConst())
{
Node ret = nm->mkConst(Word::find(node[0], node[1]) != std::string::npos);
}
else if (checkEntailLengthOne(t))
{
- const std::vector<unsigned>& vec = s.getVec();
-
+ std::vector<Node> vec = Word::getChars(node[0]);
+ Node emp = Word::mkEmptyWord(t.getType());
NodeBuilder<> nb(OR);
- nb << nm->mkConst(String("")).eqNode(t);
- for (unsigned c : vec)
+ nb << emp.eqNode(t);
+ for (const Node& c : vec)
{
- std::vector<unsigned> sv = {c};
- nb << nm->mkConst(String(sv)).eqNode(t);
+ nb << c.eqNode(t);
}
// str.contains("ABCabc", t) --->
return changed;
}
-Node SequencesRewriter::canonicalStrForSymbolicLength(Node len)
+Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
{
NodeManager* nm = NodeManager::currentNM();
Rational ratLen = len.getConst<Rational>();
Assert(ratLen.getDenominator() == 1);
Integer intLen = ratLen.getNumerator();
- res = nm->mkConst(String(std::string(intLen.getUnsignedInt(), 'A')));
+ uint32_t u = intLen.getUnsignedInt();
+ if (stype.isString())
+ {
+ res = nm->mkConst(String(std::string(u, 'A')));
+ }
+ else
+ {
+ Unimplemented() << "canonicalStrForSymbolicLength for non-string";
+ }
}
else if (len.getKind() == kind::PLUS)
{
NodeBuilder<> concatBuilder(kind::STRING_CONCAT);
for (const auto& n : len)
{
- Node sn = canonicalStrForSymbolicLength(n);
+ Node sn = canonicalStrForSymbolicLength(n, stype);
if (sn.isNull())
{
return Node::null();
Assert(ratReps.getDenominator() == 1);
Integer intReps = ratReps.getNumerator();
- Node nRep = canonicalStrForSymbolicLength(len[1]);
+ Node nRep = canonicalStrForSymbolicLength(len[1], stype);
std::vector<Node> nRepChildren;
utils::getConcat(nRep, nRepChildren);
NodeBuilder<> concatBuilder(kind::STRING_CONCAT);
{
NodeManager* nm = NodeManager::currentNM();
Node len = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n));
- Node res = canonicalStrForSymbolicLength(len);
+ Node res = canonicalStrForSymbolicLength(len, n.getType());
return res.isNull() ? n : res;
}
bool SequencesRewriter::checkEntailMultisetSubset(Node a, Node b)
{
- NodeManager* nm = NodeManager::currentNM();
-
std::vector<Node> avec;
utils::getConcat(getMultisetApproximation(a), avec);
std::vector<Node> bvec;
{
Node cn = ncp.first;
Assert(cn.isConst());
- std::vector<unsigned> cc_vec;
- const std::vector<unsigned>& cvec = cn.getConst<String>().getVec();
- for (unsigned i = 0, size = cvec.size(); i < size; i++)
+ std::vector<Node> cnChars = Word::getChars(cn);
+ for (const Node& ch : cnChars)
{
- // make the character
- cc_vec.clear();
- cc_vec.insert(cc_vec.end(), cvec.begin() + i, cvec.begin() + i + 1);
- Node ch = nm->mkConst(String(cc_vec));
count_const[j][ch] += ncp.second;
if (std::find(chars.begin(), chars.end(), ch) == chars.end())
{
Node SequencesRewriter::checkEntailHomogeneousString(Node a)
{
- NodeManager* nm = NodeManager::currentNM();
-
std::vector<Node> avec;
utils::getConcat(getMultisetApproximation(a), avec);
bool cValid = false;
- unsigned c = 0;
+ Node c;
for (const Node& ac : avec)
{
if (ac.isConst())
{
- std::vector<unsigned> acv = ac.getConst<String>().getVec();
- for (unsigned cc : acv)
+ std::vector<Node> acv = Word::getChars(ac);
+ for (const Node& cc : acv)
{
if (!cValid)
{
if (!cValid)
{
- return nm->mkConst(String(""));
+ return Word::mkEmptyWord(a.getType());
}
- std::vector<unsigned> cv = {c};
- return nm->mkConst(String(cv));
+ return c;
}
Node SequencesRewriter::getMultisetApproximation(Node a)
#include "proof/proof_manager.h"
#include "smt/logic_exception.h"
#include "theory/strings/sequences_rewriter.h"
+#include "theory/strings/word.h"
using namespace CVC4;
using namespace CVC4::kind;
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
d_one = NodeManager::currentNM()->mkConst(Rational(1));
d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
- d_empty_str = NodeManager::currentNM()->mkConst(String(""));
}
StringsPreprocess::~StringsPreprocess(){
Node c3 = nm->mkNode(GT, m, d_zero);
Node cond = nm->mkNode(AND, c1, c2, c3);
- Node sk1 = n == d_zero ? d_empty_str
+ Node emp = Word::mkEmptyWord(t.getType());
+
+ Node sk1 = n == d_zero ? emp
: d_sc->mkSkolemCached(
s, n, SkolemCache::SK_PREFIX, "sspre");
Node sk2 = SequencesRewriter::checkEntailArith(t12, lt0)
- ? d_empty_str
+ ? emp
: d_sc->mkSkolemCached(
s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2));
Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m);
Node b1 = nm->mkNode(AND, b11, b12, b13, b14);
- Node b2 = skt.eqNode(d_empty_str);
+ Node b2 = skt.eqNode(emp);
Node lemma = nm->mkNode(ITE, cond, b1, b2);
// assert:
Node cc1 = skk.eqNode(negone);
// y = ""
- Node cond2 = y.eqNode(d_empty_str);
+ Node emp = Word::mkEmptyWord(x.getType());
+ Node cond2 = y.eqNode(emp);
// skk = n
Node cc2 = skk.eqNode(t[2]);
Node nonneg = nm->mkNode(GEQ, n, d_zero);
- lem = nm->mkNode(
- ITE, nonneg, nm->mkNode(AND, conc), itost.eqNode(d_empty_str));
+ Node emp = Word::mkEmptyWord(t.getType());
+ lem = nm->mkNode(ITE, nonneg, nm->mkNode(AND, conc), itost.eqNode(emp));
new_nodes.push_back(lem);
// assert:
// IF n>=0
Node lem = stoit.eqNode(d_neg_one);
conc1.push_back(lem);
- Node sEmpty = s.eqNode(d_empty_str);
+ Node emp = Word::mkEmptyWord(s.getType());
+ Node sEmpty = s.eqNode(emp);
Node k = nm->mkSkolem("k", nm->integerType());
Node kc1 = nm->mkNode(GEQ, k, d_zero);
Node kc2 = nm->mkNode(LT, k, lens);
// the index to begin searching in x for y after the i^th occurrence of y in
// x, and Us( i ) is the result of processing the remainder after processing
// the i^th occurrence of y in x.
- Node assert = nm->mkNode(
- ITE, y.eqNode(d_empty_str), rpaw.eqNode(x), nm->mkNode(AND, lem));
+ Node emp = Word::mkEmptyWord(t.getType());
+ Node assert =
+ nm->mkNode(ITE, y.eqNode(emp), rpaw.eqNode(x), nm->mkNode(AND, lem));
new_nodes.push_back(assert);
// Thus, replaceall( x, y, z ) = rpaw
projects / cvc5.git / commitdiff