Better normalization of string concatenation (#1719)

2 files changed, 95 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 0777d696f..1c885434c 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/strings/theory_strings_rewriter.h"
 
 #include <stdint.h>
+#include <algorithm>
 
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
@@ -348,6 +349,32 @@ Node TheoryStringsRewriter::rewriteConcat(Node node)
   if( !preNode.isNull() && ( preNode.getKind()!=kind::CONST_STRING || !preNode.getConst<String>().isEmptyString() ) ){
     node_vec.push_back( preNode );
   }
+
+  // Sort adjacent operands in str.++ that all result in the same string or the
+  // empty string.
+  //
+  // E.g.: (str.++ ... (str.replace "A" x "") "A" (str.substr "A" 0 z) ...) -->
+  // (str.++ ... [sort those 3 arguments] ... )
+  size_t lastIdx = 0;
+  Node lastX;
+  for (size_t i = 0; i < node_vec.size(); i++)
+  {
+    Node s = getStringOrEmpty(node_vec[i]);
+    bool nextX = false;
+    if (s != lastX)
+    {
+      nextX = true;
+    }
+
+    if (nextX)
+    {
+      std::sort(node_vec.begin() + lastIdx, node_vec.begin() + i);
+      lastX = s;
+      lastIdx = i;
+    }
+  }
+  std::sort(node_vec.begin() + lastIdx, node_vec.end());
+
   retNode = mkConcat( kind::STRING_CONCAT, node_vec );
   Trace("strings-prerewrite") << "Strings::rewriteConcat end " << retNode
                               << std::endl;
@@ -3280,6 +3307,57 @@ Node TheoryStringsRewriter::mkSubstrChain(Node base,
   return base;
 }
 
+Node TheoryStringsRewriter::getStringOrEmpty(Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node res;
+  while (res.isNull())
+  {
+    switch (n.getKind())
+    {
+      case kind::STRING_STRREPL:
+      {
+        Node empty = nm->mkConst(::CVC4::String(""));
+        if (n[0] == empty)
+        {
+          // (str.replace "" x y) --> y
+          n = n[2];
+          break;
+        }
+
+        Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0]));
+        if (strlen == nm->mkConst(Rational(1)) && n[2] == empty)
+        {
+          // (str.replace "A" x "") --> "A"
+          res = n[0];
+          break;
+        }
+
+        res = n;
+        break;
+      }
+      case kind::STRING_SUBSTR:
+      {
+        Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0]));
+        if (strlen == nm->mkConst(Rational(1)))
+        {
+          // (str.substr "A" x y) --> "A"
+          res = n[0];
+          break;
+        }
+        res = n;
+          break;
+      }
+      default:
+      {
+        res = n;
+        break;
+      }
+    }
+  }
+  return res;
+}
+
 Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c)
 {
   Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 0e4cb594a..9671fa815 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -437,6 +437,23 @@ private:
   static Node mkSubstrChain(Node base,
                             const std::vector<Node>& ss,
                             const std::vector<Node>& ls);
+
+  /**
+   * Overapproximates the possible values of node n. This overapproximation
+   * assumes that n can return a value x or the empty string and tries to find
+   * the simplest x such that this holds. In the general case, x is the same as
+   * the input n. This overapproximation can be used to sort terms with the
+   * same possible values in string concatenation for example.
+   *
+   * Example:
+   *
+   * getStringOrEmpty( (str.replace "" x y) ) --> y because (str.replace "" x y)
+   * either returns y or ""
+   *
+   * getStringOrEmpty( (str.substr "ABC" x y) ) --> (str.substr "ABC" x y)
+   * because the function could not compute a simpler
+   */
+  static Node getStringOrEmpty(Node n);
 };/* class TheoryStringsRewriter */
 
 }/* CVC4::theory::strings namespace */