diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-05 16:50:48 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-05 16:50:48 -0600 |
| commit | 2ef5f132c1169cbeadd580638cbc35b6e454d6a5 (patch) | |
| tree | e52fe812aafe511293e345c494f4a389eec0f855 /src/options | |
| parent | cc5ea0ed533e081ecccca57cf1c4efb63296f995 (diff) | |
Change default sygus enumeration mode to auto (#2689)
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/options_handler.cpp | 7 | ||||
| -rw-r--r-- | src/options/quantifiers_modes.h | 2 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 4 |
3 files changed, 11 insertions, 2 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index e4c0276ea..565f28334 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -538,6 +538,9 @@ enum \n\ var-agnostic \n\ + Use sygus solver to enumerate terms that are agnostic to variables. \n\ \n\ +auto (default) \n\ ++ Internally decide the best policy for each enumerator. \n\ +\n\ "; const std::string OptionsHandler::s_macrosQuantHelp = "\ @@ -987,6 +990,10 @@ OptionsHandler::stringToSygusActiveGenMode(std::string option, { return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC; } + else if (optarg == "auto") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO; + } else if (optarg == "help") { puts(s_sygusActiveGenHelp.c_str()); diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 392393a91..05388cdf6 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -272,6 +272,8 @@ enum SygusActiveGenMode SYGUS_ACTIVE_GEN_ENUM, /** use variable-agnostic enumerators */ SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, + /** internally decide the best policy for each enumerator */ + SYGUS_ACTIVE_GEN_AUTO, }; enum MacrosQuantMode { diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 0b28c6a27..c555c37bf 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1044,7 +1044,7 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-active-gen=MODE" type = "CVC4::theory::quantifiers::SygusActiveGenMode" - default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE" + default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO" handler = "stringToSygusActiveGenMode" includes = ["options/quantifiers_modes.h"] read_only = true @@ -1135,7 +1135,7 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-pbe-multi-fair" type = "bool" - default = "true" + default = "false" help = "when using multiple enumerators, ensure that we only register value of minimial term size" [[option]] |