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/expr/buffered_proof_generator.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/expr/buffered_proof_generator.cpp')
-rw-r--r-- | src/expr/buffered_proof_generator.cpp | 82 |
1 files changed, 82 insertions, 0 deletions
diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp new file mode 100644 index 000000000..aa0fe19bd --- /dev/null +++ b/src/expr/buffered_proof_generator.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file buffered_proof_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of a proof generator for buffered proof steps + **/ + +#include "expr/buffered_proof_generator.h" + +#include "expr/proof.h" + +namespace CVC4 { + +BufferedProofGenerator::BufferedProofGenerator(context::Context* c, + ProofNodeManager* pnm) + : ProofGenerator(), d_facts(c), d_pnm(pnm) +{ +} + +bool BufferedProofGenerator::addStep(Node fact, + ProofStep ps, + CDPOverwrite opolicy) +{ + // check duplicates if we are not always overwriting + if (opolicy != CDPOverwrite::ALWAYS) + { + 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; + } + } + } + // note that this replaces the value fact is mapped to if there is already one + d_facts.insert(fact, std::make_shared<ProofStep>(ps)); + return true; +} + +std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact) +{ + Trace("pfee-fact-gen") << "BufferedProofGenerator::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 CVC4 |