diff options
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 */ + |