diff options
Diffstat (limited to 'src/proof/lemma_proof.h')
-rw-r--r-- | src/proof/lemma_proof.h | 115 |
1 files changed, 0 insertions, 115 deletions
diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h deleted file mode 100644 index ffc6655a6..000000000 --- a/src/proof/lemma_proof.h +++ /dev/null @@ -1,115 +0,0 @@ -/********************* */ -/*! \file lemma_proof.h - ** \verbatim - ** Top contributors (to current version): - ** Guy Katz, Alex Ozdemir, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** 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" -#include <iosfwd> - -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 */ - 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; - - //* Original lemma */ - void setOriginalLemma(Node lemma); - Node getOriginalLemma() 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 */ - // 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; - - //* The original lemma, as asserted by the owner theory solver */ - 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 */ |