diff options
Diffstat (limited to 'src/options/bv_bitblast_mode.h')
-rw-r--r-- | src/options/bv_bitblast_mode.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h index 871333b35..270f2346d 100644 --- a/src/options/bv_bitblast_mode.h +++ b/src/options/bv_bitblast_mode.h @@ -88,6 +88,27 @@ enum BvProofFormat BITVECTOR_PROOF_LRAT, }; +/** + * When the BV solver does eager bit-blasting backed by DRAT-producing SAT solvers, proofs + * can be written in a variety of formats. + */ +enum BvOptimizeSatProof +{ + /** + * Do not optimize the SAT proof. + */ + BITVECTOR_OPTIMIZE_SAT_PROOF_NONE = 0, + /** + * Optimize the SAT proof, but do not shrink the formula + */ + BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF = 1, + /** + * Optimize the SAT proof and shrink the formula + */ + BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA = 2, +}; + + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ @@ -95,6 +116,7 @@ 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); +std::ostream& operator<<(std::ostream& out, theory::bv::BvOptimizeSatProof level); }/* CVC4 namespace */ |