diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-26 00:05:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-25 22:05:28 -0700 |
commit | 8476f38b6a3288eebe50e12a2dc6b76a10b65aae (patch) | |
tree | 7efd22b84214e599d6f43aeb1139fc34469e1b5c /src | |
parent | 1cacd328b60713e21af6836c65007ebe3bfffa81 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/sets/cardinality_extension.cpp | 15 |
1 files changed, 14 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()) { |