diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 14:07:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-20 14:07:37 -0500 |
commit | 964760cf81eb7414a11bbd89ef3a16e8927d6947 (patch) | |
tree | 0c574e99433c722e69af6efeeefbe0901010f7b7 /test/unit | |
parent | aa44c35f035f1cab03de0c5fe7c0f16b20f44696 (diff) |
Split string-specific operators from TheoryStringsRewriter (#3920)
Organization towards theory of sequences.
The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/unit/theory/sequences_rewriter_white.h (renamed from test/unit/theory/theory_strings_rewriter_white.h) | 90 |
2 files changed, 46 insertions, 46 deletions
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 35f2f7bfa..d6a6b701c 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -2,6 +2,7 @@ cvc4_add_unit_test_black(regexp_operation_black theory) cvc4_add_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_unit_test_white(sequences_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_unit_test_white(theory_bv_white theory) @@ -9,7 +10,6 @@ cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) -cvc4_add_unit_test_white(theory_strings_rewriter_white theory) cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_unit_test_white(theory_strings_word_white theory) cvc4_add_unit_test_white(theory_white theory) diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h index af8b24a0b..200a36d0b 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/sequences_rewriter_white.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_strings_rewriter_white.h +/*! \file sequences_rewriter_white.h ** \verbatim ** Top contributors (to current version): ** Andres Noetzli @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Unit tests for the strings rewriter + ** \brief Unit tests for the strings/sequences rewriter ** - ** Unit tests for the strings rewriter. + ** Unit tests for the strings/sequences rewriter. **/ #include "expr/node.h" @@ -20,7 +20,7 @@ #include "smt/smt_engine_scope.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/rewriter.h" -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" #include <cxxtest/TestSuite.h> #include <iostream> @@ -33,10 +33,10 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::strings; -class TheoryStringsRewriterWhite : public CxxTest::TestSuite +class SequencesRewriterWhite : public CxxTest::TestSuite { public: - TheoryStringsRewriterWhite() {} + SequencesRewriterWhite() {} void setUp() override { @@ -107,23 +107,23 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node three = d_nm->mkConst(Rational(3)); Node i = d_nm->mkVar("i", intType); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(a)); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(a, true)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(a)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(a, true)); Node substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr)); - TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr, true)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr)); + TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr, true)); substr = d_nm->mkNode(kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_CONCAT, a, x), zero, one); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr)); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr, true)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr, true)); substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, two); - TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr)); - TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr, true)); + TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr)); + TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr, true)); } void testCheckEntailArith() @@ -138,10 +138,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite // 1 >= (str.len (str.substr z n 1)) ---> true Node substr_z = d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_SUBSTR, z, n, one)); - TS_ASSERT(TheoryStringsRewriter::checkEntailArith(one, substr_z)); + TS_ASSERT(SequencesRewriter::checkEntailArith(one, substr_z)); // (str.len (str.substr z n 1)) >= 1 ---> false - TS_ASSERT(!TheoryStringsRewriter::checkEntailArith(substr_z, one)); + TS_ASSERT(!SequencesRewriter::checkEntailArith(substr_z, one)); } void testCheckEntailArithWithAssumption() @@ -165,25 +165,25 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x_plus_slen_y, zero)); // x + (str.len y) = 0 |= 0 >= x --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_slen_y_eq_zero, zero, x, false)); // x + (str.len y) = 0 |= 0 > x --> false - TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption( 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(!TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption( 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(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); Node five = d_nm->mkConst(Rational(5)); @@ -193,11 +193,11 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, six)); // x + 5 < 6 |= 0 >= x --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_five_lt_six, zero, x, false)); // x + 5 < 6 |= 0 > x --> false - TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption( x_plus_five_lt_six, zero, x, true)); Node neg_x = d_nm->mkNode(kind::UMINUS, x); @@ -205,16 +205,16 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, five)); // x + 5 < 5 |= -x >= 0 --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_five_lt_five, neg_x, zero, false)); // x + 5 < 5 |= 0 > x --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( 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(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( assm, x, d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_ITOS, x)), @@ -243,7 +243,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite // (str.substr "A" x x) --> "" Node n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, x); - Node res = TheoryStringsRewriter::rewriteSubstr(n); + Node res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, empty); // (str.substr "A" (+ x 1) x) -> "" @@ -251,7 +251,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite a, d_nm->mkNode(kind::PLUS, x, d_nm->mkConst(Rational(1))), x); - res = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, empty); // (str.substr "A" (+ x (str.len s2)) x) -> "" @@ -260,24 +260,24 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite a, d_nm->mkNode(kind::PLUS, x, d_nm->mkNode(kind::STRING_LENGTH, s)), x); - res = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::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 = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::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 = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::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 = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, n); // (str.substr (str.substr s x x) x x) -> "" @@ -440,8 +440,8 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite x, d_nm->mkNode(kind::STRING_STRREPL, x, gh, ij), ij); - Node res_concat1 = TheoryStringsRewriter::lengthPreserveRewrite(concat1); - Node res_concat2 = TheoryStringsRewriter::lengthPreserveRewrite(concat2); + Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1); + Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2); TS_ASSERT_EQUALS(res_concat1, res_concat2); } @@ -1049,32 +1049,32 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node empty_x_y = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::EQUAL, empty, x), d_nm->mkNode(kind::EQUAL, empty, y)); - sameNormalForm(TheoryStringsRewriter::inferEqsFromContains(empty, xy), + sameNormalForm(SequencesRewriter::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(TheoryStringsRewriter::inferEqsFromContains(x, bxya), f); + sameNormalForm(SequencesRewriter::inferEqsFromContains(x, bxya), f); // inferEqsFromContains(x, y) returns null - Node n = TheoryStringsRewriter::inferEqsFromContains(x, y); + Node n = SequencesRewriter::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(TheoryStringsRewriter::inferEqsFromContains(x, x), eq_x_x); + sameNormalForm(SequencesRewriter::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(TheoryStringsRewriter::inferEqsFromContains(repl, x), + sameNormalForm(SequencesRewriter::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(TheoryStringsRewriter::inferEqsFromContains(x, repl), + sameNormalForm(SequencesRewriter::inferEqsFromContains(x, repl), eq_x_repl); } @@ -1402,7 +1402,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> nb; std::vector<Node> ne; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); TS_ASSERT(!res); } @@ -1414,7 +1414,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> nb; std::vector<Node> ne; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); TS_ASSERT(!res); } @@ -1430,7 +1430,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> n1r = {cd}; std::vector<Node> nbr = {ab}; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1); TS_ASSERT(res); TS_ASSERT_EQUALS(n1, n1r); TS_ASSERT_EQUALS(nb, nbr); @@ -1448,7 +1448,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> n1r = {c, x}; std::vector<Node> nbr = {ab}; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1); TS_ASSERT(res); TS_ASSERT_EQUALS(n1, n1r); TS_ASSERT_EQUALS(nb, nbr); @@ -1466,7 +1466,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> n1r = {a}; std::vector<Node> ner = {bc}; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1); TS_ASSERT(res); TS_ASSERT_EQUALS(n1, n1r); TS_ASSERT_EQUALS(ne, ner); @@ -1484,7 +1484,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> n1r = {x, a}; std::vector<Node> ner = {bc}; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1); TS_ASSERT(res); TS_ASSERT_EQUALS(n1, n1r); TS_ASSERT_EQUALS(ne, ner); |