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 | |
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>
-rw-r--r-- | src/options/bv_bitblast_mode.cpp | 21 | ||||
-rw-r--r-- | src/options/bv_bitblast_mode.h | 22 | ||||
-rw-r--r-- | src/options/bv_options.toml | 11 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 39 | ||||
-rw-r--r-- | src/options/options_handler.h | 3 |
5 files changed, 96 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 */ + 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 */ diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 6dd755625..9529b7500 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -14,6 +14,17 @@ header = "options/bv_options.h" help = "choose which UNSAT proof format to use, see --bv-sat-solver=help" [[option]] + name = "bvOptimizeSatProof" + category = "expert" + long = "bv-optimize-sat-proof=MODE" + type = "CVC4::theory::bv::BvOptimizeSatProof" + default = "CVC4::theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA" + handler = "stringToBvOptimizeSatProof" + predicates = ["satSolverEnabledBuild"] + includes = ["options/bv_bitblast_mode.h"] + help = "enable SAT proof optimizations, see --bv-optimize-sat-proof=help" + +[[option]] name = "bvSatSolver" smt_name = "bv-sat-solver" category = "expert" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index f171c907e..7a4967de5 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1245,6 +1245,45 @@ theory::bv::BvProofFormat OptionsHandler::stringToBvProofFormat( } } +const std::string OptionsHandler::s_bvOptimizeSatProofHelp = + "\ +Optimization levels currently supported by the --bv-optimize-sat-proof option:\n\ +\n\ + none : Do not optimize the SAT proof\n\ +\n\ + proof : Use drat-trim to shrink the SAT proof\n\ +\n\ + formula : Use drat-trim to shrink the SAT proof and formula (default)\ +"; + +theory::bv::BvOptimizeSatProof OptionsHandler::stringToBvOptimizeSatProof( + std::string option, std::string optarg) +{ + if (optarg == "none") + { + return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE; + } + else if (optarg == "proof") + { + return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF; + } + else if (optarg == "formula") + { + return theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA; + } + else if (optarg == "help") + { + puts(s_bvOptimizeSatProofHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --bv-optimize-sat-proof: `") + + optarg + "'. Try --bv-optimize-sat-proof=help."); + } +} + + const std::string OptionsHandler::s_bitblastingModeHelp = "\ Bit-blasting modes currently supported by the --bitblast option:\n\ \n\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 16ddbce4d..5c354be57 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -148,6 +148,8 @@ public: theory::bv::BvProofFormat stringToBvProofFormat(std::string option, std::string optarg); + theory::bv::BvOptimizeSatProof stringToBvOptimizeSatProof(std::string option, + std::string optarg); theory::strings::ProcessLoopMode stringToStringsProcessLoopMode( std::string option, std::string optarg); @@ -238,6 +240,7 @@ public: static const std::string s_bitblastingModeHelp; static const std::string s_bvSatSolverHelp; static const std::string s_bvProofFormatHelp; + static const std::string s_bvOptimizeSatProofHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; static const std::string s_stringToStringsProcessLoopModeHelp; |