#include "theory/strings/theory_strings_rewriter.h"
#include <stdint.h>
+#include <algorithm>
#include "options/strings_options.h"
#include "smt/logic_exception.h"
if( !preNode.isNull() && ( preNode.getKind()!=kind::CONST_STRING || !preNode.getConst<String>().isEmptyString() ) ){
node_vec.push_back( preNode );
}
+
+ // Sort adjacent operands in str.++ that all result in the same string or the
+ // empty string.
+ //
+ // E.g.: (str.++ ... (str.replace "A" x "") "A" (str.substr "A" 0 z) ...) -->
+ // (str.++ ... [sort those 3 arguments] ... )
+ size_t lastIdx = 0;
+ Node lastX;
+ for (size_t i = 0; i < node_vec.size(); i++)
+ {
+ Node s = getStringOrEmpty(node_vec[i]);
+ bool nextX = false;
+ if (s != lastX)
+ {
+ nextX = true;
+ }
+
+ if (nextX)
+ {
+ std::sort(node_vec.begin() + lastIdx, node_vec.begin() + i);
+ lastX = s;
+ lastIdx = i;
+ }
+ }
+ std::sort(node_vec.begin() + lastIdx, node_vec.end());
+
retNode = mkConcat( kind::STRING_CONCAT, node_vec );
Trace("strings-prerewrite") << "Strings::rewriteConcat end " << retNode
<< std::endl;
return base;
}
+Node TheoryStringsRewriter::getStringOrEmpty(Node n)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node res;
+ while (res.isNull())
+ {
+ switch (n.getKind())
+ {
+ case kind::STRING_STRREPL:
+ {
+ Node empty = nm->mkConst(::CVC4::String(""));
+ if (n[0] == empty)
+ {
+ // (str.replace "" x y) --> y
+ n = n[2];
+ break;
+ }
+
+ Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0]));
+ if (strlen == nm->mkConst(Rational(1)) && n[2] == empty)
+ {
+ // (str.replace "A" x "") --> "A"
+ res = n[0];
+ break;
+ }
+
+ res = n;
+ break;
+ }
+ case kind::STRING_SUBSTR:
+ {
+ Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0]));
+ if (strlen == nm->mkConst(Rational(1)))
+ {
+ // (str.substr "A" x y) --> "A"
+ res = n[0];
+ break;
+ }
+ res = n;
+ break;
+ }
+ default:
+ {
+ res = n;
+ break;
+ }
+ }
+ }
+ return res;
+}
+
Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c)
{
Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c
static Node mkSubstrChain(Node base,
const std::vector<Node>& ss,
const std::vector<Node>& ls);
+
+ /**
+ * Overapproximates the possible values of node n. This overapproximation
+ * assumes that n can return a value x or the empty string and tries to find
+ * the simplest x such that this holds. In the general case, x is the same as
+ * the input n. This overapproximation can be used to sort terms with the
+ * same possible values in string concatenation for example.
+ *
+ * Example:
+ *
+ * getStringOrEmpty( (str.replace "" x y) ) --> y because (str.replace "" x y)
+ * either returns y or ""
+ *
+ * getStringOrEmpty( (str.substr "ABC" x y) ) --> (str.substr "ABC" x y)
+ * because the function could not compute a simpler
+ */
+ static Node getStringOrEmpty(Node n);
};/* class TheoryStringsRewriter */
}/* CVC4::theory::strings namespace */
res = TheoryStringsRewriter::rewriteSubstr(n);
TS_ASSERT_EQUALS(res, n);
}
+
+ void testRewriteConcat()
+ {
+ TypeNode intType = d_nm->integerType();
+ TypeNode strType = d_nm->stringType();
+
+ Node empty = d_nm->mkConst(::CVC4::String(""));
+ Node a = d_nm->mkConst(::CVC4::String("A"));
+ Node zero = d_nm->mkConst(Rational(0));
+ Node three = d_nm->mkConst(Rational(3));
+
+ Node i = d_nm->mkVar("i", intType);
+ Node s = d_nm->mkVar("s", strType);
+ Node x = d_nm->mkVar("x", strType);
+ Node y = d_nm->mkVar("y", strType);
+
+ // Same normal form for:
+ //
+ // (str.++ (str.replace "A" x "") "A")
+ //
+ // (str.++ "A" (str.replace "A" x ""))
+ Node repl_a_x_e = d_nm->mkNode(kind::STRING_STRREPL, a, x, empty);
+ Node repl_a = d_nm->mkNode(kind::STRING_CONCAT, repl_a_x_e, a);
+ Node a_repl = d_nm->mkNode(kind::STRING_CONCAT, a, repl_a_x_e);
+ Node res_repl_a = Rewriter::rewrite(repl_a);
+ Node res_a_repl = Rewriter::rewrite(a_repl);
+ TS_ASSERT_EQUALS(res_repl_a, res_a_repl);
+
+ // Same normal form for:
+ //
+ // (str.++ y (str.replace "" x (str.substr y 0 3)) (str.substr y 0 3) "A" (str.substr y 0 3))
+ //
+ // (str.++ y (str.substr y 0 3) (str.replace "" x (str.substr y 0 3)) "A" (str.substr y 0 3))
+ Node z = d_nm->mkNode(kind::STRING_SUBSTR, y, zero, three);
+ Node repl_e_x_z = d_nm->mkNode(kind::STRING_STRREPL, empty, x, z);
+ repl_a = d_nm->mkNode(kind::STRING_CONCAT, y, repl_e_x_z, z, a, z);
+ a_repl = d_nm->mkNode(kind::STRING_CONCAT, y, z, repl_e_x_z, a, z);
+ res_repl_a = Rewriter::rewrite(repl_a);
+ res_a_repl = Rewriter::rewrite(a_repl);
+ TS_ASSERT_EQUALS(res_repl_a, res_a_repl);
+
+ // Same normal form for:
+ //
+ // (str.++ "A" (str.replace "A" x "") (str.substr "A" 0 i))
+ //
+ // (str.++ (str.substr "A" 0 i) (str.replace "A" x "") "A")
+ Node substr_a = d_nm->mkNode(kind::STRING_SUBSTR, a, zero, i);
+ Node a_substr_repl =
+ d_nm->mkNode(kind::STRING_CONCAT, a, substr_a, repl_a_x_e);
+ Node substr_repl_a =
+ d_nm->mkNode(kind::STRING_CONCAT, substr_a, repl_a_x_e, a);
+ Node res_a_substr_repl = Rewriter::rewrite(a_substr_repl);
+ Node res_substr_repl_a = Rewriter::rewrite(substr_repl_a);
+ TS_ASSERT_EQUALS(res_a_substr_repl, res_substr_repl_a);
+
+ // Same normal form for:
+ //
+ // (str.++ (str.replace "" x (str.substr "A" 0 i)) (str.substr "A" 0 i) (str.at "A" i))
+ //
+ // (str.++ (str.at "A" i) (str.replace "" x (str.substr "A" 0 i)) (str.substr "A" 0 i))
+ Node charat_a = d_nm->mkNode(kind::STRING_CHARAT, a, i);
+ Node repl_e_x_s = d_nm->mkNode(kind::STRING_STRREPL, empty, x, substr_a);
+ Node repl_substr_a =
+ d_nm->mkNode(kind::STRING_CONCAT, repl_e_x_s, substr_a, charat_a);
+ Node a_repl_substr =
+ d_nm->mkNode(kind::STRING_CONCAT, charat_a, repl_e_x_s, substr_a);
+ Node res_repl_substr_a = Rewriter::rewrite(repl_substr_a);
+ Node res_a_repl_substr = Rewriter::rewrite(a_repl_substr);
+ TS_ASSERT_EQUALS(res_repl_substr_a, res_a_repl_substr);
+ }
};
projects / cvc5.git / commitdiff