From 090d8bc3c31404140856e51d2cc5a5aa1335b3b3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 12 Jul 2020 17:37:03 -0700 Subject: Remove ExprSequence (#4724) Now that we can break the old API, we don't need an ExprSequence anymore. This commit removes ExprSequence and replaces all of its uses with Sequence. Note that I had to temporarily make sequence.h public because we currently include it in a "public" header because we still generate the code for Expr::mkConst(). --- src/theory/strings/word.cpp | 85 ++++++++++++++++++++++----------------------- 1 file changed, 41 insertions(+), 44 deletions(-) (limited to 'src/theory/strings/word.cpp') diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index fec567733..49221409e 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -32,9 +32,9 @@ Node Word::mkEmptyWord(TypeNode tn) } else if (tn.isSequence()) { - std::vector seq; + std::vector seq; return NodeManager::currentNM()->mkConst( - ExprSequence(tn.getSequenceElementType().toType(), seq)); + Sequence(tn.getSequenceElementType(), seq)); } Unimplemented(); return Node::null(); @@ -59,20 +59,17 @@ Node Word::mkWordFlatten(const std::vector& xs) } else if (k == CONST_SEQUENCE) { - std::vector seq; + std::vector seq; TypeNode tn = xs[0].getType(); for (TNode x : xs) { Assert(x.getType() == tn); - const Sequence& sx = x.getConst().getSequence(); + const Sequence& sx = x.getConst(); const std::vector& vecc = sx.getVec(); - for (const Node& c : vecc) - { - seq.push_back(c.toExpr()); - } + seq.insert(seq.end(), vecc.begin(), vecc.end()); } return NodeManager::currentNM()->mkConst( - ExprSequence(tn.getSequenceElementType().toType(), seq)); + Sequence(tn.getSequenceElementType(), seq)); } Unimplemented(); return Node::null(); @@ -87,7 +84,7 @@ size_t Word::getLength(TNode x) } else if (k == CONST_SEQUENCE) { - return x.getConst().getSequence().size(); + return x.getConst().size(); } Unimplemented() << "Word::getLength on " << x; return 0; @@ -113,12 +110,12 @@ std::vector Word::getChars(TNode x) } else if (k == CONST_SEQUENCE) { - Type t = x.getConst().getType(); - const Sequence& sx = x.getConst().getSequence(); + TypeNode t = x.getConst().getType(); + const Sequence& sx = x.getConst(); const std::vector& vec = sx.getVec(); for (const Node& v : vec) { - ret.push_back(nm->mkConst(ExprSequence(t, {v.toExpr()}))); + ret.push_back(nm->mkConst(Sequence(t, {v}))); } return ret; } @@ -141,8 +138,8 @@ bool Word::strncmp(TNode x, TNode y, std::size_t n) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.strncmp(sy, n); } Unimplemented(); @@ -162,8 +159,8 @@ bool Word::rstrncmp(TNode x, TNode y, std::size_t n) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.rstrncmp(sy, n); } Unimplemented(); @@ -183,8 +180,8 @@ std::size_t Word::find(TNode x, TNode y, std::size_t start) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.find(sy, start); } Unimplemented(); @@ -204,8 +201,8 @@ std::size_t Word::rfind(TNode x, TNode y, std::size_t start) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.rfind(sy, start); } Unimplemented(); @@ -225,8 +222,8 @@ bool Word::hasPrefix(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.hasPrefix(sy); } Unimplemented(); @@ -246,8 +243,8 @@ bool Word::hasSuffix(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.hasSuffix(sy); } Unimplemented(); @@ -271,11 +268,11 @@ Node Word::replace(TNode x, TNode y, TNode t) { Assert(y.getKind() == CONST_SEQUENCE); Assert(t.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); - const Sequence& st = t.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); + const Sequence& st = t.getConst(); Sequence res = sx.replace(sy, st); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); @@ -291,9 +288,9 @@ Node Word::substr(TNode x, std::size_t i) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst().getSequence(); + const Sequence& sx = x.getConst(); Sequence res = sx.substr(i); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); @@ -309,9 +306,9 @@ Node Word::substr(TNode x, std::size_t i, std::size_t j) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst().getSequence(); + const Sequence& sx = x.getConst(); Sequence res = sx.substr(i, j); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); @@ -330,9 +327,9 @@ Node Word::suffix(TNode x, std::size_t i) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst().getSequence(); + const Sequence& sx = x.getConst(); Sequence res = sx.suffix(i); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); @@ -351,8 +348,8 @@ bool Word::noOverlapWith(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.noOverlapWith(sy); } Unimplemented(); @@ -372,8 +369,8 @@ std::size_t Word::overlap(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.overlap(sy); } Unimplemented(); @@ -393,8 +390,8 @@ std::size_t Word::roverlap(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst().getSequence(); - const Sequence& sy = y.getConst().getSequence(); + const Sequence& sx = x.getConst(); + const Sequence& sy = y.getConst(); return sx.roverlap(sy); } Unimplemented(); @@ -410,7 +407,7 @@ bool Word::isRepeated(TNode x) } else if (k == CONST_SEQUENCE) { - return x.getConst().getSequence().isRepeated(); + return x.getConst().isRepeated(); } Unimplemented(); return false; @@ -454,12 +451,12 @@ Node Word::reverse(TNode x) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst().getSequence(); + const Sequence& sx = x.getConst(); const std::vector& vecc = sx.getVec(); std::vector vecr(vecc.begin(), vecc.end()); std::reverse(vecr.begin(), vecr.end()); Sequence res(sx.getType(), vecr); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); -- cgit v1.2.3