diff options
Diffstat (limited to 'src/expr/buffered_proof_generator.cpp')
-rw-r--r-- | src/expr/buffered_proof_generator.cpp | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp index b37295c52..2cbbd7e91 100644 --- a/src/expr/buffered_proof_generator.cpp +++ b/src/expr/buffered_proof_generator.cpp @@ -81,4 +81,23 @@ std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact) return cdp.getProofFor(fact); } +bool BufferedProofGenerator::hasProofFor(Node f) +{ + NodeProofStepMap::iterator it = d_facts.find(f); + if (it == d_facts.end()) + { + Node symFact = CDProof::getSymmFact(f); + if (symFact.isNull()) + { + return false; + } + it = d_facts.find(symFact); + if (it == d_facts.end()) + { + return false; + } + } + return true; +} + } // namespace cvc5 |