diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 14:48:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-12 14:48:31 -0500 |
commit | 2174ab36023326cd998565bbf35d31c38bc10594 (patch) | |
tree | a61a1cb1cc00faa1339adf315fd4037b0ca08b1a /src/expr/lazy_proof.cpp | |
parent | 27413a45e28001f6155d529a59d679556cdc011e (diff) |
(proof-new) Improve interfaces to proof generators (#4803)
This includes configurable naming and a caching policy for term conversion proof generator.
Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.
Diffstat (limited to 'src/expr/lazy_proof.cpp')
-rw-r--r-- | src/expr/lazy_proof.cpp | 66 |
1 files changed, 43 insertions, 23 deletions
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index df0258af7..dc984438c 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -20,8 +20,9 @@ namespace CVC4 { LazyCDProof::LazyCDProof(ProofNodeManager* pnm, ProofGenerator* dpg, - context::Context* c) - : CDProof(pnm, c), d_gens(c ? c : &d_context), d_defaultGen(dpg) + context::Context* c, + std::string name) + : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg) { } @@ -56,36 +57,47 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact) if (it == visited.end()) { visited.insert(cur); - if (cur->getRule() == PfRule::ASSUME) + Node cfact = cur->getResult(); + if (getProof(cfact).get() != cur) + { + // We don't own this proof, skip it. This is to ensure that this method + // is idempotent, since it may be the case that a previous call to + // getProofFor connected a proof from a proof generator as a child of + // a ProofNode in the range of the map in CDProof. Thus, this ensures + // we don't touch such proofs. + Trace("lazy-cdproof") << "...skip unowned proof" << std::endl; + } + else if (cur->getRule() == PfRule::ASSUME) { - Node afact = cur->getResult(); bool isSym = false; - ProofGenerator* pg = getGeneratorFor(afact, isSym); + ProofGenerator* pg = getGeneratorFor(cfact, isSym); if (pg != nullptr) { - Trace("lazy-cdproof") << "LazyCDProof: Call generator for assumption " - << afact << std::endl; - Node afactGen = isSym ? CDProof::getSymmFact(afact) : afact; - Assert(!afactGen.isNull()); - // use the addProofTo interface - if (!pg->addProofTo(afactGen, this)) + Trace("lazy-cdproof") + << "LazyCDProof: Call generator " << pg->identify() + << " for assumption " << cfact << std::endl; + Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact; + Assert(!cfactGen.isNull()); + // Do not use the addProofTo interface, instead use the update node + // interface, since this ensures that we don't take ownership for + // the current proof. Instead, it is only linked, and ignored on + // future calls to getProofFor due to the check above. + std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen); + if (isSym) { - Trace("lazy-cdproof") << "LazyCDProof: Failed added fact for " - << afactGen << std::endl; - Assert(false) << "Proof generator " << pg->identify() - << " could not add proof for fact " << afactGen - << std::endl; + d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); } else { - Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for " - << afactGen << std::endl; + d_manager->updateNode(cur, pgc.get()); } + Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for " + << cfactGen << std::endl; } else { - Trace("lazy-cdproof") - << "LazyCDProof: No generator for " << afact << std::endl; + Trace("lazy-cdproof") << "LazyCDProof: " << identify() + << " : No generator for " << cfact << std::endl; } // Notice that we do not traverse the proofs that have been generated // lazily by the proof generators here. In other words, we assume that @@ -104,11 +116,14 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact) } while (!visit.empty()); // we have now updated the ASSUME leafs of opf, return it Trace("lazy-cdproof") << "...finished" << std::endl; + Assert(opf->getResult() == fact); return opf; } void LazyCDProof::addLazyStep(Node expected, ProofGenerator* pg, + bool isClosed, + const char* ctx, bool forceOverwrite, PfRule idNull) { @@ -117,7 +132,8 @@ void LazyCDProof::addLazyStep(Node expected, // null generator, should have given a proof rule if (idNull == PfRule::ASSUME) { - Assert(false); + Unreachable() << "LazyCDProof::addLazyStep: " << identify() + << ": failed to provide proof generator for " << expected; return; } Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected @@ -138,6 +154,12 @@ void LazyCDProof::addLazyStep(Node expected, } // just store now d_gens.insert(expected, pg); + // debug checking + if (isClosed) + { + Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl; + pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx); + } } ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, @@ -191,6 +213,4 @@ bool LazyCDProof::hasGenerator(Node fact) const return it != d_gens.end(); } -std::string LazyCDProof::identify() const { return "LazyCDProof"; } - } // namespace CVC4 |