From 176b119d86fe34878a4c9d4d7ee8f982db311b39 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 19 Nov 2018 21:46:29 -0800 Subject: [PATCH] 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 --- src/proof/lemma_proof.cpp | 89 +++++++++++++++++++++++++++++---------- src/proof/lemma_proof.h | 28 +++++++++++- 2 files changed, 92 insertions(+), 25 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 LemmaProofRecipe::ProofStep::getAssertions() const { } void LemmaProofRecipe::addStep(ProofStep& proofStep) { - d_proofSteps.push_front(proofStep); + d_proofSteps.push_back(proofStep); } std::set LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const { @@ -47,14 +47,15 @@ std::set LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) con std::set existingAssertions = getBaseAssertions(); - std::list::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 neededAssertions = step->getAssertions(); + std::set neededAssertions = d_proofSteps[revIndex].getAssertions(); std::set 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::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::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::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 */ diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h index 13d23debd..857632083 100644 --- a/src/proof/lemma_proof.h +++ b/src/proof/lemma_proof.h @@ -23,6 +23,7 @@ #include "prop/sat_solver_types.h" #include "util/proof.h" #include "expr/node.h" +#include namespace CVC4 { @@ -48,10 +49,28 @@ public: theory::TheoryId getTheory() const; //* Rewrite rules */ - typedef std::map::const_iterator RewriteIterator; + using RewriteIterator = std::map::const_iterator; RewriteIterator rewriteBegin() const; RewriteIterator rewriteEnd() const; + // Steps iterator + // The default iterator for a LemmaProofRecipe + using iterator = std::vector::reverse_iterator; + std::vector::reverse_iterator begin(); + std::vector::reverse_iterator end(); + + using const_iterator = std::vector::const_reverse_iterator; + std::vector::const_reverse_iterator begin() const; + std::vector::const_reverse_iterator end() const; + + using difference_type = ptrdiff_t; + using size_type = size_t; + using value_type = ProofStep; + using pointer = ProofStep *; + using const_pointer = const ProofStep *; + using reference = ProofStep &; + using const_reference = const ProofStep &; + void addRewriteRule(Node assertion, Node explanation); bool wasRewritten(Node assertion) const; Node getExplanation(Node assertion) const; @@ -77,7 +96,8 @@ private: std::set d_baseAssertions; //* The various steps needed to derive the empty clause */ - std::list d_proofSteps; + // The "first" step is actually at the back. + std::vector d_proofSteps; //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */ std::map d_assertionToExplanation; @@ -86,6 +106,10 @@ private: Node d_originalLemma; }; +std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe::ProofStep & step); + +std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe & recipe); + } /* CVC4 namespace */ #endif /* __CVC4__LEMMA_PROOF_H */ -- 2.30.2