Add str.code support in old string rewriter

2 files changed, 29 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings_rewriter_old.cpp b/src/theory/strings/theory_strings_rewriter_old.cpp
index 4cc297364..40496b941 100644
--- a/src/theory/strings/theory_strings_rewriter_old.cpp
+++ b/src/theory/strings/theory_strings_rewriter_old.cpp
@@ -1211,6 +1211,10 @@ RewriteResponse TheoryStringsRewriterOld::postRewrite(TNode node) {
   } else if(node.getKind() == kind::STRING_IN_REGEXP) {
     retNode = rewriteMembership(node);
   }
+  else if (node.getKind() == STRING_CODE)
+  {
+    retNode = rewriteStringCode(node);
+  }
 
   Trace("strings-postrewrite") << "Strings::postRewrite returning " << retNode << std::endl;
   if( orig!=retNode ){
@@ -1395,6 +1399,29 @@ RewriteResponse TheoryStringsRewriterOld::preRewrite(TNode node) {
   return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
 
+Node TheoryStringsRewriterOld::rewriteStringCode(Node n)
+{
+  Assert(n.getKind() == kind::STRING_CODE);
+  if (n[0].isConst())
+  {
+    CVC4::String s = n[0].getConst<String>();
+    Node ret;
+    if (s.size() == 1)
+    {
+      std::vector<unsigned> vec = s.getVec();
+      Assert(vec.size() == 1);
+      ret = NodeManager::currentNM()->mkConst(
+          Rational(CVC4::String::convertUnsignedIntToCode(vec[0])));
+    }
+    else
+    {
+      ret = NodeManager::currentNM()->mkConst(Rational(-1));
+    }
+    return ret;
+  }
+
+  return n;
+}
 
 Node TheoryStringsRewriterOld::rewriteContains( Node node ) {
   if( node[0] == node[1] ){
diff --git a/src/theory/strings/theory_strings_rewriter_old.h b/src/theory/strings/theory_strings_rewriter_old.h
index ca9d331f8..43e387e01 100644
--- a/src/theory/strings/theory_strings_rewriter_old.h
+++ b/src/theory/strings/theory_strings_rewriter_old.h
@@ -54,6 +54,8 @@ public:
   static inline void init() {}
   static inline void shutdown() {}
 
+  static Node rewriteStringCode(Node node);
+
   static Node rewriteContains( Node n );
   static Node rewriteIndexof( Node n );
   static Node rewriteReplace( Node n );