Basic rewrites for tolower/toupper (#3095)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index a84f2b21228cb564dd6f3fcb5e3b719aab04700b..6a8cf3e985d10441e076b6a85def4683e79a134d 100644 (file)
--- 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 eb78c1611b7846c7e846797a8294aa8bd0703df5..aae919a2f5b5a5e638bc397892228623f321c2c2 100644 (file)
--- 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 (file)
index 0000000..7b8b393
--- /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)