diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-01 09:08:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-01 09:08:46 -0500 |
commit | 79881c196e29ef341166e7a31c1183e8b537d069 (patch) | |
tree | 25466cceb67c54895bf012fd745dd864d356b153 /src/options | |
parent | 7537ff075dbb2d814d722d2d72586ce78235467c (diff) |
Regular expression intersection modes (#3134)
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/CMakeLists.txt | 4 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 57 | ||||
-rw-r--r-- | src/options/options_handler.h | 7 | ||||
-rw-r--r-- | src/options/strings_modes.cpp (renamed from src/options/strings_process_loop_mode.cpp) | 31 | ||||
-rw-r--r-- | src/options/strings_modes.h (renamed from src/options/strings_process_loop_mode.h) | 43 | ||||
-rw-r--r-- | src/options/strings_options.toml | 14 |
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" |