From: Andrew Reynolds Date: Thu, 12 Nov 2020 16:33:32 +0000 (-0600) Subject: (proof-new) Proofs for skolemization (#5339) X-Git-Tag: cvc5-1.0.0~2608 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f367612a386d21315cee7d377176bc83a1402c5;p=cvc5.git (proof-new) Proofs for skolemization (#5339) This adds support for proofs in the quantifiers module that performs skolemization. Also fixes a bug in the proof checker for skolemization. --- diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 8371492b5..5f6e4a119 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -97,6 +97,7 @@ Node QuantifiersProofRuleChecker::checkInternal( else { std::vector echildren(children[0][0].begin(), children[0][0].end()); + echildren[1] = echildren[1].notNode(); exists = nm->mkNode(EXISTS, echildren); } std::vector skolems; diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 43f656a2a..61dd0c15e 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/skolemize.h" +#include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_util.h" @@ -27,24 +28,65 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Skolemize::Skolemize(QuantifiersEngine* qe, context::UserContext* u) - : d_quantEngine(qe), d_skolemized(u) +Skolemize::Skolemize(QuantifiersEngine* qe, + context::UserContext* u, + ProofNodeManager* pnm) + : d_quantEngine(qe), + d_skolemized(u), + d_pnm(pnm), + d_epg(pnm == nullptr ? nullptr + : new EagerProofGenerator(pnm, u, "Skolemize::epg")) { } -Node Skolemize::process(Node q) +TrustNode Skolemize::process(Node q) { + Assert(q.getKind() == FORALL); // do skolemization - if (d_skolemized.find(q) == d_skolemized.end()) + if (d_skolemized.find(q) != d_skolemized.end()) { + return TrustNode::null(); + } + Node lem; + ProofGenerator* pg = nullptr; + if (isProofEnabled() && !options::dtStcInduction() + && !options::intWfInduction()) + { + // if using proofs and not using induction, we use the justified + // skolemization + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* skm = nm->getSkolemManager(); + std::vector echildren(q.begin(), q.end()); + echildren[1] = echildren[1].notNode(); + Node existsq = nm->mkNode(EXISTS, echildren); + Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv"); + Node qnot = q.notNode(); + CDProof cdp(d_pnm); + cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {}); + std::shared_ptr pf = cdp.getProofFor(res); + std::vector assumps; + assumps.push_back(qnot); + std::shared_ptr pfs = d_pnm->mkScope({pf}, assumps); + lem = nm->mkNode(IMPLIES, qnot, res); + d_epg->setProofFor(lem, pfs); + pg = d_epg.get(); + Trace("quantifiers-sk") + << "Skolemize (with proofs) : " << d_skolem_constants[q] << " for " + << std::endl; + Trace("quantifiers-sk") << " " << q << std::endl; + Trace("quantifiers-sk") << " " << res << std::endl; + } + else + { + // otherwise, we use the more general skolemization with inductive + // strengthening, which does not support proofs Node body = getSkolemizedBody(q); NodeBuilder<> nb(kind::OR); nb << q << body.notNode(); - Node lem = nb; - d_skolemized[q] = lem; - return lem; + lem = nb; } - return Node::null(); + d_skolemized[q] = lem; + return TrustNode::mkTrustLemma(lem, pg); } bool Skolemize::getSkolemConstants(Node q, std::vector& skolems) @@ -274,16 +316,8 @@ Node Skolemize::mkSkolemizedBody(Node f, ret, f.getAttribute(InstLevelAttribute())); } - if (Trace.isOn("quantifiers-sk")) - { - Trace("quantifiers-sk") << "Skolemize : "; - for (unsigned i = 0; i < sk.size(); i++) - { - Trace("quantifiers-sk") << sk[i] << " "; - } - Trace("quantifiers-sk") << "for " << std::endl; - Trace("quantifiers-sk") << " " << f << std::endl; - } + Trace("quantifiers-sk") << "Skolemize : " << sk << " for " << std::endl; + Trace("quantifiers-sk") << " " << f << std::endl; return ret; } @@ -291,14 +325,17 @@ Node Skolemize::mkSkolemizedBody(Node f, Node Skolemize::getSkolemizedBody(Node f) { Assert(f.getKind() == FORALL); - if (d_skolem_body.find(f) == d_skolem_body.end()) + std::unordered_map::iterator it = + d_skolem_body.find(f); + if (it == d_skolem_body.end()) { std::vector fvTypes; std::vector fvs; Node sub; std::vector sub_vars; - d_skolem_body[f] = mkSkolemizedBody( + Node ret = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars); + d_skolem_body[f] = ret; // store sub quantifier information if (!sub.isNull()) { @@ -320,8 +357,9 @@ Node Skolemize::getSkolemizedBody(Node f) f, f[0][i], d_skolem_constants[f][i]); } } + return ret; } - return d_skolem_body[f]; + return it->second; } bool Skolemize::isInductionTerm(Node n) @@ -332,7 +370,7 @@ bool Skolemize::isInductionTerm(Node n) const DType& dt = tn.getDType(); return !dt.isCodatatype(); } - if (options::intWfInduction() && n.getType().isInteger()) + if (options::intWfInduction() && tn.isInteger()) { return true; } @@ -364,6 +402,8 @@ bool Skolemize::printSkolemization(std::ostream& out) return printed; } +bool Skolemize::isProofEnabled() const { return d_epg != nullptr; } + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 6db3f6215..4469fe851 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/type_node.h" #include "theory/quantifiers/quant_util.h" +#include "theory/trust_node.h" namespace CVC4 { @@ -63,15 +64,16 @@ class Skolemize typedef context::CDHashMap NodeNodeMap; public: - Skolemize(QuantifiersEngine* qe, context::UserContext* u); + Skolemize(QuantifiersEngine* qe, + context::UserContext* u, + ProofNodeManager* pnm); ~Skolemize() {} /** skolemize quantified formula q - * If the return value ret of this function - * is non-null, then ret is a new skolemization lemma - * we generated for q. These lemmas are constructed - * once per user-context. + * If the return value ret of this function is non-null, then ret is a trust + * node corresponding to a new skolemization lemma we generated for q. These + * lemmas are constructed once per user-context. */ - Node process(Node q); + TrustNode process(Node q); /** get skolem constants for quantified formula q */ bool getSkolemConstants(Node q, std::vector& skolems); /** get the i^th skolem constant for quantified formula q */ @@ -119,6 +121,8 @@ class Skolemize bool printSkolemization(std::ostream& out); private: + /** Are proofs enabled? */ + bool isProofEnabled() const; /** get self selectors * For datatype constructor dtc with type dt, * this collects the set of datatype selector applications, @@ -139,6 +143,10 @@ class Skolemize d_skolem_constants; /** map from quantified formulas to their skolemized body */ std::unordered_map d_skolem_body; + /** Pointer to the proof node manager */ + ProofNodeManager* d_pnm; + /** Eager proof generator for skolemization lemmas */ + std::unique_ptr d_epg; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index cceb04d9f..7f0b46c99 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,7 +30,8 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, +QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, + DecisionManager& dm, ProofNodeManager* pnm) : d_te(te), d_context(te->getSatContext()), @@ -49,7 +50,7 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)), - d_skolemize(new quantifiers::Skolemize(this, d_userContext)), + d_skolemize(new quantifiers::Skolemize(this, d_userContext, pnm)), d_term_enum(new quantifiers::TermEnumeration), d_conflict_c(d_context, false), d_quants_prereg(d_userContext), @@ -809,16 +810,16 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ } if( !pol ){ // do skolemization - Node lem = d_skolemize->process(f); + TrustNode lem = d_skolemize->process(f); if (!lem.isNull()) { if (Trace.isOn("quantifiers-sk-debug")) { - Node slem = Rewriter::rewrite(lem); + Node slem = Rewriter::rewrite(lem.getNode()); Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } - getOutputChannel().lemma( + getOutputChannel().trustedLemma( lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY); } return;