From 8476f38b6a3288eebe50e12a2dc6b76a10b65aae Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 26 Apr 2020 00:05:28 -0500 Subject: [PATCH] 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. --- src/theory/sets/cardinality_extension.cpp | 15 ++++++++++++++- test/regress/CMakeLists.txt | 1 + .../regress1/sets/issue4391-card-lasso.smt2 | 14 ++++++++++++++ 3 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/sets/issue4391-card-lasso.smt2 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& curr, std::vector& 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 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) -- 2.30.2