diff options
Diffstat (limited to 'src/theory/strings/word.cpp')
-rw-r--r-- | src/theory/strings/word.cpp | 35 |
1 files changed, 18 insertions, 17 deletions
diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index 484b0df2d..35b315e35 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -27,7 +27,8 @@ Node Word::mkEmptyWord(TypeNode tn) { if (tn.isString()) { - return mkEmptyWord(CONST_STRING); + std::vector<unsigned> vec; + return NodeManager::currentNM()->mkConst(String(vec)); } else if (tn.isSequence()) { @@ -39,17 +40,6 @@ Node Word::mkEmptyWord(TypeNode tn) return Node::null(); } -Node Word::mkEmptyWord(Kind k) -{ - if (k == CONST_STRING) - { - std::vector<unsigned> vec; - return NodeManager::currentNM()->mkConst(String(vec)); - } - Unimplemented(); - return Node::null(); -} - Node Word::mkWordFlatten(const std::vector<Node>& xs) { Assert(!xs.empty()); @@ -81,7 +71,8 @@ Node Word::mkWordFlatten(const std::vector<Node>& xs) seq.push_back(c.toExpr()); } } - return NodeManager::currentNM()->mkConst(ExprSequence(tn.toType(), seq)); + return NodeManager::currentNM()->mkConst( + ExprSequence(tn.getSequenceElementType().toType(), seq)); } Unimplemented(); return Node::null(); @@ -98,17 +89,17 @@ size_t Word::getLength(TNode x) { return x.getConst<ExprSequence>().getSequence().size(); } - Unimplemented(); + Unimplemented() << "Word::getLength on " << x; return 0; } std::vector<Node> Word::getChars(TNode x) { Kind k = x.getKind(); + std::vector<Node> ret; + NodeManager* nm = NodeManager::currentNM(); if (k == CONST_STRING) { - std::vector<Node> ret; - NodeManager* nm = NodeManager::currentNM(); std::vector<unsigned> ccVec; const std::vector<unsigned>& cvec = x.getConst<String>().getVec(); for (unsigned chVal : cvec) @@ -120,8 +111,18 @@ std::vector<Node> Word::getChars(TNode x) } return ret; } + else if (k == CONST_SEQUENCE) + { + Type t = x.getConst<ExprSequence>().getType(); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const std::vector<Node>& vec = sx.getVec(); + for (const Node& v : vec) + { + ret.push_back(nm->mkConst(ExprSequence(t, {v.toExpr()}))); + } + return ret; + } Unimplemented(); - std::vector<Node> ret; return ret; } |