Add reasoning for inequalities in str rewriter (#1713)

3 files changed, 101 insertions, 22 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 8f9d4c596..0777d696f 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1520,15 +1520,13 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
         }
       }
 
-      if (tot_len == nm->mkConst(Rational(1)))
+      // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
+      Node n1_lt_tot_len =
+          Rewriter::rewrite(nm->mkNode(kind::LT, node[1], tot_len));
+      if (checkEntailArithWithAssumption(n1_lt_tot_len, zero, node[2], false))
       {
-        Node n1_eq_zero =
-            Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[1], zero));
-        if (checkEntailArithWithAssumption(n1_eq_zero, zero, node[2], false))
-        {
-          Node ret = nm->mkConst(::CVC4::String(""));
-          return returnRewrite(node, ret, "ss-len-one-unsat");
-        }
+        Node ret = nm->mkConst(::CVC4::String(""));
+        return returnRewrite(node, ret, "ss-start-entails-zero-len");
       }
     }
     if (!curr.isNull())
@@ -3019,8 +3017,7 @@ bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption,
         toVisit.push_back(currChild);
       }
     }
-    else if (curr.getKind() == kind::VARIABLE
-             && Theory::theoryOf(curr) == THEORY_ARITH)
+    else if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH)
     {
       candVars.insert(curr);
     }
@@ -3040,8 +3037,7 @@ bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption,
       toVisit.push_back(currChild);
     }
 
-    if (curr.getKind() == kind::VARIABLE
-        && Theory::theoryOf(curr) == THEORY_ARITH
+    if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH
         && candVars.find(curr) != candVars.end())
     {
       v = curr;
@@ -3071,14 +3067,55 @@ bool TheoryStringsRewriter::checkEntailArithWithAssumption(Node assumption,
                                                            Node b,
                                                            bool strict)
 {
-  // TODO: Add support for inequality assumptions.
-  Assert(assumption.getKind() == kind::EQUAL);
   Assert(Rewriter::rewrite(assumption) == assumption);
 
   NodeManager* nm = NodeManager::currentNM();
 
+  if (!assumption.isConst() && assumption.getKind() != kind::EQUAL)
+  {
+    // We rewrite inequality assumptions from x <= y to x + (str.len s) = y
+    // where s is some fresh string variable. We use (str.len s) because
+    // (str.len s) must be non-negative for the equation to hold.
+    Node x, y;
+    if (assumption.getKind() == kind::GEQ)
+    {
+      x = assumption[0];
+      y = assumption[1];
+    }
+    else
+    {
+      // (not (>= s t)) --> (>= (t - 1) s)
+      Assert(assumption.getKind() == kind::NOT
+             && assumption[0].getKind() == kind::GEQ);
+      x = nm->mkNode(kind::MINUS, assumption[0][1], nm->mkConst(Rational(1)));
+      y = assumption[0][0];
+    }
+
+    Node s = nm->mkBoundVar("s", nm->stringType());
+    Node slen = nm->mkNode(kind::STRING_LENGTH, s);
+    assumption = Rewriter::rewrite(
+        nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen)));
+  }
+
   Node diff = nm->mkNode(kind::MINUS, a, b);
-  return checkEntailArithWithEqAssumption(assumption, diff, strict);
+  bool res = false;
+  if (assumption.isConst())
+  {
+    bool assumptionBool = assumption.getConst<bool>();
+    if (assumptionBool)
+    {
+      res = checkEntailArith(diff, strict);
+    }
+    else
+    {
+      res = true;
+    }
+  }
+  else
+  {
+    res = checkEntailArithWithEqAssumption(assumption, diff, strict);
+  }
+  return res;
 }
 
 bool TheoryStringsRewriter::checkEntailArithWithAssumptions(
@@ -3090,7 +3127,6 @@ bool TheoryStringsRewriter::checkEntailArithWithAssumptions(
   bool res = false;
   for (const auto& assumption : assumptions)
   {
-    Assert(assumption.getKind() == kind::EQUAL);
     Assert(Rewriter::rewrite(assumption) == assumption);
 
     if (checkEntailArithWithAssumption(assumption, a, b, strict))
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 31ad1406a..0e4cb594a 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -376,7 +376,7 @@ private:
    * Checks whether assumption |= a >= b (if strict is false) or
    * assumption |= a > b (if strict is true). The function returns true if it
    * can be shown that the entailment holds and false otherwise. Assumption
-   * must be in rewritten form and an equality assumption.
+   * must be in rewritten form. Assumption may be an equality or an inequality.
    *
    * Example:
    *
@@ -393,7 +393,8 @@ private:
    * Checks whether assumptions |= a >= b (if strict is false) or
    * assumptions |= a > b (if strict is true). The function returns true if it
    * can be shown that the entailment holds and false otherwise. Assumptions
-   * must be in rewritten form and must be equality assumptions.
+   * must be in rewritten form. Assumptions may be an equalities or an
+   * inequalities.
    *
    * Example:
    *
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index a1e878f6e..a17299f80 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -72,27 +72,53 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node x_plus_slen_y_eq_zero =
         Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x_plus_slen_y, zero));
 
-    // x + (str.len y) = 0 /\ 0 >= x --> true
+    // x + (str.len y) = 0 |= 0 >= x --> true
     TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
         x_plus_slen_y_eq_zero, zero, x, false));
 
-    // x + (str.len y) = 0 /\ 0 > x --> false
+    // x + (str.len y) = 0 |= 0 > x --> false
     TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption(
         x_plus_slen_y_eq_zero, zero, x, true));
 
     Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nm->mkNode(
         kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, z), zero));
 
-    // x + (str.len y) + z = 0 /\ 0 > x --> false
+    // x + (str.len y) + z = 0 |= 0 > x --> false
     TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption(
         x_plus_slen_y_plus_z_eq_zero, zero, x, true));
 
     Node x_plus_slen_y_plus_slen_y_eq_zero = Rewriter::rewrite(d_nm->mkNode(
         kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, slen_y), zero));
 
-    // x + (str.len y) + (str.len y) = 0 /\ 0 >= x --> true
+    // x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true
     TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
         x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false));
+
+    Node five = d_nm->mkConst(Rational(5));
+    Node six = d_nm->mkConst(Rational(6));
+    Node x_plus_five = d_nm->mkNode(kind::PLUS, x, five);
+    Node x_plus_five_lt_six =
+        Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, six));
+
+    // x + 5 < 6 |= 0 >= x --> true
+    TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
+        x_plus_five_lt_six, zero, x, false));
+
+    // x + 5 < 6 |= 0 > x --> false
+    TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption(
+        x_plus_five_lt_six, zero, x, true));
+
+    Node neg_x = d_nm->mkNode(kind::UMINUS, x);
+    Node x_plus_five_lt_five =
+        Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, five));
+
+    // x + 5 < 5 |= -x >= 0 --> true
+    TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
+        x_plus_five_lt_five, neg_x, zero, false));
+
+    // x + 5 < 5 |= 0 > x --> true
+    TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
+        x_plus_five_lt_five, zero, x, false));
   }
 
   void testRewriteSubstr()
@@ -102,6 +128,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     Node empty = d_nm->mkConst(::CVC4::String(""));
     Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
+    Node two = d_nm->mkConst(Rational(2));
+    Node three = d_nm->mkConst(Rational(3));
+
     Node s = d_nm->mkVar("s", strType);
     Node x = d_nm->mkVar("x", intType);
     Node y = d_nm->mkVar("y", intType);
@@ -132,5 +162,17 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y);
     res = TheoryStringsRewriter::rewriteSubstr(n);
     TS_ASSERT_EQUALS(res, n);
+
+    // (str.substr "ABCD" (+ x 3) x) -> ""
+    n = d_nm->mkNode(
+        kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, three), x);
+    res = TheoryStringsRewriter::rewriteSubstr(n);
+    TS_ASSERT_EQUALS(res, empty);
+
+    // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
+    n = d_nm->mkNode(
+        kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x);
+    res = TheoryStringsRewriter::rewriteSubstr(n);
+    TS_ASSERT_EQUALS(res, n);
   }
 };