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.

6 files changed, 175 insertions, 16 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index b86db8d00..fc725978e 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -37,6 +37,8 @@ libcvc4_add_sources(
   set_language.h
   smt_modes.cpp
   smt_modes.h
+  strings_process_loop_mode.cpp
+  strings_process_loop_mode.h
   sygus_out_mode.h
   theoryof_mode.cpp
   theoryof_mode.h
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index c08c59d89..84b9f3b4c 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1337,6 +1337,61 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(
   }
 }
 
+const std::string OptionsHandler::s_stringToStringsProcessLoopModeHelp =
+    "Loop processing modes supported by the --strings-process-loop-mode "
+    "option:\n"
+    "\n"
+    "full (default)\n"
+    "+ Perform full processing of looping word equations\n"
+    "\n"
+    "simple (default with --strings-fmf)\n"
+    "+ Omit normal loop breaking\n"
+    "\n"
+    "simple-abort\n"
+    "+ Abort when normal loop breaking is required\n"
+    "\n"
+    "none\n"
+    "+ Omit loop processing\n"
+    "\n"
+    "abort\n"
+    "+ Abort if looping word equations are encountered\n";
+
+theory::strings::ProcessLoopMode OptionsHandler::stringToStringsProcessLoopMode(
+    std::string option, std::string optarg)
+{
+  if (optarg == "full")
+  {
+    return theory::strings::ProcessLoopMode::FULL;
+  }
+  else if (optarg == "simple")
+  {
+    return theory::strings::ProcessLoopMode::SIMPLE;
+  }
+  else if (optarg == "simple-abort")
+  {
+    return theory::strings::ProcessLoopMode::SIMPLE_ABORT;
+  }
+  else if (optarg == "none")
+  {
+    return theory::strings::ProcessLoopMode::NONE;
+  }
+  else if (optarg == "abort")
+  {
+    return theory::strings::ProcessLoopMode::ABORT;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_stringToStringsProcessLoopModeHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(
+        std::string("unknown option for --strings-process-loop-mode: `")
+        + optarg + "'.  Try --strings-process-loop-mode=help.");
+  }
+}
+
 const std::string OptionsHandler::s_boolToBVModeHelp =
     "\
 BoolToBV pass modes supported by the --bool-to-bv option:\n\
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;
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 3544c37fe..fd00b8917 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -129,22 +129,14 @@ header = "options/strings_options.h"
   help       = "check entailment between length terms to reduce splitting"
 
 [[option]]
-  name       = "stringProcessLoop"
-  category   = "regular"
-  long       = "strings-process-loop"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "reduce looping word equations to regular expressions"
-
-[[option]]
-  name       = "stringAbortLoop"
-  category   = "regular"
-  long       = "strings-abort-loop"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "abort when a looping word equation is encountered"
+  name       = "stringProcessLoopMode"
+  category   = "expert"
+  long       = "strings-process-loop-mode=MODE"
+  type       = "CVC4::theory::strings::ProcessLoopMode"
+  default    = "CVC4::theory::strings::ProcessLoopMode::FULL"
+  handler    = "stringToStringsProcessLoopMode"
+  includes   = ["options/strings_process_loop_mode.h"]
+  help       = "choose how to process looping string equations, see --strings-process-loop-mode=help for details"
 
 [[option]]
   name       = "stringInferAsLemmas"
diff --git a/src/options/strings_process_loop_mode.cpp b/src/options/strings_process_loop_mode.cpp
new file mode 100644
index 000000000..59667ea75
--- /dev/null
+++ b/src/options/strings_process_loop_mode.cpp
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file strings_process_loop_mode.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Modes for processing looping word equations in the string solver.
+ **
+ ** Modes for processing looping word equations in the string solver.
+ **/
+
+#include "options/strings_process_loop_mode.h"
+
+#include <cstdint>
+#include <iostream>
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out,
+                         theory::strings::ProcessLoopMode mode)
+{
+  switch (mode)
+  {
+    case theory::strings::ProcessLoopMode::FULL:
+      out << "ProcessLoopMode::FULL";
+      break;
+    case theory::strings::ProcessLoopMode::SIMPLE:
+      out << "ProcessLoopMode::SIMPLE";
+      break;
+    case theory::strings::ProcessLoopMode::SIMPLE_ABORT:
+      out << "ProcessLoopMode::SIMPLE_ABORT";
+      break;
+    case theory::strings::ProcessLoopMode::NONE:
+      out << "ProcessLoopMode::NONE";
+      break;
+    case theory::strings::ProcessLoopMode::ABORT:
+      out << "ProcessLoopMode::ABORT";
+      break;
+    default:
+      out << "ProcessLoopMode:UNKNOWN![" << static_cast<int64_t>(mode) << "]";
+  }
+  return out;
+}
+
+}  // namespace CVC4
diff --git a/src/options/strings_process_loop_mode.h b/src/options/strings_process_loop_mode.h
new file mode 100644
index 000000000..2933e034f
--- /dev/null
+++ b/src/options/strings_process_loop_mode.h
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file strings_process_loop_mode.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Modes for processing looping word equations in the string solver.
+ **
+ ** Modes for processing looping word equations in the string solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H
+#define __CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+/** Enumeration of bit-blasting modes */
+enum class ProcessLoopMode
+{
+  /** Perform full loop processing. */
+  FULL,
+
+  /** Omit normal loop breaking. */
+  SIMPLE,
+
+  /** Abort if normal loop breaking is required. */
+  SIMPLE_ABORT,
+
+  /** Omit loop processing. */
+  NONE,
+
+  /** Abort if looping word equations are encountered. */
+  ABORT
+}; // enum ProcessLoopMode
+
+}  // namespace strings
+}  // namespace theory
+
+std::ostream& operator<<(std::ostream& out,
+                         theory::strings::ProcessLoopMode mode);
+
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */