diff options
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/options_handler.cpp | 44 | ||||
-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 | 16 |
4 files changed, 70 insertions, 3 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 565f28334..bd5b00728 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -508,6 +508,21 @@ trust \n\ \n\ "; +const std::string OptionsHandler::s_sygusFilterSolHelp = + "\ +Modes for filtering sygus solutions supported by --sygus-filter-sol:\n\ +\n\ +none (default) \n\ ++ Do not filter sygus solutions.\n\ +\n\ +strong \n\ ++ Filter solutions that are logically stronger than others.\n\ +\n\ +weak \n\ ++ Filter solutions that are logically weaker than others.\n\ +\n\ +"; + const std::string OptionsHandler::s_sygusInvTemplHelp = "\ Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ \n\ @@ -951,6 +966,35 @@ theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode( } } +theory::quantifiers::SygusFilterSolMode +OptionsHandler::stringToSygusFilterSolMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::SYGUS_FILTER_SOL_NONE; + } + else if (optarg == "strong") + { + return theory::quantifiers::SYGUS_FILTER_SOL_STRONG; + } + else if (optarg == "weak") + { + return theory::quantifiers::SYGUS_FILTER_SOL_WEAK; + } + else if (optarg == "help") + { + puts(s_cegisSampleHelp.c_str()); + exit(1); + } + else + { + throw OptionException( + std::string("unknown option for --sygus-filter-sol: `") + optarg + + "'. Try --sygus-filter-sol help."); + } +} + theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 3078db0f8..53e317895 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -112,6 +112,8 @@ public: std::string option, std::string optarg); theory::quantifiers::CegisSampleMode stringToCegisSampleMode( std::string option, std::string optarg); + theory::quantifiers::SygusFilterSolMode stringToSygusFilterSolMode( + std::string option, std::string optarg); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( std::string option, std::string optarg); theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode( @@ -248,6 +250,7 @@ public: static const std::string s_cegqiSingleInvHelp; static const std::string s_cegqiSingleInvRconsHelp; static const std::string s_cegisSampleHelp; + static const std::string s_sygusFilterSolHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_sygusActiveGenHelp; static const std::string s_termDbModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 05388cdf6..41378d2cd 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -276,6 +276,16 @@ enum SygusActiveGenMode SYGUS_ACTIVE_GEN_AUTO, }; +enum SygusFilterSolMode +{ + /** do not filter solutions */ + SYGUS_FILTER_SOL_NONE, + /** filter logically stronger solutions */ + SYGUS_FILTER_SOL_STRONG, + /** filter logically weaker solutions */ + SYGUS_FILTER_SOL_WEAK, +}; + enum MacrosQuantMode { /** infer all definitions */ MACROS_QUANT_MODE_ALL, diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c555c37bf..d9d3e0d38 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1403,12 +1403,22 @@ header = "options/quantifiers_options.h" help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" [[option]] - name = "sygusSolFilterImplied" + name = "sygusFilterSolMode" category = "regular" - long = "sygus-sol-filter-implied" + long = "sygus-filter-sol=MODE" + type = "CVC4::theory::quantifiers::SygusFilterSolMode" + default = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE" + handler = "stringToSygusFilterSolMode" + includes = ["options/quantifiers_modes.h"] + help = "mode for filtering sygus solutions" + +[[option]] + name = "sygusFilterSolRevSubsume" + category = "expert" + long = "sygus-filter-sol-rev" type = "bool" default = "false" - help = "use sygus to enumerate interesting satisfiability queries" + help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" [[option]] name = "sygusExprMinerCheckUseExport" |