Fix sets cardinality cycle rule (#4392)

Fixes #4391.

The sets cardinality cycle rule is analogous to the S-Cycle rule for strings (see Liang et al CAV 2014). This rule is typically never applied but can be applied in rare cases where theory combination does not determine a correct arrangement of equalities over sets terms that is consistent with the arithmetic arrangement of their cardinalities at full effort. Notice the regression from #4391 has non-linear arithmetic, (mod 0 d), which is translated to UF.

The cardinality cycle rule had a bug: it assumed that cycles that were encountered were loops e1 = e2 = ... = e1 but in general they can be lassos e1 = ... = e2 = ... = e2. This ensures the Venn region cycle e2 = ... = e2 is the conclusion in this case, instead of unsoundly concluding e1 = ... = e2.

Strings does not have a similar issue:
https://github.com/CVC4/CVC4/blob/master/src/theory/strings/core_solver.cpp#L488
Here, when a cycle is encountered, it is processed at the point in traversal where the loop is closed.

This is not critical for SMT-COMP but should be in the 1.8 release.

3 files changed, 29 insertions, 1 deletions

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 15e22104c..f37e06918 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -318,6 +318,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
                                               std::vector<Node>& curr,
                                               std::vector<Node>& exp)
 {
+  Trace("sets-cycle-debug") << "Traverse eqc " << eqc << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   if (std::find(curr.begin(), curr.end(), eqc) != curr.end())
   {
@@ -326,11 +327,21 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
     {
       // all regions must be equal
       std::vector<Node> conc;
+      bool foundLoopStart = false;
       for (const Node& cc : curr)
       {
-        conc.push_back(curr[0].eqNode(cc));
+        if (cc == eqc)
+        {
+          foundLoopStart = true;
+        }
+        else if (foundLoopStart && eqc != cc)
+        {
+          conc.push_back(eqc.eqNode(cc));
+        }
       }
       Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(AND, conc);
+      Trace("sets-cycle-debug")
+          << "CYCLE: " << fact << " from " << exp << std::endl;
       d_im.assertInference(fact, exp, "card_cycle");
       d_im.flushPendingLemmas();
     }
@@ -611,6 +622,8 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
     exp.push_back(eqc.eqNode(n));
     for (const Node& cpnc : d_card_parent[n])
     {
+      Trace("sets-cycle-debug")
+          << "Traverse card parent " << eqc << " -> " << cpnc << std::endl;
       checkCardCyclesRec(cpnc, curr, exp);
       if (d_im.hasProcessed())
       {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cf953c252..935a4694f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1706,6 +1706,7 @@ set(regress_1_tests
   regress1/sets/insert_invariant_37_2.smt2
   regress1/sets/issue2568.smt2
   regress1/sets/issue2904.smt2
+  regress1/sets/issue4391-card-lasso.smt2
   regress1/sets/lemmabug-ListElts317minimized.smt2
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2
diff --git a/test/regress/regress1/sets/issue4391-card-lasso.smt2 b/test/regress/regress1/sets/issue4391-card-lasso.smt2
new file mode 100644
index 000000000..871d758f3
--- /dev/null
+++ b/test/regress/regress1/sets/issue4391-card-lasso.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun d () Int)
+(declare-fun b () (Set Int))
+(declare-fun c () (Set Int))
+(declare-fun e () (Set Int))
+
+(assert (= e (union b e)))
+(assert (= (card b) d))
+(assert (= (card c) 0))
+(assert (= 0 (mod 0 d)))
+(assert (> (card (setminus e (intersection (intersection e b) (setminus e c)))) 1))
+
+(check-sat)