diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-17 17:37:03 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-17 17:37:03 +0200 |
commit | 0834e9e263b1ecd014ef347d0f080ac1505fdcb4 (patch) | |
tree | 60ab31a4769f75c1bd0e29590fe2ae9a30da0c9b /src/options | |
parent | 20c1eb502d1b9f2b19419ec925e306744d9e53bf (diff) |
sygusComp2018: update policies for solution reconstruction (#2109)
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/options_handler.cpp | 58 | ||||
-rw-r--r-- | src/options/options_handler.h | 3 | ||||
-rw-r--r-- | src/options/quantifiers_modes.h | 33 | ||||
-rw-r--r-- | src/options/quantifiers_options.toml | 40 |
4 files changed, 119 insertions, 15 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 2b1d72802..8f179531b 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -489,6 +489,30 @@ all \n\ \n\ "; +const std::string OptionsHandler::s_cegqiSingleInvRconsHelp = + "\ +Modes for reconstruction solutions while using single invocation techniques,\ +supported by --cegqi-si-rcons:\n\ +\n\ +none \n\ ++ Do not try to reconstruct solutions in the original (user-provided) grammar\ + when using single invocation techniques. In this mode, solutions produced by\ + CVC4 may violate grammar restrictions.\n\ +\n\ +try \n\ ++ Try to reconstruct solutions in the original grammar when using single\ + invocation techniques in an incomplete (fail-fast) manner.\n\ +\n\ +all-limit \n\ ++ Try to reconstruct solutions in the original grammar, but termintate if a\ + maximum number of rounds for reconstruction is exceeded.\n\ +\n\ +all \n\ ++ Try to reconstruct solutions in the original grammar. In this mode,\ + we do not terminate until a solution is successfully reconstructed. \n\ +\n\ +"; + const std::string OptionsHandler::s_cegisSampleHelp = "\ Modes for sampling with counterexample-guided inductive synthesis (CEGIS),\ @@ -878,8 +902,6 @@ OptionsHandler::stringToCegqiSingleInvMode(std::string option, return theory::quantifiers::CEGQI_SI_MODE_NONE; } else if(optarg == "use" || optarg == "default") { return theory::quantifiers::CEGQI_SI_MODE_USE; - } else if(optarg == "all-abort") { - return theory::quantifiers::CEGQI_SI_MODE_ALL_ABORT; } else if(optarg == "all") { return theory::quantifiers::CEGQI_SI_MODE_ALL; } else if(optarg == "help") { @@ -891,6 +913,38 @@ OptionsHandler::stringToCegqiSingleInvMode(std::string option, } } +theory::quantifiers::CegqiSingleInvRconsMode +OptionsHandler::stringToCegqiSingleInvRconsMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::CEGQI_SI_RCONS_MODE_NONE; + } + else if (optarg == "try") + { + return theory::quantifiers::CEGQI_SI_RCONS_MODE_TRY; + } + else if (optarg == "all") + { + return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL; + } + else if (optarg == "all-limit") + { + return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT; + } + else if (optarg == "help") + { + puts(s_cegqiSingleInvRconsHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --cegqi-si-rcons: `") + + optarg + "'. Try --cegqi-si-rcons help."); + } +} + theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode( std::string option, std::string optarg) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 4cdd445ed..ab107ae78 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -108,6 +108,8 @@ public: std::string option, std::string optarg); theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode( std::string option, std::string optarg); + theory::quantifiers::CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode( + std::string option, std::string optarg); theory::quantifiers::CegisSampleMode stringToCegisSampleMode( std::string option, std::string optarg); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( @@ -245,6 +247,7 @@ public: static const std::string s_sygusSolutionOutModeHelp; static const std::string s_cbqiBvIneqModeHelp; static const std::string s_cegqiSingleInvHelp; + static const std::string s_cegqiSingleInvRconsHelp; static const std::string s_cegisSampleHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_termDbModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index a949b97be..afb54002c 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -208,12 +208,41 @@ enum CegqiSingleInvMode { CEGQI_SI_MODE_NONE, /** use single invocation techniques */ CEGQI_SI_MODE_USE, - /** always use single invocation techniques, abort if solution reconstruction will fail */ - CEGQI_SI_MODE_ALL_ABORT, /** always use single invocation techniques */ CEGQI_SI_MODE_ALL, }; +/** Solution reconstruction modes for single invocation conjectures + * + * These modes indicate the policy when CVC4 solves a synthesis conjecture using + * single invocation techniques for a sygus problem with a user-specified + * grammar. + */ +enum CegqiSingleInvRconsMode +{ + /** + * Do not try to reconstruct solutions to single invocation conjectures. With + * this mode, solutions produced by CVC4 may violate grammar restrictions. + */ + CEGQI_SI_RCONS_MODE_NONE, + /** + * Try to reconstruct solution to single invocation conjectures in an + * incomplete (fail fast) way. + */ + CEGQI_SI_RCONS_MODE_TRY, + /** + * Reconstruct solutions to single invocation conjectures, but fail if we + * reach an upper limit on number of iterations in the enumeration + */ + CEGQI_SI_RCONS_MODE_ALL_LIMIT, + /** + * Reconstruct solutions to single invocation conjectures. This method + * relies on an expensive enumeration technique which only terminates when + * we succesfully reconstruct the solution, although it may not terminate. + */ + CEGQI_SI_RCONS_MODE_ALL, +}; + enum CegisSampleMode { /** do not use samples for CEGIS */ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index ecdf87a47..bf514ada7 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -917,11 +917,30 @@ header = "options/quantifiers_options.h" [[option]] name = "cegqiSingleInvReconstruct" category = "regular" - long = "cegqi-si-reconstruct" + long = "cegqi-si-rcons=MODE" + type = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode" + default = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT" + handler = "stringToCegqiSingleInvRconsMode" + includes = ["options/quantifiers_modes.h"] + help = "policy for reconstructing solutions for single invocation conjectures" + +[[option]] + name = "cegqiSingleInvReconstructLimit" + category = "regular" + long = "cegqi-si-rcons-limit=N" + type = "int" + default = "10000" + read_only = true + help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)" + +[[option]] + name = "cegqiSingleInvReconstructConst" + category = "regular" + long = "cegqi-si-reconstruct-const" type = "bool" default = "true" read_only = true - help = "reconstruct solutions for single invocation conjectures in original grammar" + help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" [[option]] name = "cegqiSolMinCore" @@ -942,15 +961,6 @@ header = "options/quantifiers_options.h" help = "minimize individual instantiations for single invocation conjectures based on unsat core" [[option]] - name = "cegqiSingleInvReconstructConst" - category = "regular" - long = "cegqi-si-reconstruct-const" - type = "bool" - default = "true" - read_only = true - help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" - -[[option]] name = "cegqiSingleInvAbort" category = "regular" long = "cegqi-si-abort" @@ -1119,6 +1129,14 @@ header = "options/quantifiers_options.h" help = "mode for using samples in the counterexample-guided inductive synthesis loop" [[option]] + name = "minSynthSol" + category = "regular" + long = "min-synth-sol" + type = "bool" + default = "true" + help = "Minimize synthesis solutions" + +[[option]] name = "sygusEvalOpt" category = "regular" long = "sygus-eval-opt" |