diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-09 15:11:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-09 15:11:01 -0500 |
commit | 9a939deab1a788b29b573ae7fb72a6088a1d7edf (patch) | |
tree | d403a57bac514c9e1320cdc171597c977b952ee0 /src/theory/eager_proof_generator.cpp | |
parent | 060eedcd5fdb0316d323c4528402034629285b97 (diff) |
(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.
Diffstat (limited to 'src/theory/eager_proof_generator.cpp')
-rw-r--r-- | src/theory/eager_proof_generator.cpp | 23 |
1 files changed, 19 insertions, 4 deletions
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<Node>& exp, const std::vector<Node>& args, bool isConflict) { - std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, n); - return mkTrustNode(n, pf, isConflict); + // if no children, its easy + if (exp.empty()) + { + std::shared_ptr<ProofNode> 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<ProofNode> 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<ProofNode> 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; } |