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/options_handler.h | |
| 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/options_handler.h')
| -rw-r--r-- | src/options/options_handler.h | 3 |
1 files changed, 3 insertions, 0 deletions
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; |