diff options
Diffstat (limited to 'src/proof/lemma_proof.h')
-rw-r--r-- | src/proof/lemma_proof.h | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h new file mode 100644 index 000000000..e96ff5337 --- /dev/null +++ b/src/proof/lemma_proof.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file lemma_proof.h +** \verbatim +** +** \brief A class for recoding the steps required in order to prove a theory lemma. +** +** A class for recoding the steps required in order to prove a theory lemma. +** +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__LEMMA_PROOF_H +#define __CVC4__LEMMA_PROOF_H + +#include "expr/expr.h" +#include "proof/clause_id.h" +#include "prop/sat_solver_types.h" +#include "util/proof.h" +#include "expr/node.h" + +namespace CVC4 { + +class LemmaProofRecipe { +public: + class ProofStep { + public: + ProofStep(theory::TheoryId theory, Node literalToProve); + theory::TheoryId getTheory() const; + Node getLiteral() const; + void addAssertion(const Node& assertion); + std::set<Node> getAssertions() const; + + private: + theory::TheoryId d_theory; + Node d_literalToProve; + std::set<Node> d_assertions; + }; + + //* The lemma assertions and owner */ + void addBaseAssertion(Node baseAssertion); + std::set<Node> getBaseAssertions() const; + theory::TheoryId getTheory() const; + + //* Rewrite rules */ + typedef std::map<Node, Node>::const_iterator RewriteIterator; + RewriteIterator rewriteBegin() const; + RewriteIterator rewriteEnd() const; + + void addRewriteRule(Node assertion, Node explanation); + bool wasRewritten(Node assertion) const; + Node getExplanation(Node assertion) const; + + //* Proof Steps */ + void addStep(ProofStep& proofStep); + const ProofStep* getStep(unsigned index) const; + ProofStep* getStep(unsigned index); + unsigned getNumSteps() const; + std::set<Node> getMissingAssertionsForStep(unsigned index) const; + bool simpleLemma() const; + bool compositeLemma() const; + + void dump(const char *tag) const; + bool operator<(const LemmaProofRecipe& other) const; + +private: + //* The list of assertions for this lemma */ + std::set<Node> d_baseAssertions; + + //* The various steps needed to derive the empty clause */ + std::list<ProofStep> d_proofSteps; + + //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */ + std::map<Node, Node> d_assertionToExplanation; +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_PROOF_H */ |