diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-11-19 21:46:29 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-19 21:46:29 -0800 |
commit | 176b119d86fe34878a4c9d4d7ee8f982db311b39 (patch) | |
tree | 7ae98acb8da4ed60fa13187fbbfafb83bad1725d /src/proof/lemma_proof.cpp | |
parent | 2afbc4bbcccf9f91439809ee0026027a432a3061 (diff) |
Change lemma proof step storage & iterators (#2712)
Proof steps were in a std::list, which is a linked list, but really, we
only needed a stack, so I changed it to a vector, because LL's are
usually slower.
Also added an iterator for the proof steps, and << implementations
Diffstat (limited to 'src/proof/lemma_proof.cpp')
-rw-r--r-- | src/proof/lemma_proof.cpp | 89 |
1 files changed, 66 insertions, 23 deletions
diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp index 6b413ade3..392805473 100644 --- a/src/proof/lemma_proof.cpp +++ b/src/proof/lemma_proof.cpp @@ -39,7 +39,7 @@ std::set<Node> LemmaProofRecipe::ProofStep::getAssertions() const { } void LemmaProofRecipe::addStep(ProofStep& proofStep) { - d_proofSteps.push_front(proofStep); + d_proofSteps.push_back(proofStep); } std::set<Node> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const { @@ -47,14 +47,15 @@ std::set<Node> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) con std::set<Node> existingAssertions = getBaseAssertions(); - std::list<ProofStep>::const_iterator step = d_proofSteps.begin(); - while (index != 0) { - existingAssertions.insert(step->getLiteral().negate()); - ++step; - --index; + // The literals for all the steps "before" (i.e. behind) the step indicated + // by the index are considered "existing" + size_t revIndex = d_proofSteps.size() - 1 - index; + for (size_t i = d_proofSteps.size() - 1; i != revIndex; --i) + { + existingAssertions.insert(d_proofSteps[i].getLiteral().negate()); } - std::set<Node> neededAssertions = step->getAssertions(); + std::set<Node> neededAssertions = d_proofSteps[revIndex].getAssertions(); std::set<Node> result; std::set_difference(neededAssertions.begin(), neededAssertions.end(), @@ -85,12 +86,12 @@ void LemmaProofRecipe::dump(const char *tag) const { Debug(tag) << std::endl << std::endl << "Proof steps:" << std::endl; count = 1; - for (std::list<ProofStep>::const_iterator step = d_proofSteps.begin(); step != d_proofSteps.end(); ++step) { - Debug(tag) << "\tStep #" << count << ": " << "\t[" << step->getTheory() << "] "; - if (step->getLiteral() == Node()) { + for (const auto& step : (*this)) { + Debug(tag) << "\tStep #" << count << ": " << "\t[" << step.getTheory() << "] "; + if (step.getLiteral() == Node()) { Debug(tag) << "Contradiction"; } else { - Debug(tag) << step->getLiteral(); + Debug(tag) << step.getLiteral(); } Debug(tag) << std::endl; @@ -158,6 +159,22 @@ LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const { return d_assertionToExplanation.end(); } +LemmaProofRecipe::iterator LemmaProofRecipe::begin() { + return d_proofSteps.rbegin(); +} + +LemmaProofRecipe::iterator LemmaProofRecipe::end() { + return d_proofSteps.rend(); +} + +LemmaProofRecipe::const_iterator LemmaProofRecipe::begin() const { + return d_proofSteps.crbegin(); +} + +LemmaProofRecipe::const_iterator LemmaProofRecipe::end() const { + return d_proofSteps.crend(); +} + bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const { return d_baseAssertions < other.d_baseAssertions; } @@ -173,25 +190,17 @@ bool LemmaProofRecipe::compositeLemma() const { const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const { Assert(index < d_proofSteps.size()); - std::list<ProofStep>::const_iterator it = d_proofSteps.begin(); - while (index != 0) { - ++it; - --index; - } + size_t revIndex = d_proofSteps.size() - 1 - index; - return &(*it); + return &d_proofSteps[revIndex]; } LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) { Assert(index < d_proofSteps.size()); - std::list<ProofStep>::iterator it = d_proofSteps.begin(); - while (index != 0) { - ++it; - --index; - } + size_t revIndex = d_proofSteps.size() - 1 - index; - return &(*it); + return &d_proofSteps[revIndex]; } unsigned LemmaProofRecipe::getNumSteps() const { @@ -206,5 +215,39 @@ Node LemmaProofRecipe::getOriginalLemma() const { return d_originalLemma; } +std::ostream& operator<<(std::ostream& out, + const LemmaProofRecipe::ProofStep& step) +{ + out << "Proof Step("; + out << " lit = " << step.getLiteral() << ","; + out << " assertions = " << step.getAssertions() << ","; + out << " theory = " << step.getTheory(); + out << " )"; + return out; +} + +std::ostream& operator<<(std::ostream& out, const LemmaProofRecipe& recipe) +{ + out << "LemmaProofRecipe("; + out << "\n original lemma = " << recipe.getOriginalLemma(); + out << "\n actual clause = " << recipe.getBaseAssertions(); + out << "\n theory = " << recipe.getTheory(); + out << "\n steps = "; + for (const auto& step : recipe) + { + out << "\n " << step; + } + out << "\n rewrites = "; + for (LemmaProofRecipe::RewriteIterator i = recipe.rewriteBegin(), + end = recipe.rewriteEnd(); + i != end; + ++i) + { + out << "\n Rewrite(" << i->first << ", explanation = " << i->second + << ")"; + } + out << "\n)"; + return out; +} } /* namespace CVC4 */ |