Merge pull request #9 from 4tXJ7f/lengthPreserve

2 files changed, 108 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 1c7d3e53d..9c1857800 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -19,10 +19,13 @@
 #include <stdint.h>
 #include <algorithm>
 
+#include "expr/node_builder.h"
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/theory.h"
+#include "util/integer.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace CVC4;
@@ -2016,6 +2019,31 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
       return returnRewrite(node, negone, "idof-nctn");
     }
   }
+  else
+  {
+    Node new_len = node[2];
+    std::vector<Node> nr;
+    if (stripSymbolicLength(children0, nr, 1, new_len))
+    {
+      // Normalize the string before the start index.
+      //
+      // For example:
+      // str.indexof(str.++("ABCD", x), y, 3) --->
+      // str.indexof(str.++("AAAD", x), y, 3)
+      Node nodeNr = mkConcat(kind::STRING_CONCAT, nr);
+      Node normNr = lengthPreserveRewrite(nodeNr);
+      if (normNr != nodeNr)
+      {
+        std::vector<Node> normNrChildren;
+        getConcat(normNr, normNrChildren);
+        std::vector<Node> children(normNrChildren);
+        children.insert(children.end(), children0.begin(), children0.end());
+        Node nn = mkConcat(kind::STRING_CONCAT, children);
+        Node res = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
+        return returnRewrite(node, res, "idof-norm-prefix");
+      }
+    }
+  }
 
   if (node[2].isConst() && node[2].getConst<Rational>().sgn()==0)
   {
@@ -3036,6 +3064,70 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
   return changed;
 }
 
+Node TheoryStringsRewriter::canonicalStrForSymbolicLength(Node len)
+{
+  NodeManager* nm = NodeManager::currentNM();
+
+  Node res;
+  if (len.getKind() == kind::CONST_RATIONAL)
+  {
+    // c -> "A" repeated c times
+    Rational ratLen = len.getConst<Rational>();
+    Assert(ratLen.getDenominator() == 1);
+    Integer intLen = ratLen.getNumerator();
+    res = nm->mkConst(String(std::string(intLen.getUnsignedInt(), 'A')));
+  }
+  else if (len.getKind() == kind::PLUS)
+  {
+    // x + y -> norm(x) + norm(y)
+    NodeBuilder<> concatBuilder(kind::STRING_CONCAT);
+    for (const auto& n : len)
+    {
+      Node sn = canonicalStrForSymbolicLength(n);
+      if (sn.isNull())
+      {
+        return Node::null();
+      }
+      std::vector<Node> snChildren;
+      getConcat(sn, snChildren);
+      concatBuilder.append(snChildren);
+    }
+    res = concatBuilder.constructNode();
+  }
+  else if (len.getKind() == kind::MULT && len.getNumChildren() == 2
+           && len[0].isConst())
+  {
+    // c * x -> norm(x) repeated c times
+    Rational ratReps = len[0].getConst<Rational>();
+    Assert(ratReps.getDenominator() == 1);
+    Integer intReps = ratReps.getNumerator();
+
+    Node nRep = canonicalStrForSymbolicLength(len[1]);
+    std::vector<Node> nRepChildren;
+    getConcat(nRep, nRepChildren);
+    NodeBuilder<> concatBuilder(kind::STRING_CONCAT);
+    for (size_t i = 0, reps = intReps.getUnsignedInt(); i < reps; i++)
+    {
+      concatBuilder.append(nRepChildren);
+    }
+    res = concatBuilder.constructNode();
+  }
+  else if (len.getKind() == kind::STRING_LENGTH)
+  {
+    // len(x) -> x
+    res = len[0];
+  }
+  return res;
+}
+
+Node TheoryStringsRewriter::lengthPreserveRewrite(Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node len = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n));
+  Node res = canonicalStrForSymbolicLength(len);
+  return res.isNull() ? n : res;
+}
+
 bool TheoryStringsRewriter::checkEntailNonEmpty(Node a)
 {
   Node len = NodeManager::currentNM()->mkNode(STRING_LENGTH, a);
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 4c78a1945..59842dd53 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -377,6 +377,22 @@ class TheoryStringsRewriter {
                                      std::vector<Node>& nb,
                                      std::vector<Node>& ne,
                                      int dir = 0);
+
+  /**
+   * Given a symbolic length n, returns the canonical string for that length.
+   * For example if n is constant, this function returns a string consisting of
+   * "A" repeated n times. Returns the null node if no such string exists.
+   */
+  static Node canonicalStrForSymbolicLength(Node n);
+
+  /** length preserving rewrite
+   *
+   * Given input n, this returns a string n' whose length is equivalent to n.
+   * We apply certain normalizations to n', such as replacing all constants
+   * that are not relevant to length by "A".
+   */
+  static Node lengthPreserveRewrite(Node n);
+
   /** entail non-empty
    *
    * Checks whether string a is entailed to be non-empty. Is equivalent to