Convert more cases of strings to words (#4206)

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