From 3f3a0445fe772360d8a2da3069a5f082c031d7f8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Apr 2020 02:34:33 -0500
Subject: Convert more cases of strings to words (#4206)

---
 src/theory/strings/word.cpp | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'src/theory/strings/word.cpp')

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
-- 
cgit v1.2.3