}
void LemmaProofRecipe::addStep(ProofStep& proofStep) {
- d_proofSteps.push_front(proofStep);
+ d_proofSteps.push_back(proofStep);
}
std::set<Node> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const {
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(),
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;
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;
}
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 {
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 */
#include "prop/sat_solver_types.h"
#include "util/proof.h"
#include "expr/node.h"
+#include <iosfwd>
namespace CVC4 {
theory::TheoryId getTheory() const;
//* Rewrite rules */
- typedef std::map<Node, Node>::const_iterator RewriteIterator;
+ using RewriteIterator = std::map<Node, Node>::const_iterator;
RewriteIterator rewriteBegin() const;
RewriteIterator rewriteEnd() const;
+ // Steps iterator
+ // The default iterator for a LemmaProofRecipe
+ using iterator = std::vector<ProofStep>::reverse_iterator;
+ std::vector<ProofStep>::reverse_iterator begin();
+ std::vector<ProofStep>::reverse_iterator end();
+
+ using const_iterator = std::vector<ProofStep>::const_reverse_iterator;
+ std::vector<ProofStep>::const_reverse_iterator begin() const;
+ std::vector<ProofStep>::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;
std::set<Node> d_baseAssertions;
//* The various steps needed to derive the empty clause */
- std::list<ProofStep> d_proofSteps;
+ // The "first" step is actually at the back.
+ std::vector<ProofStep> d_proofSteps;
//* A map from assertions to their rewritten explanations (toAssert --> toExplain) */
std::map<Node, Node> d_assertionToExplanation;
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 */