diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-18 13:44:57 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-18 13:44:57 -0700 |
commit | c2faac74261f433927ecf7f1c21cf623a2103321 (patch) | |
tree | 6288f82df026fa45bce7a973688914f7eb0ac8f5 | |
parent | 626a1634fc21aed6e1149e5579ce112c1efc72bc (diff) |
Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:
```
Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
```
The rewrite `RPL_X_Y_X_SIMP` rewrites terms of the form `(str.replace x
y x)`, where `x` is of length one and `(= y "")` rewrites to a
conjunction of equalities of the form `(= y_i "")` where `y_i` is some
term. The function responsible for collecting the terms `y_i` from this
conjunction, `collectEmptyEqs()`, returns a `bool` and a vector of
`Node`s. The `bool` indicates whether all equalities in the conjunction
were of the form `(= y_i "")`. The rewrite `RPL_X_Y_X_SIMP` only applies
if this is true. However, `collectEmptyEqs()` had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
`collectEmptyEqs()` and adds tests.
-rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 22 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress2/strings/issue6483.smt2 | 15 | ||||
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_utils_white.cpp | 61 |
5 files changed, 90 insertions, 10 deletions
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 5a4a25e88..0c8d7c372 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -243,19 +243,21 @@ std::pair<bool, std::vector<Node> > collectEmptyEqs(Node x) { for (const Node& c : x) { - if (c.getKind() == EQUAL) + if (c.getKind() != EQUAL) { - if (Word::isEmpty(c[0])) - { - emptyNodes.insert(c[1]); - } - else if (Word::isEmpty(c[1])) - { - emptyNodes.insert(c[0]); - } + allEmptyEqs = false; + continue; } - else + + if (Word::isEmpty(c[0])) { + emptyNodes.insert(c[1]); + } + else if (Word::isEmpty(c[1])) + { + emptyNodes.insert(c[0]); + } + else { allEmptyEqs = false; } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5e9b38e8d..7358ecca4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2410,6 +2410,7 @@ set(regress_2_tests regress2/strings/cmu-repl-len-nterm.smt2 regress2/strings/issue3203.smt2 regress2/strings/issue5381.smt2 + regress2/strings/issue6483.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/range-perf.smt2 diff --git a/test/regress/regress2/strings/issue6483.smt2 b/test/regress/regress2/strings/issue6483.smt2 new file mode 100644 index 000000000..3ee748d27 --- /dev/null +++ b/test/regress/regress2/strings/issue6483.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_SLIA) +(declare-fun a () String) +(assert + (xor + (= (= (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") + (str.replace "B" (str.replace "B" a (str.++ a "B")) a)) + (not + (= (str.replace "B" (str.replace a "B" "") "B") + (str.replace "B" a (str.++ a "B"))))) + (= (str.replace "B" a "") + (str.replace "B" a + (ite (not (= (str.replace "" (str.replace a "" a) "") "")) "" + (str.replace "" (str.replace a "B" "") "B")))))) +(set-info :status unsat) +(check-sat) diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index d0c0e2bd2..9fb0e21f1 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -35,6 +35,7 @@ cvc5_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc5_add_unit_test_white(theory_sets_type_enumerator_white theory) cvc5_add_unit_test_white(theory_sets_type_rules_white theory) cvc5_add_unit_test_white(theory_strings_skolem_cache_black theory) +cvc5_add_unit_test_white(theory_strings_utils_white theory) cvc5_add_unit_test_white(theory_strings_word_white theory) cvc5_add_unit_test_white(theory_white theory) cvc5_add_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/theory/theory_strings_utils_white.cpp b/test/unit/theory/theory_strings_utils_white.cpp new file mode 100644 index 000000000..7fb5614cd --- /dev/null +++ b/test/unit/theory/theory_strings_utils_white.cpp @@ -0,0 +1,61 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Unit tests for the string utils + */ + +#include <vector> +#include <unordered_set> + +#include "expr/node.h" +#include "test_node.h" +#include "theory/strings/theory_strings_utils.h" + +namespace cvc5 { + +using namespace kind; +using namespace theory; +using namespace theory::strings; + +namespace test { + +class TestTheoryWhiteStringsUtils : public TestNode +{ +}; + +TEST_F(TestTheoryWhiteStringsUtils, collect_empty_eqs) +{ + TypeNode strType = d_nodeManager->stringType(); + + Node empty = d_nodeManager->mkConst(String("")); + Node a = d_nodeManager->mkConst(::cvc5::String("A")); + Node x = d_nodeManager->mkVar("x", strType); + + Node emptyEqX = empty.eqNode(x); + Node emptyEqA = a.eqNode(empty); + Node xEqA = x.eqNode(a); + + std::vector<Node> emptyNodes; + bool allEmptyEqs; + std::unordered_set<Node> expected = {a, x}; + + std::tie(allEmptyEqs, emptyNodes) = utils::collectEmptyEqs(d_nodeManager->mkNode(AND, emptyEqX, emptyEqA)); + ASSERT_TRUE(allEmptyEqs); + ASSERT_EQ(std::unordered_set<Node>(emptyNodes.begin(), emptyNodes.end()), expected); + + std::tie(allEmptyEqs, emptyNodes) = utils::collectEmptyEqs(d_nodeManager->mkNode(AND, emptyEqX, xEqA, emptyEqA)); + ASSERT_FALSE(allEmptyEqs); + ASSERT_EQ(std::unordered_set<Node>(emptyNodes.begin(), emptyNodes.end()), expected); +} + +} // namespace test +} // namespace cvc5 |