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.
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";
SETS_UP_CLOSURE,
SETS_UP_CLOSURE_2,
SETS_UP_UNIV,
- SETS_UNIV_TYPE,
//-------------------- sets cardinality solver
// split on emptyset
SETS_CARD_SPLIT_EMPTY,
{
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<Node> 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;
}
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
{
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
{
*/
std::map<Node, std::vector<std::pair<Node, Node>>> 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<Node, std::map<Node, std::vector<Node> > > d_ff;
/** Maps equivalence classes to their "normal form" (see checkNormalForms). */
}
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;
}
{
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(
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
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff