1 /********************* */ 2 /*! \file lemma_proof.h 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 "cvc4_private.h" 17 18 #ifndef __CVC4__LEMMA_PROOF_H 19 #define __CVC4__LEMMA_PROOF_H 20 21 #include "expr/expr.h" 22 #include "proof/clause_id.h" 23 #include "prop/sat_solver_types.h" 24 #include "util/proof.h" 25 #include "expr/node.h" 26 #include <iosfwd> 27 28 namespace CVC4 { 29 30 class LemmaProofRecipe { 31 public: 32 class ProofStep { 33 public: 34 ProofStep(theory::TheoryId theory, Node literalToProve); 35 theory::TheoryId getTheory() const; 36 Node getLiteral() const; 37 void addAssertion(const Node& assertion); 38 std::set<Node> getAssertions() const; 39 40 private: 41 theory::TheoryId d_theory; 42 Node d_literalToProve; 43 std::set<Node> d_assertions; 44 }; 45 46 //* The lemma assertions and owner */ 47 void addBaseAssertion(Node baseAssertion); 48 std::set<Node> getBaseAssertions() const; 49 theory::TheoryId getTheory() const; 50 51 //* Rewrite rules */ 52 using RewriteIterator = std::map<Node, Node>::const_iterator; 53 RewriteIterator rewriteBegin() const; 54 RewriteIterator rewriteEnd() const; 55 56 // Steps iterator 57 // The default iterator for a LemmaProofRecipe 58 using iterator = std::vector<ProofStep>::reverse_iterator; 59 std::vector<ProofStep>::reverse_iterator begin(); 60 std::vector<ProofStep>::reverse_iterator end(); 61 62 using const_iterator = std::vector<ProofStep>::const_reverse_iterator; 63 std::vector<ProofStep>::const_reverse_iterator begin() const; 64 std::vector<ProofStep>::const_reverse_iterator end() const; 65 66 using difference_type = ptrdiff_t; 67 using size_type = size_t; 68 using value_type = ProofStep; 69 using pointer = ProofStep *; 70 using const_pointer = const ProofStep *; 71 using reference = ProofStep &; 72 using const_reference = const ProofStep &; 73 74 void addRewriteRule(Node assertion, Node explanation); 75 bool wasRewritten(Node assertion) const; 76 Node getExplanation(Node assertion) const; 77 78 //* Original lemma */ 79 void setOriginalLemma(Node lemma); 80 Node getOriginalLemma() const; 81 82 //* Proof Steps */ 83 void addStep(ProofStep& proofStep); 84 const ProofStep* getStep(unsigned index) const; 85 ProofStep* getStep(unsigned index); 86 unsigned getNumSteps() const; 87 std::set<Node> getMissingAssertionsForStep(unsigned index) const; 88 bool simpleLemma() const; 89 bool compositeLemma() const; 90 91 void dump(const char *tag) const; 92 bool operator<(const LemmaProofRecipe& other) const; 93 94 private: 95 //* The list of assertions for this lemma */ 96 std::set<Node> d_baseAssertions; 97 98 //* The various steps needed to derive the empty clause */ 99 // The "first" step is actually at the back. 100 std::vector<ProofStep> d_proofSteps; 101 102 //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */ 103 std::map<Node, Node> d_assertionToExplanation; 104 105 //* The original lemma, as asserted by the owner theory solver */ 106 Node d_originalLemma; 107 }; 108 109 std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe::ProofStep & step); 110 111 std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe & recipe); 112 113 } /* CVC4 namespace */ 114 115 #endif /* __CVC4__LEMMA_PROOF_H */ 116