From: Alex Ozdemir Date: Tue, 23 Apr 2019 22:58:57 +0000 (-0700) Subject: [BV] An option for SAT proof optimization (#2915) X-Git-Tag: cvc5-1.0.0~4168 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=df5f15a17a8f3b92ae1ea776e5cf079d61e6404c;p=cvc5.git [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 --- 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 @@ -13,6 +13,17 @@ header = "options/bv_options.h" includes = ["options/bv_bitblast_mode.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" 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;