diff options
Diffstat (limited to 'src/proof/clausal_bitvector_proof.h')
-rw-r--r-- | src/proof/clausal_bitvector_proof.h | 49 |
1 files changed, 45 insertions, 4 deletions
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h index 85e409e0d..b53bcd5e2 100644 --- a/src/proof/clausal_bitvector_proof.h +++ b/src/proof/clausal_bitvector_proof.h @@ -2,7 +2,7 @@ /*! \file clausal_bitvector_proof.h ** \verbatim ** Top contributors (to current version): - ** Alex Ozdemir + ** Alex Ozdemir, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -61,8 +61,7 @@ class ClausalBitVectorProof : public BitVectorProof protected: // A list of all clauses and their ids which are passed into the SAT solver - std::vector<std::pair<ClauseId, std::unique_ptr<prop::SatClause>>> - d_usedClauses; + std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses; // Stores the proof recieved from the SAT solver. std::ostringstream d_binaryDratProof; }; @@ -77,7 +76,6 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof TheoryProofEngine* proofEngine) : ClausalBitVectorProof(bv, proofEngine) { - // That's all! } void printTheoryLemmaProof(std::vector<Expr>& lemma, @@ -87,6 +85,49 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof void printBBDeclarationAndCnf(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) override; +}; + +/** + * A DRAT proof for a bit-vector problem + */ +class LfscDratBitVectorProof : public LfscClausalBitVectorProof +{ + public: + LfscDratBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) + : LfscClausalBitVectorProof(bv, proofEngine) + { + } + + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; +}; + +/** + * An LRAT proof for a bit-vector problem + */ +class LfscLratBitVectorProof : public LfscClausalBitVectorProof +{ + public: + LfscLratBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine) + : LfscClausalBitVectorProof(bv, proofEngine) + { + } + + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; +}; + +/** + * An Extended Resolution proof for a bit-vector problem + */ +class LfscErBitVectorProof : public LfscClausalBitVectorProof +{ + public: + LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + : LfscClausalBitVectorProof(bv, proofEngine) + { + } + void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; }; |