From e5c444d39c034972bce2f11c8c1c73bccd32b2bf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Mar 2022 15:55:52 -0600 Subject: [PATCH] Always purify universe from set minus (#8201) This fixes a bug in our handling of set cardinality + set universe (also used for set complement). The bug was caused by using the rewritten form of terms to compute siblings in the cardinality graph. This is problematic for (set.minus set.universe t) whose sibling was computed to be rewrite( (set.inter set.universe t) ) = t. To avoid the issue, we now purify the argument of set.minus to avoid this behavior. Fixes #5400. Fixes the first benchmark on #5402. This also eliminates a spurious lemma schema for set universe that was leftover from handling set subtyping. --- src/theory/inference_id.cpp | 1 - src/theory/inference_id.h | 1 - src/theory/sets/cardinality_extension.cpp | 16 ++++++++-- src/theory/sets/cardinality_extension.h | 4 +-- src/theory/sets/term_registry.cpp | 22 -------------- src/theory/sets/theory_sets_private.cpp | 29 ++++++++++++++++++- test/regress/CMakeLists.txt | 3 ++ .../sets/issue5400-2-card-minus-univ.smt2 | 7 +++++ .../sets/issue5400-card-minus-univ.smt2 | 10 +++++++ .../regress0/sets/issue5402-1-card.smt2 | 7 +++++ 10 files changed, 71 insertions(+), 29 deletions(-) create mode 100644 test/regress/regress0/sets/issue5400-2-card-minus-univ.smt2 create mode 100644 test/regress/regress0/sets/issue5400-card-minus-univ.smt2 create mode 100644 test/regress/regress0/sets/issue5402-1-card.smt2 diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 5968a2ff2..b5980d781 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -330,7 +330,6 @@ const char* toString(InferenceId i) case InferenceId::SETS_UP_CLOSURE: return "SETS_UP_CLOSURE"; case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2"; case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV"; - case InferenceId::SETS_UNIV_TYPE: return "SETS_UNIV_TYPE"; case InferenceId::SETS_CARD_SPLIT_EMPTY: return "SETS_CARD_SPLIT_EMPTY"; case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE"; case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 76c330cae..4734e0d60 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -477,7 +477,6 @@ enum class InferenceId SETS_UP_CLOSURE, SETS_UP_CLOSURE_2, SETS_UP_UNIV, - SETS_UNIV_TYPE, //-------------------- sets cardinality solver // split on emptyset SETS_CARD_SPLIT_EMPTY, diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 7bb752acd..5abbaab5c 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -386,10 +386,19 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, { continue; } + // should not have universe as children here, since this is either + // rewritten, or eliminated via purification from the first argument of + // set minus. + Assert(n[0].getKind() != SET_UNIVERSE && n[1].getKind() != SET_UNIVERSE); Trace("sets-debug") << "Build cardinality parents for " << n << "..." << std::endl; std::vector sib; unsigned true_sib = 0; + // Note that we use the rewriter to get the form of the siblings here. + // This is required to ensure that the lookups in the equality engine are + // accurate. However, it may lead to issues if the rewritten form of a + // node leads to unexpected relationships in the graph. To avoid this, + // we ensure that universe is not a child of a set in the assertions above. if (n.getKind() == SET_INTER) { d_localBase[n] = n; @@ -883,7 +892,8 @@ void CardinalityExtension::checkNormalForm(Node eqc, } if (!success) { - Assert(d_im.hasSent()); + Assert(d_im.hasSent()) + << "failed to send a lemma to resolve why Venn regions are different"; return; } // Send to parents (a parent is a set that contains a term in this equivalence @@ -925,7 +935,9 @@ void CardinalityExtension::checkNormalForm(Node eqc, { if (std::find(ffpc.begin(), ffpc.end(), nfeqci) == ffpc.end()) { - ffpc.insert(ffpc.end(), nfeqc.begin(), nfeqc.end()); + Trace("sets-nf-debug") << "Add to flat form " << nfeqci << " to " + << cbase << " in " << p << std::endl; + ffpc.push_back(nfeqci); } else { diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index 21d5e6e37..ac8ebfb66 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -366,8 +366,8 @@ class CardinalityExtension : protected EnvObj */ std::map>> d_cardParent; /** - * Maps equivalence classes + set terms in that equivalence class to their - * "flat form" (see checkNormalForms). + * Maps equivalence classes + "base" terms of set terms in that equivalence + * class to their "flat form" (see checkNormalForms). */ std::map > > d_ff; /** Maps equivalence classes to their "normal form" (see checkNormalForms). */ diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index d4b5aa824..93a700a5f 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -91,28 +91,6 @@ Node TermRegistry::getUnivSet(TypeNode tn) } NodeManager* nm = NodeManager::currentNM(); Node n = nm->mkNullaryOperator(tn, SET_UNIVERSE); - for (it = d_univset.begin(); it != d_univset.end(); ++it) - { - Node n1; - Node n2; - if (tn.isSubtypeOf(it->first)) - { - n1 = n; - n2 = it->second; - } - else if (it->first.isSubtypeOf(tn)) - { - n1 = it->second; - n2 = n; - } - if (!n1.isNull()) - { - Node ulem = nm->mkNode(SET_SUBSET, n1, n2); - Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" - << std::endl; - d_im.lemma(ulem, InferenceId::SETS_UNIV_TYPE); - } - } d_univset[tn] = n; return n; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index a08c051f6..b465c4162 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1320,8 +1320,35 @@ TrustNode TheorySetsPrivate::ppRewrite(Node node, { case kind::SET_CHOOSE: return expandChooseOperator(node, lems); case kind::SET_IS_SINGLETON: return expandIsSingletonOperator(node); - default: return TrustNode::null(); + case kind::SET_MINUS: + { + if (node[0].getKind() == kind::SET_UNIVERSE) + { + // Due to complications involving the cardinality graph, we must purify + // universe from argument of set minus, so that + // (set.minus set.universe x) + // is replaced by + // (set.minus univ x) + // along with the lemma (= univ set.universe), where univ is the + // purification skolem for set.universe. We require this purification + // since the cardinality graph incorrectly thinks that + // rewrite( (set.inter set.universe x) ), which evaluates to x, is + // a sibling of (set.minus set.universe x). + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node sk = sm->mkPurifySkolem(node[0], "univ"); + Trace("ajr-temp") << "PURIFY " << node[0] << " returns " << sk + << std::endl; + Node eq = sk.eqNode(node[0]); + lems.push_back(SkolemLemma(TrustNode::mkTrustLemma(eq), sk)); + Node ret = nm->mkNode(kind::SET_MINUS, sk, node[1]); + return TrustNode::mkTrustRewrite(node, ret, nullptr); + } + } + break; + default: break; } + return TrustNode::null(); } TrustNode TheorySetsPrivate::expandChooseOperator( diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6bafac256..129fbb85b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1214,6 +1214,9 @@ set(regress_0_tests regress0/sets/insert.smt2 regress0/sets/int-real-univ-unsat.smt2 regress0/sets/int-real-univ.smt2 + regress0/sets/issue5400-card-minus-univ.smt2 + regress0/sets/issue5400-2-card-minus-univ.smt2 + regress0/sets/issue5402-1-card.smt2 regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 diff --git a/test/regress/regress0/sets/issue5400-2-card-minus-univ.smt2 b/test/regress/regress0/sets/issue5400-2-card-minus-univ.smt2 new file mode 100644 index 000000000..a9ad6edfd --- /dev/null +++ b/test/regress/regress0/sets/issue5400-2-card-minus-univ.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --sets-ext +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun s () (Set Int)) +(assert (or (set.is_singleton (set.complement s)) (and (= 0 (set.card s)) (= 1 (set.card s))))) +(check-sat) diff --git a/test/regress/regress0/sets/issue5400-card-minus-univ.smt2 b/test/regress/regress0/sets/issue5400-card-minus-univ.smt2 new file mode 100644 index 000000000..4925abfb3 --- /dev/null +++ b/test/regress/regress0/sets/issue5400-card-minus-univ.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --sets-ext +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun st5 () (Set Int)) +(declare-fun st6 () (Set Int)) +(declare-fun st11 () (Set Int)) +(assert (or (set.is_singleton (set.complement st6)) (>= 10 (set.card st11) 65 0 0))) +(assert (set.is_singleton st5)) +(check-sat) diff --git a/test/regress/regress0/sets/issue5402-1-card.smt2 b/test/regress/regress0/sets/issue5402-1-card.smt2 new file mode 100644 index 000000000..2752bce06 --- /dev/null +++ b/test/regress/regress0/sets/issue5402-1-card.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --sets-ext +; EXPECT: sat +(set-logic ALL) +(declare-fun s () (Set Int)) +(assert (set.is_singleton (set.complement (set.singleton 0)))) +(assert (= 2 (set.card s))) +(check-sat) -- 2.30.2