[BV Proofs] Option for proof format (#2777)

We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!

My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`

and that I could not provide random other option values.

1 files changed, 21 insertions, 0 deletions

diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 530632674..fa5791ac9 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -68,12 +68,33 @@ enum SatSolverMode
   SAT_SOLVER_CADICAL,
 }; /* enum SatSolver */
 
+/**
+ * When the BV solver does eager bitblasting backed by CryptoMiniSat, proofs
+ * can be written in a variety of formats.
+ */
+enum BvProofFormat
+{
+  /**
+   * Write extended resolution proofs.
+   */
+  BITVECTOR_PROOF_ER,
+  /**
+   * Write DRAT proofs.
+   */
+  BITVECTOR_PROOF_DRAT,
+  /**
+   * Write LRAT proofs.
+   */
+  BITVECTOR_PROOF_LRAT,
+};
+
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 
 std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode);
 std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode);
 std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode);
+std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format);
 
 }/* CVC4 namespace */