From c2faac74261f433927ecf7f1c21cf623a2103321 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 18 May 2021 13:44:57 -0700 Subject: Fix `collectEmptyEqs()` in string utils 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. --- src/theory/strings/theory_strings_utils.cpp | 22 +++++---- test/regress/CMakeLists.txt | 1 + test/regress/regress2/strings/issue6483.smt2 | 15 ++++++ test/unit/theory/CMakeLists.txt | 1 + test/unit/theory/theory_strings_utils_white.cpp | 61 +++++++++++++++++++++++++ 5 files changed, 90 insertions(+), 10 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..0c8d7c372 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -243,19 +243,21 @@ 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; } - 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 +#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 -- cgit v1.2.3