From: Andrew Reynolds Date: Thu, 5 Dec 2019 15:19:56 +0000 (-0600) Subject: Refactor mode options for Unif+PI (#3531) X-Git-Tag: cvc5-1.0.0~3795 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f17b72fcdb535a5c06620900d2c35d2709abe968;p=cvc5.git Refactor mode options for Unif+PI (#3531) --- 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" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c47506510..075c8fa00 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1923,16 +1923,6 @@ void SmtEngine::setDefaults() { options::cbqi.set(true); } } - // setting unif requirements - if (options::sygusUnifBooleanHeuristicDt() - && !options::sygusUnifCondIndependent()) - { - options::sygusUnifCondIndependent.set(true); - } - if (options::sygusUnifCondIndependent() && !options::sygusUnif()) - { - options::sygusUnif.set(true); - } } if (options::sygusInference()) { diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 399a9576c..8da328eb6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -151,7 +151,7 @@ bool CegisUnif::getEnumValues(const std::vector& enums, // set enums for condition enumerators if (index == 1) { - if (options::sygusUnifCondIndependent()) + if (usingConditionPool()) { Assert(es.size() == 1); // whether valueus exhausted @@ -228,6 +228,11 @@ bool CegisUnif::getEnumValues(const std::vector& enums, return !addedUnifEnumSymBreakLemma; } +bool CegisUnif::usingConditionPool() const +{ + return d_sygus_unif.usingConditionPool(); +} + void CegisUnif::setConditions( const std::map>& unif_cenums, const std::map>& unif_cvalues, @@ -250,7 +255,7 @@ void CegisUnif::setConditions( // d_sygus_unif.setConditions(e, cost_lit, unif_cenums[e], // unif_cvalues[e]); if condition enumerator had value and it is being // passively generated, exclude this value - if (options::sygusUnifCondIndependent() && !itc->second.empty()) + if (usingConditionPool() && !itc->second.empty()) { Node eu = itc->second[0]; Assert(d_tds->isEnumerator(eu)); @@ -321,7 +326,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, // if condition values are being indepedently enumerated, they should be // communicated to the decision tree strategies indepedently of we // proceeding to attempt solution building - if (options::sygusUnifCondIndependent()) + if (usingConditionPool()) { setConditions(unif_cenums, unif_cvalues, lems); } @@ -353,7 +358,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, } // TODO tie this to the lemma for getting a new condition value - Assert(options::sygusUnifCondIndependent() || !lemmas.empty()); + Assert(usingConditionPool() || !lemmas.empty()); for (const Node& lem : lemmas) { Trace("cegis-unif-lemma") @@ -400,6 +405,9 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( { d_initialized = false; d_tds = d_qe->getTermDatabaseSygus(); + SygusUnifPiMode mode = options::sygusUnifPi(); + d_useCondPool = + mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN; } Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) @@ -415,7 +423,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) TypeNode ct = c.getType(); Node eu = nm->mkSkolem("eu", ct); Node ceu; - if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty()) + if (!d_useCondPool && !ci.second.d_enums[0].empty()) { // make a new conditional enumerator as well, starting the // second type around @@ -554,7 +562,7 @@ void CegisUnifEnumDecisionStrategy::initialize( DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this); // create single condition enumerator for each decision tree strategy - if (options::sygusUnifCondIndependent()) + if (d_useCondPool) { // allocate a condition enumerator for each candidate for (std::pair& ci : d_ce_info) @@ -576,7 +584,7 @@ void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt( if (index == 1) { // we always use (cost-1) conditions, or 1 if in the indepedent case - num_enums = !options::sygusUnifCondIndependent() ? num_enums - 1 : 1; + num_enums = !d_useCondPool ? num_enums - 1 : 1; } if (num_enums > 0) { @@ -622,7 +630,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, // if we are using a single independent enumerator for conditions, then we // allocate an active guard, and are eligible to use variable-agnostic // enumeration. - if (options::sygusUnifCondIndependent() && index == 1) + if (d_useCondPool && index == 1) { erole = ROLE_ENUM_POOL; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ac859750f..d476d5fb3 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -103,6 +103,11 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf TermDbSygus* d_tds; /** reference to the parent conjecture */ SynthConjecture* d_parent; + /** + * Whether we are using condition pool enumeration (Section 4 of Barbosa et al + * FMCAD 2019). This is determined by option::sygusUnifPi(). + */ + bool d_useCondPool; /** whether this module has been initialized */ bool d_initialized; /** null node */ @@ -294,6 +299,12 @@ class CegisUnif : public Cegis std::map>& unif_cenums, std::map>& unif_cvalues, std::vector& lems); + + /** + * Whether we are using condition pool enumeration (Section 4 of Barbosa et al + * FMCAD 2019). This is determined by option::sygusUnifPi(). + */ + bool usingConditionPool() const; /** * Sygus unif utility. This class implements the core algorithm (e.g. decision * tree learning) that this module relies upon. diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 5e4513ff3..84b160bb3 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -1187,7 +1187,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // TODO #1935 ITEs are added to Boolean grammars so that we can infer // unification strategies. We can do away with this if we can infer // unification strategies from and/or/not - if (k == ITE && !options::sygusUnif()) + if (k == ITE && options::sygusUnifPi() == SYGUS_UNIF_PI_NONE) { continue; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 5d4aaf7ae..1a491394f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -29,7 +29,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusUnifRl::SygusUnifRl(SynthConjecture* p) : d_parent(p) {} +SygusUnifRl::SygusUnifRl(SynthConjecture* p) + : d_parent(p), d_useCondPool(false), d_useCondPoolIGain(false) +{ +} SygusUnifRl::~SygusUnifRl() {} void SygusUnifRl::initializeCandidate( QuantifiersEngine* qe, @@ -57,6 +60,11 @@ void SygusUnifRl::initializeCandidate( d_cand_to_eval_hds[f].clear(); d_cand_to_hd_count[f] = 0; } + // check whether we are using condition enumeration + SygusUnifPiMode mode = options::sygusUnifPi(); + d_useCondPool = + mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN; + d_useCondPoolIGain = mode == SYGUS_UNIF_PI_CENUM_IGAIN; } void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector& lemmas) @@ -348,8 +356,7 @@ Node SygusUnifRl::constructSol( } EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()]; Node sol = itd->second.buildSol(etis->d_cons, lemmas); - Assert(options::sygusUnifCondIndependent() || !sol.isNull() - || !lemmas.empty()); + Assert(d_useCondPool || !sol.isNull() || !lemmas.empty()); return sol; } @@ -386,6 +393,11 @@ std::vector SygusUnifRl::getEvalPointHeads(Node c) return it->second; } +bool SygusUnifRl::usingConditionPool() const { return d_useCondPool; } +bool SygusUnifRl::usingConditionPoolInfoGain() const +{ + return d_useCondPoolIGain; +} void SygusUnifRl::registerStrategy( Node f, std::vector& enums, @@ -516,7 +528,7 @@ void SygusUnifRl::DecisionTreeInfo::setConditions( d_enums.insert(d_enums.end(), enums.begin(), enums.end()); d_conds.insert(d_conds.end(), conds.begin(), conds.end()); // add to condition pool - if (options::sygusUnifCondIndependent()) + if (d_unif->usingConditionPool()) { d_cond_mvs.insert(conds.begin(), conds.end()); if (Trace.isOn("sygus-unif-cond-pool")) @@ -552,8 +564,8 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, << " conditions..." << std::endl; // reset the trie d_pt_sep.d_trie.clear(); - return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas) - : buildSolMinCond(cons, lemmas); + return d_unif->usingConditionPool() ? buildSolAllCond(cons, lemmas) + : buildSolMinCond(cons, lemmas); } Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons, @@ -840,7 +852,7 @@ Node SygusUnifRl::DecisionTreeInfo::extractSol(Node cons, std::map& hd_mv) { // rebuild decision tree using heuristic learning - if (options::sygusUnifBooleanHeuristicDt()) + if (d_unif->usingConditionPoolInfoGain()) { recomputeSolHeuristically(hd_mv); } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index c5b02a481..827919308 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -103,9 +103,21 @@ class SygusUnifRl : public SygusUnif /** retrieve the head of evaluation points for candidate c, if any */ std::vector getEvalPointHeads(Node c); + /** + * Whether we are using condition pool enumeration (Section 4 of Barbosa et al + * FMCAD 2019). This is determined by option::sygusUnifPi(). + */ + bool usingConditionPool() const; + /** Whether we are additionally using information gain. */ + bool usingConditionPoolInfoGain() const; + protected: /** reference to the parent conjecture */ SynthConjecture* d_parent; + /** Whether we are using condition pool enumeration */ + bool d_useCondPool; + /** Whether we are additionally using information gain heuristics */ + bool d_useCondPoolIGain; /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */ std::unordered_set d_unif_candidates; /** construct sol */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index da4275365..c980e5413 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -65,7 +65,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p) { d_modules.push_back(d_ceg_pbe.get()); } - if (options::sygusUnif()) + if (options::sygusUnifPi() != SYGUS_UNIF_PI_NONE) { d_modules.push_back(d_ceg_cegisUnif.get()); } diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index c02d2b31f..1bb85bed9 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --cegqi-si=all --sygus-out=status -; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z))))))) diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2 index 6c5039c2b..b851d2e19 100644 --- a/test/regress/regress1/quantifiers/horn-simple.smt2 +++ b/test/regress/regress1/quantifiers/horn-simple.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-unif --sygus-infer +; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress1/sygus/car_3.lus.sy b/test/regress/regress1/sygus/car_3.lus.sy index 088613f21..9432d3131 100755 --- a/test/regress/regress1/sygus/car_3.lus.sy +++ b/test/regress/regress1/sygus/car_3.lus.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-unif --sygus-unif-cond-independent --sygus-unif-boolean-heuristic-dt --decision=justification +; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification (set-logic LIA) diff --git a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy index 7d1c35234..df0214316 100644 --- a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy +++ b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-unif --sygus-bool-ite-return-const --sygus-out=status +; COMMAND-LINE: --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status (set-logic LIA) (define-fun diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress1/sygus/cegisunif-depth1.sy index 1e810fea3..9f6f65907 100644 --- a/test/regress/regress1/sygus/cegisunif-depth1.sy +++ b/test/regress/regress1/sygus/cegisunif-depth1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-unif --sygus-out=status +; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy index 15df2d507..7229dea2e 100644 --- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy +++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-unif +; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete (set-logic SAT) (synth-fun u ((x Int)) Int) diff --git a/test/regress/regress1/sygus/planning-unif.sy b/test/regress/regress1/sygus/planning-unif.sy index 39c89dc53..3a715501a 100644 --- a/test/regress/regress1/sygus/planning-unif.sy +++ b/test/regress/regress1/sygus/planning-unif.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-unif --sygus-out=status +; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status (set-logic LIA) (define-fun get-y ((currPoint Int)) Int diff --git a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy index 4b0cefcda..6b647b77d 100644 --- a/test/regress/regress2/sygus/cegisunif-depth1-bv.sy +++ b/test/regress/regress2/sygus/cegisunif-depth1-bv.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-unif --sygus-out=status +; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status (set-logic BV) (synth-fun f ((x (BitVec 64)) (y (BitVec 64))) (BitVec 64)