From: Aina Niemetz Date: Wed, 24 Feb 2021 12:22:21 +0000 (-0800) Subject: google test: theory: Migrate sequences_rewriter_white. (#5975) X-Git-Tag: cvc5-1.0.0~2222 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d45b6fb6f797eb9dc51ea70b20ec875d1dfe49d;p=cvc5.git google test: theory: Migrate sequences_rewriter_white. (#5975) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 818e4d271..1af33ff19 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -12,7 +12,7 @@ cvc4_add_unit_test_black(regexp_operation_black theory) cvc4_add_cxx_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) -cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory) +cvc4_add_unit_test_white(sequences_rewriter_white theory) cvc4_add_unit_test_white(strings_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) cvc4_add_unit_test_white(theory_bags_normal_form_white theory) diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp new file mode 100644 index 000000000..590fa2ace --- /dev/null +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -0,0 +1,1912 @@ +/********************* */ +/*! \file sequences_rewriter_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andres Noetzli, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Unit tests for the strings/sequences rewriter + ** + ** Unit tests for the strings/sequences rewriter. + **/ + +#include +#include +#include + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "test_smt.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 "theory/strings/strings_rewriter.h" + +namespace CVC4 { + +using namespace smt; +using namespace theory; +using namespace theory::quantifiers; +using namespace theory::strings; + +namespace test { + +class TestTheoryWhiteSequencesRewriter : public TestSmt +{ + protected: + void SetUp() override + { + TestSmt::SetUp(); + Options opts; + d_rewriter.reset(new ExtendedRewriter(true)); + } + + std::unique_ptr d_rewriter; + + void inNormalForm(Node t) + { + Node res_t = d_rewriter->extendedRewrite(t); + + std::cout << std::endl; + std::cout << t << " ---> " << res_t << std::endl; + ASSERT_EQ(t, res_t); + } + + void sameNormalForm(Node t1, Node t2) + { + Node res_t1 = d_rewriter->extendedRewrite(t1); + Node res_t2 = d_rewriter->extendedRewrite(t2); + + std::cout << std::endl; + std::cout << t1 << " ---> " << res_t1 << std::endl; + std::cout << t2 << " ---> " << res_t2 << std::endl; + ASSERT_EQ(res_t1, res_t2); + } + + void differentNormalForms(Node t1, Node t2) + { + Node res_t1 = d_rewriter->extendedRewrite(t1); + Node res_t2 = d_rewriter->extendedRewrite(t2); + + std::cout << std::endl; + std::cout << t1 << " ---> " << res_t1 << std::endl; + std::cout << t2 << " ---> " << res_t2 << std::endl; + ASSERT_NE(res_t1, res_t2); + } +}; + +TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); + Node aaad = d_nodeManager->mkConst(::CVC4::String("AAAD")); + Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node negOne = d_nodeManager->mkConst(Rational(-1)); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node two = d_nodeManager->mkConst(Rational(2)); + Node three = d_nodeManager->mkConst(Rational(3)); + Node i = d_nodeManager->mkVar("i", intType); + + ASSERT_TRUE(StringsEntail::checkLengthOne(a)); + ASSERT_TRUE(StringsEntail::checkLengthOne(a, true)); + + Node substr = d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, one); + ASSERT_TRUE(StringsEntail::checkLengthOne(substr)); + ASSERT_FALSE(StringsEntail::checkLengthOne(substr, true)); + + substr = + d_nodeManager->mkNode(kind::STRING_SUBSTR, + d_nodeManager->mkNode(kind::STRING_CONCAT, a, x), + zero, + one); + ASSERT_TRUE(StringsEntail::checkLengthOne(substr)); + ASSERT_TRUE(StringsEntail::checkLengthOne(substr, true)); + + substr = d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, two); + ASSERT_FALSE(StringsEntail::checkLengthOne(substr)); + ASSERT_FALSE(StringsEntail::checkLengthOne(substr, true)); +} + +TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_arith) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node z = d_nodeManager->mkVar("z", strType); + Node n = d_nodeManager->mkVar("n", intType); + Node one = d_nodeManager->mkConst(Rational(1)); + + // 1 >= (str.len (str.substr z n 1)) ---> true + Node substr_z = d_nodeManager->mkNode( + kind::STRING_LENGTH, + d_nodeManager->mkNode(kind::STRING_SUBSTR, z, n, one)); + ASSERT_TRUE(ArithEntail::check(one, substr_z)); + + // (str.len (str.substr z n 1)) >= 1 ---> false + ASSERT_FALSE(ArithEntail::check(substr_z, one)); +} + +TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node x = d_nodeManager->mkVar("x", intType); + Node y = d_nodeManager->mkVar("y", strType); + Node z = d_nodeManager->mkVar("z", intType); + + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + + Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y); + Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y); + Node x_plus_slen_y_eq_zero = Rewriter::rewrite( + d_nodeManager->mkNode(kind::EQUAL, x_plus_slen_y, zero)); + + // x + (str.len y) = 0 |= 0 >= x --> true + ASSERT_TRUE( + ArithEntail::checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, false)); + + // x + (str.len y) = 0 |= 0 > x --> false + ASSERT_FALSE( + ArithEntail::checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, true)); + + Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nodeManager->mkNode( + kind::EQUAL, d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, z), zero)); + + // x + (str.len y) + z = 0 |= 0 > x --> false + ASSERT_FALSE(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_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, slen_y), + zero)); + + // x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true + ASSERT_TRUE(ArithEntail::checkWithAssumption( + x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); + + Node five = d_nodeManager->mkConst(Rational(5)); + Node six = d_nodeManager->mkConst(Rational(6)); + Node x_plus_five = d_nodeManager->mkNode(kind::PLUS, x, five); + Node x_plus_five_lt_six = + Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six)); + + // x + 5 < 6 |= 0 >= x --> true + ASSERT_TRUE( + ArithEntail::checkWithAssumption(x_plus_five_lt_six, zero, x, false)); + + // x + 5 < 6 |= 0 > x --> false + ASSERT_TRUE( + !ArithEntail::checkWithAssumption(x_plus_five_lt_six, zero, x, true)); + + Node neg_x = d_nodeManager->mkNode(kind::UMINUS, x); + Node x_plus_five_lt_five = + Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five)); + + // x + 5 < 5 |= -x >= 0 --> true + ASSERT_TRUE(ArithEntail::checkWithAssumption( + x_plus_five_lt_five, neg_x, zero, false)); + + // x + 5 < 5 |= 0 > x --> true + ASSERT_TRUE( + ArithEntail::checkWithAssumption(x_plus_five_lt_five, zero, x, false)); + + // 0 < x |= x >= (str.len (int.to.str x)) + Node assm = Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, zero, x)); + ASSERT_TRUE(ArithEntail::checkWithAssumption( + assm, + x, + d_nodeManager->mkNode(kind::STRING_LENGTH, + d_nodeManager->mkNode(kind::STRING_ITOS, x)), + false)); +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); + Node negone = d_nodeManager->mkConst(Rational(-1)); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node two = d_nodeManager->mkConst(Rational(2)); + Node three = d_nodeManager->mkConst(Rational(3)); + + Node s = d_nodeManager->mkVar("s", strType); + Node s2 = d_nodeManager->mkVar("s2", strType); + Node x = d_nodeManager->mkVar("x", intType); + Node y = d_nodeManager->mkVar("y", intType); + + // (str.substr "A" x x) --> "" + Node n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, x); + Node res = StringsRewriter(nullptr).rewriteSubstr(n); + ASSERT_EQ(res, empty); + + // (str.substr "A" (+ x 1) x) -> "" + n = d_nodeManager->mkNode( + kind::STRING_SUBSTR, + a, + d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))), + x); + res = StringsRewriter(nullptr).rewriteSubstr(n); + ASSERT_EQ(res, empty); + + // (str.substr "A" (+ x (str.len s2)) x) -> "" + n = d_nodeManager->mkNode( + kind::STRING_SUBSTR, + a, + d_nodeManager->mkNode( + kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)), + x); + res = StringsRewriter(nullptr).rewriteSubstr(n); + ASSERT_EQ(res, empty); + + // (str.substr "A" x y) -> (str.substr "A" x y) + n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, y); + res = StringsRewriter(nullptr).rewriteSubstr(n); + ASSERT_EQ(res, n); + + // (str.substr "ABCD" (+ x 3) x) -> "" + n = d_nodeManager->mkNode(kind::STRING_SUBSTR, + abcd, + d_nodeManager->mkNode(kind::PLUS, x, three), + x); + res = StringsRewriter(nullptr).rewriteSubstr(n); + ASSERT_EQ(res, empty); + + // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x) + n = d_nodeManager->mkNode( + kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x); + res = StringsRewriter(nullptr).rewriteSubstr(n); + ASSERT_EQ(res, n); + + // (str.substr (str.substr s x x) x x) -> "" + n = d_nodeManager->mkNode(kind::STRING_SUBSTR, + d_nodeManager->mkNode(kind::STRING_SUBSTR, s, x, x), + x, + x); + sameNormalForm(n, empty); + + // Same normal form for: + // + // (str.substr (str.replace "" s "B") x x) + // + // (str.replace "" s (str.substr "B" x x))) + Node lhs = d_nodeManager->mkNode( + kind::STRING_SUBSTR, + d_nodeManager->mkNode(kind::STRING_STRREPL, empty, s, b), + x, + x); + Node rhs = d_nodeManager->mkNode( + kind::STRING_STRREPL, + empty, + s, + d_nodeManager->mkNode(kind::STRING_SUBSTR, b, x, x)); + sameNormalForm(lhs, rhs); + + // Same normal form: + // + // (str.substr (str.replace s "A" "B") 0 x) + // + // (str.replace (str.substr s 0 x) "A" "B") + Node substr_repl = d_nodeManager->mkNode( + kind::STRING_SUBSTR, + d_nodeManager->mkNode(kind::STRING_STRREPL, s, a, b), + zero, + x); + Node repl_substr = d_nodeManager->mkNode( + kind::STRING_STRREPL, + d_nodeManager->mkNode(kind::STRING_SUBSTR, s, zero, x), + a, + b); + sameNormalForm(substr_repl, repl_substr); + + // Same normal form: + // + // (str.substr (str.replace s (str.substr (str.++ s2 "A") 0 1) "B") 0 x) + // + // (str.replace (str.substr s 0 x) (str.substr (str.++ s2 "A") 0 1) "B") + Node substr_y = + d_nodeManager->mkNode(kind::STRING_SUBSTR, + d_nodeManager->mkNode(kind::STRING_CONCAT, s2, a), + zero, + one); + substr_repl = d_nodeManager->mkNode( + kind::STRING_SUBSTR, + d_nodeManager->mkNode(kind::STRING_STRREPL, s, substr_y, b), + zero, + x); + repl_substr = d_nodeManager->mkNode( + kind::STRING_STRREPL, + d_nodeManager->mkNode(kind::STRING_SUBSTR, s, zero, x), + substr_y, + b); + sameNormalForm(substr_repl, repl_substr); + + // (str.substr (str.int.to.str x) x x) ---> empty + Node substr_itos = d_nodeManager->mkNode( + kind::STRING_SUBSTR, d_nodeManager->mkNode(kind::STRING_ITOS, x), x, x); + sameNormalForm(substr_itos, empty); + + // (str.substr s (* (- 1) (str.len s)) 1) ---> empty + Node substr = d_nodeManager->mkNode( + kind::STRING_SUBSTR, + s, + d_nodeManager->mkNode( + kind::MULT, negone, d_nodeManager->mkNode(kind::STRING_LENGTH, s)), + one); + sameNormalForm(substr, empty); +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node three = d_nodeManager->mkConst(Rational(3)); + + Node i = d_nodeManager->mkVar("i", intType); + Node s = d_nodeManager->mkVar("s", strType); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->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_nodeManager->mkNode(kind::STRING_STRREPL, a, x, empty); + Node repl_a = d_nodeManager->mkNode(kind::STRING_CONCAT, repl_a_x_e, a); + Node a_repl = d_nodeManager->mkNode(kind::STRING_CONCAT, a, repl_a_x_e); + sameNormalForm(repl_a, 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_nodeManager->mkNode(kind::STRING_SUBSTR, y, zero, three); + Node repl_e_x_z = d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, z); + repl_a = d_nodeManager->mkNode(kind::STRING_CONCAT, y, repl_e_x_z, z, a, z); + a_repl = d_nodeManager->mkNode(kind::STRING_CONCAT, y, z, repl_e_x_z, a, z); + sameNormalForm(repl_a, 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_nodeManager->mkNode(kind::STRING_SUBSTR, a, zero, i); + Node a_substr_repl = + d_nodeManager->mkNode(kind::STRING_CONCAT, a, substr_a, repl_a_x_e); + Node substr_repl_a = + d_nodeManager->mkNode(kind::STRING_CONCAT, substr_a, repl_a_x_e, a); + sameNormalForm(a_substr_repl, 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_nodeManager->mkNode(kind::STRING_CHARAT, a, i); + Node repl_e_x_s = + d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, substr_a); + Node repl_substr_a = d_nodeManager->mkNode( + kind::STRING_CONCAT, repl_e_x_s, substr_a, charat_a); + Node a_repl_substr = d_nodeManager->mkNode( + kind::STRING_CONCAT, charat_a, repl_e_x_s, substr_a); + sameNormalForm(repl_substr_a, a_repl_substr); +} + +TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); + Node f = d_nodeManager->mkConst(::CVC4::String("F")); + Node gh = d_nodeManager->mkConst(::CVC4::String("GH")); + Node ij = d_nodeManager->mkConst(::CVC4::String("IJ")); + + Node i = d_nodeManager->mkVar("i", intType); + Node s = d_nodeManager->mkVar("s", strType); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + + // Same length preserving rewrite for: + // + // (str.++ "ABCD" (str.++ x x)) + // + // (str.++ "GH" (str.repl "GH" "IJ") "IJ") + Node concat1 = + d_nodeManager->mkNode(kind::STRING_CONCAT, + abcd, + d_nodeManager->mkNode(kind::STRING_CONCAT, x, x)); + Node concat2 = d_nodeManager->mkNode( + kind::STRING_CONCAT, + gh, + x, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, gh, ij), + ij); + Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1); + Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2); + ASSERT_EQ(res_concat1, res_concat2); +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); + Node aaad = d_nodeManager->mkConst(::CVC4::String("AAAD")); + Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node c = d_nodeManager->mkConst(::CVC4::String("C")); + Node ccc = d_nodeManager->mkConst(::CVC4::String("CCC")); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node negOne = d_nodeManager->mkConst(Rational(-1)); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node two = d_nodeManager->mkConst(Rational(2)); + Node three = d_nodeManager->mkConst(Rational(3)); + Node i = d_nodeManager->mkVar("i", intType); + Node j = d_nodeManager->mkVar("j", intType); + + // Same normal form for: + // + // (str.to.int (str.indexof "A" x 1)) + // + // (str.to.int (str.indexof "B" x 1)) + Node a_idof_x = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, x, two); + Node itos_a_idof_x = d_nodeManager->mkNode(kind::STRING_ITOS, a_idof_x); + Node b_idof_x = d_nodeManager->mkNode(kind::STRING_STRIDOF, b, x, two); + Node itos_b_idof_x = d_nodeManager->mkNode(kind::STRING_ITOS, b_idof_x); + sameNormalForm(itos_a_idof_x, itos_b_idof_x); + + // Same normal form for: + // + // (str.indexof (str.++ "ABCD" x) y 3) + // + // (str.indexof (str.++ "AAAD" x) y 3) + Node idof_abcd = + d_nodeManager->mkNode(kind::STRING_STRIDOF, + d_nodeManager->mkNode(kind::STRING_CONCAT, abcd, x), + y, + three); + Node idof_aaad = + d_nodeManager->mkNode(kind::STRING_STRIDOF, + d_nodeManager->mkNode(kind::STRING_CONCAT, aaad, x), + y, + three); + sameNormalForm(idof_abcd, idof_aaad); + + // (str.indexof (str.substr x 1 i) "A" i) ---> -1 + Node idof_substr = d_nodeManager->mkNode( + kind::STRING_STRIDOF, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, i), + a, + i); + sameNormalForm(idof_substr, negOne); + + { + // Same normal form for: + // + // (str.indexof (str.++ "B" (str.substr "CCC" i j) x "A") "A" 0) + // + // (+ 1 (str.len (str.substr "CCC" i j)) + // (str.indexof (str.++ "A" x y) "A" 0)) + Node lhs = d_nodeManager->mkNode( + kind::STRING_STRIDOF, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + b, + d_nodeManager->mkNode(kind::STRING_SUBSTR, ccc, i, j), + x, + a), + a, + zero); + Node rhs = d_nodeManager->mkNode( + kind::PLUS, + one, + d_nodeManager->mkNode( + kind::STRING_LENGTH, + d_nodeManager->mkNode(kind::STRING_SUBSTR, ccc, i, j)), + d_nodeManager->mkNode(kind::STRING_STRIDOF, + d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), + a, + zero)); + sameNormalForm(lhs, rhs); + } + + { + // Same normal form for: + // + // (str.indexof (str.++ "B" "C" "A" x y) "A" 0) + // + // (+ 2 (str.indexof (str.++ "A" x y) "A" 0)) + Node lhs = d_nodeManager->mkNode( + kind::STRING_STRIDOF, + d_nodeManager->mkNode(kind::STRING_CONCAT, b, c, a, x, y), + a, + zero); + Node rhs = d_nodeManager->mkNode( + kind::PLUS, + two, + d_nodeManager->mkNode( + kind::STRING_STRIDOF, + d_nodeManager->mkNode(kind::STRING_CONCAT, a, x, y), + a, + zero)); + sameNormalForm(lhs, rhs); + } +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); + Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node c = d_nodeManager->mkConst(::CVC4::String("C")); + Node d = d_nodeManager->mkConst(::CVC4::String("D")); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node z = d_nodeManager->mkVar("z", strType); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node n = d_nodeManager->mkVar("n", intType); + + // (str.replace (str.replace x "B" x) x "A") --> + // (str.replace (str.replace x "B" "A") x "A") + Node repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, x), + x, + a); + Node repl_repl_short = d_nodeManager->mkNode( + kind::STRING_STRREPL, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a), + x, + a); + sameNormalForm(repl_repl, repl_repl_short); + + // (str.replace "A" (str.replace "B", x, "C") "D") --> "A" + repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + a, + d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, c), + d); + sameNormalForm(repl_repl, a); + + // (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A" + repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + a, + d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, a), + d); + differentNormalForms(repl_repl, a); + + // Same normal form for: + // + // (str.replace x (str.++ x y z) y) + // + // (str.replace x (str.++ x y z) z) + Node xyz = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y, z); + Node repl_x_xyz = d_nodeManager->mkNode(kind::STRING_STRREPL, x, xyz, y); + Node repl_x_zyx = d_nodeManager->mkNode(kind::STRING_STRREPL, x, xyz, z); + sameNormalForm(repl_x_xyz, repl_x_zyx); + + // (str.replace "" (str.++ x x) x) --> "" + Node repl_empty_xx = + d_nodeManager->mkNode(kind::STRING_STRREPL, + empty, + d_nodeManager->mkNode(kind::STRING_CONCAT, x, x), + x); + sameNormalForm(repl_empty_xx, empty); + + // (str.replace "AB" (str.++ x "A") x) --> (str.replace "AB" (str.++ x "A") + // "") + Node repl_ab_xa_x = + d_nodeManager->mkNode(kind::STRING_STRREPL, + d_nodeManager->mkNode(kind::STRING_CONCAT, a, b), + d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), + x); + Node repl_ab_xa_e = + d_nodeManager->mkNode(kind::STRING_STRREPL, + d_nodeManager->mkNode(kind::STRING_CONCAT, a, b), + d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), + empty); + sameNormalForm(repl_ab_xa_x, repl_ab_xa_e); + + // (str.replace "AB" (str.++ x "A") x) -/-> (str.replace "AB" (str.++ "A" x) + // "") + Node repl_ab_ax_e = + d_nodeManager->mkNode(kind::STRING_STRREPL, + d_nodeManager->mkNode(kind::STRING_CONCAT, a, b), + d_nodeManager->mkNode(kind::STRING_CONCAT, a, x), + empty); + differentNormalForms(repl_ab_ax_e, repl_ab_xa_e); + + // (str.replace "" (str.replace y x "A") y) ---> "" + repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + empty, + d_nodeManager->mkNode(kind::STRING_STRREPL, y, x, a), + y); + sameNormalForm(repl_repl, empty); + + // (str.replace "" (str.replace x y x) x) ---> "" + repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + empty, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x), + x); + sameNormalForm(repl_repl, empty); + + // (str.replace "" (str.substr x 0 1) x) ---> "" + repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + empty, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, one), + x); + sameNormalForm(repl_repl, empty); + + // Same normal form for: + // + // (str.replace "" (str.replace x y x) y) + // + // (str.replace "" x y) + repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + empty, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x), + y); + Node repl = d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y); + sameNormalForm(repl_repl, repl); + + // Same normal form: + // + // (str.replace "B" (str.replace x "A" "B") "B") + // + // (str.replace "B" x "B")) + repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + b, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b), + b); + repl = d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, b); + sameNormalForm(repl_repl, repl); + + // Different normal forms for: + // + // (str.replace "B" (str.replace "" x "A") "B") + // + // (str.replace "B" x "B") + repl_repl = d_nodeManager->mkNode( + kind::STRING_STRREPL, + b, + d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, a), + b); + repl = d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, b); + differentNormalForms(repl_repl, repl); + + { + // Same normal form: + // + // (str.replace (str.++ "AB" x) "C" y) + // + // (str.++ "AB" (str.replace x "C" y)) + Node lhs = + d_nodeManager->mkNode(kind::STRING_STRREPL, + d_nodeManager->mkNode(kind::STRING_CONCAT, ab, x), + c, + y); + Node rhs = d_nodeManager->mkNode( + kind::STRING_CONCAT, + ab, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, c, y)); + sameNormalForm(lhs, rhs); + } +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + std::vector emptyVec; + Node sigStar = d_nodeManager->mkNode( + kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec)); + Node foo = d_nodeManager->mkConst(String("FOO")); + Node a = d_nodeManager->mkConst(String("A")); + Node b = d_nodeManager->mkConst(String("B")); + Node re = + d_nodeManager->mkNode(kind::REGEXP_CONCAT, + d_nodeManager->mkNode(kind::STRING_TO_REGEXP, a), + sigStar, + d_nodeManager->mkNode(kind::STRING_TO_REGEXP, b)); + + // Same normal form: + // + // (str.replace_re + // "AZZZB" + // (re.++ (str.to_re "A") re.all (str.to_re "B")) + // "FOO") + // + // "FOO" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, + d_nodeManager->mkConst(String("AZZZB")), + re, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "ZAZZZBZZB" + // (re.++ (str.to_re "A") re.all (str.to_re "B")) + // "FOO") + // + // "ZFOOZZB" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, + d_nodeManager->mkConst(String("ZAZZZBZZB")), + re, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZZB")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "ZAZZZBZAZB" + // (re.++ (str.to_re "A") re.all (str.to_re "B")) + // "FOO") + // + // "ZFOOZAZB" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, + d_nodeManager->mkConst(String("ZAZZZBZAZB")), + re, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZAZB")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "ZZZ" + // (re.++ (str.to_re "A") re.all (str.to_re "B")) + // "FOO") + // + // "ZZZ" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, + d_nodeManager->mkConst(String("ZZZ")), + re, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("ZZZ")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "ZZZ" + // re.all + // "FOO") + // + // "FOOZZZ" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, + d_nodeManager->mkConst(String("ZZZ")), + sigStar, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("FOOZZZ")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "" + // re.all + // "FOO") + // + // "FOO" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE, + d_nodeManager->mkConst(String("")), + sigStar, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + sameNormalForm(t, res); + } +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + std::vector emptyVec; + Node sigStar = d_nodeManager->mkNode( + kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec)); + Node foo = d_nodeManager->mkConst(String("FOO")); + Node a = d_nodeManager->mkConst(String("A")); + Node b = d_nodeManager->mkConst(String("B")); + Node re = + d_nodeManager->mkNode(kind::REGEXP_CONCAT, + d_nodeManager->mkNode(kind::STRING_TO_REGEXP, a), + sigStar, + d_nodeManager->mkNode(kind::STRING_TO_REGEXP, b)); + + // Same normal form: + // + // (str.replace_re + // "AZZZB" + // (re.++ (str.to_re "A") re.all (str.to_re "B")) + // "FOO") + // + // "FOO" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, + d_nodeManager->mkConst(String("AZZZB")), + re, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "ZAZZZBZZB" + // (re.++ (str.to_re "A") re.all (str.to_re "B")) + // "FOO") + // + // "ZFOOZZB" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, + d_nodeManager->mkConst(String("ZAZZZBZZB")), + re, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZZB")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "ZAZZZBZAZB" + // (re.++ (str.to_re "A") re.all (str.to_re "B")) + // "FOO") + // + // "ZFOOZFOO" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, + d_nodeManager->mkConst(String("ZAZZZBZAZB")), + re, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZFOO")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "ZZZ" + // (re.++ (str.to_re "A") re.all (str.to_re "B")) + // "FOO") + // + // "ZZZ" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, + d_nodeManager->mkConst(String("ZZZ")), + re, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("ZZZ")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "ZZZ" + // re.all + // "FOO") + // + // "FOOFOOFOO" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, + d_nodeManager->mkConst(String("ZZZ")), + sigStar, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("FOOFOOFOO")); + sameNormalForm(t, res); + } + + // Same normal form: + // + // (str.replace_re + // "" + // re.all + // "FOO") + // + // "" + { + Node t = d_nodeManager->mkNode(kind::STRING_REPLACE_RE_ALL, + d_nodeManager->mkConst(String("")), + sigStar, + foo); + Node res = d_nodeManager->mkConst(::CVC4::String("")); + sameNormalForm(t, res); + } +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); + Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node c = d_nodeManager->mkConst(::CVC4::String("C")); + Node e = d_nodeManager->mkConst(::CVC4::String("E")); + Node h = d_nodeManager->mkConst(::CVC4::String("H")); + Node j = d_nodeManager->mkConst(::CVC4::String("J")); + Node p = d_nodeManager->mkConst(::CVC4::String("P")); + Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); + Node def = d_nodeManager->mkConst(::CVC4::String("DEF")); + Node ghi = d_nodeManager->mkConst(::CVC4::String("GHI")); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); + Node yx = d_nodeManager->mkNode(kind::STRING_CONCAT, y, x); + Node z = d_nodeManager->mkVar("z", strType); + Node n = d_nodeManager->mkVar("n", intType); + Node m = d_nodeManager->mkVar("m", intType); + Node one = d_nodeManager->mkConst(Rational(1)); + Node two = d_nodeManager->mkConst(Rational(2)); + Node three = d_nodeManager->mkConst(Rational(3)); + Node four = d_nodeManager->mkConst(Rational(4)); + Node t = d_nodeManager->mkConst(true); + Node f = d_nodeManager->mkConst(false); + + // Same normal form for: + // + // (str.replace "A" (str.substr x 1 3) y z) + // + // (str.replace "A" (str.substr x 1 4) y z) + Node substr_3 = d_nodeManager->mkNode( + kind::STRING_STRREPL, + a, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three), + z); + Node substr_4 = d_nodeManager->mkNode( + kind::STRING_STRREPL, + a, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, four), + z); + sameNormalForm(substr_3, substr_4); + + // Same normal form for: + // + // (str.replace "A" (str.++ y (str.substr x 1 3)) y z) + // + // (str.replace "A" (str.++ y (str.substr x 1 4)) y z) + Node concat_substr_3 = d_nodeManager->mkNode( + kind::STRING_STRREPL, + a, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + y, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three)), + z); + Node concat_substr_4 = d_nodeManager->mkNode( + kind::STRING_STRREPL, + a, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + y, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, four)), + z); + sameNormalForm(concat_substr_3, concat_substr_4); + + // (str.contains "A" (str.++ a (str.replace "B", x, "C")) --> false + Node ctn_repl = d_nodeManager->mkNode( + kind::STRING_STRCTN, + a, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + a, + d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, c))); + sameNormalForm(ctn_repl, f); + + // (str.contains x (str.++ x x)) --> (= x "") + Node x_cnts_x_x = d_nodeManager->mkNode( + kind::STRING_STRCTN, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, x)); + sameNormalForm(x_cnts_x_x, d_nodeManager->mkNode(kind::EQUAL, x, empty)); + + // Same normal form for: + // + // (str.contains (str.++ y x) (str.++ x z y)) + // + // (and (str.contains (str.++ y x) (str.++ x y)) (= z "")) + Node yx_cnts_xzy = d_nodeManager->mkNode( + kind::STRING_STRCTN, + yx, + d_nodeManager->mkNode(kind::STRING_CONCAT, x, z, y)); + Node yx_cnts_xy = + d_nodeManager->mkNode(kind::AND, + d_nodeManager->mkNode(kind::EQUAL, z, empty), + d_nodeManager->mkNode(kind::STRING_STRCTN, yx, xy)); + sameNormalForm(yx_cnts_xzy, yx_cnts_xy); + + // Same normal form for: + // + // (str.contains (str.substr x n (str.len y)) y) + // + // (= (str.substr x n (str.len y)) y) + Node ctn_substr = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_SUBSTR, + x, + n, + d_nodeManager->mkNode(kind::STRING_LENGTH, y)), + y); + Node substr_eq = d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_SUBSTR, + x, + n, + d_nodeManager->mkNode(kind::STRING_LENGTH, y)), + y); + sameNormalForm(ctn_substr, substr_eq); + + // Same normal form for: + // + // (str.contains x (str.replace y x y)) + // + // (str.contains x y) + Node ctn_repl_y_x_y = d_nodeManager->mkNode( + kind::STRING_STRCTN, + x, + d_nodeManager->mkNode(kind::STRING_STRREPL, y, x, y)); + Node ctn_x_y = d_nodeManager->mkNode(kind::STRING_STRCTN, x, y); + sameNormalForm(ctn_repl_y_x_y, ctn_repl_y_x_y); + + // Same normal form for: + // + // (str.contains x (str.replace x y x)) + // + // (= x (str.replace x y x)) + Node ctn_repl_self = d_nodeManager->mkNode( + kind::STRING_STRCTN, + x, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x)); + Node eq_repl = d_nodeManager->mkNode( + kind::EQUAL, x, d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x)); + sameNormalForm(ctn_repl_self, eq_repl); + + // (str.contains x (str.++ "A" (str.replace x y x))) ---> false + Node ctn_repl_self_f = d_nodeManager->mkNode( + kind::STRING_STRCTN, + x, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + a, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x))); + sameNormalForm(ctn_repl_self_f, f); + + // Same normal form for: + // + // (str.contains x (str.replace "" x y)) + // + // (= "" (str.replace "" x y)) + Node ctn_repl_empty = d_nodeManager->mkNode( + kind::STRING_STRCTN, + x, + d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y)); + Node eq_repl_empty = d_nodeManager->mkNode( + kind::EQUAL, + empty, + d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y)); + sameNormalForm(ctn_repl_empty, eq_repl_empty); + + // Same normal form for: + // + // (str.contains x (str.++ x y)) + // + // (= "" y) + Node ctn_x_x_y = d_nodeManager->mkNode( + kind::STRING_STRCTN, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, y)); + Node eq_emp_y = d_nodeManager->mkNode(kind::EQUAL, empty, y); + sameNormalForm(ctn_x_x_y, eq_emp_y); + + // Same normal form for: + // + // (str.contains (str.++ y x) (str.++ x y)) + // + // (= (str.++ y x) (str.++ x y)) + Node ctn_yxxy = d_nodeManager->mkNode(kind::STRING_STRCTN, yx, xy); + Node eq_yxxy = d_nodeManager->mkNode(kind::EQUAL, yx, xy); + sameNormalForm(ctn_yxxy, eq_yxxy); + + // (str.contains (str.replace x y x) x) ---> true + ctn_repl = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x), + x); + sameNormalForm(ctn_repl, t); + + // (str.contains (str.replace (str.++ x y) z (str.++ y x)) x) ---> true + ctn_repl = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, xy, z, yx), + x); + sameNormalForm(ctn_repl, t); + + // (str.contains (str.++ z (str.replace (str.++ x y) z (str.++ y x))) x) + // ---> true + ctn_repl = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + z, + d_nodeManager->mkNode(kind::STRING_STRREPL, xy, z, yx)), + x); + sameNormalForm(ctn_repl, t); + + // Same normal form for: + // + // (str.contains (str.replace x y x) y) + // + // (str.contains x y) + Node lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x), + y); + Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, y); + sameNormalForm(lhs, rhs); + + // Same normal form for: + // + // (str.contains (str.replace x y x) "B") + // + // (str.contains x "B") + lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x), + b); + rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, b); + sameNormalForm(lhs, rhs); + + // Same normal form for: + // + // (str.contains (str.replace x y x) (str.substr z n 1)) + // + // (str.contains x (str.substr z n 1)) + Node substr_z = d_nodeManager->mkNode(kind::STRING_SUBSTR, z, n, one); + lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x), + substr_z); + rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, substr_z); + sameNormalForm(lhs, rhs); + + // Same normal form for: + // + // (str.contains (str.replace x y z) z) + // + // (str.contains (str.replace x z y) y) + lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, z), + z); + rhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, z, y), + y); + sameNormalForm(lhs, rhs); + + // Same normal form for: + // + // (str.contains (str.replace x "A" "B") "A") + // + // (str.contains (str.replace x "A" "") "A") + lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b), + a); + rhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, empty), + a); + sameNormalForm(lhs, rhs); + + { + // (str.contains (str.++ x "A") (str.++ "B" x)) ---> false + Node ctn = + d_nodeManager->mkNode(kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), + d_nodeManager->mkNode(kind::STRING_CONCAT, b, x)); + sameNormalForm(ctn, f); + } + + { + // Same normal form for: + // + // (str.contains (str.replace x "ABC" "DEF") "GHI") + // + // (str.contains x "GHI") + lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, abc, def), + ghi); + rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, ghi); + sameNormalForm(lhs, rhs); + } + + { + // Different normal forms for: + // + // (str.contains (str.replace x "ABC" "DEF") "B") + // + // (str.contains x "B") + lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, abc, def), + b); + rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, b); + differentNormalForms(lhs, rhs); + } + + { + // Different normal forms for: + // + // (str.contains (str.replace x "B" "DEF") "ABC") + // + // (str.contains x "ABC") + lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, def), + abc); + rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc); + differentNormalForms(lhs, rhs); + } + + { + // Same normal form for: + // + // (str.contains (str.++ (str.substr "DEF" n m) x) "AB") + // + // (str.contains x "AB") + lhs = d_nodeManager->mkNode( + kind::STRING_STRCTN, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + d_nodeManager->mkNode(kind::STRING_SUBSTR, def, n, m), + x), + ab); + rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, ab); + sameNormalForm(lhs, rhs); + } + + { + // Same normal form for: + // + // (str.contains "ABC" (str.at x n)) + // + // (or (= x "") + // (= x "A") (= x "B") (= x "C")) + Node cat = d_nodeManager->mkNode(kind::STRING_CHARAT, x, n); + lhs = d_nodeManager->mkNode(kind::STRING_STRCTN, abc, cat); + rhs = d_nodeManager->mkNode(kind::OR, + d_nodeManager->mkNode(kind::EQUAL, cat, empty), + d_nodeManager->mkNode(kind::EQUAL, cat, a), + d_nodeManager->mkNode(kind::EQUAL, cat, b), + d_nodeManager->mkNode(kind::EQUAL, cat, c)); + sameNormalForm(lhs, rhs); + } +} + +TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains) +{ + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); + Node f = d_nodeManager->mkConst(false); + + // inferEqsFromContains("", (str.++ x y)) returns something equivalent to + // (= "" y) + Node empty_x_y = + d_nodeManager->mkNode(kind::AND, + d_nodeManager->mkNode(kind::EQUAL, empty, x), + d_nodeManager->mkNode(kind::EQUAL, empty, y)); + sameNormalForm(StringsEntail::inferEqsFromContains(empty, xy), empty_x_y); + + // inferEqsFromContains(x, (str.++ x y)) returns false + Node bxya = d_nodeManager->mkNode(kind::STRING_CONCAT, b, y, x, a); + sameNormalForm(StringsEntail::inferEqsFromContains(x, bxya), f); + + // inferEqsFromContains(x, y) returns null + Node n = StringsEntail::inferEqsFromContains(x, y); + ASSERT_TRUE(n.isNull()); + + // inferEqsFromContains(x, x) returns something equivalent to (= x x) + Node eq_x_x = d_nodeManager->mkNode(kind::EQUAL, 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_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a); + Node eq_repl_x = d_nodeManager->mkNode(kind::EQUAL, 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_nodeManager->mkNode(kind::EQUAL, x, repl); + sameNormalForm(StringsEntail::inferEqsFromContains(x, repl), eq_x_repl); +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_prefix_suffix) +{ + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node xx = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x); + Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a); + Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); + Node f = d_nodeManager->mkConst(false); + + // Same normal form for: + // + // (str.prefix (str.++ x y) x) + // + // (= y "") + Node p_xy = d_nodeManager->mkNode(kind::STRING_PREFIX, xy, x); + Node empty_y = d_nodeManager->mkNode(kind::EQUAL, y, empty); + sameNormalForm(p_xy, empty_y); + + // Same normal form for: + // + // (str.suffix (str.++ x x) x) + // + // (= x "") + Node p_xx = d_nodeManager->mkNode(kind::STRING_SUFFIX, xx, x); + Node empty_x = d_nodeManager->mkNode(kind::EQUAL, x, empty); + sameNormalForm(p_xx, empty_x); + + // (str.suffix x (str.++ x x "A")) ---> false + Node p_xxa = d_nodeManager->mkNode(kind::STRING_SUFFIX, xxa, x); + sameNormalForm(p_xxa, f); +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext) +{ + TypeNode strType = d_nodeManager->stringType(); + TypeNode intType = d_nodeManager->integerType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node aaa = d_nodeManager->mkConst(::CVC4::String("AAA")); + Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node ba = d_nodeManager->mkConst(::CVC4::String("BA")); + Node w = d_nodeManager->mkVar("w", strType); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node z = d_nodeManager->mkVar("z", strType); + Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a); + Node f = d_nodeManager->mkConst(false); + Node n = d_nodeManager->mkVar("n", intType); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node three = d_nodeManager->mkConst(Rational(3)); + + // Same normal form for: + // + // (= "" (str.replace "" x "B")) + // + // (not (= x "")) + Node empty_repl = d_nodeManager->mkNode( + kind::EQUAL, + empty, + d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, b)); + Node empty_x = d_nodeManager->mkNode( + kind::NOT, d_nodeManager->mkNode(kind::EQUAL, x, empty)); + sameNormalForm(empty_repl, empty_x); + + // Same normal form for: + // + // (= "" (str.replace x y (str.++ x x "A"))) + // + // (and (= x "") (not (= y ""))) + Node empty_repl_xaa = d_nodeManager->mkNode( + kind::EQUAL, + empty, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, xxa)); + Node empty_xy = d_nodeManager->mkNode( + kind::AND, + d_nodeManager->mkNode(kind::EQUAL, x, empty), + d_nodeManager->mkNode(kind::NOT, + d_nodeManager->mkNode(kind::EQUAL, y, empty))); + sameNormalForm(empty_repl_xaa, empty_xy); + + // (= "" (str.replace (str.++ x x "A") x y)) ---> false + Node empty_repl_xxaxy = d_nodeManager->mkNode( + kind::EQUAL, + empty, + d_nodeManager->mkNode(kind::STRING_STRREPL, xxa, x, y)); + Node eq_xxa_repl = d_nodeManager->mkNode( + kind::EQUAL, + xxa, + d_nodeManager->mkNode(kind::STRING_STRREPL, empty, y, x)); + sameNormalForm(empty_repl_xxaxy, f); + + // Same normal form for: + // + // (= "" (str.replace "A" x y)) + // + // (= "A" (str.replace "" y x)) + Node empty_repl_axy = d_nodeManager->mkNode( + kind::EQUAL, empty, d_nodeManager->mkNode(kind::STRING_STRREPL, a, x, y)); + Node eq_a_repl = d_nodeManager->mkNode( + kind::EQUAL, a, d_nodeManager->mkNode(kind::STRING_STRREPL, empty, y, x)); + sameNormalForm(empty_repl_axy, eq_a_repl); + + // Same normal form for: + // + // (= "" (str.replace x "A" "")) + // + // (str.prefix x "A") + Node empty_repl_a = d_nodeManager->mkNode( + kind::EQUAL, + empty, + d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, empty)); + Node prefix_a = d_nodeManager->mkNode(kind::STRING_PREFIX, x, a); + sameNormalForm(empty_repl_a, prefix_a); + + // Same normal form for: + // + // (= "" (str.substr x 1 2)) + // + // (<= (str.len x) 1) + Node empty_substr = d_nodeManager->mkNode( + kind::EQUAL, + empty, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three)); + Node leq_len_x = d_nodeManager->mkNode( + kind::LEQ, d_nodeManager->mkNode(kind::STRING_LENGTH, x), one); + sameNormalForm(empty_substr, leq_len_x); + + // Different normal form for: + // + // (= "" (str.substr x 0 n)) + // + // (<= n 0) + Node empty_substr_x = d_nodeManager->mkNode( + kind::EQUAL, + empty, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, n)); + Node leq_n = d_nodeManager->mkNode(kind::LEQ, n, zero); + differentNormalForms(empty_substr_x, leq_n); + + // Same normal form for: + // + // (= "" (str.substr "A" 0 n)) + // + // (<= n 0) + Node empty_substr_a = d_nodeManager->mkNode( + kind::EQUAL, + empty, + d_nodeManager->mkNode(kind::STRING_SUBSTR, a, zero, n)); + sameNormalForm(empty_substr_a, leq_n); + + // Same normal form for: + // + // (= (str.++ x x a) (str.replace y (str.++ x x a) y)) + // + // (= (str.++ x x a) y) + Node eq_xxa_repl_y = d_nodeManager->mkNode( + kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_STRREPL, y, xxa, y)); + Node eq_xxa_y = d_nodeManager->mkNode(kind::EQUAL, xxa, y); + sameNormalForm(eq_xxa_repl_y, eq_xxa_y); + + // (= (str.++ x x a) (str.replace (str.++ x x a) "A" "B")) ---> false + Node eq_xxa_repl_xxa = d_nodeManager->mkNode( + kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_STRREPL, xxa, a, b)); + sameNormalForm(eq_xxa_repl_xxa, f); + + // Same normal form for: + // + // (= (str.replace x "A" "B") "") + // + // (= x "") + Node eq_repl = d_nodeManager->mkNode( + kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b), empty); + Node eq_x = d_nodeManager->mkNode(kind::EQUAL, x, empty); + sameNormalForm(eq_repl, eq_x); + + { + // Same normal form for: + // + // (= (str.replace y "A" "B") "B") + // + // (= (str.replace y "B" "A") "A") + Node lhs = d_nodeManager->mkNode( + kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b), b); + Node rhs = d_nodeManager->mkNode( + kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a), a); + sameNormalForm(lhs, rhs); + } + + { + // Same normal form for: + // + // (= (str.++ x "A" y) (str.++ "A" "A" (str.substr "AAA" 0 n))) + // + // (= (str.++ y x) (str.++ (str.substr "AAA" 0 n) "A")) + Node lhs = d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_CONCAT, x, a, y), + d_nodeManager->mkNode( + kind::STRING_CONCAT, + a, + a, + d_nodeManager->mkNode(kind::STRING_SUBSTR, aaa, zero, n))); + Node rhs = d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_CONCAT, x, y), + d_nodeManager->mkNode( + kind::STRING_CONCAT, + d_nodeManager->mkNode(kind::STRING_SUBSTR, aaa, zero, n), + a)); + sameNormalForm(lhs, rhs); + } + + { + // Same normal form for: + // + // (= (str.++ "A" x) "A") + // + // (= x "") + Node lhs = d_nodeManager->mkNode( + kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, a, x), a); + Node rhs = d_nodeManager->mkNode(kind::EQUAL, x, empty); + sameNormalForm(lhs, rhs); + } + + { + // (= (str.++ x "A") "") ---> false + Node eq = d_nodeManager->mkNode( + kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, a), empty); + sameNormalForm(eq, f); + } + + { + // (= (str.++ x "B") "AAA") ---> false + Node eq = d_nodeManager->mkNode( + kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, b), aaa); + sameNormalForm(eq, f); + } + + { + // (= (str.++ x "AAA") "A") ---> false + Node eq = d_nodeManager->mkNode( + kind::EQUAL, d_nodeManager->mkNode(kind::STRING_CONCAT, x, aaa), a); + sameNormalForm(eq, f); + } + + { + // (= (str.++ "AAA" (str.substr "A" 0 n)) (str.++ x "B")) ---> false + Node eq = d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + aaa, + d_nodeManager->mkNode( + kind::STRING_CONCAT, + a, + a, + d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, n))), + d_nodeManager->mkNode(kind::STRING_CONCAT, x, b)); + sameNormalForm(eq, f); + } + + { + // (= (str.++ "A" (int.to.str n)) "A") -/-> false + Node eq = d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_CONCAT, + a, + d_nodeManager->mkNode(kind::STRING_ITOS, n)), + a); + differentNormalForms(eq, f); + } + + { + // (= (str.++ "A" x y) (str.++ x "B" z)) --> false + Node eq = d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_CONCAT, a, x, y), + d_nodeManager->mkNode(kind::STRING_CONCAT, x, b, z)); + sameNormalForm(eq, f); + } + + { + // (= (str.++ "B" x y) (str.++ x "AAA" z)) --> false + Node eq = d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_CONCAT, b, x, y), + d_nodeManager->mkNode(kind::STRING_CONCAT, x, aaa, z)); + sameNormalForm(eq, f); + } + + { + Node xrepl = d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b); + + // Same normal form for: + // + // (= (str.++ "B" (str.replace x "A" "B") z y w) + // (str.++ z x "BA" z)) + // + // (and (= (str.++ "B" (str.replace x "A" "B") z) + // (str.++ z x "B")) + // (= (str.++ y w) (str.++ "A" z))) + Node lhs = d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_CONCAT, b, xrepl, z, y, w), + d_nodeManager->mkNode(kind::STRING_CONCAT, z, x, ba, z)); + Node rhs = d_nodeManager->mkNode( + kind::AND, + d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_CONCAT, b, xrepl, z), + d_nodeManager->mkNode(kind::STRING_CONCAT, z, x, b)), + d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::STRING_CONCAT, y, w), + d_nodeManager->mkNode(kind::STRING_CONCAT, a, z))); + sameNormalForm(lhs, rhs); + } +} + +TEST_F(TestTheoryWhiteSequencesRewriter, strip_constant_endpoints) +{ + TypeNode intType = d_nodeManager->integerType(); + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(::CVC4::String("")); + Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); + Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); + Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); + Node bc = d_nodeManager->mkConst(::CVC4::String("BC")); + Node c = d_nodeManager->mkConst(::CVC4::String("C")); + Node cd = d_nodeManager->mkConst(::CVC4::String("CD")); + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node n = d_nodeManager->mkVar("n", intType); + + { + // stripConstantEndpoints({ "" }, { "A" }, {}, {}, 0) ---> false + std::vector n1 = {empty}; + std::vector n2 = {a}; + std::vector nb; + std::vector ne; + bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0); + ASSERT_FALSE(res); + } + + { + // stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0) + // ---> false + std::vector n1 = {a}; + std::vector n2 = {a, d_nodeManager->mkNode(kind::STRING_ITOS, n)}; + std::vector nb; + std::vector ne; + bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0); + ASSERT_FALSE(res); + } + + { + // stripConstantEndpoints({ "ABCD" }, { "C" }, {}, {}, 1) + // ---> true + // n1 is updated to { "CD" } + // nb is updated to { "AB" } + std::vector n1 = {abcd}; + std::vector n2 = {c}; + std::vector nb; + std::vector ne; + std::vector n1r = {cd}; + std::vector nbr = {ab}; + bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1); + ASSERT_TRUE(res); + ASSERT_EQ(n1, n1r); + ASSERT_EQ(nb, nbr); + } + + { + // stripConstantEndpoints({ "ABC", x }, { "CD" }, {}, {}, 1) + // ---> true + // n1 is updated to { "C", x } + // nb is updated to { "AB" } + std::vector n1 = {abc, x}; + std::vector n2 = {cd}; + std::vector nb; + std::vector ne; + std::vector n1r = {c, x}; + std::vector nbr = {ab}; + bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1); + ASSERT_TRUE(res); + ASSERT_EQ(n1, n1r); + ASSERT_EQ(nb, nbr); + } + + { + // stripConstantEndpoints({ "ABC" }, { "A" }, {}, {}, -1) + // ---> true + // n1 is updated to { "A" } + // nb is updated to { "BC" } + std::vector n1 = {abc}; + std::vector n2 = {a}; + std::vector nb; + std::vector ne; + std::vector n1r = {a}; + std::vector ner = {bc}; + bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1); + ASSERT_TRUE(res); + ASSERT_EQ(n1, n1r); + ASSERT_EQ(ne, ner); + } + + { + // stripConstantEndpoints({ x, "ABC" }, { y, "A" }, {}, {}, -1) + // ---> true + // n1 is updated to { x, "A" } + // nb is updated to { "BC" } + std::vector n1 = {x, abc}; + std::vector n2 = {y, a}; + std::vector nb; + std::vector ne; + std::vector n1r = {x, a}; + std::vector ner = {bc}; + bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1); + ASSERT_TRUE(res); + ASSERT_EQ(n1, n1r); + ASSERT_EQ(ne, ner); + } +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership) +{ + TypeNode strType = d_nodeManager->stringType(); + + std::vector vec_empty; + Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); + Node re_abc = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, abc); + Node x = d_nodeManager->mkVar("x", strType); + + { + // Same normal form for: + // + // (str.in.re x (re.++ (re.* re.allchar) + // (re.* re.allchar) + // (str.to.re "ABC") + // (re.* re.allchar))) + // + // (str.contains x "ABC") + Node sig_star = d_nodeManager->mkNode( + kind::REGEXP_STAR, + d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty)); + Node lhs = d_nodeManager->mkNode( + kind::STRING_IN_REGEXP, + x, + d_nodeManager->mkNode( + kind::REGEXP_CONCAT, sig_star, sig_star, re_abc, sig_star)); + Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc); + sameNormalForm(lhs, rhs); + } + + { + // Different normal forms for: + // + // (str.in.re x (re.++ (re.* re.allchar) (str.to.re "ABC"))) + // + // (str.contains x "ABC") + Node sig_star = d_nodeManager->mkNode( + kind::REGEXP_STAR, + d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty)); + Node lhs = d_nodeManager->mkNode( + kind::STRING_IN_REGEXP, + x, + d_nodeManager->mkNode(kind::REGEXP_CONCAT, sig_star, re_abc)); + Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc); + differentNormalForms(lhs, rhs); + } +} + +TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_regexp_concat) +{ + TypeNode strType = d_nodeManager->stringType(); + + std::vector emptyArgs; + Node x = d_nodeManager->mkVar("x", strType); + Node y = d_nodeManager->mkVar("y", strType); + Node allStar = d_nodeManager->mkNode( + kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyArgs)); + Node xReg = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, x); + Node yReg = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, y); + + { + // In normal form: + // + // (re.++ (re.* re.allchar) (re.union (str.to.re x) (str.to.re y))) + Node n = d_nodeManager->mkNode( + kind::REGEXP_CONCAT, + allStar, + d_nodeManager->mkNode(kind::REGEXP_UNION, xReg, yReg)); + inNormalForm(n); + } + + { + // In normal form: + // + // (re.++ (str.to.re x) (re.* re.allchar)) + Node n = d_nodeManager->mkNode(kind::REGEXP_CONCAT, xReg, allStar); + inNormalForm(n); + } +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h deleted file mode 100644 index 09cb925a3..000000000 --- a/test/unit/theory/sequences_rewriter_white.h +++ /dev/null @@ -1,1795 +0,0 @@ -/********************* */ -/*! \file sequences_rewriter_white.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Unit tests for the strings/sequences rewriter - ** - ** Unit tests for the strings/sequences rewriter. - **/ - -#include - -#include -#include -#include - -#include "expr/node.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#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 "theory/strings/strings_rewriter.h" - -using namespace CVC4; -using namespace CVC4::smt; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::theory::strings; - -class SequencesRewriterWhite : public CxxTest::TestSuite -{ - public: - SequencesRewriterWhite() {} - - void setUp() override - { - Options opts; - opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager; - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm, &opts); - d_scope = new SmtScope(d_smt); - d_smt->finishInit(); - d_rewriter = new ExtendedRewriter(true); - } - - void tearDown() override - { - delete d_rewriter; - delete d_scope; - delete d_smt; - delete d_em; - } - - void inNormalForm(Node t) - { - Node res_t = d_rewriter->extendedRewrite(t); - - std::cout << std::endl; - std::cout << t << " ---> " << res_t << std::endl; - TS_ASSERT_EQUALS(t, res_t); - } - - void sameNormalForm(Node t1, Node t2) - { - Node res_t1 = d_rewriter->extendedRewrite(t1); - Node res_t2 = d_rewriter->extendedRewrite(t2); - - std::cout << std::endl; - std::cout << t1 << " ---> " << res_t1 << std::endl; - std::cout << t2 << " ---> " << res_t2 << std::endl; - TS_ASSERT_EQUALS(res_t1, res_t2); - } - - void differentNormalForms(Node t1, Node t2) - { - Node res_t1 = d_rewriter->extendedRewrite(t1); - Node res_t2 = d_rewriter->extendedRewrite(t2); - - std::cout << std::endl; - std::cout << t1 << " ---> " << res_t1 << std::endl; - std::cout << t2 << " ---> " << res_t2 << std::endl; - TS_ASSERT_DIFFERS(res_t1, res_t2); - } - - void testCheckEntailLengthOne() - { - TypeNode intType = d_nm->integerType(); - TypeNode strType = d_nm->stringType(); - - Node a = d_nm->mkConst(::CVC4::String("A")); - Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); - Node aaad = d_nm->mkConst(::CVC4::String("AAAD")); - Node b = d_nm->mkConst(::CVC4::String("B")); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node negOne = d_nm->mkConst(Rational(-1)); - Node zero = d_nm->mkConst(Rational(0)); - Node one = d_nm->mkConst(Rational(1)); - Node two = d_nm->mkConst(Rational(2)); - Node three = d_nm->mkConst(Rational(3)); - Node i = d_nm->mkVar("i", intType); - - TS_ASSERT(StringsEntail::checkLengthOne(a)); - TS_ASSERT(StringsEntail::checkLengthOne(a, true)); - - Node substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one); - 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(StringsEntail::checkLengthOne(substr)); - TS_ASSERT(StringsEntail::checkLengthOne(substr, true)); - - substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, two); - TS_ASSERT(!StringsEntail::checkLengthOne(substr)); - TS_ASSERT(!StringsEntail::checkLengthOne(substr, true)); - } - - void testCheckEntailArith() - { - TypeNode intType = d_nm->integerType(); - TypeNode strType = d_nm->stringType(); - - Node z = d_nm->mkVar("z", strType); - Node n = d_nm->mkVar("n", intType); - Node one = d_nm->mkConst(Rational(1)); - - // 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(ArithEntail::check(one, substr_z)); - - // (str.len (str.substr z n 1)) >= 1 ---> false - TS_ASSERT(!ArithEntail::check(substr_z, one)); - } - - void testCheckEntailArithWithAssumption() - { - TypeNode intType = d_nm->integerType(); - TypeNode strType = d_nm->stringType(); - - Node x = d_nm->mkVar("x", intType); - Node y = d_nm->mkVar("y", strType); - Node z = d_nm->mkVar("z", intType); - - Node zero = d_nm->mkConst(Rational(0)); - Node one = d_nm->mkConst(Rational(1)); - - Node empty = d_nm->mkConst(::CVC4::String("")); - Node a = d_nm->mkConst(::CVC4::String("A")); - - Node slen_y = d_nm->mkNode(kind::STRING_LENGTH, y); - Node x_plus_slen_y = d_nm->mkNode(kind::PLUS, x, slen_y); - 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 - TS_ASSERT(ArithEntail::checkWithAssumption( - x_plus_slen_y_eq_zero, zero, x, false)); - - // x + (str.len y) = 0 |= 0 > x --> false - 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(!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(ArithEntail::checkWithAssumption( - 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( - ArithEntail::checkWithAssumption(x_plus_five_lt_six, zero, x, false)); - - // x + 5 < 6 |= 0 > x --> false - 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(ArithEntail::checkWithAssumption( - x_plus_five_lt_five, neg_x, zero, false)); - - // x + 5 < 5 |= 0 > x --> true - 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(ArithEntail::checkWithAssumption( - assm, - x, - d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_ITOS, x)), - false)); - } - - void testRewriteSubstr() - { - 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 b = d_nm->mkConst(::CVC4::String("B")); - Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); - Node negone = d_nm->mkConst(Rational(-1)); - Node zero = d_nm->mkConst(Rational(0)); - Node one = d_nm->mkConst(Rational(1)); - Node two = d_nm->mkConst(Rational(2)); - Node three = d_nm->mkConst(Rational(3)); - - Node s = d_nm->mkVar("s", strType); - Node s2 = d_nm->mkVar("s2", strType); - Node x = d_nm->mkVar("x", intType); - Node y = d_nm->mkVar("y", intType); - - // (str.substr "A" x x) --> "" - Node n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, x); - Node res = StringsRewriter(nullptr).rewriteSubstr(n); - TS_ASSERT_EQUALS(res, empty); - - // (str.substr "A" (+ x 1) x) -> "" - n = d_nm->mkNode(kind::STRING_SUBSTR, - a, - d_nm->mkNode(kind::PLUS, x, d_nm->mkConst(Rational(1))), - x); - res = StringsRewriter(nullptr).rewriteSubstr(n); - TS_ASSERT_EQUALS(res, empty); - - // (str.substr "A" (+ x (str.len s2)) x) -> "" - n = d_nm->mkNode( - kind::STRING_SUBSTR, - a, - d_nm->mkNode(kind::PLUS, x, d_nm->mkNode(kind::STRING_LENGTH, s)), - x); - res = StringsRewriter(nullptr).rewriteSubstr(n); - TS_ASSERT_EQUALS(res, empty); - - // (str.substr "A" x y) -> (str.substr "A" x y) - n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y); - res = StringsRewriter(nullptr).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 = StringsRewriter(nullptr).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 = StringsRewriter(nullptr).rewriteSubstr(n); - TS_ASSERT_EQUALS(res, n); - - // (str.substr (str.substr s x x) x x) -> "" - n = d_nm->mkNode( - kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_SUBSTR, s, x, x), x, x); - sameNormalForm(n, empty); - - // Same normal form for: - // - // (str.substr (str.replace "" s "B") x x) - // - // (str.replace "" s (str.substr "B" x x))) - Node lhs = d_nm->mkNode(kind::STRING_SUBSTR, - d_nm->mkNode(kind::STRING_STRREPL, empty, s, b), - x, - x); - Node rhs = d_nm->mkNode(kind::STRING_STRREPL, - empty, - s, - d_nm->mkNode(kind::STRING_SUBSTR, b, x, x)); - sameNormalForm(lhs, rhs); - - // Same normal form: - // - // (str.substr (str.replace s "A" "B") 0 x) - // - // (str.replace (str.substr s 0 x) "A" "B") - Node substr_repl = d_nm->mkNode(kind::STRING_SUBSTR, - d_nm->mkNode(kind::STRING_STRREPL, s, a, b), - zero, - x); - Node repl_substr = - d_nm->mkNode(kind::STRING_STRREPL, - d_nm->mkNode(kind::STRING_SUBSTR, s, zero, x), - a, - b); - sameNormalForm(substr_repl, repl_substr); - - // Same normal form: - // - // (str.substr (str.replace s (str.substr (str.++ s2 "A") 0 1) "B") 0 x) - // - // (str.replace (str.substr s 0 x) (str.substr (str.++ s2 "A") 0 1) "B") - Node substr_y = d_nm->mkNode(kind::STRING_SUBSTR, - d_nm->mkNode(kind::STRING_CONCAT, s2, a), - zero, - one); - substr_repl = - d_nm->mkNode(kind::STRING_SUBSTR, - d_nm->mkNode(kind::STRING_STRREPL, s, substr_y, b), - zero, - x); - repl_substr = d_nm->mkNode(kind::STRING_STRREPL, - d_nm->mkNode(kind::STRING_SUBSTR, s, zero, x), - substr_y, - b); - sameNormalForm(substr_repl, repl_substr); - - // (str.substr (str.int.to.str x) x x) ---> empty - Node substr_itos = d_nm->mkNode( - kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_ITOS, x), x, x); - sameNormalForm(substr_itos, empty); - - // (str.substr s (* (- 1) (str.len s)) 1) ---> empty - Node substr = d_nm->mkNode( - kind::STRING_SUBSTR, - s, - d_nm->mkNode(kind::MULT, negone, d_nm->mkNode(kind::STRING_LENGTH, s)), - one); - sameNormalForm(substr, empty); - } - - 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); - sameNormalForm(repl_a, 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); - sameNormalForm(repl_a, 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); - sameNormalForm(a_substr_repl, 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); - sameNormalForm(repl_substr_a, a_repl_substr); - } - - void testLengthPreserveRewrite() - { - TypeNode intType = d_nm->integerType(); - TypeNode strType = d_nm->stringType(); - - Node empty = d_nm->mkConst(::CVC4::String("")); - Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); - Node f = d_nm->mkConst(::CVC4::String("F")); - Node gh = d_nm->mkConst(::CVC4::String("GH")); - Node ij = d_nm->mkConst(::CVC4::String("IJ")); - - 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 length preserving rewrite for: - // - // (str.++ "ABCD" (str.++ x x)) - // - // (str.++ "GH" (str.repl "GH" "IJ") "IJ") - Node concat1 = d_nm->mkNode( - kind::STRING_CONCAT, abcd, d_nm->mkNode(kind::STRING_CONCAT, x, x)); - Node concat2 = d_nm->mkNode(kind::STRING_CONCAT, - gh, - x, - d_nm->mkNode(kind::STRING_STRREPL, x, gh, ij), - ij); - Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1); - Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2); - TS_ASSERT_EQUALS(res_concat1, res_concat2); - } - - void testRewriteIndexOf() - { - TypeNode intType = d_nm->integerType(); - TypeNode strType = d_nm->stringType(); - - Node a = d_nm->mkConst(::CVC4::String("A")); - Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); - Node aaad = d_nm->mkConst(::CVC4::String("AAAD")); - Node b = d_nm->mkConst(::CVC4::String("B")); - Node c = d_nm->mkConst(::CVC4::String("C")); - Node ccc = d_nm->mkConst(::CVC4::String("CCC")); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node negOne = d_nm->mkConst(Rational(-1)); - Node zero = d_nm->mkConst(Rational(0)); - Node one = d_nm->mkConst(Rational(1)); - Node two = d_nm->mkConst(Rational(2)); - Node three = d_nm->mkConst(Rational(3)); - Node i = d_nm->mkVar("i", intType); - Node j = d_nm->mkVar("j", intType); - - // Same normal form for: - // - // (str.to.int (str.indexof "A" x 1)) - // - // (str.to.int (str.indexof "B" x 1)) - Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, two); - Node itos_a_idof_x = d_nm->mkNode(kind::STRING_ITOS, a_idof_x); - Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, two); - Node itos_b_idof_x = d_nm->mkNode(kind::STRING_ITOS, b_idof_x); - sameNormalForm(itos_a_idof_x, itos_b_idof_x); - - // Same normal form for: - // - // (str.indexof (str.++ "ABCD" x) y 3) - // - // (str.indexof (str.++ "AAAD" x) y 3) - Node idof_abcd = d_nm->mkNode(kind::STRING_STRIDOF, - d_nm->mkNode(kind::STRING_CONCAT, abcd, x), - y, - three); - Node idof_aaad = d_nm->mkNode(kind::STRING_STRIDOF, - d_nm->mkNode(kind::STRING_CONCAT, aaad, x), - y, - three); - sameNormalForm(idof_abcd, idof_aaad); - - // (str.indexof (str.substr x 1 i) "A" i) ---> -1 - Node idof_substr = - d_nm->mkNode(kind::STRING_STRIDOF, - d_nm->mkNode(kind::STRING_SUBSTR, x, one, i), - a, - i); - sameNormalForm(idof_substr, negOne); - - { - // Same normal form for: - // - // (str.indexof (str.++ "B" (str.substr "CCC" i j) x "A") "A" 0) - // - // (+ 1 (str.len (str.substr "CCC" i j)) - // (str.indexof (str.++ "A" x y) "A" 0)) - Node lhs = d_nm->mkNode( - kind::STRING_STRIDOF, - d_nm->mkNode(kind::STRING_CONCAT, - b, - d_nm->mkNode(kind::STRING_SUBSTR, ccc, i, j), - x, - a), - a, - zero); - Node rhs = d_nm->mkNode( - kind::PLUS, - one, - d_nm->mkNode(kind::STRING_LENGTH, - d_nm->mkNode(kind::STRING_SUBSTR, ccc, i, j)), - d_nm->mkNode(kind::STRING_STRIDOF, - d_nm->mkNode(kind::STRING_CONCAT, x, a), - a, - zero)); - sameNormalForm(lhs, rhs); - } - - { - // Same normal form for: - // - // (str.indexof (str.++ "B" "C" "A" x y) "A" 0) - // - // (+ 2 (str.indexof (str.++ "A" x y) "A" 0)) - Node lhs = d_nm->mkNode(kind::STRING_STRIDOF, - d_nm->mkNode(kind::STRING_CONCAT, b, c, a, x, y), - a, - zero); - Node rhs = - d_nm->mkNode(kind::PLUS, - two, - d_nm->mkNode(kind::STRING_STRIDOF, - d_nm->mkNode(kind::STRING_CONCAT, a, x, y), - a, - zero)); - sameNormalForm(lhs, rhs); - } - } - - void testRewriteReplace() - { - 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 ab = d_nm->mkConst(::CVC4::String("AB")); - Node b = d_nm->mkConst(::CVC4::String("B")); - Node c = d_nm->mkConst(::CVC4::String("C")); - Node d = d_nm->mkConst(::CVC4::String("D")); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node z = d_nm->mkVar("z", strType); - Node zero = d_nm->mkConst(Rational(0)); - Node one = d_nm->mkConst(Rational(1)); - Node n = d_nm->mkVar("n", intType); - - // (str.replace (str.replace x "B" x) x "A") --> - // (str.replace (str.replace x "B" "A") x "A") - Node repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - d_nm->mkNode(kind::STRING_STRREPL, x, b, x), - x, - a); - Node repl_repl_short = - d_nm->mkNode(kind::STRING_STRREPL, - d_nm->mkNode(kind::STRING_STRREPL, x, b, a), - x, - a); - sameNormalForm(repl_repl, repl_repl_short); - - // (str.replace "A" (str.replace "B", x, "C") "D") --> "A" - repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - a, - d_nm->mkNode(kind::STRING_STRREPL, b, x, c), - d); - sameNormalForm(repl_repl, a); - - // (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A" - repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - a, - d_nm->mkNode(kind::STRING_STRREPL, b, x, a), - d); - differentNormalForms(repl_repl, a); - - // Same normal form for: - // - // (str.replace x (str.++ x y z) y) - // - // (str.replace x (str.++ x y z) z) - Node xyz = d_nm->mkNode(kind::STRING_CONCAT, x, y, z); - Node repl_x_xyz = d_nm->mkNode(kind::STRING_STRREPL, x, xyz, y); - Node repl_x_zyx = d_nm->mkNode(kind::STRING_STRREPL, x, xyz, z); - sameNormalForm(repl_x_xyz, repl_x_zyx); - - // (str.replace "" (str.++ x x) x) --> "" - Node repl_empty_xx = d_nm->mkNode(kind::STRING_STRREPL, - empty, - d_nm->mkNode(kind::STRING_CONCAT, x, x), - x); - sameNormalForm(repl_empty_xx, empty); - - // (str.replace "AB" (str.++ x "A") x) --> (str.replace "AB" (str.++ x "A") - // "") - Node repl_ab_xa_x = d_nm->mkNode(kind::STRING_STRREPL, - d_nm->mkNode(kind::STRING_CONCAT, a, b), - d_nm->mkNode(kind::STRING_CONCAT, x, a), - x); - Node repl_ab_xa_e = d_nm->mkNode(kind::STRING_STRREPL, - d_nm->mkNode(kind::STRING_CONCAT, a, b), - d_nm->mkNode(kind::STRING_CONCAT, x, a), - empty); - sameNormalForm(repl_ab_xa_x, repl_ab_xa_e); - - // (str.replace "AB" (str.++ x "A") x) -/-> (str.replace "AB" (str.++ "A" x) - // "") - Node repl_ab_ax_e = d_nm->mkNode(kind::STRING_STRREPL, - d_nm->mkNode(kind::STRING_CONCAT, a, b), - d_nm->mkNode(kind::STRING_CONCAT, a, x), - empty); - differentNormalForms(repl_ab_ax_e, repl_ab_xa_e); - - // (str.replace "" (str.replace y x "A") y) ---> "" - repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - empty, - d_nm->mkNode(kind::STRING_STRREPL, y, x, a), - y); - sameNormalForm(repl_repl, empty); - - // (str.replace "" (str.replace x y x) x) ---> "" - repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - empty, - d_nm->mkNode(kind::STRING_STRREPL, x, y, x), - x); - sameNormalForm(repl_repl, empty); - - // (str.replace "" (str.substr x 0 1) x) ---> "" - repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - empty, - d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one), - x); - sameNormalForm(repl_repl, empty); - - // Same normal form for: - // - // (str.replace "" (str.replace x y x) y) - // - // (str.replace "" x y) - repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - empty, - d_nm->mkNode(kind::STRING_STRREPL, x, y, x), - y); - Node repl = d_nm->mkNode(kind::STRING_STRREPL, empty, x, y); - sameNormalForm(repl_repl, repl); - - // Same normal form: - // - // (str.replace "B" (str.replace x "A" "B") "B") - // - // (str.replace "B" x "B")) - repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - b, - d_nm->mkNode(kind::STRING_STRREPL, x, a, b), - b); - repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b); - sameNormalForm(repl_repl, repl); - - // Different normal forms for: - // - // (str.replace "B" (str.replace "" x "A") "B") - // - // (str.replace "B" x "B") - repl_repl = d_nm->mkNode(kind::STRING_STRREPL, - b, - d_nm->mkNode(kind::STRING_STRREPL, empty, x, a), - b); - repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b); - differentNormalForms(repl_repl, repl); - - { - // Same normal form: - // - // (str.replace (str.++ "AB" x) "C" y) - // - // (str.++ "AB" (str.replace x "C" y)) - Node lhs = d_nm->mkNode( - kind::STRING_STRREPL, d_nm->mkNode(kind::STRING_CONCAT, ab, x), c, y); - Node rhs = d_nm->mkNode( - kind::STRING_CONCAT, ab, d_nm->mkNode(kind::STRING_STRREPL, x, c, y)); - sameNormalForm(lhs, rhs); - } - } - - void testRewriteReplaceRe() - { - TypeNode intType = d_nm->integerType(); - TypeNode strType = d_nm->stringType(); - - std::vector emptyVec; - Node sigStar = d_nm->mkNode(kind::REGEXP_STAR, - d_nm->mkNode(kind::REGEXP_SIGMA, emptyVec)); - Node foo = d_nm->mkConst(String("FOO")); - Node a = d_nm->mkConst(String("A")); - Node b = d_nm->mkConst(String("B")); - Node re = d_nm->mkNode(kind::REGEXP_CONCAT, - d_nm->mkNode(kind::STRING_TO_REGEXP, a), - sigStar, - d_nm->mkNode(kind::STRING_TO_REGEXP, b)); - - // Same normal form: - // - // (str.replace_re - // "AZZZB" - // (re.++ (str.to_re "A") re.all (str.to_re "B")) - // "FOO") - // - // "FOO" - { - Node t = d_nm->mkNode( - kind::STRING_REPLACE_RE, d_nm->mkConst(String("AZZZB")), re, foo); - Node res = d_nm->mkConst(::CVC4::String("FOO")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "ZAZZZBZZB" - // (re.++ (str.to_re "A") re.all (str.to_re "B")) - // "FOO") - // - // "ZFOOZZB" - { - Node t = d_nm->mkNode( - kind::STRING_REPLACE_RE, d_nm->mkConst(String("ZAZZZBZZB")), re, foo); - Node res = d_nm->mkConst(::CVC4::String("ZFOOZZB")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "ZAZZZBZAZB" - // (re.++ (str.to_re "A") re.all (str.to_re "B")) - // "FOO") - // - // "ZFOOZAZB" - { - Node t = d_nm->mkNode(kind::STRING_REPLACE_RE, - d_nm->mkConst(String("ZAZZZBZAZB")), - re, - foo); - Node res = d_nm->mkConst(::CVC4::String("ZFOOZAZB")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "ZZZ" - // (re.++ (str.to_re "A") re.all (str.to_re "B")) - // "FOO") - // - // "ZZZ" - { - Node t = d_nm->mkNode( - kind::STRING_REPLACE_RE, d_nm->mkConst(String("ZZZ")), re, foo); - Node res = d_nm->mkConst(::CVC4::String("ZZZ")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "ZZZ" - // re.all - // "FOO") - // - // "FOOZZZ" - { - Node t = d_nm->mkNode( - kind::STRING_REPLACE_RE, d_nm->mkConst(String("ZZZ")), sigStar, foo); - Node res = d_nm->mkConst(::CVC4::String("FOOZZZ")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "" - // re.all - // "FOO") - // - // "FOO" - { - Node t = d_nm->mkNode( - kind::STRING_REPLACE_RE, d_nm->mkConst(String("")), sigStar, foo); - Node res = d_nm->mkConst(::CVC4::String("FOO")); - sameNormalForm(t, res); - } - } - - void testRewriteReplaceReAll() - { - TypeNode intType = d_nm->integerType(); - TypeNode strType = d_nm->stringType(); - - std::vector emptyVec; - Node sigStar = d_nm->mkNode(kind::REGEXP_STAR, - d_nm->mkNode(kind::REGEXP_SIGMA, emptyVec)); - Node foo = d_nm->mkConst(String("FOO")); - Node a = d_nm->mkConst(String("A")); - Node b = d_nm->mkConst(String("B")); - Node re = d_nm->mkNode(kind::REGEXP_CONCAT, - d_nm->mkNode(kind::STRING_TO_REGEXP, a), - sigStar, - d_nm->mkNode(kind::STRING_TO_REGEXP, b)); - - // Same normal form: - // - // (str.replace_re - // "AZZZB" - // (re.++ (str.to_re "A") re.all (str.to_re "B")) - // "FOO") - // - // "FOO" - { - Node t = d_nm->mkNode( - kind::STRING_REPLACE_RE_ALL, d_nm->mkConst(String("AZZZB")), re, foo); - Node res = d_nm->mkConst(::CVC4::String("FOO")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "ZAZZZBZZB" - // (re.++ (str.to_re "A") re.all (str.to_re "B")) - // "FOO") - // - // "ZFOOZZB" - { - Node t = d_nm->mkNode(kind::STRING_REPLACE_RE_ALL, - d_nm->mkConst(String("ZAZZZBZZB")), - re, - foo); - Node res = d_nm->mkConst(::CVC4::String("ZFOOZZB")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "ZAZZZBZAZB" - // (re.++ (str.to_re "A") re.all (str.to_re "B")) - // "FOO") - // - // "ZFOOZFOO" - { - Node t = d_nm->mkNode(kind::STRING_REPLACE_RE_ALL, - d_nm->mkConst(String("ZAZZZBZAZB")), - re, - foo); - Node res = d_nm->mkConst(::CVC4::String("ZFOOZFOO")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "ZZZ" - // (re.++ (str.to_re "A") re.all (str.to_re "B")) - // "FOO") - // - // "ZZZ" - { - Node t = d_nm->mkNode( - kind::STRING_REPLACE_RE_ALL, d_nm->mkConst(String("ZZZ")), re, foo); - Node res = d_nm->mkConst(::CVC4::String("ZZZ")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "ZZZ" - // re.all - // "FOO") - // - // "FOOFOOFOO" - { - Node t = d_nm->mkNode(kind::STRING_REPLACE_RE_ALL, - d_nm->mkConst(String("ZZZ")), - sigStar, - foo); - Node res = d_nm->mkConst(::CVC4::String("FOOFOOFOO")); - sameNormalForm(t, res); - } - - // Same normal form: - // - // (str.replace_re - // "" - // re.all - // "FOO") - // - // "" - { - Node t = d_nm->mkNode( - kind::STRING_REPLACE_RE_ALL, d_nm->mkConst(String("")), sigStar, foo); - Node res = d_nm->mkConst(::CVC4::String("")); - sameNormalForm(t, res); - } - } - - void testRewriteContains() - { - 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 ab = d_nm->mkConst(::CVC4::String("AB")); - Node b = d_nm->mkConst(::CVC4::String("B")); - Node c = d_nm->mkConst(::CVC4::String("C")); - Node e = d_nm->mkConst(::CVC4::String("E")); - Node h = d_nm->mkConst(::CVC4::String("H")); - Node j = d_nm->mkConst(::CVC4::String("J")); - Node p = d_nm->mkConst(::CVC4::String("P")); - Node abc = d_nm->mkConst(::CVC4::String("ABC")); - Node def = d_nm->mkConst(::CVC4::String("DEF")); - Node ghi = d_nm->mkConst(::CVC4::String("GHI")); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y); - Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x); - Node z = d_nm->mkVar("z", strType); - Node n = d_nm->mkVar("n", intType); - Node m = d_nm->mkVar("m", intType); - Node one = d_nm->mkConst(Rational(1)); - Node two = d_nm->mkConst(Rational(2)); - Node three = d_nm->mkConst(Rational(3)); - Node four = d_nm->mkConst(Rational(4)); - Node t = d_nm->mkConst(true); - Node f = d_nm->mkConst(false); - - // Same normal form for: - // - // (str.replace "A" (str.substr x 1 3) y z) - // - // (str.replace "A" (str.substr x 1 4) y z) - Node substr_3 = - d_nm->mkNode(kind::STRING_STRREPL, - a, - d_nm->mkNode(kind::STRING_SUBSTR, x, one, three), - z); - Node substr_4 = - d_nm->mkNode(kind::STRING_STRREPL, - a, - d_nm->mkNode(kind::STRING_SUBSTR, x, one, four), - z); - sameNormalForm(substr_3, substr_4); - - // Same normal form for: - // - // (str.replace "A" (str.++ y (str.substr x 1 3)) y z) - // - // (str.replace "A" (str.++ y (str.substr x 1 4)) y z) - Node concat_substr_3 = d_nm->mkNode( - kind::STRING_STRREPL, - a, - d_nm->mkNode(kind::STRING_CONCAT, - y, - d_nm->mkNode(kind::STRING_SUBSTR, x, one, three)), - z); - Node concat_substr_4 = d_nm->mkNode( - kind::STRING_STRREPL, - a, - d_nm->mkNode(kind::STRING_CONCAT, - y, - d_nm->mkNode(kind::STRING_SUBSTR, x, one, four)), - z); - sameNormalForm(concat_substr_3, concat_substr_4); - - // (str.contains "A" (str.++ a (str.replace "B", x, "C")) --> false - Node ctn_repl = - d_nm->mkNode(kind::STRING_STRCTN, - a, - d_nm->mkNode(kind::STRING_CONCAT, - a, - d_nm->mkNode(kind::STRING_STRREPL, b, x, c))); - sameNormalForm(ctn_repl, f); - - // (str.contains x (str.++ x x)) --> (= x "") - Node x_cnts_x_x = d_nm->mkNode( - kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_CONCAT, x, x)); - sameNormalForm(x_cnts_x_x, d_nm->mkNode(kind::EQUAL, x, empty)); - - // Same normal form for: - // - // (str.contains (str.++ y x) (str.++ x z y)) - // - // (and (str.contains (str.++ y x) (str.++ x y)) (= z "")) - Node yx_cnts_xzy = d_nm->mkNode( - kind::STRING_STRCTN, yx, d_nm->mkNode(kind::STRING_CONCAT, x, z, y)); - Node yx_cnts_xy = d_nm->mkNode(kind::AND, - d_nm->mkNode(kind::EQUAL, z, empty), - d_nm->mkNode(kind::STRING_STRCTN, yx, xy)); - sameNormalForm(yx_cnts_xzy, yx_cnts_xy); - - // Same normal form for: - // - // (str.contains (str.substr x n (str.len y)) y) - // - // (= (str.substr x n (str.len y)) y) - Node ctn_substr = d_nm->mkNode( - kind::STRING_STRCTN, - d_nm->mkNode( - kind::STRING_SUBSTR, x, n, d_nm->mkNode(kind::STRING_LENGTH, y)), - y); - Node substr_eq = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::STRING_SUBSTR, x, n, d_nm->mkNode(kind::STRING_LENGTH, y)), - y); - sameNormalForm(ctn_substr, substr_eq); - - // Same normal form for: - // - // (str.contains x (str.replace y x y)) - // - // (str.contains x y) - Node ctn_repl_y_x_y = d_nm->mkNode( - kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_STRREPL, y, x, y)); - Node ctn_x_y = d_nm->mkNode(kind::STRING_STRCTN, x, y); - sameNormalForm(ctn_repl_y_x_y, ctn_repl_y_x_y); - - // Same normal form for: - // - // (str.contains x (str.replace x y x)) - // - // (= x (str.replace x y x)) - Node ctn_repl_self = d_nm->mkNode( - kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_STRREPL, x, y, x)); - Node eq_repl = d_nm->mkNode( - kind::EQUAL, x, d_nm->mkNode(kind::STRING_STRREPL, x, y, x)); - sameNormalForm(ctn_repl_self, eq_repl); - - // (str.contains x (str.++ "A" (str.replace x y x))) ---> false - Node ctn_repl_self_f = - d_nm->mkNode(kind::STRING_STRCTN, - x, - d_nm->mkNode(kind::STRING_CONCAT, - a, - d_nm->mkNode(kind::STRING_STRREPL, x, y, x))); - sameNormalForm(ctn_repl_self_f, f); - - // Same normal form for: - // - // (str.contains x (str.replace "" x y)) - // - // (= "" (str.replace "" x y)) - Node ctn_repl_empty = - d_nm->mkNode(kind::STRING_STRCTN, - x, - d_nm->mkNode(kind::STRING_STRREPL, empty, x, y)); - Node eq_repl_empty = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, empty, x, y)); - sameNormalForm(ctn_repl_empty, eq_repl_empty); - - // Same normal form for: - // - // (str.contains x (str.++ x y)) - // - // (= "" y) - Node ctn_x_x_y = d_nm->mkNode( - kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_CONCAT, x, y)); - Node eq_emp_y = d_nm->mkNode(kind::EQUAL, empty, y); - sameNormalForm(ctn_x_x_y, eq_emp_y); - - // Same normal form for: - // - // (str.contains (str.++ y x) (str.++ x y)) - // - // (= (str.++ y x) (str.++ x y)) - Node ctn_yxxy = d_nm->mkNode(kind::STRING_STRCTN, yx, xy); - Node eq_yxxy = d_nm->mkNode(kind::EQUAL, yx, xy); - sameNormalForm(ctn_yxxy, eq_yxxy); - - // (str.contains (str.replace x y x) x) ---> true - ctn_repl = d_nm->mkNode( - kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), x); - sameNormalForm(ctn_repl, t); - - // (str.contains (str.replace (str.++ x y) z (str.++ y x)) x) ---> true - ctn_repl = d_nm->mkNode( - kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, xy, z, yx), x); - sameNormalForm(ctn_repl, t); - - // (str.contains (str.++ z (str.replace (str.++ x y) z (str.++ y x))) x) - // ---> true - ctn_repl = d_nm->mkNode( - kind::STRING_STRCTN, - d_nm->mkNode(kind::STRING_CONCAT, - z, - d_nm->mkNode(kind::STRING_STRREPL, xy, z, yx)), - x); - sameNormalForm(ctn_repl, t); - - // Same normal form for: - // - // (str.contains (str.replace x y x) y) - // - // (str.contains x y) - Node lhs = d_nm->mkNode( - kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), y); - Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, y); - sameNormalForm(lhs, rhs); - - // Same normal form for: - // - // (str.contains (str.replace x y x) "B") - // - // (str.contains x "B") - lhs = d_nm->mkNode( - kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), b); - rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b); - sameNormalForm(lhs, rhs); - - // Same normal form for: - // - // (str.contains (str.replace x y x) (str.substr z n 1)) - // - // (str.contains x (str.substr z n 1)) - Node substr_z = d_nm->mkNode(kind::STRING_SUBSTR, z, n, one); - lhs = d_nm->mkNode(kind::STRING_STRCTN, - d_nm->mkNode(kind::STRING_STRREPL, x, y, x), - substr_z); - rhs = d_nm->mkNode(kind::STRING_STRCTN, x, substr_z); - sameNormalForm(lhs, rhs); - - // Same normal form for: - // - // (str.contains (str.replace x y z) z) - // - // (str.contains (str.replace x z y) y) - lhs = d_nm->mkNode( - kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, z), z); - rhs = d_nm->mkNode( - kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, z, y), y); - sameNormalForm(lhs, rhs); - - // Same normal form for: - // - // (str.contains (str.replace x "A" "B") "A") - // - // (str.contains (str.replace x "A" "") "A") - lhs = d_nm->mkNode( - kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), a); - rhs = d_nm->mkNode(kind::STRING_STRCTN, - d_nm->mkNode(kind::STRING_STRREPL, x, a, empty), - a); - sameNormalForm(lhs, rhs); - - { - // (str.contains (str.++ x "A") (str.++ "B" x)) ---> false - Node ctn = d_nm->mkNode(kind::STRING_STRCTN, - d_nm->mkNode(kind::STRING_CONCAT, x, a), - d_nm->mkNode(kind::STRING_CONCAT, b, x)); - sameNormalForm(ctn, f); - } - - { - // Same normal form for: - // - // (str.contains (str.replace x "ABC" "DEF") "GHI") - // - // (str.contains x "GHI") - lhs = d_nm->mkNode(kind::STRING_STRCTN, - d_nm->mkNode(kind::STRING_STRREPL, x, abc, def), - ghi); - rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ghi); - sameNormalForm(lhs, rhs); - } - - { - // Different normal forms for: - // - // (str.contains (str.replace x "ABC" "DEF") "B") - // - // (str.contains x "B") - lhs = d_nm->mkNode(kind::STRING_STRCTN, - d_nm->mkNode(kind::STRING_STRREPL, x, abc, def), - b); - rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b); - differentNormalForms(lhs, rhs); - } - - { - // Different normal forms for: - // - // (str.contains (str.replace x "B" "DEF") "ABC") - // - // (str.contains x "ABC") - lhs = d_nm->mkNode(kind::STRING_STRCTN, - d_nm->mkNode(kind::STRING_STRREPL, x, b, def), - abc); - rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); - differentNormalForms(lhs, rhs); - } - - { - // Same normal form for: - // - // (str.contains (str.++ (str.substr "DEF" n m) x) "AB") - // - // (str.contains x "AB") - lhs = d_nm->mkNode( - kind::STRING_STRCTN, - d_nm->mkNode(kind::STRING_CONCAT, - d_nm->mkNode(kind::STRING_SUBSTR, def, n, m), - x), - ab); - rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ab); - sameNormalForm(lhs, rhs); - } - - { - // Same normal form for: - // - // (str.contains "ABC" (str.at x n)) - // - // (or (= x "") - // (= x "A") (= x "B") (= x "C")) - Node cat = d_nm->mkNode(kind::STRING_CHARAT, x, n); - lhs = d_nm->mkNode(kind::STRING_STRCTN, abc, cat); - rhs = d_nm->mkNode(kind::OR, - d_nm->mkNode(kind::EQUAL, cat, empty), - d_nm->mkNode(kind::EQUAL, cat, a), - d_nm->mkNode(kind::EQUAL, cat, b), - d_nm->mkNode(kind::EQUAL, cat, c)); - sameNormalForm(lhs, rhs); - } - } - - void testInferEqsFromContains() - { - TypeNode strType = d_nm->stringType(); - - Node empty = d_nm->mkConst(::CVC4::String("")); - Node a = d_nm->mkConst(::CVC4::String("A")); - Node b = d_nm->mkConst(::CVC4::String("B")); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y); - Node f = d_nm->mkConst(false); - - // inferEqsFromContains("", (str.++ x y)) returns something equivalent to - // (= "" y) - Node empty_x_y = d_nm->mkNode(kind::AND, - d_nm->mkNode(kind::EQUAL, empty, x), - d_nm->mkNode(kind::EQUAL, empty, 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(StringsEntail::inferEqsFromContains(x, bxya), f); - - // inferEqsFromContains(x, y) returns null - 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(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(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(StringsEntail::inferEqsFromContains(x, repl), eq_x_repl); - } - - void testRewritePrefixSuffix() - { - TypeNode strType = d_nm->stringType(); - - Node empty = d_nm->mkConst(::CVC4::String("")); - Node a = d_nm->mkConst(::CVC4::String("A")); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node xx = d_nm->mkNode(kind::STRING_CONCAT, x, x); - Node xxa = d_nm->mkNode(kind::STRING_CONCAT, x, x, a); - Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y); - Node f = d_nm->mkConst(false); - - // Same normal form for: - // - // (str.prefix (str.++ x y) x) - // - // (= y "") - Node p_xy = d_nm->mkNode(kind::STRING_PREFIX, xy, x); - Node empty_y = d_nm->mkNode(kind::EQUAL, y, empty); - sameNormalForm(p_xy, empty_y); - - // Same normal form for: - // - // (str.suffix (str.++ x x) x) - // - // (= x "") - Node p_xx = d_nm->mkNode(kind::STRING_SUFFIX, xx, x); - Node empty_x = d_nm->mkNode(kind::EQUAL, x, empty); - sameNormalForm(p_xx, empty_x); - - // (str.suffix x (str.++ x x "A")) ---> false - Node p_xxa = d_nm->mkNode(kind::STRING_SUFFIX, xxa, x); - sameNormalForm(p_xxa, f); - } - - void testRewriteEqualityExt() - { - TypeNode strType = d_nm->stringType(); - TypeNode intType = d_nm->integerType(); - - Node empty = d_nm->mkConst(::CVC4::String("")); - Node a = d_nm->mkConst(::CVC4::String("A")); - Node aaa = d_nm->mkConst(::CVC4::String("AAA")); - Node b = d_nm->mkConst(::CVC4::String("B")); - Node ba = d_nm->mkConst(::CVC4::String("BA")); - Node w = d_nm->mkVar("w", strType); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node z = d_nm->mkVar("z", strType); - Node xxa = d_nm->mkNode(kind::STRING_CONCAT, x, x, a); - Node f = d_nm->mkConst(false); - Node n = d_nm->mkVar("n", intType); - Node zero = d_nm->mkConst(Rational(0)); - Node one = d_nm->mkConst(Rational(1)); - Node three = d_nm->mkConst(Rational(3)); - - // Same normal form for: - // - // (= "" (str.replace "" x "B")) - // - // (not (= x "")) - Node empty_repl = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, empty, x, b)); - Node empty_x = d_nm->mkNode(kind::NOT, d_nm->mkNode(kind::EQUAL, x, empty)); - sameNormalForm(empty_repl, empty_x); - - // Same normal form for: - // - // (= "" (str.replace x y (str.++ x x "A"))) - // - // (and (= x "") (not (= y ""))) - Node empty_repl_xaa = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, x, y, xxa)); - Node empty_xy = d_nm->mkNode( - kind::AND, - d_nm->mkNode(kind::EQUAL, x, empty), - d_nm->mkNode(kind::NOT, d_nm->mkNode(kind::EQUAL, y, empty))); - sameNormalForm(empty_repl_xaa, empty_xy); - - // (= "" (str.replace (str.++ x x "A") x y)) ---> false - Node empty_repl_xxaxy = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, xxa, x, y)); - Node eq_xxa_repl = d_nm->mkNode( - kind::EQUAL, xxa, d_nm->mkNode(kind::STRING_STRREPL, empty, y, x)); - sameNormalForm(empty_repl_xxaxy, f); - - // Same normal form for: - // - // (= "" (str.replace "A" x y)) - // - // (= "A" (str.replace "" y x)) - Node empty_repl_axy = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, a, x, y)); - Node eq_a_repl = d_nm->mkNode( - kind::EQUAL, a, d_nm->mkNode(kind::STRING_STRREPL, empty, y, x)); - sameNormalForm(empty_repl_axy, eq_a_repl); - - // Same normal form for: - // - // (= "" (str.replace x "A" "")) - // - // (str.prefix x "A") - Node empty_repl_a = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, x, a, empty)); - Node prefix_a = d_nm->mkNode(kind::STRING_PREFIX, x, a); - sameNormalForm(empty_repl_a, prefix_a); - - // Same normal form for: - // - // (= "" (str.substr x 1 2)) - // - // (<= (str.len x) 1) - Node empty_substr = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_SUBSTR, x, one, three)); - Node leq_len_x = - d_nm->mkNode(kind::LEQ, d_nm->mkNode(kind::STRING_LENGTH, x), one); - sameNormalForm(empty_substr, leq_len_x); - - // Different normal form for: - // - // (= "" (str.substr x 0 n)) - // - // (<= n 0) - Node empty_substr_x = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_SUBSTR, x, zero, n)); - Node leq_n = d_nm->mkNode(kind::LEQ, n, zero); - differentNormalForms(empty_substr_x, leq_n); - - // Same normal form for: - // - // (= "" (str.substr "A" 0 n)) - // - // (<= n 0) - Node empty_substr_a = d_nm->mkNode( - kind::EQUAL, empty, d_nm->mkNode(kind::STRING_SUBSTR, a, zero, n)); - sameNormalForm(empty_substr_a, leq_n); - - // Same normal form for: - // - // (= (str.++ x x a) (str.replace y (str.++ x x a) y)) - // - // (= (str.++ x x a) y) - Node eq_xxa_repl_y = d_nm->mkNode( - kind::EQUAL, xxa, d_nm->mkNode(kind::STRING_STRREPL, y, xxa, y)); - Node eq_xxa_y = d_nm->mkNode(kind::EQUAL, xxa, y); - sameNormalForm(eq_xxa_repl_y, eq_xxa_y); - - // (= (str.++ x x a) (str.replace (str.++ x x a) "A" "B")) ---> false - Node eq_xxa_repl_xxa = d_nm->mkNode( - kind::EQUAL, xxa, d_nm->mkNode(kind::STRING_STRREPL, xxa, a, b)); - sameNormalForm(eq_xxa_repl_xxa, f); - - // Same normal form for: - // - // (= (str.replace x "A" "B") "") - // - // (= x "") - Node eq_repl = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), empty); - Node eq_x = d_nm->mkNode(kind::EQUAL, x, empty); - sameNormalForm(eq_repl, eq_x); - - { - // Same normal form for: - // - // (= (str.replace y "A" "B") "B") - // - // (= (str.replace y "B" "A") "A") - Node lhs = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), b); - Node rhs = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, b, a), a); - sameNormalForm(lhs, rhs); - } - - { - // Same normal form for: - // - // (= (str.++ x "A" y) (str.++ "A" "A" (str.substr "AAA" 0 n))) - // - // (= (str.++ y x) (str.++ (str.substr "AAA" 0 n) "A")) - Node lhs = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::STRING_CONCAT, x, a, y), - d_nm->mkNode(kind::STRING_CONCAT, - a, - a, - d_nm->mkNode(kind::STRING_SUBSTR, aaa, zero, n))); - Node rhs = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::STRING_CONCAT, x, y), - d_nm->mkNode(kind::STRING_CONCAT, - d_nm->mkNode(kind::STRING_SUBSTR, aaa, zero, n), - a)); - sameNormalForm(lhs, rhs); - } - - { - // Same normal form for: - // - // (= (str.++ "A" x) "A") - // - // (= x "") - Node lhs = - d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, a, x), a); - Node rhs = d_nm->mkNode(kind::EQUAL, x, empty); - sameNormalForm(lhs, rhs); - } - - { - // (= (str.++ x "A") "") ---> false - Node eq = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, x, a), empty); - sameNormalForm(eq, f); - } - - { - // (= (str.++ x "B") "AAA") ---> false - Node eq = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, x, b), aaa); - sameNormalForm(eq, f); - } - - { - // (= (str.++ x "AAA") "A") ---> false - Node eq = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, x, aaa), a); - sameNormalForm(eq, f); - } - - { - // (= (str.++ "AAA" (str.substr "A" 0 n)) (str.++ x "B")) ---> false - Node eq = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::STRING_CONCAT, - aaa, - d_nm->mkNode(kind::STRING_CONCAT, - a, - a, - d_nm->mkNode(kind::STRING_SUBSTR, x, zero, n))), - d_nm->mkNode(kind::STRING_CONCAT, x, b)); - sameNormalForm(eq, f); - } - - { - // (= (str.++ "A" (int.to.str n)) "A") -/-> false - Node eq = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::STRING_CONCAT, a, d_nm->mkNode(kind::STRING_ITOS, n)), - a); - differentNormalForms(eq, f); - } - - { - // (= (str.++ "A" x y) (str.++ x "B" z)) --> false - Node eq = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::STRING_CONCAT, a, x, y), - d_nm->mkNode(kind::STRING_CONCAT, x, b, z)); - sameNormalForm(eq, f); - } - - { - // (= (str.++ "B" x y) (str.++ x "AAA" z)) --> false - Node eq = d_nm->mkNode(kind::EQUAL, - d_nm->mkNode(kind::STRING_CONCAT, b, x, y), - d_nm->mkNode(kind::STRING_CONCAT, x, aaa, z)); - sameNormalForm(eq, f); - } - - { - Node xrepl = d_nm->mkNode(kind::STRING_STRREPL, x, a, b); - - // Same normal form for: - // - // (= (str.++ "B" (str.replace x "A" "B") z y w) - // (str.++ z x "BA" z)) - // - // (and (= (str.++ "B" (str.replace x "A" "B") z) - // (str.++ z x "B")) - // (= (str.++ y w) (str.++ "A" z))) - Node lhs = - d_nm->mkNode(kind::EQUAL, - d_nm->mkNode(kind::STRING_CONCAT, b, xrepl, z, y, w), - d_nm->mkNode(kind::STRING_CONCAT, z, x, ba, z)); - Node rhs = d_nm->mkNode( - kind::AND, - d_nm->mkNode(kind::EQUAL, - d_nm->mkNode(kind::STRING_CONCAT, b, xrepl, z), - d_nm->mkNode(kind::STRING_CONCAT, z, x, b)), - d_nm->mkNode(kind::EQUAL, - d_nm->mkNode(kind::STRING_CONCAT, y, w), - d_nm->mkNode(kind::STRING_CONCAT, a, z))); - sameNormalForm(lhs, rhs); - } - } - - void testStripConstantEndpoints() - { - 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 ab = d_nm->mkConst(::CVC4::String("AB")); - Node abc = d_nm->mkConst(::CVC4::String("ABC")); - Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); - Node bc = d_nm->mkConst(::CVC4::String("BC")); - Node c = d_nm->mkConst(::CVC4::String("C")); - Node cd = d_nm->mkConst(::CVC4::String("CD")); - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node n = d_nm->mkVar("n", intType); - - { - // stripConstantEndpoints({ "" }, { "A" }, {}, {}, 0) ---> false - std::vector n1 = {empty}; - std::vector n2 = {a}; - std::vector nb; - std::vector ne; - bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0); - TS_ASSERT(!res); - } - - { - // stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0) - // ---> false - std::vector n1 = {a}; - std::vector n2 = {a, d_nm->mkNode(kind::STRING_ITOS, n)}; - std::vector nb; - std::vector ne; - bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 0); - TS_ASSERT(!res); - } - - { - // stripConstantEndpoints({ "ABCD" }, { "C" }, {}, {}, 1) - // ---> true - // n1 is updated to { "CD" } - // nb is updated to { "AB" } - std::vector n1 = {abcd}; - std::vector n2 = {c}; - std::vector nb; - std::vector ne; - std::vector n1r = {cd}; - std::vector nbr = {ab}; - bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1); - TS_ASSERT(res); - TS_ASSERT_EQUALS(n1, n1r); - TS_ASSERT_EQUALS(nb, nbr); - } - - { - // stripConstantEndpoints({ "ABC", x }, { "CD" }, {}, {}, 1) - // ---> true - // n1 is updated to { "C", x } - // nb is updated to { "AB" } - std::vector n1 = {abc, x}; - std::vector n2 = {cd}; - std::vector nb; - std::vector ne; - std::vector n1r = {c, x}; - std::vector nbr = {ab}; - bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, 1); - TS_ASSERT(res); - TS_ASSERT_EQUALS(n1, n1r); - TS_ASSERT_EQUALS(nb, nbr); - } - - { - // stripConstantEndpoints({ "ABC" }, { "A" }, {}, {}, -1) - // ---> true - // n1 is updated to { "A" } - // nb is updated to { "BC" } - std::vector n1 = {abc}; - std::vector n2 = {a}; - std::vector nb; - std::vector ne; - std::vector n1r = {a}; - std::vector ner = {bc}; - bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1); - TS_ASSERT(res); - TS_ASSERT_EQUALS(n1, n1r); - TS_ASSERT_EQUALS(ne, ner); - } - - { - // stripConstantEndpoints({ x, "ABC" }, { y, "A" }, {}, {}, -1) - // ---> true - // n1 is updated to { x, "A" } - // nb is updated to { "BC" } - std::vector n1 = {x, abc}; - std::vector n2 = {y, a}; - std::vector nb; - std::vector ne; - std::vector n1r = {x, a}; - std::vector ner = {bc}; - bool res = StringsEntail::stripConstantEndpoints(n1, n2, nb, ne, -1); - TS_ASSERT(res); - TS_ASSERT_EQUALS(n1, n1r); - TS_ASSERT_EQUALS(ne, ner); - } - } - - void testRewriteMembership() - { - TypeNode strType = d_nm->stringType(); - - std::vector vec_empty; - Node abc = d_nm->mkConst(::CVC4::String("ABC")); - Node re_abc = d_nm->mkNode(kind::STRING_TO_REGEXP, abc); - Node x = d_nm->mkVar("x", strType); - - { - // Same normal form for: - // - // (str.in.re x (re.++ (re.* re.allchar) - // (re.* re.allchar) - // (str.to.re "ABC") - // (re.* re.allchar))) - // - // (str.contains x "ABC") - Node sig_star = d_nm->mkNode(kind::REGEXP_STAR, - d_nm->mkNode(kind::REGEXP_SIGMA, vec_empty)); - Node lhs = d_nm->mkNode( - kind::STRING_IN_REGEXP, - x, - d_nm->mkNode( - kind::REGEXP_CONCAT, sig_star, sig_star, re_abc, sig_star)); - Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); - sameNormalForm(lhs, rhs); - } - - { - // Different normal forms for: - // - // (str.in.re x (re.++ (re.* re.allchar) (str.to.re "ABC"))) - // - // (str.contains x "ABC") - Node sig_star = d_nm->mkNode(kind::REGEXP_STAR, - d_nm->mkNode(kind::REGEXP_SIGMA, vec_empty)); - Node lhs = - d_nm->mkNode(kind::STRING_IN_REGEXP, - x, - d_nm->mkNode(kind::REGEXP_CONCAT, sig_star, re_abc)); - Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); - differentNormalForms(lhs, rhs); - } - } - - void testRewriteRegexpConcat() - { - TypeNode strType = d_nm->stringType(); - - std::vector emptyArgs; - Node x = d_nm->mkVar("x", strType); - Node y = d_nm->mkVar("y", strType); - Node allStar = d_nm->mkNode(kind::REGEXP_STAR, - d_nm->mkNode(kind::REGEXP_SIGMA, emptyArgs)); - Node xReg = d_nm->mkNode(kind::STRING_TO_REGEXP, x); - Node yReg = d_nm->mkNode(kind::STRING_TO_REGEXP, y); - - { - // In normal form: - // - // (re.++ (re.* re.allchar) (re.union (str.to.re x) (str.to.re y))) - Node n = d_nm->mkNode(kind::REGEXP_CONCAT, - allStar, - d_nm->mkNode(kind::REGEXP_UNION, xReg, yReg)); - inNormalForm(n); - } - - { - // In normal form: - // - // (re.++ (str.to.re x) (re.* re.allchar)) - Node n = d_nm->mkNode(kind::REGEXP_CONCAT, xReg, allStar); - inNormalForm(n); - } - } - - private: - ExprManager* d_em; - SmtEngine* d_smt; - SmtScope* d_scope; - ExtendedRewriter* d_rewriter; - - NodeManager* d_nm; -};