From 2ac7e8c916bfb33eb73cd90b20a92bef7036ac6b Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 9 Jan 2020 16:45:38 -0800 Subject: [PATCH] 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. --- .../strings/theory_strings_preprocess.cpp | 30 +++++++++++++------ 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a3b864089..6272ad129 100644 --- 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 -- 2.30.2