From e25d2ce5eff672bb5b58c245f0414a1ed9c51a6c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 9 Jul 2021 12:24:50 -0500 Subject: [PATCH] Fix sets cardinality inference involving equivalent parents (#6855) This fixes an unsoundness issue in the sets + cardinality solver. One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that: if T = (union T S), then (intersect T S) = S. The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms. This PR also does some minor cleanup. --- src/theory/sets/cardinality_extension.cpp | 40 +++++++++---------- src/theory/sets/cardinality_extension.h | 7 +++- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sets/sets-uc-wrong.smt2 | 12 ++++++ 4 files changed, 37 insertions(+), 23 deletions(-) create mode 100644 test/regress/regress1/sets/sets-uc-wrong.smt2 diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 063c440a5..62dedb35a 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -305,7 +305,7 @@ void CardinalityExtension::checkCardCycles() // build order of equivalence classes, also build cardinality graph const std::vector& setEqc = d_state.getSetsEqClasses(); d_oSetEqc.clear(); - d_card_parent.clear(); + d_cardParent.clear(); for (const Node& s : setEqc) { std::vector curr; @@ -317,7 +317,6 @@ void CardinalityExtension::checkCardCycles() } } - Trace("sets") << "d_card_parent: " << d_card_parent << std::endl; Trace("sets") << "d_oSetEqc: " << d_oSetEqc << std::endl; Trace("sets") << "Done check cardinality cycles" << std::endl; } @@ -432,14 +431,6 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, { return; } - else - { - // justify why there is no edge to parents (necessary?) - for (unsigned e = 0; e < n_parents; e++) - { - Node p = (e == true_sib) ? u : n[e]; - } - } continue; } std::vector card_parents; @@ -521,7 +512,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, card_parent_ids.push_back(is_union ? 2 : e); } } - Assert(d_card_parent[n].empty()); + Assert(d_cardParent[n].empty()); Trace("sets-debug") << "get parent representatives..." << std::endl; // for each parent, take their representatives for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++) @@ -573,9 +564,9 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, else { bool dup = false; - for (unsigned l = 0, numcpn = d_card_parent[n].size(); l < numcpn; l++) + for (unsigned l = 0, numcpn = d_cardParent[n].size(); l < numcpn; l++) { - Node cpnl = d_card_parent[n][l]; + Node cpnl = d_cardParent[n][l].first; if (eqcc != cpnl) { continue; @@ -613,7 +604,13 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, conc.push_back(cpk.eqNode(n)); } } - d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2, cpk.eqNode(cpnl)); + // use the original term, not the representative. + // for example, we conclude T = (union T S) => (intersect T S) = S + // here where we do not use the representative of T or (union T S). + Node cpnlb = d_cardParent[n][l].second; + d_im.assertInference(conc, + InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2, + cpk.eqNode(cpnlb)); d_im.doPendingLemmas(); if (d_im.hasSent()) { @@ -622,18 +619,18 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, } if (!dup) { - d_card_parent[n].push_back(eqcc); + d_cardParent[n].emplace_back(eqcc, cpk); } } } // now recurse on parents (to ensure their normal will be computed after // this eqc) exp.push_back(eqc.eqNode(n)); - for (const Node& cpnc : d_card_parent[n]) + for (const std::pair& cpnc : d_cardParent[n]) { - Trace("sets-cycle-debug") - << "Traverse card parent " << eqc << " -> " << cpnc << std::endl; - checkCardCyclesRec(cpnc, curr, exp); + Trace("sets-cycle-debug") << "Traverse card parent " << eqc << " -> " + << cpnc.first << std::endl; + checkCardCyclesRec(cpnc.first, curr, exp); if (d_im.hasSent()) { return; @@ -897,7 +894,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, for (const Node& n : nvsets) { Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl; - if (d_card_parent[n].empty()) + if (d_cardParent[n].empty()) { // nothing to do continue; @@ -905,8 +902,9 @@ void CardinalityExtension::checkNormalForm(Node eqc, Assert(d_localBase.find(n) != d_localBase.end()); Node cbase = d_localBase[n]; Trace("sets-nf-debug") << "Card base is " << cbase << std::endl; - for (const Node& p : d_card_parent[n]) + for (const std::pair& cp : d_cardParent[n]) { + Node p = cp.first; Trace("sets-nf-debug") << "Check parent " << p << std::endl; if (parents_proc[cbase].find(p) != parents_proc[cbase].end()) { diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index ce2f29bd5..bddcfaf1b 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -357,9 +357,12 @@ class CardinalityExtension std::vector d_oSetEqc; /** * This maps set terms to the set of representatives of their "parent" sets, - * see checkCardCycles. + * see checkCardCycles. Parents are stored as a pair of the form + * (r, t) + * where t is the parent term and r is the representative of equivalence + * class of t. */ - std::map > d_card_parent; + std::map>> d_cardParent; /** * Maps equivalence classes + set terms in that equivalence class to their * "flat form" (see checkNormalForms). diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ea78096dc..cdc77c980 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2068,6 +2068,7 @@ set(regress_1_tests regress1/sets/remove_check_free_31_6.smt2 regress1/sets/sets-disequal.smt2 regress1/sets/sets-tuple-poly.cvc + regress1/sets/sets-uc-wrong.smt2 regress1/sets/set-comp-sat.smt2 regress1/sets/sharingbug.smt2 regress1/sets/univ-set-uf-elim.smt2 diff --git a/test/regress/regress1/sets/sets-uc-wrong.smt2 b/test/regress/regress1/sets/sets-uc-wrong.smt2 new file mode 100644 index 000000000..e8b768d36 --- /dev/null +++ b/test/regress/regress1/sets/sets-uc-wrong.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -i +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(declare-fun t () (Set Int)) +(declare-fun s () (Set Int)) +(declare-const v Bool) +(assert (forall ((q Bool)) (distinct v (subset s t)))) +(assert (= 1 (card t))) +(check-sat) +(assert v) +(check-sat) -- 2.30.2