Regular expression intersection modes (#3134)

1 files changed, 54 insertions, 3 deletions

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\
 ";