From 2ef5f132c1169cbeadd580638cbc35b6e454d6a5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Nov 2018 16:50:48 -0600 Subject: [PATCH] Change default sygus enumeration mode to auto (#2689) --- src/options/options_handler.cpp | 7 ++ src/options/quantifiers_modes.h | 2 + src/options/quantifiers_options.toml | 4 +- src/theory/quantifiers/sygus/cegis.cpp | 24 ++--- src/theory/quantifiers/sygus/cegis_unif.cpp | 21 ++-- src/theory/quantifiers/sygus/sygus_pbe.cpp | 3 +- .../quantifiers/sygus/synth_conjecture.cpp | 13 ++- .../quantifiers/sygus/term_database_sygus.cpp | 97 +++++++++++++++++-- .../quantifiers/sygus/term_database_sygus.h | 46 ++++++--- 9 files changed, 158 insertions(+), 59 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]] diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 79bec60ee..6aca71ca3 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -69,17 +69,10 @@ bool Cegis::processInitialize(Node n, { Trace("cegis") << "Initialize cegis..." << std::endl; unsigned csize = candidates.size(); - // We only can use actively-generated enumerators if there is only one - // function-to-synthesize. Otherwise, we would have to generate a "product" of - // two actively-generated enumerators. That is, given a conjecture with two - // functions-to-synthesize with enumerators e_f and e_g, if: - // e_f -> t1, ..., tn - // e_g -> s1, ..., sm - // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj) - // for each i,j. We do not do this and revert to the default behavior of - // this module instead. - bool isActiveGen = - options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1; + // The role of enumerators is to be either the single solution or part of + // a solution involving multiple enumerators. + EnumeratorRole erole = + csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION; // initialize an enumerator for each candidate for (unsigned i = 0; i < csize; i++) { @@ -98,13 +91,8 @@ bool Cegis::processInitialize(Node n, } } Trace("cegis") << std::endl; - // variable agnostic enumerators require an active guard - d_tds->registerEnumerator(candidates[i], - candidates[i], - d_parent, - isActiveGen, - do_repair_const, - isActiveGen); + d_tds->registerEnumerator( + candidates[i], candidates[i], d_parent, erole, do_repair_const); } return true; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index dbde79aae..18e313bf0 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -44,7 +44,12 @@ bool CegisUnif::processInitialize(Node n, std::map pt_to_cond; // strategy lemmas for each strategy point std::map> strategy_lemmas; - // Initialize strategies for all functions-to-synhesize + // Initialize strategies for all functions-to-synthesize + // The role of non-unification enumerators is to be either the single solution + // or part of a solution involving multiple enumerators. + EnumeratorRole eroleNonUnif = candidates.size() == 1 + ? ROLE_ENUM_SINGLE_SOLUTION + : ROLE_ENUM_MULTI_SOLUTION; for (const Node& f : candidates) { // Init UNIF util for this candidate @@ -53,7 +58,7 @@ bool CegisUnif::processInitialize(Node n, if (!d_sygus_unif.usingUnif(f)) { Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl; - d_tds->registerEnumerator(f, f, d_parent); + d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif); d_non_unif_candidates.push_back(f); } else @@ -462,7 +467,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) exclude_cons, term_irrelevant); d_virtual_enum = nm->mkSkolem("_ve", vtn); - d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent); + d_tds->registerEnumerator( + d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); } // if new_size is a power of two, then isPow2 returns log2(new_size)+1 // otherwise, this returns 0. In the case it returns 0, we don't care @@ -606,20 +612,17 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, } // register the enumerator si.d_enums[index].push_back(e); - bool mkActiveGuard = false; - bool isActiveGen = false; + EnumeratorRole erole = ROLE_ENUM_CONSTRAINED; // 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) { - mkActiveGuard = true; - isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; + erole = ROLE_ENUM_POOL; } Trace("cegis-unif-enum") << "* Registering new enumerator " << e << " to strategy point " << si.d_pt << "\n"; - d_tds->registerEnumerator( - e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen); + d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false); } void CegisUnifEnumDecisionStrategy::registerEvalPts( diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index b49c29c53..f91dd5d30 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -179,7 +179,6 @@ bool SygusPbe::initialize(Node n, return false; } } - bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; for (const Node& c : candidates) { Assert(d_examples.find(c) != d_examples.end()); @@ -203,7 +202,7 @@ bool SygusPbe::initialize(Node n, for (const Node& e : d_candidate_to_enum[c]) { TypeNode etn = e.getType(); - d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen); + d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false); d_enum_to_candidate[e] = c; TNode te = e; // initialize static symmetry breaking lemmas for it diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 03344d2e7..2bfde2d80 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -703,13 +703,13 @@ class EnumValGeneratorBasic : public EnumValGenerator */ bool increment() override { + ++d_te; if (d_te.isFinished()) { d_currTerm = Node::null(); return false; } d_currTerm = *d_te; - ++d_te; if (options::sygusSymBreakDynamic()) { Node nextb = d_tds->sygusToBuiltin(d_currTerm); @@ -773,15 +773,18 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) else { // Actively-generated enumerators are currently either variable agnostic - // or basic. + // or basic. The auto mode always prefers the optimized enumerator over + // the basic one. Assert(d_tds->isBasicEnumerator(e)); - if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM) + if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC) { - d_evg[e].reset(new SygusEnumerator(d_tds, this)); + d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); } else { - d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); + Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM + || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO); + d_evg[e].reset(new SygusEnumerator(d_tds, this)); } } Trace("sygus-active-gen") diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 9af990086..5cf230820 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -58,6 +58,19 @@ void TypeNodeIdTrie::assignIds(std::map& assign, } } +std::ostream& operator<<(std::ostream& os, EnumeratorRole r) +{ + switch (r) + { + case ROLE_ENUM_POOL: os << "POOL"; break; + case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break; + case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break; + case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break; + default: os << "enum_" << static_cast(r); break; + } + return os; +} + TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe) : d_quantEngine(qe), d_syexp(new SygusExplain(this)), @@ -454,9 +467,8 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { void TermDbSygus::registerEnumerator(Node e, Node f, SynthConjecture* conj, - bool mkActiveGuard, - bool useSymbolicCons, - bool isActiveGen) + EnumeratorRole erole, + bool useSymbolicCons) { if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) { @@ -470,13 +482,6 @@ void TermDbSygus::registerEnumerator(Node e, d_enum_to_conjecture[e] = conj; d_enum_to_synth_fun[e] = f; NodeManager* nm = NodeManager::currentNM(); - if( mkActiveGuard ){ - // make the guard - Node ag = nm->mkSkolem("eG", nm->booleanType()); - // must ensure it is a literal immediately here - ag = d_quantEngine->getValuation().ensureLiteral(ag); - d_enum_to_active_guard[e] = ag; - } Trace("sygus-db") << " registering symmetry breaking clauses..." << std::endl; @@ -554,6 +559,66 @@ void TermDbSygus::registerEnumerator(Node e, } Trace("sygus-db") << " ...finished" << std::endl; + // determine if we are actively-generated + bool isActiveGen = false; + if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE) + { + if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED) + { + // If the enumerator is a solution for a conjecture with multiple + // functions, we do not use active generation. If we did, we would have to + // generate a "product" of two actively-generated enumerators. That is, + // given a conjecture with two functions-to-synthesize with enumerators + // e_f and e_g, and if these enumerators generated: + // e_f -> t1, ..., tn + // e_g -> s1, ..., sm + // The sygus module in charge of this conjecture would expect + // constructCandidates calls of the form + // (e_f,e_g) -> (ti, sj) + // for each i,j. We instead use passive enumeration in this case. + // + // If the enumerator is constrained, it cannot be actively generated. + } + else if (erole == ROLE_ENUM_POOL) + { + // If the enumerator is used for generating a pool of values, we always + // use active generation. + isActiveGen = true; + } + else if (erole == ROLE_ENUM_SINGLE_SOLUTION) + { + // If the enumerator is the single function-to-synthesize, if auto is + // enabled, we infer whether it is better to enable active generation. + if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO) + { + // We use active generation if the grammar of the enumerator does not + // have ITE and is not Boolean. Experimentally, it is better to + // use passive generation for these cases since it enables useful + // search space pruning techniques, e.g. evaluation unfolding, + // conjecture-specific symmetry breaking. Also, if sygus-stream is + // enabled, we always use active generation, since the use cases of + // sygus stream are to find many solutions to an easy problem, where + // the bottleneck often becomes the large number of "exclude the current + // solution" clauses. + const Datatype& dt = et.getDatatype(); + if (options::sygusStream() + || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean())) + { + isActiveGen = true; + } + } + else + { + isActiveGen = true; + } + } + else + { + Unreachable("Unknown enumerator mode in registerEnumerator"); + } + } + Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole + << " returned " << isActiveGen << std::endl; // Currently, actively-generated enumerators are either basic or variable // agnostic. bool isVarAgnostic = @@ -607,6 +672,18 @@ void TermDbSygus::registerEnumerator(Node e, } d_enum_active_gen[e] = isActiveGen; d_enum_basic[e] = isActiveGen && !isVarAgnostic; + + // We make an active guard if we will be explicitly blocking solutions for + // the enumerator. This is the case if the role of the enumerator is to + // populate a pool of terms, or (some cases) of when it is actively generated. + if (isActiveGen || erole == ROLE_ENUM_POOL) + { + // make the guard + Node ag = nm->mkSkolem("eG", nm->booleanType()); + // must ensure it is a literal immediately here + ag = d_quantEngine->getValuation().ensureLiteral(ag); + d_enum_to_active_guard[e] = ag; + } } bool TermDbSygus::isEnumerator(Node e) const diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 713e322a4..2e8604411 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -48,6 +48,23 @@ class TypeNodeIdTrie void assignIds(std::map& assign, unsigned& idCount); }; +/** role for registering an enumerator */ +enum EnumeratorRole +{ + /** The enumerator populates a pool of terms (e.g. for PBE). */ + ROLE_ENUM_POOL, + /** The enumerator is the single solution of the problem. */ + ROLE_ENUM_SINGLE_SOLUTION, + /** + * The enumerator is part of the solution of the problem (e.g. multiple + * functions to synthesize). + */ + ROLE_ENUM_MULTI_SOLUTION, + /** The enumerator must satisfy some set of constraints */ + ROLE_ENUM_CONSTRAINED, +}; +std::ostream& operator<<(std::ostream& os, EnumeratorRole r); + // TODO :issue #1235 split and document this class class TermDbSygus { public: @@ -80,29 +97,32 @@ class TermDbSygus { //------------------------------enumerators /** * Register a variable e that we will do enumerative search on. + * * conj : the conjecture that the enumeration of e is for. - * f : the synth-fun that the enumeration of e is for. - * mkActiveGuard : whether we want to make an active guard for e - * (see d_enum_to_active_guard), - * useSymbolicCons : whether we want model values for e to include symbolic - * constructors like the "any constant" variable. - * isActiveGen : if this flag is true, the enumerator will be - * actively-generated based on the mode specified by --sygus-active-gen. + * + * f : the synth-fun that the enumeration of e is for.Notice that enumerator + * e may not be one-to-one with f in synthesis-through-unification approaches + * (e.g. decision tree construction for PBE synthesis). + * + * erole : the role of this enumerator (see definition of EnumeratorRole). + * Depending on this and the policy for actively-generated enumerators + * (--sygus-active-gen), the enumerator may be "actively-generated". * For example, if --sygus-active-gen=var-agnostic, then the enumerator will * only generate values whose variables are in canonical order (only x1-x2 * and not x2-x1 will be generated, assuming x1 and x2 are in the same * "subclass", see getSubclassForVar). * - * Notice that enumerator e may not be one-to-one with f in - * synthesis-through-unification approaches (e.g. decision tree construction - * for PBE synthesis). + * useSymbolicCons : whether we want model values for e to include symbolic + * constructors like the "any constant" variable. + * + * An "active guard" may be allocated by this method for e based on erole + * and the policies for active generation. */ void registerEnumerator(Node e, Node f, SynthConjecture* conj, - bool mkActiveGuard = false, - bool useSymbolicCons = false, - bool isActiveGen = false); + EnumeratorRole erole, + bool useSymbolicCons = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ -- 2.30.2