1 files changed, 48 insertions, 7 deletions
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index 85e409e0d..b10b1ad1c 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.
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
-#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#ifndef CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#define CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
 
 #include <iostream>
 #include <sstream>
@@ -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;
 };
 
@@ -94,4 +135,4 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof
 
 }  // namespace CVC4
 
-#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
+#endif /* CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */