Optimize str.substr reduction (#3595)

This commit optimizes the `str.substr` reduction by replacing the
if-then-else term for the length of the suffix `len(sk2) = ite(len(s) >=
n+m, len(s) - (n + m), 0)` with `(len(sk2) = len(s) - (n + m) v
len(sk2) = 0) ^ len(skt) <= m`. Experiments have shown that the latter
encoding is more efficient.

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index a3b864089511f8d0261da8f603bae32d1f399f74..6272ad1291ddc6e89a1666160c2b8d95542578e4 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -78,14 +78,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2));
     //length of first skolem is second argument
     Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
-    //length of second skolem is abs difference between end point and end of string
-    Node b13 = nm->mkNode(STRING_LENGTH, sk2)
-                   .eqNode(nm->mkNode(ITE,
-                                      nm->mkNode(GEQ, lt0, t12),
-                                      nm->mkNode(MINUS, lt0, t12),
-                                      d_zero));
-
-    Node b1 = nm->mkNode(AND, b11, b12, b13);
+    Node lsk2 = nm->mkNode(STRING_LENGTH, sk2);
+    // Length of the suffix is either 0 (in the case where m + n > len(s)) or
+    // len(s) - n -m
+    Node b13 = nm->mkNode(
+        OR,
+        nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))),
+        nm->mkNode(EQUAL, lsk2, d_zero));
+    // Length of the result is at most m
+    Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m);
+
+    Node b1 = nm->mkNode(AND, b11, b12, b13, b14);
     Node b2 = skt.eqNode(d_empty_str);
     Node lemma = nm->mkNode(ITE, cond, b1, b2);
 
@@ -93,8 +96,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     // IF    n >=0 AND n < len( s ) AND m > 0
     // THEN: s = sk1 ++ skt ++ sk2 AND
     //       len( sk1 ) = n AND
-    //       len( sk2 ) = ite( len( s ) >= n+m, len( s )-(n+m), 0 )
+    //       ( len( sk2 ) = len( s )-(n+m) OR len( sk2 ) = 0 ) AND
+    //       len( skt ) <= m
     // ELSE: skt = ""
+    //
+    // Note: The length of sk2 is either 0 (if the n + m is greater or equal to
+    // the length of s) or len(s) - (n + m) otherwise. If n + m is greater or
+    // equal to the length of s, then len(s) - (n + m) is negative and in
+    // conflict with lengths always being positive, so only len(sk2) = 0 may be
+    // satisfied. If n + m is less than the length of s, then len(sk2) = 0
+    // cannot be satisfied because we have the constraint that len(skt) <= m,
+    // so sk2 must be greater than 0.
     new_nodes.push_back( lemma );
 
     // Thus, substr( s, n, m ) = skt