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.cpp17
1 files changed, 16 insertions, 1 deletions
diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index 085078dea..e9ab2652e 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -283,7 +283,7 @@ std::size_t Word::roverlap(TNode x, TNode y)
return 0;
}
-Node Word::splitConstant(Node x, Node y, size_t& index, bool isRev)
+Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
{
Assert(x.isConst() && y.isConst());
size_t lenA = getLength(x);
@@ -308,6 +308,21 @@ Node Word::splitConstant(Node x, Node y, size_t& index, bool isRev)
return Node::null();
}
+Node Word::reverse(TNode x)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Kind k = x.getKind();
+ if (k == CONST_STRING)
+ {
+ String sx = x.getConst<String>();
+ std::vector<unsigned> nvec = sx.getVec();
+ std::reverse(nvec.begin(), nvec.end());
+ return nm->mkConst(String(nvec));
+ }
+ Unimplemented();
+ return Node::null();
+}
+
} // namespace strings
} // namespace theory
} // namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback