From: Andrew Reynolds Date: Wed, 9 Sep 2020 20:11:01 +0000 (-0500) Subject: (proof-new) Generalize single step helper in eager proof generator (#5046) X-Git-Tag: cvc5-1.0.0~2883 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9a939deab1a788b29b573ae7fb72a6088a1d7edf;p=cvc5.git (proof-new) Generalize single step helper in eager proof generator (#5046) This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas. --- diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp index c390a4b25..81c3e7816 100644 --- a/src/theory/combination_care_graph.cpp +++ b/src/theory/combination_care_graph.cpp @@ -63,15 +63,15 @@ void CombinationCareGraph::combineTheories() Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; - Node split = equality.orNode(equality.notNode()); TrustNode tsplit; if (isProofEnabled()) { // make proof of splitting lemma - tsplit = d_cmbsPg->mkTrustNode(split, PfRule::SPLIT, {equality}); + tsplit = d_cmbsPg->mkTrustNodeSplit(equality); } else { + Node split = equality.orNode(equality.notNode()); tsplit = TrustNode::mkTrustLemma(split, nullptr); } sendLemma(tsplit, carePair.d_theory); diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index 09f02708b..ddf1a4d3a 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -14,6 +14,7 @@ #include "theory/eager_proof_generator.h" +#include "expr/proof.h" #include "expr/proof_node_manager.h" namespace CVC4 { @@ -93,13 +94,27 @@ TrustNode EagerProofGenerator::mkTrustNode(Node n, return TrustNode::mkTrustLemma(n, this); } -TrustNode EagerProofGenerator::mkTrustNode(Node n, +TrustNode EagerProofGenerator::mkTrustNode(Node conc, PfRule id, + const std::vector& exp, const std::vector& args, bool isConflict) { - std::shared_ptr pf = d_pnm->mkNode(id, {}, args, n); - return mkTrustNode(n, pf, isConflict); + // if no children, its easy + if (exp.empty()) + { + std::shared_ptr pf = d_pnm->mkNode(id, {}, args, conc); + return mkTrustNode(conc, pf, isConflict); + } + // otherwise, we use CDProof + SCOPE + CDProof cdp(d_pnm); + cdp.addStep(conc, id, exp, args); + std::shared_ptr pf = cdp.getProofFor(conc); + // We use mkNode instead of mkScope, since there is no reason to check + // whether the free assumptions of pf are in exp, since they are by the + // construction above. + std::shared_ptr pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp); + return mkTrustNode(pfs->getResult(), pfs, isConflict); } TrustNode EagerProofGenerator::mkTrustedPropagation( @@ -117,7 +132,7 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f) { // make the lemma Node lem = f.orNode(f.notNode()); - return mkTrustNode(lem, PfRule::SPLIT, {f}, false); + return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false); } std::string EagerProofGenerator::identify() const { return d_name; } diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 226750a91..018bf7aea 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -116,20 +116,21 @@ class EagerProofGenerator : public ProofGenerator std::shared_ptr pf, bool isConflict = false); /** - * Make trust node from a single step proof (with no premises). This is a - * convenience function that avoids the need to explictly construct ProofNode - * by the caller. + * Make trust node from a single step proof. This is a convenience function + * that avoids the need to explictly construct ProofNode by the caller. * - * @param n The proven node, - * @param id The rule of the proof concluding n - * @param args The arguments to the proof concluding n, + * @param conc The conclusion of the rule, + * @param id The rule of the proof concluding conc + * @param exp The explanation (premises) to the proof concluding conc, + * @param args The arguments to the proof concluding conc, * @param isConflict Whether the returned trust node is a conflict (otherwise * it is a lemma), * @return The trust node corresponding to the fact that this generator has - * a proof of n. + * a proof of (children => exp), or of exp if children is empty. */ - TrustNode mkTrustNode(Node n, + TrustNode mkTrustNode(Node conc, PfRule id, + const std::vector& exp, const std::vector& args, bool isConflict = false); /** diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 3e6f66b73..080349f73 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -52,7 +52,11 @@ TermRegistry::TermRegistry(SolverState& s, d_proxyVar(s.getUserContext()), d_proxyVarToLength(s.getUserContext()), d_lengthLemmaTermsCache(s.getUserContext()), - d_epg(nullptr) + d_epg(pnm ? new EagerProofGenerator( + pnm, + s.getUserContext(), + "strings::TermRegistry::EagerProofGenerator") + : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -282,7 +286,7 @@ void TermRegistry::registerTerm(Node n, int effort) if (d_epg != nullptr) { regTermLem = d_epg->mkTrustNode( - eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {n}); + eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n}); } else { @@ -384,7 +388,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n) // it is a simple rewrite to justify this if (d_epg != nullptr) { - return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {ret}); + return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret}); } return TrustNode::mkTrustLemma(ret, nullptr); } @@ -508,7 +512,7 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma( if (d_epg != nullptr) { - return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {n}); + return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n}); } return TrustNode::mkTrustLemma(lenLemma, nullptr); }