From 5151238c98492fe332a2603c05752f3319ae8035 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Dec 2020 09:41:31 -0600 Subject: [PATCH] (proof-new) Proofs for expand definitions (#5562) --- src/expr/proof_rule.cpp | 1 + src/expr/proof_rule.h | 3 + src/smt/expand_definitions.cpp | 125 +++++++++++++++++++++++---- src/smt/expand_definitions.h | 18 ++++ src/smt/preprocessor.cpp | 1 + src/theory/builtin/proof_checker.cpp | 21 +++-- 6 files changed, 144 insertions(+), 25 deletions(-) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 4ba483101..885c36131 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -40,6 +40,7 @@ const char* toString(PfRule id) case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA"; case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS"; case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; + case PfRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF"; case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; case PfRule::TRUST_REWRITE: return "TRUST_REWRITE"; case PfRule::TRUST_SUBS: return "TRUST_SUBS"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 58dfd973c..f00ef8367 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -231,6 +231,9 @@ enum class PfRule : uint32_t THEORY_PREPROCESS, // where F was added as a new assertion by theory preprocessing. THEORY_PREPROCESS_LEMMA, + // where F is an equality of the form t = t' where t was replaced by t' + // based on theory expand definitions. + THEORY_EXPAND_DEF, // where F is an existential (exists ((x T)) (P x)) used for introducing // a witness term (witness ((x T)) (P x)). WITNESS_AXIOM, 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); } diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 4e2e78bae..332a90d4e 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -75,10 +75,11 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3); pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3); pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3); + pc->registerTrustedChecker(PfRule::THEORY_EXPAND_DEF, this, 3); pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3); pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); - pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 3); + pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -335,7 +336,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, else if (id == PfRule::MACRO_SR_PRED_INTRO) { Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " " - << args.size() << std::endl; + << args[0] << std::endl; Assert(1 <= args.size() && args.size() <= 3); MethodId ids, idr; if (!getMethodIds(args, ids, idr, 1)) @@ -347,6 +348,9 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, { return Node::null(); } + Trace("builtin-pfcheck") << "Result is " << res << std::endl; + Trace("builtin-pfcheck") << "Witness form is " + << SkolemManager::getWitnessForm(res) << std::endl; // **** NOTE: can rewrite the witness form here. This enables certain lemmas // to be provable, e.g. (= k t) where k is a purification Skolem for t. res = Rewriter::rewrite(SkolemManager::getWitnessForm(res)); @@ -356,6 +360,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, << "Failed to rewrite to true, res=" << res << std::endl; return Node::null(); } + Trace("builtin-pfcheck") << "...success" << std::endl; return args[0]; } else if (id == PfRule::MACRO_SR_PRED_ELIM) @@ -412,11 +417,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(args.size() == 1); return RemoveTermFormulas::getAxiomFor(args[0]); } - else if (id == PfRule::PREPROCESS || id == PfRule::THEORY_PREPROCESS - || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA - || id == PfRule::PREPROCESS_LEMMA || id == PfRule::THEORY_REWRITE - || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS - || id == PfRule::TRUST_SUBS_MAP) + else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA + || id == PfRule::THEORY_PREPROCESS + || id == PfRule::THEORY_PREPROCESS_LEMMA + || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM + || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE + || id == PfRule::TRUST_SUBS || id == PfRule::TRUST_SUBS_MAP) { // "trusted" rules Assert(children.empty()); @@ -424,6 +430,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(args[0].getType().isBoolean()); return args[0]; } + // no rule return Node::null(); } -- 2.30.2