Split sequences rewriter (#4194)

This is in preparation for making the strings rewriter configurable for stats.

This moves all utility functions from SequencesRewriter to a proper place. This includes three new groupings of utility functions: those involving arithmetic entailments, those involving string entailments, those involving regular expression entailments. Here, "entailments" loosely means any question regarding a (set of) terms or formulas.

No major code changes. Added some missing documentation and lightly cleaned a few blocks of code in cpp.

1 files changed, 36 insertions, 43 deletions

diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h
index c823c0704..4cc679ca8 100644
--- a/test/unit/theory/sequences_rewriter_white.h
+++ b/test/unit/theory/sequences_rewriter_white.h
@@ -20,7 +20,9 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/extended_rewrite.h"
 #include "theory/rewriter.h"
+#include "theory/strings/arith_entail.h"
 #include "theory/strings/sequences_rewriter.h"
+#include "theory/strings/strings_entail.h"
 
 #include <cxxtest/TestSuite.h>
 #include <iostream>
@@ -108,23 +110,23 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
     Node three = d_nm->mkConst(Rational(3));
     Node i = d_nm->mkVar("i", intType);
 
-    TS_ASSERT(SequencesRewriter::checkEntailLengthOne(a));
-    TS_ASSERT(SequencesRewriter::checkEntailLengthOne(a, true));
+    TS_ASSERT(StringsEntail::checkLengthOne(a));
+    TS_ASSERT(StringsEntail::checkLengthOne(a, true));
 
     Node substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one);
-    TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr));
-    TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr, true));
+    TS_ASSERT(StringsEntail::checkLengthOne(substr));
+    TS_ASSERT(!StringsEntail::checkLengthOne(substr, true));
 
     substr = d_nm->mkNode(kind::STRING_SUBSTR,
                           d_nm->mkNode(kind::STRING_CONCAT, a, x),
                           zero,
                           one);
-    TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr));
-    TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr, true));
+    TS_ASSERT(StringsEntail::checkLengthOne(substr));
+    TS_ASSERT(StringsEntail::checkLengthOne(substr, true));
 
     substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, two);
-    TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr));
-    TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr, true));
+    TS_ASSERT(!StringsEntail::checkLengthOne(substr));
+    TS_ASSERT(!StringsEntail::checkLengthOne(substr, true));
   }
 
   void testCheckEntailArith()
@@ -139,10 +141,10 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
     // 1 >= (str.len (str.substr z n 1)) ---> true
     Node substr_z = d_nm->mkNode(kind::STRING_LENGTH,
                                  d_nm->mkNode(kind::STRING_SUBSTR, z, n, one));
-    TS_ASSERT(SequencesRewriter::checkEntailArith(one, substr_z));
+    TS_ASSERT(ArithEntail::check(one, substr_z));
 
     // (str.len (str.substr z n 1)) >= 1 ---> false
-    TS_ASSERT(!SequencesRewriter::checkEntailArith(substr_z, one));
+    TS_ASSERT(!ArithEntail::check(substr_z, one));
   }
 
   void testCheckEntailArithWithAssumption()
@@ -166,25 +168,25 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
         Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x_plus_slen_y, zero));
 
     // x + (str.len y) = 0 |= 0 >= x --> true
-    TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption(
+    TS_ASSERT(ArithEntail::checkWithAssumption(
         x_plus_slen_y_eq_zero, zero, x, false));
 
     // x + (str.len y) = 0 |= 0 > x --> false
-    TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption(
+    TS_ASSERT(!ArithEntail::checkWithAssumption(
         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
-    TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption(
+    TS_ASSERT(!ArithEntail::checkWithAssumption(
         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
-    TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption(
+    TS_ASSERT(ArithEntail::checkWithAssumption(
         x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false));
 
     Node five = d_nm->mkConst(Rational(5));
@@ -194,28 +196,28 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
         Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, six));
 
     // x + 5 < 6 |= 0 >= x --> true
-    TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption(
-        x_plus_five_lt_six, zero, x, false));
+    TS_ASSERT(
+        ArithEntail::checkWithAssumption(x_plus_five_lt_six, zero, x, false));
 
     // x + 5 < 6 |= 0 > x --> false
-    TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption(
-        x_plus_five_lt_six, zero, x, true));
+    TS_ASSERT(
+        !ArithEntail::checkWithAssumption(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(SequencesRewriter::checkEntailArithWithAssumption(
+    TS_ASSERT(ArithEntail::checkWithAssumption(
         x_plus_five_lt_five, neg_x, zero, false));
 
     // x + 5 < 5 |= 0 > x --> true
-    TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption(
-        x_plus_five_lt_five, zero, x, false));
+    TS_ASSERT(
+        ArithEntail::checkWithAssumption(x_plus_five_lt_five, zero, x, false));
 
     // 0 < x |= x >= (str.len (int.to.str x))
     Node assm = Rewriter::rewrite(d_nm->mkNode(kind::LT, zero, x));
-    TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption(
+    TS_ASSERT(ArithEntail::checkWithAssumption(
         assm,
         x,
         d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_ITOS, x)),
@@ -1050,33 +1052,30 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
     Node empty_x_y = d_nm->mkNode(kind::AND,
                                   d_nm->mkNode(kind::EQUAL, empty, x),
                                   d_nm->mkNode(kind::EQUAL, empty, y));
-    sameNormalForm(SequencesRewriter::inferEqsFromContains(empty, xy),
-                   empty_x_y);
+    sameNormalForm(StringsEntail::inferEqsFromContains(empty, xy), empty_x_y);
 
     // inferEqsFromContains(x, (str.++ x y)) returns false
     Node bxya = d_nm->mkNode(kind::STRING_CONCAT, b, y, x, a);
-    sameNormalForm(SequencesRewriter::inferEqsFromContains(x, bxya), f);
+    sameNormalForm(StringsEntail::inferEqsFromContains(x, bxya), f);
 
     // inferEqsFromContains(x, y) returns null
-    Node n = SequencesRewriter::inferEqsFromContains(x, y);
+    Node n = StringsEntail::inferEqsFromContains(x, y);
     TS_ASSERT(n.isNull());
 
     // inferEqsFromContains(x, x) returns something equivalent to (= x x)
     Node eq_x_x = d_nm->mkNode(kind::EQUAL, x, x);
-    sameNormalForm(SequencesRewriter::inferEqsFromContains(x, x), eq_x_x);
+    sameNormalForm(StringsEntail::inferEqsFromContains(x, x), eq_x_x);
 
     // inferEqsFromContains((str.replace x "B" "A"), x) returns something
     // equivalent to (= (str.replace x "B" "A") x)
     Node repl = d_nm->mkNode(kind::STRING_STRREPL, x, b, a);
     Node eq_repl_x = d_nm->mkNode(kind::EQUAL, repl, x);
-    sameNormalForm(SequencesRewriter::inferEqsFromContains(repl, x),
-                   eq_repl_x);
+    sameNormalForm(StringsEntail::inferEqsFromContains(repl, x), eq_repl_x);
 
     // inferEqsFromContains(x, (str.replace x "B" "A")) returns something
     // equivalent to (= (str.replace x "B" "A") x)
     Node eq_x_repl = d_nm->mkNode(kind::EQUAL, x, repl);
-    sameNormalForm(SequencesRewriter::inferEqsFromContains(x, repl),
-                   eq_x_repl);
+    sameNormalForm(StringsEntail::inferEqsFromContains(x, repl), eq_x_repl);
   }
 
   void testRewritePrefixSuffix()
@@ -1402,8 +1401,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
       std::vector<Node> n2 = {a};
       std::vector<Node> nb;
       std::vector<Node> ne;
-      bool res =
-          SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0);
+      bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0);
       TS_ASSERT(!res);
     }
 
@@ -1414,8 +1412,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
       std::vector<Node> n2 = {a, d_nm->mkNode(kind::STRING_ITOS, n)};
       std::vector<Node> nb;
       std::vector<Node> ne;
-      bool res =
-          SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0);
+      bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0);
       TS_ASSERT(!res);
     }
 
@@ -1430,8 +1427,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
       std::vector<Node> ne;
       std::vector<Node> n1r = {cd};
       std::vector<Node> nbr = {ab};
-      bool res =
-          SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1);
+      bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1);
       TS_ASSERT(res);
       TS_ASSERT_EQUALS(n1, n1r);
       TS_ASSERT_EQUALS(nb, nbr);
@@ -1448,8 +1444,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
       std::vector<Node> ne;
       std::vector<Node> n1r = {c, x};
       std::vector<Node> nbr = {ab};
-      bool res =
-          SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1);
+      bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1);
       TS_ASSERT(res);
       TS_ASSERT_EQUALS(n1, n1r);
       TS_ASSERT_EQUALS(nb, nbr);
@@ -1466,8 +1461,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
       std::vector<Node> ne;
       std::vector<Node> n1r = {a};
       std::vector<Node> ner = {bc};
-      bool res =
-          SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1);
+      bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1);
       TS_ASSERT(res);
       TS_ASSERT_EQUALS(n1, n1r);
       TS_ASSERT_EQUALS(ne, ner);
@@ -1484,8 +1478,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
       std::vector<Node> ne;
       std::vector<Node> n1r = {x, a};
       std::vector<Node> ner = {bc};
-      bool res =
-          SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1);
+      bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1);
       TS_ASSERT(res);
       TS_ASSERT_EQUALS(n1, n1r);
       TS_ASSERT_EQUALS(ne, ner);