(proof-new) Proofs for sets purification lemmas (#6416)

This adds proofs for sets purification lemmas, which are of the form (= t (skolem t)) and (member t (skolem (singleton t))). Each can be trivially justified in the internal calculus by MACRO_SR_PRED_INTRO.

diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp
index 285d53c4a1dea00be6f70dc256631bf64dbd039d..f759c2a7b15ff093265b70410ea49e75ffcb4c48 100644 (file)
--- a/src/theory/sets/skolem_cache.cpp
+++ b/src/theory/sets/skolem_cache.cpp
@@ -35,8 +35,19 @@ Node SkolemCache::mkTypedSkolemCached(
   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
   if (it == d_skolemCache[a][b].end())
   {
-    Node sk = mkTypedSkolem(tn, c);
+    SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+    Node sk;
+    if (id == SkolemId::SK_PURIFY)
+    {
+      Assert(a.getType() == tn);
+      sk = sm->mkPurifySkolem(a, c);
+    }
+    else
+    {
+      sk = sm->mkDummySkolem(c, tn, "sets skolem");
+    }
     d_skolemCache[a][b][id] = sk;
+    d_allSkolems.insert(sk);
     return sk;
   }
   return it->second;

diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
index af9d9e42dcce22a6b4c49ef5348f63e5ca5f141c..be8e5858edea5489c88863bd352b57370026d3cf 100644 (file)
--- a/src/theory/sets/term_registry.cpp
+++ b/src/theory/sets/term_registry.cpp
@@ -27,11 +27,15 @@ namespace sets {
 
 TermRegistry::TermRegistry(SolverState& state,
                            InferenceManager& im,
-                           SkolemCache& skc)
+                           SkolemCache& skc,
+                           ProofNodeManager* pnm)
     : d_im(im),
       d_skCache(skc),
       d_proxy(state.getUserContext()),
-      d_proxy_to_term(state.getUserContext())
+      d_proxy_to_term(state.getUserContext()),
+      d_epg(
+          pnm ? new EagerProofGenerator(pnm, nullptr, "sets::TermRegistry::epg")
+              : nullptr)
 {
 }
 
@@ -51,17 +55,15 @@ Node TermRegistry::getProxy(Node n)
   NodeManager* nm = NodeManager::currentNM();
   Node k = d_skCache.mkTypedSkolemCached(
       n.getType(), n, SkolemCache::SK_PURIFY, "sp");
+
   d_proxy[n] = k;
   d_proxy_to_term[k] = n;
   Node eq = k.eqNode(n);
-  Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
-  d_im.lemma(eq, InferenceId::SETS_PROXY);
+  sendSimpleLemmaInternal(eq, InferenceId::SETS_PROXY);
   if (nk == SINGLETON)
   {
     Node slem = nm->mkNode(MEMBER, n[0], k);
-    Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
-                        << std::endl;
-    d_im.lemma(slem, InferenceId::SETS_PROXY_SINGLETON);
+    sendSimpleLemmaInternal(slem, InferenceId::SETS_PROXY_SINGLETON);
   }
   return k;
 }
@@ -152,6 +154,21 @@ void TermRegistry::debugPrintSet(Node s, const char* c) const
   }
 }
 
+void TermRegistry::sendSimpleLemmaInternal(Node n, InferenceId id)
+{
+  Trace("sets-lemma") << "Sets::Lemma : " << n << " by " << id << std::endl;
+  if (d_epg.get() != nullptr)
+  {
+    TrustNode teq =
+        d_epg->mkTrustNode(n, PfRule::MACRO_SR_PRED_INTRO, {}, {n});
+    d_im.trustedLemma(teq, id);
+  }
+  else
+  {
+    d_im.lemma(n, id);
+  }
+}
+
 }  // namespace sets
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h
index 718559a0a053001212be2e3f7f693411089abdc4..f98f204e009bb21c06ef59f3cdbc22bd67014b13 100644 (file)
--- a/src/theory/sets/term_registry.h
+++ b/src/theory/sets/term_registry.h
@@ -22,6 +22,7 @@
 #include <vector>
 
 #include "context/cdhashmap.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/skolem_cache.h"
 #include "theory/sets/solver_state.h"
@@ -39,7 +40,10 @@ class TermRegistry
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
  public:
-  TermRegistry(SolverState& state, InferenceManager& im, SkolemCache& skc);
+  TermRegistry(SolverState& state,
+               InferenceManager& im,
+               SkolemCache& skc,
+               ProofNodeManager* pnm);
   /** Get type constraint skolem
    *
    * The sets theory solver outputs equality lemmas of the form:
@@ -72,6 +76,8 @@ class TermRegistry
   void debugPrintSet(Node s, const char* c) const;
 
  private:
+  /** Send simple lemma internal */
+  void sendSimpleLemmaInternal(Node n, InferenceId id);
   /** The inference manager */
   InferenceManager& d_im;
   /** Reference to the skolem cache */
@@ -86,6 +92,8 @@ class TermRegistry
   std::map<TypeNode, Node> d_emptyset;
   /** Map from types to universe set of that type */
   std::map<TypeNode, Node> d_univset;
+  /** Eager proof generator for purification lemmas */
+  std::unique_ptr<EagerProofGenerator> d_epg;
 }; /* class TheorySetsPrivate */
 
 }  // namespace sets

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 8406bd14ab03a6f6d10f70a56502a19bf11ec6bf..4cca76057a21574bb4dc9c3ecbd7ba2a2818eaa0 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -37,7 +37,7 @@ TheorySets::TheorySets(context::Context* c,
       d_skCache(),
       d_state(c, u, valuation, d_skCache),
       d_im(*this, d_state, nullptr),
-      d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)),
+      d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)),
       d_notify(*d_internal.get(), d_im)
 {
   // use the official theory state and inference manager objects

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 034af284808ec7f8579a72be043729d265fd1c92..fad14bb71af3fce6765a93a1c072646fd030e55a 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -38,7 +38,8 @@ namespace sets {
 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
                                      SolverState& state,
                                      InferenceManager& im,
-                                     SkolemCache& skc)
+                                     SkolemCache& skc,
+                                     ProofNodeManager* pnm)
     : d_deq(state.getSatContext()),
       d_termProcessed(state.getUserContext()),
       d_fullCheckIncomplete(false),
@@ -47,7 +48,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
       d_state(state),
       d_im(im),
       d_skCache(skc),
-      d_treg(state, im, skc),
+      d_treg(state, im, skc, pnm),
       d_rels(new TheorySetsRels(state, im, skc, d_treg)),
       d_cardSolver(new CardinalityExtension(state, im, d_treg)),
       d_rels_enabled(false),

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 9bca25ea23eebce310c649b80f78fb249581efa0..952bfd83b2ab51db281ffd0943e6e0494f9ac3d8 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -136,7 +136,8 @@ class TheorySetsPrivate {
   TheorySetsPrivate(TheorySets& external,
                     SolverState& state,
                     InferenceManager& im,
-                    SkolemCache& skc);
+                    SkolemCache& skc,
+                    ProofNodeManager* pnm);
 
   ~TheorySetsPrivate();