diff options
Diffstat (limited to 'src/theory/strings/word.cpp')
-rw-r--r-- | src/theory/strings/word.cpp | 85 |
1 files changed, 41 insertions, 44 deletions
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<Expr> seq; + std::vector<Node> 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<Node>& xs) } else if (k == CONST_SEQUENCE) { - std::vector<Expr> seq; + std::vector<Node> seq; TypeNode tn = xs[0].getType(); for (TNode x : xs) { Assert(x.getType() == tn); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); const std::vector<Node>& 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<ExprSequence>().getSequence().size(); + return x.getConst<Sequence>().size(); } Unimplemented() << "Word::getLength on " << x; return 0; @@ -113,12 +110,12 @@ std::vector<Node> Word::getChars(TNode x) } else if (k == CONST_SEQUENCE) { - Type t = x.getConst<ExprSequence>().getType(); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + TypeNode t = x.getConst<Sequence>().getType(); + const Sequence& sx = x.getConst<Sequence>(); const std::vector<Node>& 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); - const Sequence& st = t.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); + const Sequence& st = t.getConst<Sequence>(); 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<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); 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<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); 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<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); 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<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.roverlap(sy); } Unimplemented(); @@ -410,7 +407,7 @@ bool Word::isRepeated(TNode x) } else if (k == CONST_SEQUENCE) { - return x.getConst<ExprSequence>().getSequence().isRepeated(); + return x.getConst<Sequence>().isRepeated(); } Unimplemented(); return false; @@ -454,12 +451,12 @@ Node Word::reverse(TNode x) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); const std::vector<Node>& vecc = sx.getVec(); std::vector<Node> 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(); |