diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-15 10:28:47 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-15 10:28:47 -0800 |
commit | 4a38be3b9ac133655602a989f1136cd24ed89bc6 (patch) | |
tree | d8a03c6a78a822b658587cbd06af2e0c1e5bd50f /src/options/options_handler.h | |
parent | da504025a3a77e9a3201af33ee6f96f937802807 (diff) |
Strings: Add option to change loop process mode (#2794)
This commit adds an option `--strings-process-loop-mode` that allows
finer-grained control over CVC4 processes looping word equation. In
particular, performing normal loop breaking sometimes leads to worse
performance. The "simple" mode disables that inference.
Diffstat (limited to 'src/options/options_handler.h')
-rw-r--r-- | src/options/options_handler.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 126538436..8b2629db7 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -37,6 +37,7 @@ #include "options/printer_modes.h" #include "options/quantifiers_modes.h" #include "options/smt_modes.h" +#include "options/strings_process_loop_mode.h" #include "options/sygus_out_mode.h" #include "options/theoryof_mode.h" #include "options/ufss_mode.h" @@ -148,6 +149,9 @@ public: theory::bv::BvProofFormat stringToBvProofFormat(std::string option, std::string optarg); + theory::strings::ProcessLoopMode stringToStringsProcessLoopMode( + std::string option, std::string optarg); + // theory/uf/options_handlers.h theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg); @@ -236,6 +240,7 @@ public: static const std::string s_bvProofFormatHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; + static const std::string s_stringToStringsProcessLoopModeHelp; static const std::string s_boolToBVModeHelp; static const std::string s_cegqiFairModeHelp; static const std::string s_decisionModeHelp; |