diff options
-rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 21 | ||||
-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 | 65 |
5 files changed, 94 insertions, 9 deletions
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 5a4a25e88..5df744412 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -243,16 +243,19 @@ 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; + } + + if (Word::isEmpty(c[0])) + { + emptyNodes.insert(c[1]); + } + else if (Word::isEmpty(c[1])) + { + emptyNodes.insert(c[0]); } else { 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..1860c3be8 --- /dev/null +++ b/test/unit/theory/theory_strings_utils_white.cpp @@ -0,0 +1,65 @@ +/****************************************************************************** + * 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 <unordered_set> +#include <vector> + +#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 |