From 388cfb3cd1e80d50751b468112e91664c5c4e47a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 4 May 2022 20:26:46 -0500 Subject: [PATCH] Use purification for set comprehension reduction (#8711) Currently, the reduction lemma does not purify set comprehension from its reduction predicate. This means that our rewriter (if it were smart enough) should rewrite the reduction predicate to true. Moreover, a new forthcoming model-based instantiation technique was giving wrong answers when set comprehensions were present since it could prove the reductions were tautological. --- src/theory/sets/theory_sets_private.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 6ac904ed0..e29821d55 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -710,6 +710,7 @@ void TheorySetsPrivate::checkDisequalities() void TheorySetsPrivate::checkReduceComprehensions() { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); const std::vector& comps = d_state.getComprehensionSets(); for (const Node& n : comps) { @@ -733,9 +734,12 @@ void TheorySetsPrivate::checkReduceComprehensions() body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); Node bvl = nm->mkNode(BOUND_VAR_LIST, subs); body = nm->mkNode(EXISTS, bvl, body); - Node mem = nm->mkNode(SET_MEMBER, v, n); - Node lem = - nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem)); + Node k = sm->mkPurifySkolem(n, "kcomp"); + Node mem = nm->mkNode(SET_MEMBER, v, k); + Node lem = nm->mkNode( + AND, + k.eqNode(n), + nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem))); Trace("sets-comprehension") << "Comprehension reduction: " << lem << std::endl; d_im.lemma(lem, InferenceId::SETS_COMPREHENSION); -- 2.30.2