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.

diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 5a4a25e88cb45f7675096dc4f0a4d61d2a2c5679..5df7444129b78a2eef3099e49f1f5b5467462c61 100644 (file)
--- 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 5e9b38e8de8ececee4d8022a2736166cc95e1202..7358ecca4de421bcddcc9a4b7aa74d1cea6e3768 100644 (file)
--- 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 (file)
index 0000000..3ee748d
--- /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 d0c0e2bd21531ed41c6cadd650a9cfbda2f71175..9fb0e21f1a8cff106d9fc045b7d2492fc4fd1994 100644 (file)
--- 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 (file)
index 0000000..1860c3b
--- /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