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.

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