From f17b72fcdb535a5c06620900d2c35d2709abe968 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Dec 2019 09:19:56 -0600 Subject: Refactor mode options for Unif+PI (#3531) --- src/options/options_handler.cpp | 52 ++++++++++++++++++++++++++++++++++++ src/options/options_handler.h | 3 +++ src/options/quantifiers_modes.h | 18 +++++++++++++ src/options/quantifiers_options.toml | 29 ++++++-------------- 4 files changed, 81 insertions(+), 21 deletions(-) (limited to 'src/options') diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index faf358573..35827d3b0 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -569,6 +569,27 @@ auto (default) \n\ \n\ "; +const std::string OptionsHandler::s_sygusUnifPiHelp = + "\ +Modes for piecewise-independent unification supported by --sygus-unif-pi:\n\ +\n\ +none \n\ ++ Do not use piecewise-independent unification.\n\ +\n\ +complete \n\ ++ Use complete approach for piecewise-independent unification (see Section 3\n\ +of Barbosa et al FMCAD 2019).\n\ +\n\ +cond-enum \n\ ++ Use unconstrained condition enumeration for piecewise-independent\n\ +unification (see Section 4 of Barbosa et al FMCAD 2019).\n\ +\n\ +cond-enum-igain \n\ ++ Same as cond-enum, but additionally uses an information gain heuristic\n\ +when doing decision tree learning.\n\ +\n\ +"; + const std::string OptionsHandler::s_sygusGrammarConsHelp = "\ Modes for default SyGuS grammars, supported by --sygus-grammar-cons:\n\ @@ -1141,6 +1162,37 @@ OptionsHandler::stringToSygusGrammarConsMode(std::string option, } } +theory::quantifiers::SygusUnifPiMode OptionsHandler::stringToSygusUnifPiMode( + std::string option, std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::SYGUS_UNIF_PI_NONE; + } + else if (optarg == "complete") + { + return theory::quantifiers::SYGUS_UNIF_PI_COMPLETE; + } + else if (optarg == "cond-enum") + { + return theory::quantifiers::SYGUS_UNIF_PI_CENUM; + } + else if (optarg == "cond-enum-igain") + { + return theory::quantifiers::SYGUS_UNIF_PI_CENUM_IGAIN; + } + else if (optarg == "help") + { + puts(s_sygusUnifPiHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --sygus-unif-pi: `") + + optarg + "'. Try --sygus-unif-pi 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 eae61c5b2..2e372a00c 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -122,6 +122,8 @@ public: std::string option, std::string optarg); theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode( std::string option, std::string optarg); + theory::quantifiers::SygusUnifPiMode stringToSygusUnifPiMode( + std::string option, std::string optarg); theory::quantifiers::SygusGrammarConsMode stringToSygusGrammarConsMode( std::string option, std::string optarg); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode( @@ -277,6 +279,7 @@ public: static const std::string s_sygusFilterSolHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_sygusActiveGenHelp; + static const std::string s_sygusUnifPiHelp; static const std::string s_sygusGrammarConsHelp; static const std::string s_termDbModeHelp; static const std::string s_theoryOfModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 9ff2ac196..1a256b0bc 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -342,6 +342,24 @@ enum QuantRepMode { QUANT_REP_MODE_DEPTH, }; +/** + * Modes for piecewise-independent unification for synthesis (see Barbosa et al + * FMCAD 2019). + */ +enum SygusUnifPiMode +{ + /** do not do piecewise-independent unification for synthesis */ + SYGUS_UNIF_PI_NONE, + /** use (finite-model) complete piecewise-independent unification */ + SYGUS_UNIF_PI_COMPLETE, + /** use approach based on condition enumeration for piecewise-independent + unification */ + SYGUS_UNIF_PI_CENUM, + /** use approach based on condition enumeration with information gain + heuristics for piecewise-independent unification */ + SYGUS_UNIF_PI_CENUM_IGAIN, +}; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 171af1e47..e7a24cf3e 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -950,20 +950,15 @@ header = "options/quantifiers_options.h" help = "abort if constant repair techniques are not applicable" [[option]] - name = "sygusUnif" + name = "sygusUnifPi" category = "regular" - long = "sygus-unif" - type = "bool" - default = "false" - help = "Unification-based function synthesis" - -[[option]] - name = "sygusUnifCondIndependent" - category = "regular" - long = "sygus-unif-cond-independent" - type = "bool" - default = "false" - help = "Synthesize conditions indepedently from return values (may generate bigger solutions)" + long = "sygus-unif-pi=MODE" + type = "CVC4::theory::quantifiers::SygusUnifPiMode" + default = "CVC4::theory::quantifiers::SYGUS_UNIF_PI_NONE" + handler = "stringToSygusUnifPiMode" + includes = ["options/quantifiers_modes.h"] + read_only = true + help = "mode for synthesis via piecewise-indepedent unification" [[option]] name = "sygusUnifShuffleCond" @@ -973,14 +968,6 @@ header = "options/quantifiers_options.h" default = "false" help = "Shuffle condition pool when building solutions (may change solutions sizes)" -[[option]] - name = "sygusUnifBooleanHeuristicDt" - category = "regular" - long = "sygus-unif-boolean-heuristic-dt" - type = "bool" - default = "false" - help = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)" - [[option]] name = "sygusUnifCondIndNoRepeatSol" category = "regular" -- cgit v1.2.3