Avoid non-terminating check with assumptions in strings rewriter (#7503)

These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression.

Instead, these rewrites are now moved to the extended rewriter.

7 files changed, 73 insertions, 52 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index f5883c265..3d20f66b3 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -22,7 +22,9 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
+#include "theory/strings/arith_entail.h"
 #include "theory/strings/sequences_rewriter.h"
+#include "theory/strings/word.h"
 #include "theory/theory.h"
 
 using namespace cvc5::kind;
@@ -47,6 +49,7 @@ ExtendedRewriter::ExtendedRewriter(Rewriter& rew, bool aggr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
 }
 
 void ExtendedRewriter::setCache(Node n, Node ret) const
@@ -1702,19 +1705,50 @@ bool ExtendedRewriter::inferSubstitution(Node n,
   return false;
 }
 
-Node ExtendedRewriter::extendedRewriteStrings(Node ret) const
+Node ExtendedRewriter::extendedRewriteStrings(Node node) const
 {
-  Node new_ret;
   Trace("q-ext-rewrite-debug")
-      << "Extended rewrite strings : " << ret << std::endl;
+      << "Extended rewrite strings : " << node << std::endl;
 
-  if (ret.getKind() == EQUAL)
+  Kind k = node.getKind();
+  if (k == EQUAL)
   {
     strings::SequencesRewriter sr(&d_rew, nullptr);
-    new_ret = sr.rewriteEqualityExt(ret);
+    return sr.rewriteEqualityExt(node);
   }
+  else if (k == STRING_SUBSTR)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    Node tot_len = d_rew.rewrite(nm->mkNode(STRING_LENGTH, node[0]));
+    strings::ArithEntail aent(&d_rew);
+    // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
+    Node n1_lt_tot_len = d_rew.rewrite(nm->mkNode(LT, node[1], tot_len));
+    if (aent.checkWithAssumption(n1_lt_tot_len, d_zero, node[2], false))
+    {
+      Node ret = strings::Word::mkEmptyWord(node.getType());
+      debugExtendedRewrite(node, ret, "SS_START_ENTAILS_ZERO_LEN");
+      return ret;
+    }
 
-  return new_ret;
+    // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
+    Node non_zero_len = d_rew.rewrite(nm->mkNode(LT, d_zero, node[2]));
+    if (aent.checkWithAssumption(non_zero_len, node[1], tot_len, false))
+    {
+      Node ret = strings::Word::mkEmptyWord(node.getType());
+      debugExtendedRewrite(node, ret, "SS_NON_ZERO_LEN_ENTAILS_OOB");
+      return ret;
+    }
+    // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
+    Node geq_zero_start = d_rew.rewrite(nm->mkNode(GEQ, node[1], d_zero));
+    if (aent.checkWithAssumption(geq_zero_start, d_zero, tot_len, false))
+    {
+      Node ret = strings::Word::mkEmptyWord(node.getType());
+      debugExtendedRewrite(node, ret, "SS_GEQ_ZERO_START_ENTAILS_EMP_S");
+      return ret;
+    }
+  }
+
+  return Node::null();
 }
 
 void ExtendedRewriter::debugExtendedRewrite(Node n,
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index b4dcab041..1b9d0dae4 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -259,9 +259,10 @@ class ExtendedRewriter
    * may be applied as a preprocessing step.
    */
   bool d_aggr;
-  /** true/false nodes */
+  /** Common constant nodes */
   Node d_true;
   Node d_false;
+  Node d_zero;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h
index 295afb8c9..6529a81d1 100644
--- a/src/theory/strings/arith_entail.h
+++ b/src/theory/strings/arith_entail.h
@@ -96,6 +96,10 @@ class ArithEntail
    * checkWithAssumption(x + (str.len y) = 0, 0, x, false) = true
    *
    * Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
+   *
+   * Since this method rewrites on rewriting and may introduce new variables
+   * (slack variables for inequalities), it should *not* be called from the
+   * main rewriter of strings, or non-termination can occur.
    */
   bool checkWithAssumption(Node assumption,
                            Node a,
@@ -114,6 +118,10 @@ class ArithEntail
    * checkWithAssumptions([x + (str.len y) = 0], 0, x, false) = true
    *
    * Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
+   *
+   * Since this method rewrites on rewriting and may introduce new variables
+   * (slack variables for inequalities), it should *not* be called from the
+   * main rewriter of strings, or non-termination can occur.
    */
   bool checkWithAssumptions(std::vector<Node> assumptions,
                             Node a,
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 9887e7ef0..783e258fa 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1813,6 +1813,13 @@ Node SequencesRewriter::rewriteSubstr(Node node)
     }
   }
 
+  // (str.substr s x x) ---> "" if (str.len s) <= 1
+  if (node[1] == node[2] && d_stringsEntail.checkLengthOne(node[0]))
+  {
+    Node ret = Word::mkEmptyWord(node.getType());
+    return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
+  }
+
   // symbolic length analysis
   for (unsigned r = 0; r < 2; r++)
   {
@@ -1847,44 +1854,6 @@ Node SequencesRewriter::rewriteSubstr(Node node)
               d_arithEntail.rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt));
         }
       }
-
-      // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
-      Node n1_lt_tot_len =
-          d_arithEntail.rewrite(nm->mkNode(kind::LT, node[1], tot_len));
-      if (d_arithEntail.checkWithAssumption(
-              n1_lt_tot_len, zero, node[2], false))
-      {
-        Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, Rewrite::SS_START_ENTAILS_ZERO_LEN);
-      }
-
-      // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
-      Node non_zero_len =
-          d_arithEntail.rewrite(nm->mkNode(kind::LT, zero, node[2]));
-      if (d_arithEntail.checkWithAssumption(
-              non_zero_len, node[1], tot_len, false))
-      {
-        Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB);
-      }
-
-      // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
-      Node geq_zero_start =
-          d_arithEntail.rewrite(nm->mkNode(kind::GEQ, node[1], zero));
-      if (d_arithEntail.checkWithAssumption(
-              geq_zero_start, zero, tot_len, false))
-      {
-        Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(
-            node, ret, Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S);
-      }
-
-      // (str.substr s x x) ---> "" if (str.len s) <= 1
-      if (node[1] == node[2] && d_stringsEntail.checkLengthOne(node[0]))
-      {
-        Node ret = Word::mkEmptyWord(node.getType());
-        return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
-      }
     }
     if (!curr.isNull())
     {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cb535a469..5e64cfcbc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2287,6 +2287,7 @@ set(regress_1_tests
   regress1/strings/nf-ff-contains-abs.smt2
   regress1/strings/no-lazy-pp-quant.smt2
   regress1/strings/non_termination_regular_expression4.smt2
+  regress1/strings/non-terminating-rewrite-aent.smt2
   regress1/strings/norn-13.smt2
   regress1/strings/norn-360.smt2
   regress1/strings/norn-ab.smt2
diff --git a/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2 b/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2
new file mode 100644
index 000000000..211209255
--- /dev/null
+++ b/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(assert 
+(let ((_let_1 (str.len a))) (let ((_let_2 (str.len b))) (let ((_let_3 (+ _let_1 (* (- 1) _let_2)))) (let ((_let_4 (ite (>= _let_3 1) (str.substr a 0 _let_3) (str.substr b 0 (+ (* (- 1) _let_1) _let_2))))) (let ((_let_5 (str.len _let_4))) (let ((_let_6 (str.len c))) (let ((_let_7 (+ _let_6 (* (- 1) _let_5)))) (let ((_let_8 (ite (>= _let_7 0) (str.substr c _let_5 _let_7) (str.substr _let_4 _let_6 (+ (* (- 1) _let_6) _let_5))))) (let ((_let_9 (str.len _let_8))) (let ((_let_10 (ite (>= _let_1 _let_9) (str.substr a _let_9 (- _let_1 _let_9)) (str.substr _let_8 _let_1 (- _let_9 _let_1))))) (and (= _let_8 (str.++ a _let_10)) (not (= "" _let_10)) (>= (str.len _let_10) 1))))))))))))
+)
+(check-sat)
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index 32122e619..bcac315a7 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -248,8 +248,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
       a,
       d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))),
       x);
-  res = sr.rewriteSubstr(n);
-  ASSERT_EQ(res, empty);
+  sameNormalForm(n, empty);
 
   // (str.substr "A" (+ x (str.len s2)) x) -> ""
   n = d_nodeManager->mkNode(
@@ -258,8 +257,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
       d_nodeManager->mkNode(
           kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)),
       x);
-  res = sr.rewriteSubstr(n);
-  ASSERT_EQ(res, empty);
+  sameNormalForm(n, empty);
 
   // (str.substr "A" x y) -> (str.substr "A" x y)
   n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, y);
@@ -271,14 +269,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
                             abcd,
                             d_nodeManager->mkNode(kind::PLUS, x, three),
                             x);
-  res = sr.rewriteSubstr(n);
-  ASSERT_EQ(res, empty);
+  sameNormalForm(n, empty);
 
   // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
   n = d_nodeManager->mkNode(
       kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x);
   res = sr.rewriteSubstr(n);
-  ASSERT_EQ(res, n);
+  sameNormalForm(res, n);
 
   // (str.substr (str.substr s x x) x x) -> ""
   n = d_nodeManager->mkNode(kind::STRING_SUBSTR,