1 /********************* */
2 /*! \file lemma_proof.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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
12 ** A class for recoding the steps required in order to prove a theory lemma.
16 #include "proof/lemma_proof.h"
17 #include "theory/rewriter.h"
21 LemmaProofRecipe::ProofStep::ProofStep(theory::TheoryId theory
, Node literalToProve
) :
22 d_theory(theory
), d_literalToProve(literalToProve
) {
25 theory::TheoryId
LemmaProofRecipe::ProofStep::getTheory() const {
29 Node
LemmaProofRecipe::ProofStep::getLiteral() const {
30 return d_literalToProve
;
33 void LemmaProofRecipe::ProofStep::addAssertion(const Node
& assertion
) {
34 d_assertions
.insert(assertion
);
37 std::set
<Node
> LemmaProofRecipe::ProofStep::getAssertions() const {
41 void LemmaProofRecipe::addStep(ProofStep
& proofStep
) {
42 d_proofSteps
.push_back(proofStep
);
45 std::set
<Node
> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index
) const {
46 Assert(index
< d_proofSteps
.size());
48 std::set
<Node
> existingAssertions
= getBaseAssertions();
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
)
55 existingAssertions
.insert(d_proofSteps
[i
].getLiteral().negate());
58 std::set
<Node
> neededAssertions
= d_proofSteps
[revIndex
].getAssertions();
60 std::set
<Node
> result
;
61 std::set_difference(neededAssertions
.begin(), neededAssertions
.end(),
62 existingAssertions
.begin(), existingAssertions
.end(),
63 std::inserter(result
, result
.begin()));
67 void LemmaProofRecipe::dump(const char *tag
) const {
69 if (d_proofSteps
.size() == 1) {
70 Debug(tag
) << std::endl
<< "[Simple lemma]" << std::endl
<< std::endl
;
73 if (d_originalLemma
!= Node()) {
74 Debug(tag
) << std::endl
<< "Original lemma: " << d_originalLemma
<< std::endl
<< std::endl
;
78 Debug(tag
) << "Base assertions:" << std::endl
;
79 for (std::set
<Node
>::iterator baseIt
= d_baseAssertions
.begin();
80 baseIt
!= d_baseAssertions
.end();
82 Debug(tag
) << "\t#" << count
<< ": " << "\t" << *baseIt
<< std::endl
;
86 Debug(tag
) << std::endl
<< std::endl
<< "Proof steps:" << std::endl
;
89 for (const auto& step
: (*this)) {
90 Debug(tag
) << "\tStep #" << count
<< ": " << "\t[" << step
.getTheory() << "] ";
91 if (step
.getLiteral() == Node()) {
92 Debug(tag
) << "Contradiction";
94 Debug(tag
) << step
.getLiteral();
97 Debug(tag
) << std::endl
;
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
;
104 Debug(tag
) << std::endl
;
108 if (!d_assertionToExplanation
.empty()) {
109 Debug(tag
) << std::endl
<< "Rewrites used:" << std::endl
;
111 for (std::map
<Node
, Node
>::const_iterator rewrite
= d_assertionToExplanation
.begin();
112 rewrite
!= d_assertionToExplanation
.end();
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
;
124 void LemmaProofRecipe::addBaseAssertion(Node baseAssertion
) {
125 d_baseAssertions
.insert(baseAssertion
);
128 std::set
<Node
> LemmaProofRecipe::getBaseAssertions() const {
129 return d_baseAssertions
;
132 theory::TheoryId
LemmaProofRecipe::getTheory() const {
133 Assert(d_proofSteps
.size() > 0);
134 return d_proofSteps
.back().getTheory();
137 void LemmaProofRecipe::addRewriteRule(Node assertion
, Node explanation
) {
138 if (d_assertionToExplanation
.find(assertion
) != d_assertionToExplanation
.end()) {
139 Assert(d_assertionToExplanation
[assertion
] == explanation
);
142 d_assertionToExplanation
[assertion
] = explanation
;
145 bool LemmaProofRecipe::wasRewritten(Node assertion
) const {
146 return d_assertionToExplanation
.find(assertion
) != d_assertionToExplanation
.end();
149 Node
LemmaProofRecipe::getExplanation(Node assertion
) const {
150 Assert(d_assertionToExplanation
.find(assertion
) != d_assertionToExplanation
.end());
151 return d_assertionToExplanation
.find(assertion
)->second
;
154 LemmaProofRecipe::RewriteIterator
LemmaProofRecipe::rewriteBegin() const {
155 return d_assertionToExplanation
.begin();
158 LemmaProofRecipe::RewriteIterator
LemmaProofRecipe::rewriteEnd() const {
159 return d_assertionToExplanation
.end();
162 LemmaProofRecipe::iterator
LemmaProofRecipe::begin() {
163 return d_proofSteps
.rbegin();
166 LemmaProofRecipe::iterator
LemmaProofRecipe::end() {
167 return d_proofSteps
.rend();
170 LemmaProofRecipe::const_iterator
LemmaProofRecipe::begin() const {
171 return d_proofSteps
.crbegin();
174 LemmaProofRecipe::const_iterator
LemmaProofRecipe::end() const {
175 return d_proofSteps
.crend();
178 bool LemmaProofRecipe::operator<(const LemmaProofRecipe
& other
) const {
179 return d_baseAssertions
< other
.d_baseAssertions
;
182 bool LemmaProofRecipe::simpleLemma() const {
183 return d_proofSteps
.size() == 1;
186 bool LemmaProofRecipe::compositeLemma() const {
187 return !simpleLemma();
190 const LemmaProofRecipe::ProofStep
* LemmaProofRecipe::getStep(unsigned index
) const {
191 Assert(index
< d_proofSteps
.size());
193 size_t revIndex
= d_proofSteps
.size() - 1 - index
;
195 return &d_proofSteps
[revIndex
];
198 LemmaProofRecipe::ProofStep
* LemmaProofRecipe::getStep(unsigned index
) {
199 Assert(index
< d_proofSteps
.size());
201 size_t revIndex
= d_proofSteps
.size() - 1 - index
;
203 return &d_proofSteps
[revIndex
];
206 unsigned LemmaProofRecipe::getNumSteps() const {
207 return d_proofSteps
.size();
210 void LemmaProofRecipe::setOriginalLemma(Node lemma
) {
211 d_originalLemma
= lemma
;
214 Node
LemmaProofRecipe::getOriginalLemma() const {
215 return d_originalLemma
;
218 std::ostream
& operator<<(std::ostream
& out
,
219 const LemmaProofRecipe::ProofStep
& step
)
221 out
<< "Proof Step(";
222 out
<< " lit = " << step
.getLiteral() << ",";
223 out
<< " assertions = " << step
.getAssertions() << ",";
224 out
<< " theory = " << step
.getTheory();
229 std::ostream
& operator<<(std::ostream
& out
, const LemmaProofRecipe
& recipe
)
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
)
238 out
<< "\n " << step
;
240 out
<< "\n rewrites = ";
241 for (LemmaProofRecipe::RewriteIterator i
= recipe
.rewriteBegin(),
242 end
= recipe
.rewriteEnd();
246 out
<< "\n Rewrite(" << i
->first
<< ", explanation = " << i
->second
253 } /* namespace CVC4 */