src/proof/lemma_proof.cpp

   1 /*********************                                                        */
   2 /*! \file lemma_proof.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Guy Katz, Alex Ozdemir
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** A class for recoding the steps required in order to prove a theory lemma.
  13
  14 **/
  15
  16 #include "proof/lemma_proof.h"
  17 #include "theory/rewriter.h"
  18
  19 namespace CVC4 {
  20
  21 LemmaProofRecipe::ProofStep::ProofStep(theory::TheoryId theory, Node literalToProve) :
  22   d_theory(theory), d_literalToProve(literalToProve) {
  23 }
  24
  25 theory::TheoryId LemmaProofRecipe::ProofStep::getTheory() const {
  26   return d_theory;
  27 }
  28
  29 Node LemmaProofRecipe::ProofStep::getLiteral() const {
  30   return d_literalToProve;
  31 }
  32
  33 void LemmaProofRecipe::ProofStep::addAssertion(const Node& assertion) {
  34   d_assertions.insert(assertion);
  35 }
  36
  37 std::set<Node> LemmaProofRecipe::ProofStep::getAssertions() const {
  38   return d_assertions;
  39 }
  40
  41 void LemmaProofRecipe::addStep(ProofStep& proofStep) {
  42   d_proofSteps.push_back(proofStep);
  43 }
  44
  45 std::set<Node> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const {
  46   Assert(index < d_proofSteps.size());
  47
  48   std::set<Node> existingAssertions = getBaseAssertions();
  49
  50   // The literals for all the steps "before" (i.e. behind) the step indicated
  51   // by the index are considered "existing"
  52   size_t revIndex = d_proofSteps.size() - 1 - index;
  53   for (size_t i = d_proofSteps.size() - 1; i != revIndex; --i)
  54   {
  55     existingAssertions.insert(d_proofSteps[i].getLiteral().negate());
  56   }
  57
  58   std::set<Node> neededAssertions = d_proofSteps[revIndex].getAssertions();
  59
  60   std::set<Node> result;
  61   std::set_difference(neededAssertions.begin(), neededAssertions.end(),
  62                       existingAssertions.begin(), existingAssertions.end(),
  63                       std::inserter(result, result.begin()));
  64   return result;
  65 }
  66
  67 void LemmaProofRecipe::dump(const char *tag) const {
  68
  69   if (d_proofSteps.size() == 1) {
  70     Debug(tag) << std::endl << "[Simple lemma]" << std::endl << std::endl;
  71   }
  72
  73   if (d_originalLemma != Node()) {
  74     Debug(tag) << std::endl << "Original lemma: " << d_originalLemma << std::endl << std::endl;
  75   }
  76
  77   unsigned count = 1;
  78   Debug(tag) << "Base assertions:" << std::endl;
  79   for (std::set<Node>::iterator baseIt = d_baseAssertions.begin();
  80        baseIt != d_baseAssertions.end();
  81        ++baseIt) {
  82     Debug(tag) << "\t#" << count << ": " << "\t" << *baseIt << std::endl;
  83     ++count;
  84   }
  85
  86   Debug(tag) << std::endl << std::endl << "Proof steps:" << std::endl;
  87
  88   count = 1;
  89   for (const auto& step : (*this)) {
  90     Debug(tag) << "\tStep #" << count << ": " << "\t[" << step.getTheory() << "] ";
  91     if (step.getLiteral() == Node()) {
  92       Debug(tag) << "Contradiction";
  93     } else {
  94       Debug(tag) << step.getLiteral();
  95     }
  96
  97     Debug(tag) << std::endl;
  98
  99     std::set<Node> missingAssertions = getMissingAssertionsForStep(count - 1);
 100     for (std::set<Node>::const_iterator it = missingAssertions.begin(); it != missingAssertions.end(); ++it) {
 101       Debug(tag) << "\t\t\tMissing assertion for step: " << *it << std::endl;
 102     }
 103
 104     Debug(tag) << std::endl;
 105     ++count;
 106   }
 107
 108   if (!d_assertionToExplanation.empty()) {
 109     Debug(tag) << std::endl << "Rewrites used:" << std::endl;
 110     count = 1;
 111     for (std::map<Node, Node>::const_iterator rewrite = d_assertionToExplanation.begin();
 112          rewrite != d_assertionToExplanation.end();
 113          ++rewrite) {
 114       Debug(tag) << "\tRewrite #" << count << ":" << std::endl
 115                  << "\t\t" << rewrite->first
 116                  << std::endl << "\t\trewritten into" << std::endl
 117                  << "\t\t" << rewrite->second
 118                  << std::endl << std::endl;
 119       ++count;
 120     }
 121   }
 122 }
 123
 124 void LemmaProofRecipe::addBaseAssertion(Node baseAssertion) {
 125   d_baseAssertions.insert(baseAssertion);
 126 }
 127
 128 std::set<Node> LemmaProofRecipe::getBaseAssertions() const {
 129   return d_baseAssertions;
 130 }
 131
 132 theory::TheoryId LemmaProofRecipe::getTheory() const {
 133   Assert(d_proofSteps.size() > 0);
 134   return d_proofSteps.back().getTheory();
 135 }
 136
 137 void LemmaProofRecipe::addRewriteRule(Node assertion, Node explanation) {
 138   if (d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()) {
 139     Assert(d_assertionToExplanation[assertion] == explanation);
 140   }
 141
 142   d_assertionToExplanation[assertion] = explanation;
 143 }
 144
 145 bool LemmaProofRecipe::wasRewritten(Node assertion) const {
 146   return d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end();
 147 }
 148
 149 Node LemmaProofRecipe::getExplanation(Node assertion) const {
 150   Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end());
 151   return d_assertionToExplanation.find(assertion)->second;
 152 }
 153
 154 LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteBegin() const {
 155   return d_assertionToExplanation.begin();
 156 }
 157
 158 LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const {
 159   return d_assertionToExplanation.end();
 160 }
 161
 162 LemmaProofRecipe::iterator LemmaProofRecipe::begin() {
 163   return d_proofSteps.rbegin();
 164 }
 165
 166 LemmaProofRecipe::iterator LemmaProofRecipe::end() {
 167   return d_proofSteps.rend();
 168 }
 169
 170 LemmaProofRecipe::const_iterator LemmaProofRecipe::begin() const {
 171   return d_proofSteps.crbegin();
 172 }
 173
 174 LemmaProofRecipe::const_iterator LemmaProofRecipe::end() const {
 175   return d_proofSteps.crend();
 176 }
 177
 178 bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const {
 179     return d_baseAssertions < other.d_baseAssertions;
 180   }
 181
 182 bool LemmaProofRecipe::simpleLemma() const {
 183   return d_proofSteps.size() == 1;
 184 }
 185
 186 bool LemmaProofRecipe::compositeLemma() const {
 187   return !simpleLemma();
 188 }
 189
 190 const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const {
 191   Assert(index < d_proofSteps.size());
 192
 193   size_t revIndex = d_proofSteps.size() - 1 - index;
 194
 195   return &d_proofSteps[revIndex];
 196 }
 197
 198 LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) {
 199   Assert(index < d_proofSteps.size());
 200
 201   size_t revIndex = d_proofSteps.size() - 1 - index;
 202
 203   return &d_proofSteps[revIndex];
 204 }
 205
 206 unsigned LemmaProofRecipe::getNumSteps() const {
 207   return d_proofSteps.size();
 208 }
 209
 210 void LemmaProofRecipe::setOriginalLemma(Node lemma) {
 211   d_originalLemma = lemma;
 212 }
 213
 214 Node LemmaProofRecipe::getOriginalLemma() const {
 215   return d_originalLemma;
 216 }
 217
 218 std::ostream& operator<<(std::ostream& out,
 219                          const LemmaProofRecipe::ProofStep& step)
 220 {
 221   out << "Proof Step(";
 222   out << " lit = " << step.getLiteral() << ",";
 223   out << " assertions = " << step.getAssertions() << ",";
 224   out << " theory = " << step.getTheory();
 225   out << " )";
 226   return out;
 227 }
 228
 229 std::ostream& operator<<(std::ostream& out, const LemmaProofRecipe& recipe)
 230 {
 231   out << "LemmaProofRecipe(";
 232   out << "\n  original lemma = " << recipe.getOriginalLemma();
 233   out << "\n  actual clause  = " << recipe.getBaseAssertions();
 234   out << "\n  theory         = " << recipe.getTheory();
 235   out << "\n  steps          = ";
 236   for (const auto& step : recipe)
 237   {
 238     out << "\n    " << step;
 239   }
 240   out << "\n  rewrites       = ";
 241   for (LemmaProofRecipe::RewriteIterator i = recipe.rewriteBegin(),
 242                                          end = recipe.rewriteEnd();
 243        i != end;
 244        ++i)
 245   {
 246     out << "\n    Rewrite(" << i->first << ", explanation = " << i->second
 247         << ")";
 248   }
 249   out << "\n)";
 250   return out;
 251 }
 252
 253 } /* namespace CVC4 */