From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 5 May 2022 01:26:46 +0000 (-0500)
Subject: Use purification for set comprehension reduction (#8711)
X-Git-Tag: cvc5-1.0.1~168
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=388cfb3cd1e80d50751b468112e91664c5c4e47a;p=cvc5.git

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.
---

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<Node>& 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);