From 89ba584531115b7f6d47088d7614368ea05ab9d8 Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 1 Jun 2016 17:33:41 -0700 Subject: Merging proof branch --- src/proof/lemma_proof.cpp | 193 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 193 insertions(+) create mode 100644 src/proof/lemma_proof.cpp (limited to 'src/proof/lemma_proof.cpp') diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp new file mode 100644 index 000000000..a12a516cf --- /dev/null +++ b/src/proof/lemma_proof.cpp @@ -0,0 +1,193 @@ +/********************* */ +/*! \file lemma_proof.h +** \verbatim +** +** \brief A class for recoding the steps required in order to prove a theory lemma. +** +** A class for recoding the steps required in order to prove a theory lemma. +** +**/ + +#include "proof/lemma_proof.h" +#include "theory/rewriter.h" + +namespace CVC4 { + +LemmaProofRecipe::ProofStep::ProofStep(theory::TheoryId theory, Node literalToProve) : + d_theory(theory), d_literalToProve(literalToProve) { +} + +theory::TheoryId LemmaProofRecipe::ProofStep::getTheory() const { + return d_theory; +} + +Node LemmaProofRecipe::ProofStep::getLiteral() const { + return d_literalToProve; +} + +void LemmaProofRecipe::ProofStep::addAssertion(const Node& assertion) { + d_assertions.insert(assertion); +} + +std::set LemmaProofRecipe::ProofStep::getAssertions() const { + return d_assertions; +} + +void LemmaProofRecipe::addStep(ProofStep& proofStep) { + std::list::iterator existingFirstStep = d_proofSteps.begin(); + d_proofSteps.push_front(proofStep); +} + +std::set LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const { + Assert(index < d_proofSteps.size()); + + std::set existingAssertions = getBaseAssertions(); + + std::list::const_iterator step = d_proofSteps.begin(); + while (index != 0) { + existingAssertions.insert(step->getLiteral().negate()); + ++step; + --index; + } + + std::set neededAssertions = step->getAssertions(); + + std::set result; + std::set_difference(neededAssertions.begin(), neededAssertions.end(), + existingAssertions.begin(), existingAssertions.end(), + std::inserter(result, result.begin())); + return result; +} + +void LemmaProofRecipe::dump(const char *tag) const { + + if (d_proofSteps.size() == 1) { + Debug(tag) << std::endl << "[Simple lemma]" << std::endl << std::endl; + } + + unsigned count = 1; + Debug(tag) << "Base assertions:" << std::endl; + for (std::set::iterator baseIt = d_baseAssertions.begin(); + baseIt != d_baseAssertions.end(); + ++baseIt) { + Debug(tag) << "\t#" << count << ": " << "\t" << *baseIt << std::endl; + ++count; + } + + Debug(tag) << std::endl << std::endl << "Proof steps:" << std::endl; + + count = 1; + for (std::list::const_iterator step = d_proofSteps.begin(); step != d_proofSteps.end(); ++step) { + Debug(tag) << "\tStep #" << count << ": " << "\t[" << step->getTheory() << "] "; + if (step->getLiteral() == Node()) { + Debug(tag) << "Contradiction"; + } else { + Debug(tag) << step->getLiteral(); + } + + Debug(tag) << std::endl; + + std::set missingAssertions = getMissingAssertionsForStep(count - 1); + for (std::set::const_iterator it = missingAssertions.begin(); it != missingAssertions.end(); ++it) { + Debug(tag) << "\t\t\tMissing assertion for step: " << *it << std::endl; + } + + Debug(tag) << std::endl; + ++count; + } + + if (!d_assertionToExplanation.empty()) { + Debug(tag) << std::endl << "Rewrites used:" << std::endl; + count = 1; + for (std::map::const_iterator rewrite = d_assertionToExplanation.begin(); + rewrite != d_assertionToExplanation.end(); + ++rewrite) { + Debug(tag) << "\tRewrite #" << count << ":" << std::endl + << "\t\t" << rewrite->first + << std::endl << "\t\trewritten into" << std::endl + << "\t\t" << rewrite->second + << std::endl << std::endl; + ++count; + } + } +} + +void LemmaProofRecipe::addBaseAssertion(Node baseAssertion) { + d_baseAssertions.insert(baseAssertion); +} + +std::set LemmaProofRecipe::getBaseAssertions() const { + return d_baseAssertions; +} + +theory::TheoryId LemmaProofRecipe::getTheory() const { + Assert(d_proofSteps.size() > 0); + return d_proofSteps.back().getTheory(); +} + +void LemmaProofRecipe::addRewriteRule(Node assertion, Node explanation) { + if (d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()) { + Assert(d_assertionToExplanation[assertion] == explanation); + } + + d_assertionToExplanation[assertion] = explanation; +} + +bool LemmaProofRecipe::wasRewritten(Node assertion) const { + return d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end(); +} + +Node LemmaProofRecipe::getExplanation(Node assertion) const { + Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()); + return d_assertionToExplanation.find(assertion)->second; +} + +LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteBegin() const { + return d_assertionToExplanation.begin(); +} + +LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const { + return d_assertionToExplanation.end(); +} + +bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const { + return d_baseAssertions < other.d_baseAssertions; + } + +bool LemmaProofRecipe::simpleLemma() const { + return d_proofSteps.size() == 1; +} + +bool LemmaProofRecipe::compositeLemma() const { + return !simpleLemma(); +} + +const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const { + Assert(index < d_proofSteps.size()); + + std::list::const_iterator it = d_proofSteps.begin(); + while (index != 0) { + ++it; + --index; + } + + return &(*it); +} + +LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) { + Assert(index < d_proofSteps.size()); + + std::list::iterator it = d_proofSteps.begin(); + while (index != 0) { + ++it; + --index; + } + + return &(*it); +} + +unsigned LemmaProofRecipe::getNumSteps() const { + return d_proofSteps.size(); +} + +} /* namespace CVC4 */ -- cgit v1.2.3