diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-04-23 15:58:57 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-04-23 15:58:57 -0700 |
| commit | df5f15a17a8f3b92ae1ea776e5cf079d61e6404c (patch) | |
| tree | e710f16059c64cc5845171e20c9c472c33f8eaba /src/options/bv_bitblast_mode.cpp | |
| parent | 53cade050e191c7c0dc0ebfae716a21162bd9b22 (diff) | |
[BV] An option for SAT proof optimization (#2915)
* [BV] An option for SAT proof optimization
The option doesn't **do** anything yet, but exists.
* CopyPaste Fix: BvOptimizeSatProof documentation
It was the documentation for a different option. Now it has been
updated.
* Fix Typos per Mathias' review.
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
Diffstat (limited to 'src/options/bv_bitblast_mode.cpp')
| -rw-r--r-- | src/options/bv_bitblast_mode.cpp | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp index 4bd7b9d77..d2425831a 100644 --- a/src/options/bv_bitblast_mode.cpp +++ b/src/options/bv_bitblast_mode.cpp @@ -81,4 +81,25 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format) return out; } +std::ostream& operator<<(std::ostream& out, + theory::bv::BvOptimizeSatProof level) +{ + switch (level) + { + case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE: + out << "BITVECTOR_OPTIMIZE_SAT_PROOF_NONE"; + break; + case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF: + out << "BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF"; + break; + case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA: + out << "BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA"; + break; + default: out << "BvOptimizeSatProof:UNKNOWN![" << unsigned(level) << "]"; + } + + return out; +} + }/* CVC4 namespace */ + |