From 1fee693c6569bf68c598610be30cbc3f8cbaa3f2 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 10 Oct 2018 01:28:14 -0700
Subject: Add length-based rewrites for (str.substr _ _ _)

This commit adds two rewrites for `(str.substr _ _ _)` that use
length-based reasoning:

- `(str.substr (str.substr x a b) c d) ---> ""` if `c >= b`
- `(str.substr s x x) ---> ""` if `(str.len s) <= 1`
---
 src/theory/strings/theory_strings_rewriter.cpp | 35 ++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

(limited to 'src')

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index b2778298a..00a711a31 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1610,6 +1610,33 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
     return returnRewrite(node, ret, "ss-len-non-pos");
   }
 
+  if (node[0].getKind() == STRING_SUBSTR)
+  {
+    // (str.substr (str.substr x a b) c d) ---> "" if c >= b
+    //
+    // Note that this rewrite can be generalized to:
+    //
+    // (str.substr x a b) ---> "" if a >= (str.len x)
+    //
+    // This can be done when we generalize our entailment methods to
+    // accept an optional context. Then we could conjecture that
+    // (str.substr x a b) rewrites to "" and do a case analysis:
+    //
+    // - a < 0 or b < 0 (the result is trivially empty in these cases)
+    // - a >= (str.len x) assuming that { a >= 0, b >= 0 }
+    //
+    // For example, for (str.substr (str.substr x a a) a a), we could
+    // then deduce that under those assumptions, "a" is an
+    // over-approximation of the length of (str.substr x a a), which
+    // then allows us to reason that the result of the whole term must
+    // be empty.
+    if (checkEntailArith(node[1], node[0][2]))
+    {
+      Node ret = nm->mkConst(::CVC4::String(""));
+      return returnRewrite(node, ret, "ss-start-geq-len");
+    }
+  }
+
   std::vector<Node> n1;
   getConcat(node[0], n1);
 
@@ -1673,6 +1700,14 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
         Node ret = nm->mkConst(::CVC4::String(""));
         return returnRewrite(node, ret, "ss-start-entails-zero-len");
       }
+
+      // (str.substr s x x) ---> "" if (str.len s) <= 1
+      Node one = nm->mkConst(CVC4::Rational(1));
+      if (node[1] == node[2] && checkEntailArith(one, tot_len))
+      {
+        Node ret = nm->mkConst(::CVC4::String(""));
+        return returnRewrite(node, ret, "ss-len-one-z-z");
+      }
     }
     if (!curr.isNull())
     {
-- 
cgit v1.2.3