diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-15 23:36:21 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-15 23:36:21 -0300 |
commit | 8a126d59141d2889e3b10b07ece4b10f48511a71 (patch) | |
tree | b4d5f303a120fbf5eeba3c7cfb0c8ea81eff9555 /src/theory/uf/proof_equality_engine.cpp | |
parent | 33f51490a9df73d8fee25fb88b19a87339b28e95 (diff) |
[proof-new] A simple proof generator for buffered proof steps (#5069)
This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Diffstat (limited to 'src/theory/uf/proof_equality_engine.cpp')
-rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 56 |
1 files changed, 0 insertions, 56 deletions
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index c8f5ebb4d..5811257ed 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -573,62 +573,6 @@ void ProofEqEngine::explainWithProof(Node lit, Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl; } - -ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c, - ProofNodeManager* pnm) - : ProofGenerator(), d_facts(c), d_pnm(pnm) -{ -} - -bool ProofEqEngine::FactProofGenerator::addStep(Node fact, ProofStep ps) -{ - if (d_facts.find(fact) != d_facts.end()) - { - // duplicate - return false; - } - Node symFact = CDProof::getSymmFact(fact); - if (!symFact.isNull()) - { - if (d_facts.find(symFact) != d_facts.end()) - { - // duplicate due to symmetry - return false; - } - } - d_facts.insert(fact, std::make_shared<ProofStep>(ps)); - return true; -} - -std::shared_ptr<ProofNode> ProofEqEngine::FactProofGenerator::getProofFor( - Node fact) -{ - Trace("pfee-fact-gen") << "FactProofGenerator::getProofFor: " << fact - << std::endl; - NodeProofStepMap::iterator it = d_facts.find(fact); - if (it == d_facts.end()) - { - Node symFact = CDProof::getSymmFact(fact); - if (symFact.isNull()) - { - Trace("pfee-fact-gen") << "...cannot find step" << std::endl; - Assert(false); - return nullptr; - } - it = d_facts.find(symFact); - if (it == d_facts.end()) - { - Assert(false); - Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl; - return nullptr; - } - } - Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl; - CDProof cdp(d_pnm); - cdp.addStep(fact, *(*it).second); - return cdp.getProofFor(fact); -} - } // namespace eq } // namespace theory } // namespace CVC4 |