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.

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;