From: Andrew Reynolds Date: Fri, 23 Apr 2021 20:44:39 +0000 (-0500) Subject: (proof-new) Proofs for sets purification lemmas (#6416) X-Git-Tag: cvc5-1.0.0~1841 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=557e5658048b48b8908675b632fc977f78c71605;p=cvc5.git (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 285d53c4a..f759c2a7b 100644 --- a/src/theory/sets/skolem_cache.cpp +++ b/src/theory/sets/skolem_cache.cpp @@ -35,8 +35,19 @@ Node SkolemCache::mkTypedSkolemCached( std::map::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 af9d9e42d..be8e5858e 100644 --- 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 718559a0a..f98f204e0 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -22,6 +22,7 @@ #include #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 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 d_emptyset; /** Map from types to universe set of that type */ std::map d_univset; + /** Eager proof generator for purification lemmas */ + std::unique_ptr d_epg; }; /* class TheorySetsPrivate */ } // namespace sets diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 8406bd14a..4cca76057 100644 --- 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 034af2848..fad14bb71 100644 --- 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 9bca25ea2..952bfd83b 100644 --- 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();