diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-09 16:54:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-09 16:54:58 -0500 |
commit | 9168f325706e61bb12fec71cd375647e2102f8d3 (patch) | |
tree | aa5129a48322e43ae0f5faa9ade2decbd7091df0 /src/options | |
parent | 90ffa8b4eb26af9060e57be7fe5d6008717d3ce6 (diff) |
Support for basic actively-generated enumerators (#2606)
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/options_handler.cpp | 43 | ||||
-rw-r--r-- | src/options/options_handler.h | 3 | ||||
-rw-r--r-- | src/options/quantifiers_modes.h | 10 | ||||
-rw-r--r-- | src/options/quantifiers_options.toml | 13 |
4 files changed, 64 insertions, 5 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 22d944e4c..6eed732e2 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -525,6 +525,21 @@ post \n\ \n\ "; +const std::string OptionsHandler::s_sygusActiveGenHelp = + "\ +Modes for actively-generated sygus enumerators, supported by --sygus-active-gen:\n\ +\n\ +none \n\ ++ Do not use actively-generated sygus enumerators.\n\ +\n\ +basic \n\ ++ Use basic type enumerator as sygus enumerator.\n\ +\n\ +var-agnostic \n\ ++ Use sygus solver to enumerate terms that are agnostic to variables. \n\ +\n\ +"; + const std::string OptionsHandler::s_macrosQuantHelp = "\ Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ \n\ @@ -952,6 +967,34 @@ OptionsHandler::stringToSygusInvTemplMode(std::string option, } } +theory::quantifiers::SygusActiveGenMode +OptionsHandler::stringToSygusActiveGenMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_NONE; + } + else if (optarg == "basic") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_BASIC; + } + else if (optarg == "var-agnostic") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC; + } + else if (optarg == "help") + { + puts(s_sygusActiveGenHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + + optarg + "'. Try --sygus-inv-templ help."); + } +} + theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode( std::string option, std::string optarg) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 1869dc6a0..0205b0b73 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -114,6 +114,8 @@ public: std::string option, std::string optarg); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( std::string option, std::string optarg); + theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode( + std::string option, std::string optarg); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode( std::string option, std::string optarg); theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode( @@ -245,6 +247,7 @@ public: static const std::string s_cegqiSingleInvRconsHelp; static const std::string s_cegisSampleHelp; static const std::string s_sygusInvTemplHelp; + static const std::string s_sygusActiveGenHelp; static const std::string s_termDbModeHelp; static const std::string s_theoryOfModeHelp; static const std::string s_triggerSelModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 1fd29340d..42ab7bc06 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -262,6 +262,16 @@ enum SygusInvTemplMode { SYGUS_INV_TEMPL_MODE_POST, }; +enum SygusActiveGenMode +{ + /** do not use actively-generated enumerators */ + SYGUS_ACTIVE_GEN_NONE, + /** use basic actively-generated enumerators */ + SYGUS_ACTIVE_GEN_BASIC, + /** use variable-agnostic enumerators */ + SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, +}; + enum MacrosQuantMode { /** infer all definitions */ MACROS_QUANT_MODE_ALL, diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index eb32beef5..cbc380f43 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1032,12 +1032,15 @@ header = "options/quantifiers_options.h" help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions" [[option]] - name = "sygusEnumVarAgnostic" + name = "sygusActiveGenMode" category = "regular" - long = "sygus-var-agnostic" - type = "bool" - default = "false" - help = "when possible, use variable-agnostic enumerators" + long = "sygus-active-gen=MODE" + type = "CVC4::theory::quantifiers::SygusActiveGenMode" + default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE" + handler = "stringToSygusActiveGenMode" + includes = ["options/quantifiers_modes.h"] + read_only = true + help = "mode for actively-generated sygus enumerators" [[option]] name = "sygusMinGrammar" |