Convert more uses of string-specific functions (#4158)

Towards theory of sequences.

1 files changed, 23 insertions, 0 deletions

diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index 0faeffd99..b42cf3160 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -76,6 +76,29 @@ size_t Word::getLength(TNode x)
   return 0;
 }
 
+std::vector<Node> Word::getChars(TNode x)
+{
+  Kind k = x.getKind();
+  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)
+    {
+      ccVec.clear();
+      ccVec.push_back(chVal);
+      Node ch = nm->mkConst(String(ccVec));
+      ret.push_back(ch);
+    }
+    return ret;
+  }
+  Unimplemented();
+  std::vector<Node> ret;
+  return ret;
+}
+
 bool Word::isEmpty(TNode x) { return getLength(x) == 0; }
 
 bool Word::strncmp(TNode x, TNode y, std::size_t n)