diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-29 20:31:18 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-29 22:31:18 -0500 |
| commit | 8182ab9f7d8d6c732202371c24bafd721ef6cfcc (patch) | |
| tree | dbc0d2ee2e343375245b21dcfedcb8a48b8b500d /test/unit/theory | |
| parent | dbf1b6fb38938dc829441579860f0c9155be75f9 (diff) | |
Add rewrite for splitting equalities (#2957)
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 00eb0b495..c5db12c6c 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -1093,8 +1093,11 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite 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); @@ -1300,6 +1303,49 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite 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() |