Regular expression intersection modes (#3134)

6 files changed, 132 insertions, 24 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index fc725978e..70af2f056 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -37,8 +37,8 @@ libcvc4_add_sources(
   set_language.h
   smt_modes.cpp
   smt_modes.h
-  strings_process_loop_mode.cpp
-  strings_process_loop_mode.h
+  strings_modes.cpp
+  strings_modes.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 43602c0a1..15436646f 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1386,7 +1386,7 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(
   }
 }
 
-const std::string OptionsHandler::s_stringToStringsProcessLoopModeHelp =
+const std::string OptionsHandler::s_stringsProcessLoopModeHelp =
     "Loop processing modes supported by the --strings-process-loop-mode "
     "option:\n"
     "\n"
@@ -1430,7 +1430,7 @@ theory::strings::ProcessLoopMode OptionsHandler::stringToStringsProcessLoopMode(
   }
   else if (optarg == "help")
   {
-    puts(s_stringToStringsProcessLoopModeHelp.c_str());
+    puts(s_stringsProcessLoopModeHelp.c_str());
     exit(1);
   }
   else
@@ -1441,6 +1441,57 @@ theory::strings::ProcessLoopMode OptionsHandler::stringToStringsProcessLoopMode(
   }
 }
 
+const std::string OptionsHandler::s_regExpInterModeHelp =
+    "\
+Regular expression intersection modes supported by the --re-inter-mode option\
+\n\
+\n\
+all \n\
++ Compute intersections for all regular expressions.\n\
+\n\
+constant (default)\n\
++ Compute intersections only between regular expressions that do not contain\
+re.allchar or re.range\n\
+\n\
+one-constant\n\
++ Compute intersections only between regular expressions such that at least one\
+side does not contain re.allchar or re.range\n\
+\n\
+none\n\
++ Do not compute intersections for regular expressions\n\
+";
+
+theory::strings::RegExpInterMode OptionsHandler::stringToRegExpInterMode(
+    std::string option, std::string optarg)
+{
+  if (optarg == "all")
+  {
+    return theory::strings::RegExpInterMode::RE_INTER_ALL;
+  }
+  else if (optarg == "constant")
+  {
+    return theory::strings::RegExpInterMode::RE_INTER_CONSTANT;
+  }
+  else if (optarg == "one-constant")
+  {
+    return theory::strings::RegExpInterMode::RE_INTER_ONE_CONSTANT;
+  }
+  else if (optarg == "none")
+  {
+    return theory::strings::RegExpInterMode::RE_INTER_NONE;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_regExpInterModeHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --re-inter-mode: `")
+                          + optarg + "'.  Try --re-inter-mode=help.");
+  }
+}
+
 const std::string OptionsHandler::s_boolToBVModeHelp =
     "\
 BoolToBV pass modes supported by the --bool-to-bv option:\n\
@@ -1768,7 +1819,7 @@ literals\n\
 + block models based on the SAT skeleton\n\
 \n\
 values\n\
-+ block models based on the concrete model values for the free variables.\n\ 
++ block models based on the concrete model values for the free variables.\n\
 \n\
 ";
 
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 59503552c..9a596ddfc 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -37,7 +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/strings_modes.h"
 #include "options/sygus_out_mode.h"
 #include "options/theoryof_mode.h"
 #include "options/ufss_mode.h"
@@ -153,6 +153,8 @@ public:
 
   theory::strings::ProcessLoopMode stringToStringsProcessLoopMode(
       std::string option, std::string optarg);
+  theory::strings::RegExpInterMode stringToRegExpInterMode(std::string option,
+                                                           std::string optarg);
 
   // theory/uf/options_handlers.h
   theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg);
@@ -242,7 +244,8 @@ public:
   static const std::string s_bvOptimizeSatProofHelp;
   static const std::string s_booleanTermConversionModeHelp;
   static const std::string s_bvSlicerModeHelp;
-  static const std::string s_stringToStringsProcessLoopModeHelp;
+  static const std::string s_stringsProcessLoopModeHelp;
+  static const std::string s_regExpInterModeHelp;
   static const std::string s_boolToBVModeHelp;
   static const std::string s_cegqiFairModeHelp;
   static const std::string s_decisionModeHelp;
diff --git a/src/options/strings_process_loop_mode.cpp b/src/options/strings_modes.cpp
index 59667ea75..c56c82716 100644
--- a/src/options/strings_process_loop_mode.cpp
+++ b/src/options/strings_modes.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file strings_process_loop_mode.cpp
+/*! \file strings_modes.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andres Noetzli
@@ -9,12 +9,10 @@
  ** 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.
+ ** \brief Modes for the string solver.
  **/
 
-#include "options/strings_process_loop_mode.h"
+#include "options/strings_modes.h"
 
 #include <cstdint>
 #include <iostream>
@@ -47,4 +45,27 @@ std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out,
+                         theory::strings::RegExpInterMode mode)
+{
+  switch (mode)
+  {
+    case theory::strings::RegExpInterMode::RE_INTER_ALL:
+      out << "RegExpInterMode::RE_INTER_ALL";
+      break;
+    case theory::strings::RegExpInterMode::RE_INTER_CONSTANT:
+      out << "RegExpInterMode::RE_INTER_CONSTANT";
+      break;
+    case theory::strings::RegExpInterMode::RE_INTER_ONE_CONSTANT:
+      out << "RegExpInterMode::RE_INTER_ONE_CONSTANT";
+      break;
+    case theory::strings::RegExpInterMode::RE_INTER_NONE:
+      out << "RegExpInterMode::RE_INTER_NONE";
+      break;
+    default:
+      out << "RegExpInterMode:UNKNOWN![" << static_cast<int64_t>(mode) << "]";
+  }
+  return out;
+}
+
 }  // namespace CVC4
diff --git a/src/options/strings_process_loop_mode.h b/src/options/strings_modes.h
index fb2248eec..7823ea8c7 100644
--- a/src/options/strings_process_loop_mode.h
+++ b/src/options/strings_modes.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file strings_process_loop_mode.h
+/*! \file strings_modes.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Andres Noetzli
@@ -9,15 +9,13 @@
  ** 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.
+ ** \brief Modes for the string solver.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H
-#define CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H
+#ifndef CVC4__THEORY__STRINGS__STRINGS_MODES_H
+#define CVC4__THEORY__STRINGS__STRINGS_MODES_H
 
 #include <iosfwd>
 
@@ -25,8 +23,8 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-/** Enumeration of bit-blasting modes */
-enum class ProcessLoopMode
+/** Enumeration of string processing loop modes */
+enum ProcessLoopMode
 {
   /** Perform full loop processing. */
   FULL,
@@ -42,7 +40,29 @@ enum class ProcessLoopMode
 
   /** Abort if looping word equations are encountered. */
   ABORT
-}; // enum ProcessLoopMode
+};  // enum ProcessLoopMode
+
+/** Enumeration of regular expression intersection modes */
+enum RegExpInterMode
+{
+  /** Compute intersections for all regular expressions. */
+  RE_INTER_ALL,
+
+  /**
+   * Compute intersections only for regular expressions without re.allchar
+   * and re.range.
+   */
+  RE_INTER_CONSTANT,
+
+  /**
+   * Compute intersections only between regular expressions where one side does
+   * not contain re.allchar and re.range.
+   */
+  RE_INTER_ONE_CONSTANT,
+
+  /** Do not compute intersections of regular expressions. */
+  RE_INTER_NONE,
+};  // enum RegExpInterMode
 
 }  // namespace strings
 }  // namespace theory
@@ -50,6 +70,9 @@ enum class ProcessLoopMode
 std::ostream& operator<<(std::ostream& out,
                          theory::strings::ProcessLoopMode mode);
 
+std::ostream& operator<<(std::ostream& out,
+                         theory::strings::RegExpInterMode mode);
+
 }  // namespace CVC4
 
-#endif /* CVC4__THEORY__BV__BITBLAST_MODE_H */
+#endif /* CVC4__THEORY__STRINGS__STRINGS_MODES_H */
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index fd00b8917..2d8411256 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -135,8 +135,8 @@ header = "options/strings_options.h"
   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"
+  includes   = ["options/strings_modes.h"]
+  help       = "determines how to process looping string equations"
 
 [[option]]
   name       = "stringInferAsLemmas"
@@ -216,3 +216,13 @@ header = "options/strings_options.h"
   default    = "true"
   read_only  = true
   help       = "do flat form inferences"
+
+[[option]]
+  name       = "stringRegExpInterMode"
+  category   = "expert"
+  long       = "re-inter-mode=MODE"
+  type       = "CVC4::theory::strings::RegExpInterMode"
+  default    = "CVC4::theory::strings::RE_INTER_CONSTANT"
+  handler    = "stringToRegExpInterMode"
+  includes   = ["options/strings_modes.h"]
+  help       = "determines which regular expressions intersections to compute"