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.

1 files changed, 14 insertions, 0 deletions

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)