From c214051068aefdf831bf67e6b7d72591e5a91ece Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 18 May 2021 14:32:51 -0700 Subject: [PATCH] Fix `collectEmptyEqs()` in string utils (#6562) 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 Nodes. 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. --- src/theory/strings/theory_strings_utils.cpp | 21 +++--- test/regress/CMakeLists.txt | 1 + test/regress/regress2/strings/issue6483.smt2 | 15 +++++ test/unit/theory/CMakeLists.txt | 1 + .../theory/theory_strings_utils_white.cpp | 65 +++++++++++++++++++ 5 files changed, 94 insertions(+), 9 deletions(-) create mode 100644 test/regress/regress2/strings/issue6483.smt2 create mode 100644 test/unit/theory/theory_strings_utils_white.cpp 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 > 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 +#include + +#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 emptyNodes; + bool allEmptyEqs; + std::unordered_set expected = {a, x}; + + std::tie(allEmptyEqs, emptyNodes) = + utils::collectEmptyEqs(d_nodeManager->mkNode(AND, emptyEqX, emptyEqA)); + ASSERT_TRUE(allEmptyEqs); + ASSERT_EQ(std::unordered_set(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(emptyNodes.begin(), emptyNodes.end()), + expected); +} + +} // namespace test +} // namespace cvc5 -- 2.30.2