From 656004c54655ab15289d9e7666bda2e1c7bada1c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Oct 2020 15:20:35 -0500 Subject: [PATCH] (proof-new) Update add lazy step interface in LazyCDProof (#5299) Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments. Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed). --- src/expr/lazy_proof.cpp | 4 ++-- src/expr/lazy_proof.h | 14 +++++++------- src/expr/term_conversion_proof_generator.cpp | 10 +++++++--- src/expr/term_conversion_proof_generator.h | 5 ++++- src/preprocessing/assertion_pipeline.cpp | 2 +- src/prop/proof_cnf_stream.cpp | 14 ++++++++++---- src/smt/proof_post_processor.cpp | 8 +++----- src/smt/term_formula_removal.cpp | 5 ++--- src/smt/witness_form.cpp | 7 +++---- src/theory/quantifiers/instantiate.cpp | 10 ++++------ src/theory/theory_engine.cpp | 5 ++--- src/theory/theory_preprocessor.cpp | 8 ++++---- src/theory/trust_substitutions.cpp | 18 ++++++++---------- src/theory/trust_substitutions.h | 4 +++- src/theory/uf/proof_equality_engine.cpp | 8 ++++---- 15 files changed, 64 insertions(+), 58 deletions(-) diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index a96e30fde..267da2607 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -133,10 +133,10 @@ std::shared_ptr LazyCDProof::getProofFor(Node fact) void LazyCDProof::addLazyStep(Node expected, ProofGenerator* pg, + PfRule idNull, bool isClosed, const char* ctx, - bool forceOverwrite, - PfRule idNull) + bool forceOverwrite) { if (pg == nullptr) { diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index 691902945..e2bba3015 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -67,23 +67,23 @@ class LazyCDProof : public CDProof * * @param expected The fact that can be proven. * @param pg The generator that can proof expected. + * @param trustId If a null proof generator is provided, we add a step to + * the proof that has trustId as the rule and expected as the sole argument. + * We do this only if trustId is not PfRule::ASSUME. This is primarily used + * for identifying the kind of hole when a proof generator is not given. * @param isClosed Whether to expect that pg can provide a closed proof for * this fact. * @param ctx The context we are in (for debugging). * @param forceOverwrite If this flag is true, then this call overwrites * an existing proof generator provided for expected, if one was provided * via a previous call to addLazyStep in the current context. - * @param trustId If a null proof generator is provided, we add a step to - * the proof that has trustId as the rule and expected as the sole argument. - * We do this only if trustId is not PfRule::ASSUME. This is primarily used - * for identifying the kind of hole when a proof generator is not given. */ void addLazyStep(Node expected, ProofGenerator* pg, - bool isClosed = true, + PfRule trustId = PfRule::ASSUME, + bool isClosed = false, const char* ctx = "LazyCDProof::addLazyStep", - bool forceOverwrite = false, - PfRule trustId = PfRule::ASSUME); + bool forceOverwrite = false); /** * Does this have any proof generators? This method always returns true * if the default is non-null. diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 11e8eb054..02613345f 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -62,13 +62,17 @@ TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm, TConvProofGenerator::~TConvProofGenerator() {} -void TConvProofGenerator::addRewriteStep( - Node t, Node s, ProofGenerator* pg, bool isClosed, uint32_t tctx) +void TConvProofGenerator::addRewriteStep(Node t, + Node s, + ProofGenerator* pg, + PfRule trustId, + bool isClosed, + uint32_t tctx) { Node eq = registerRewriteStep(t, s, tctx); if (!eq.isNull()) { - d_proof.addLazyStep(eq, pg, isClosed); + d_proof.addLazyStep(eq, pg, trustId, isClosed); } } diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index 184f24e13..0a1f4e70a 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -144,6 +144,8 @@ class TConvProofGenerator : public ProofGenerator /** * Add rewrite step t --> s based on proof generator. * + * @param trustId If a null proof generator is provided, we add a step to + * the proof that has trustId as the rule and expected as the sole argument. * @param isClosed whether to expect that pg can provide a closed proof for * this fact. * @param tctx The term context identifier for the rewrite step. This @@ -154,7 +156,8 @@ class TConvProofGenerator : public ProofGenerator void addRewriteStep(Node t, Node s, ProofGenerator* pg, - bool isClosed = true, + PfRule trustId = PfRule::ASSUME, + bool isClosed = false, uint32_t tctx = 0); /** Same as above, for a single step */ void addRewriteStep(Node t, Node s, ProofStep ps, uint32_t tctx = 0); diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 78c459cb7..cd7aadf9a 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -177,7 +177,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) // rewrite( d_nodes[i] ^ n ) // allocate a fresh proof which will act as the proof generator LazyCDProof* lcp = d_pppg->allocateHelperProof(); - lcp->addLazyStep(n, pg, false); + lcp->addLazyStep(n, pg, PfRule::PREPROCESS); if (d_nodes[i].isConst() && d_nodes[i].getConst()) { // skip the AND_INTRO if the previous d_nodes[i] was true diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index b2d33a61d..790e5aeb2 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -81,8 +81,11 @@ void ProofCnfStream::convertAndAssert(TNode node, Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify() << "\n"; Node toJustify = negated ? node.notNode() : static_cast(node); - d_proof.addLazyStep( - toJustify, pg, true, "ProofCnfStream::convertAndAssert:cnf"); + d_proof.addLazyStep(toJustify, + pg, + PfRule::ASSUME, + true, + "ProofCnfStream::convertAndAssert:cnf"); } convertAndAssert(node, negated); // process saved steps in buffer @@ -519,8 +522,11 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn) Assert(trn.getGenerator()->getProofFor(proven)->isClosed()); Trace("cnf-steps") << proven << " by explainPropagation " << trn.identifyGenerator() << std::endl; - d_proof.addLazyStep( - proven, trn.getGenerator(), true, "ProofCnfStream::convertPropagation"); + d_proof.addLazyStep(proven, + trn.getGenerator(), + PfRule::ASSUME, + true, + "ProofCnfStream::convertPropagation"); // since the propagation is added directly to the SAT solver via theoryProxy, // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here NodeManager* nm = NodeManager::currentNM(); diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 0c2f8ccf8..a7723d265 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -460,8 +460,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // add previous rewrite steps for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - // not necessarily closed, so we pass false to addRewriteStep. - tcg.addRewriteStep(vvec[j], svec[j], pgs[j], false); + tcg.addRewriteStep(vvec[j], svec[j], pgs[j]); } // get the proof for the update to the current substitution Node seqss = subs.eqNode(ss); @@ -506,8 +505,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, true); for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - // not necessarily closed, so we pass false to addRewriteStep. - tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], false); + tcpg.addRewriteStep(vvec[j], svec[j], pgs[j]); } // add the proof constructed by the term conversion utility std::shared_ptr pfn = tcpg.getProofFor(eq); @@ -545,10 +543,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, Node eq = args[0].eqNode(ret); if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT) { - // rewrites from theory::Rewriter // automatically expand THEORY_REWRITE as well here if set bool elimTR = (d_elimRules.find(PfRule::THEORY_REWRITE) != d_elimRules.end()); + // rewrites from theory::Rewriter bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT); // use rewrite with proof interface Rewriter* rr = d_smte->getRewriter(); diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index cf7c00e2b..46135f12a 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -334,10 +334,9 @@ Node RemoveTermFormulas::runCurrent(std::pair& curr, ProofGenerator* expg = sm->getProofGenerator(existsAssertion); d_lp->addLazyStep(existsAssertion, expg, + PfRule::WITNESS_AXIOM, true, - "RemoveTermFormulas::run:skolem_pf", - false, - PfRule::WITNESS_AXIOM); + "RemoveTermFormulas::run:skolem_pf"); d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {}); newAssertionPg = d_lp.get(); } diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index e4f0a56dc..9c2c035a8 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -114,12 +114,11 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) d_wintroPf.addLazyStep( exists, pg, + PfRule::WITNESS_AXIOM, true, - "WitnessFormGenerator::convertToWitnessForm:witness_axiom", - false, - PfRule::WITNESS_AXIOM); + "WitnessFormGenerator::convertToWitnessForm:witness_axiom"); d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); - d_tcpg.addRewriteStep(cur, curw, &d_wintroPf); + d_tcpg.addRewriteStep(cur, curw, &d_wintroPf, PfRule::ASSUME, true); } else { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index f88c2e7a0..8549b1eae 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -268,10 +268,9 @@ bool Instantiate::addInstantiation( // add the transformation proof, or THEORY_PREPROCESS if none provided pfTmp->addLazyStep(proven, tpBody.getGenerator(), + PfRule::THEORY_PREPROCESS, true, - "Instantiate::getInstantiation:qpreprocess", - false, - PfRule::THEORY_PREPROCESS); + "Instantiate::getInstantiation:qpreprocess"); pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {}); } } @@ -477,10 +476,9 @@ Node Instantiate::getInstantiation(Node q, Node proven = trn.getProven(); pf->addLazyStep(proven, trn.getGenerator(), + PfRule::THEORY_PREPROCESS, true, - "Instantiate::getInstantiation:rewrite_inst", - false, - PfRule::THEORY_PREPROCESS); + "Instantiate::getInstantiation:rewrite_inst"); pf->addStep(newBody, PfRule::EQ_RESOLVE, {body, proven}, {}); } body = newBody; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index aaa010148..924d045da 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1462,10 +1462,9 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, { d_lazyProof->addLazyStep(tplemma.getProven(), tplemma.getGenerator(), + PfRule::PREPROCESS_LEMMA, true, - "TheoryEngine::lemma_pp", - false, - PfRule::PREPROCESS_LEMMA); + "TheoryEngine::lemma_pp"); // ---------- from d_lazyProof -------------- from theory preprocess // lemma lemma = lemmap // ------------------------------------------ EQ_RESOLVE diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index e7cdb8f2c..b37a45967 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -213,10 +213,9 @@ TrustNode TheoryPreprocessor::preprocess(TNode node, // store in the lazy proof d_lp->addLazyStep(assertion, trn.getGenerator(), + PfRule::THEORY_PREPROCESS_LEMMA, true, - "TheoryPreprocessor::rewrite_lemma_new", - false, - PfRule::THEORY_PREPROCESS_LEMMA); + "TheoryPreprocessor::rewrite_lemma_new"); d_lp->addStep(rewritten, PfRule::MACRO_SR_PRED_TRANSFORM, {assertion}, @@ -433,7 +432,8 @@ Node TheoryPreprocessor::preprocessWithProof(Node term) trn.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::preprocessWithProof"); // always use term context hash 0 (default) - d_tpg->addRewriteStep(term, termr, trn.getGenerator()); + d_tpg->addRewriteStep( + term, termr, trn.getGenerator(), PfRule::ASSUME, true); } else { diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index 482c487eb..27159f964 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -54,12 +54,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg) // current substitution node is no longer valid. d_currentSubs = Node::null(); // add to lazy proof - d_subsPg->addLazyStep(tnl.getProven(), - pg, - false, - "TrustSubstitutionMap::addSubstitution", - false, - d_trustId); + d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId); } } @@ -79,7 +74,9 @@ void TrustSubstitutionMap::addSubstitution(TNode x, addSubstitution(x, t, stepPg); } -void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn) +ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x, + TNode t, + TrustNode tn) { Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add " << x << " -> " << t << " from " << tn.getProven() @@ -89,7 +86,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn) // no generator or not proof enabled, nothing to do addSubstitution(x, t, nullptr); Trace("trust-subs") << "...no proof" << std::endl; - return; + return nullptr; } Node eq = x.eqNode(t); Node proven = tn.getProven(); @@ -100,7 +97,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn) // no rewrite required, just use the generator addSubstitution(x, t, tn.getGenerator()); Trace("trust-subs") << "...use generator directly" << std::endl; - return; + return tn.getGenerator(); } LazyCDProof* solvePg = d_helperPf.allocateProof(); // Try to transform tn.getProven() to (= x t) here, if necessary @@ -109,7 +106,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn) // failed to rewrite addSubstitution(x, t, nullptr); Trace("trust-subs") << "...failed to rewrite" << std::endl; - return; + return nullptr; } Trace("trust-subs") << "...successful rewrite" << std::endl; solvePg->addSteps(*d_tspb.get()); @@ -117,6 +114,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn) // link the given generator solvePg->addLazyStep(proven, tn.getGenerator()); addSubstitution(x, t, solvePg); + return solvePg; } void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t) diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 91555ee56..d7f48d054 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -68,8 +68,10 @@ class TrustSubstitutionMap * based on transforming the tn.getProven() to (= x t) if tn has a * non-null proof generator; otherwise if tn has no proof generator * we simply add the substitution. + * + * @return The proof generator that can prove (= x t). */ - void addSubstitutionSolved(TNode x, TNode t, TrustNode tn); + ProofGenerator* addSubstitutionSolved(TNode x, TNode t, TrustNode tn); /** * Add substitutions from trust substitution map t. This adds all * substitutions from the map t and carries over its information about proofs. diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 77ee1effd..184584aa9 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -68,7 +68,7 @@ bool ProofEqEngine::assertFact(Node lit, ps.d_args = args; d_factPg.addStep(lit, ps); // add lazy step to proof - d_proof.addLazyStep(lit, &d_factPg, false); + d_proof.addLazyStep(lit, &d_factPg); // second, assert it to the equality engine Node reason = NodeManager::currentNM()->mkAnd(exp); return assertFactInternal(atom, polarity, reason); @@ -116,7 +116,7 @@ bool ProofEqEngine::assertFact(Node lit, ps.d_args = args; d_factPg.addStep(lit, ps); // add lazy step to proof - d_proof.addLazyStep(lit, &d_factPg, false); + d_proof.addLazyStep(lit, &d_factPg); // second, assert it to the equality engine return assertFactInternal(atom, polarity, exp); } @@ -140,7 +140,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb) d_factPg.addStep(step.first, step.second); } // add lazy step to proof - d_proof.addLazyStep(lit, &d_factPg, false); + d_proof.addLazyStep(lit, &d_factPg); // second, assert it to the equality engine return assertFactInternal(atom, polarity, exp); } @@ -157,7 +157,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg) return false; } // note the proof generator is responsible for remembering the explanation - d_proof.addLazyStep(lit, pg, false); + d_proof.addLazyStep(lit, pg); // second, assert it to the equality engine return assertFactInternal(atom, polarity, exp); } -- 2.30.2