From 1840fb506e8ed97692654d333b67f7e3dcf1bb9e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 18 Jul 2019 11:35:18 -0400
Subject: [PATCH] Basic rewrites for tolower/toupper (#3095)

---
 .../strings/theory_strings_rewriter.cpp       | 27 ++++++++++++++++++-
 test/regress/CMakeLists.txt                   |  1 +
 .../regress/regress0/strings/tolower-rrs.smt2 | 15 +++++++++++
 3 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/strings/tolower-rrs.smt2

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index a84f2b212..6a8cf3e98 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2982,6 +2982,7 @@ Node TheoryStringsRewriter::rewriteStrConvert(Node node)
 {
   Kind nk = node.getKind();
   Assert(nk == STRING_TOLOWER || nk == STRING_TOUPPER);
+  NodeManager* nm = NodeManager::currentNM();
   if (node[0].isConst())
   {
     std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
@@ -3008,9 +3009,33 @@ Node TheoryStringsRewriter::rewriteStrConvert(Node node)
       newChar = CVC4::String::convertCodeToUnsignedInt(newChar);
       nvec[i] = newChar;
     }
-    Node retNode = NodeManager::currentNM()->mkConst(String(nvec));
+    Node retNode = nm->mkConst(String(nvec));
     return returnRewrite(node, retNode, "str-conv-const");
   }
+  else if (node[0].getKind() == STRING_CONCAT)
+  {
+    NodeBuilder<> concatBuilder(STRING_CONCAT);
+    for (const Node& nc : node[0])
+    {
+      concatBuilder << nm->mkNode(nk, nc);
+    }
+    // tolower( x1 ++ x2 ) --> tolower( x1 ) ++ tolower( x2 )
+    Node retNode = concatBuilder.constructNode();
+    return returnRewrite(node, retNode, "str-conv-minscope-concat");
+  }
+  else if (node[0].getKind() == STRING_TOLOWER
+           || node[0].getKind() == STRING_TOUPPER)
+  {
+    // tolower( tolower( x ) ) --> tolower( x )
+    // tolower( toupper( x ) ) --> tolower( x )
+    Node retNode = nm->mkNode(nk, node[0][0]);
+    return returnRewrite(node, retNode, "str-conv-idem");
+  }
+  else if (node[0].getKind() == STRING_ITOS)
+  {
+    // tolower( str.from.int( x ) ) --> str.from.int( x )
+    return returnRewrite(node, node[0], "str-conv-itos");
+  }
   return node;
 }
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index eb78c1611..aae919a2f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -865,6 +865,7 @@ set(regress_0_tests
   regress0/strings/strings-native-simple.cvc
   regress0/strings/strip-endpoint-itos.smt2
   regress0/strings/substr-rewrites.smt2
+  regress0/strings/tolower-rrs.smt2
   regress0/strings/tolower-simple.smt2
   regress0/strings/type001.smt2
   regress0/strings/unsound-0908.smt2
diff --git a/test/regress/regress0/strings/tolower-rrs.smt2 b/test/regress/regress0/strings/tolower-rrs.smt2
new file mode 100644
index 000000000..7b8b393cd
--- /dev/null
+++ b/test/regress/regress0/strings/tolower-rrs.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () Int)
+
+(assert (or 
+(not (= (str.tolower (str.toupper (str.tolower x))) (str.tolower x)))
+(not (= (str.tolower (str.++ x "A")) (str.++ (str.tolower x) "a")))
+(not (= (str.tolower (int.to.str y)) (int.to.str y)))
+))
+
+(check-sat)
-- 
2.30.2