From 5151238c98492fe332a2603c05752f3319ae8035 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Dec 2020 09:41:31 -0600 Subject: (proof-new) Proofs for expand definitions (#5562) --- src/smt/expand_definitions.cpp | 125 +++++++++++++++++++++++++++++++++++------ src/smt/expand_definitions.h | 18 ++++++ src/smt/preprocessor.cpp | 1 + 3 files changed, 126 insertions(+), 18 deletions(-) (limited to 'src/smt') diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 20c4f8ef6..b0460fcc5 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -32,7 +32,7 @@ namespace smt { ExpandDefs::ExpandDefs(SmtEngine& smt, ResourceManager& rm, SmtEngineStatistics& stats) - : d_smt(smt), d_resourceManager(rm), d_smtStats(stats) + : d_smt(smt), d_resourceManager(rm), d_smtStats(stats), d_tpg(nullptr) { } @@ -43,6 +43,17 @@ Node ExpandDefs::expandDefinitions( std::unordered_map& cache, bool expandOnly) { + TrustNode trn = expandDefinitions(n, cache, expandOnly, nullptr); + return trn.isNull() ? Node(n) : trn.getNode(); +} + +TrustNode ExpandDefs::expandDefinitions( + TNode n, + std::unordered_map& cache, + bool expandOnly, + TConvProofGenerator* tpg) +{ + const TNode orig = n; NodeManager* nm = d_smt.getNodeManager(); std::stack> worklist; std::stack result; @@ -75,17 +86,24 @@ Node ExpandDefs::expandDefinitions( if (i != dfuns->end()) { Node f = (*i).second.getFormula(); - // must expand its definition - Node fe = expandDefinitions(f, cache, expandOnly); + const std::vector& formals = (*i).second.getFormals(); // replacement must be closed - if ((*i).second.getFormals().size() > 0) + if (!formals.empty()) + { + f = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, formals), f); + } + // are we are producing proofs for this call? + if (tpg != nullptr) { - result.push( - nm->mkNode(LAMBDA, - nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()), - fe)); - continue; + // if this is a variable, we can simply assume it + // ------- ASSUME + // n = f + Node conc = n.eqNode(f); + tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}); } + // must recursively expand its definition + TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg); + Node fe = tfe.isNull() ? f : tfe.getNode(); // don't bother putting in the cache result.push(fe); continue; @@ -126,6 +144,9 @@ Node ExpandDefs::expandDefinitions( doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr()); } } + // the premise of the proof of expansion (if we are expanding a definition + // and proofs are enabled) + std::vector pfExpChildren; if (doExpand) { std::vector formals; @@ -180,6 +201,18 @@ Node ExpandDefs::expandDefinitions( } fm = def.getFormula(); + // are we producing proofs for this call? + if (tpg != nullptr) + { + Node pfRhs = fm; + if (!formals.empty()) + { + Node bvl = nm->mkNode(BOUND_VAR_LIST, formals); + pfRhs = nm->mkNode(LAMBDA, bvl, pfRhs); + } + Assert(func.getType().isComparableTo(pfRhs.getType())); + pfExpChildren.push_back(func.eqNode(pfRhs)); + } } Node instance = fm.substitute(formals.begin(), @@ -187,9 +220,29 @@ Node ExpandDefs::expandDefinitions( n.begin(), n.begin() + formals.size()); Debug("expand") << "made : " << instance << std::endl; - - Node expanded = expandDefinitions(instance, cache, expandOnly); - cache[n] = (n == expanded ? Node::null() : expanded); + // are we producing proofs for this call? + if (tpg != nullptr) + { + if (n != instance) + { + // This code is run both when we are doing expand definitions and + // simple beta reduction. + // + // f = (lambda ((x T)) t) [if we are expanding a definition] + // ---------------------- MACRO_SR_PRED_INTRO + // n = instance + Node conc = n.eqNode(instance); + tpg->addRewriteStep(n, + instance, + PfRule::MACRO_SR_PRED_INTRO, + pfExpChildren, + {conc}); + } + } + // now, call expand definitions again on the result + TrustNode texp = expandDefinitions(instance, cache, expandOnly, tpg); + Node expanded = texp.isNull() ? instance : texp.getNode(); + cache[n] = n == expanded ? Node::null() : expanded; result.push(expanded); continue; } @@ -201,7 +254,19 @@ Node ExpandDefs::expandDefinitions( Assert(t != NULL); TrustNode trn = t->expandDefinition(n); - node = trn.isNull() ? Node(n) : trn.getNode(); + if (!trn.isNull()) + { + node = trn.getNode(); + if (tpg != nullptr) + { + tpg->addRewriteStep( + n, node, trn.getGenerator(), PfRule::THEORY_EXPAND_DEF); + } + } + else + { + node = n; + } } // the partial functions can fall through, in which case we still @@ -252,27 +317,51 @@ Node ExpandDefs::expandDefinitions( AlwaysAssert(result.size() == 1); - return result.top(); + Node res = result.top(); + + if (res == orig) + { + return TrustNode::null(); + } + return TrustNode::mkTrustRewrite(orig, res, tpg); } void ExpandDefs::expandAssertions(AssertionPipeline& assertions, bool expandOnly) { Chat() << "expanding definitions in assertions..." << std::endl; - Trace("simplify") << "ExpandDefs::simplify(): expanding definitions" + Trace("exp-defs") << "ExpandDefs::simplify(): expanding definitions" << std::endl; TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime); std::unordered_map cache; for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) { Node assert = assertions[i]; - Node expd = expandDefinitions(assert, cache, expandOnly); - if (expd != assert) + // notice we call this method with only one value of expandOnly currently, + // hence we maintain only a single set of proof steps in d_tpg. + TrustNode expd = expandDefinitions(assert, cache, expandOnly, d_tpg.get()); + if (!expd.isNull()) { - assertions.replace(i, expd); + Trace("exp-defs") << "ExpandDefs::expandAssertions: " << assert << " -> " + << expd.getNode() << std::endl; + assertions.replaceTrusted(i, expd); } } } +void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm) +{ + if (d_tpg == nullptr) + { + d_tpg.reset(new TConvProofGenerator(pnm, + d_smt.getUserContext(), + TConvPolicy::FIXPOINT, + TConvCachePolicy::NEVER, + "ExpandDefs::TConvProofGenerator", + nullptr, + true)); + } +} + } // namespace smt } // namespace CVC4 diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index f40ee4a4e..5b75ddadd 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -20,6 +20,7 @@ #include #include "expr/node.h" +#include "expr/term_conversion_proof_generator.h" #include "preprocessing/assertion_pipeline.h" #include "smt/smt_engine_stats.h" #include "util/resource_manager.h" @@ -61,13 +62,30 @@ class ExpandDefs void expandAssertions(preprocessing::AssertionPipeline& assertions, bool expandOnly = false); + /** + * Set proof node manager, which signals this class to enable proofs using the + * given proof node manager. + */ + void setProofNodeManager(ProofNodeManager* pnm); + private: + /** + * Helper function for above, called to specify if we want proof production + * based on the optional argument tpg. + */ + theory::TrustNode expandDefinitions( + TNode n, + std::unordered_map& cache, + bool expandOnly, + TConvProofGenerator* tpg); /** Reference to the SMT engine */ SmtEngine& d_smt; /** Reference to resource manager */ ResourceManager& d_resourceManager; /** Reference to the SMT stats */ SmtEngineStatistics& d_smtStats; + /** A proof generator for the term conversion. */ + std::unique_ptr d_tpg; }; } // namespace smt diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 2c8592657..9f2c8f3e7 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -159,6 +159,7 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) { Assert(pppg != nullptr); d_pnm = pppg->getManager(); + d_exDefs.setProofNodeManager(d_pnm); d_propagator.setProof(d_pnm, d_context, pppg); d_rtf.setProofNodeManager(d_pnm); } -- cgit v1.2.3