summaryrefslogtreecommitdiff
path: root/src/theory/strings/word.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/word.cpp')
-rw-r--r--src/theory/strings/word.cpp23
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback