From d568dc52302e731bfea7f580862fc11bde76c1bf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 8 Jul 2022 23:49:19 -0500 Subject: [PATCH] Eliminate static options accesses in sygus (#8943) Towards eliminating option scopes. Also simplifies and corrects an issue in default Boolean grammar construction where included/excluded constructors were ignored. --- .../quantifiers/sygus/enum_value_manager.cpp | 3 +- .../quantifiers/sygus/sygus_enumerator.cpp | 17 +++-- .../quantifiers/sygus/sygus_enumerator.h | 11 ++- .../quantifiers/sygus/sygus_grammar_cons.cpp | 69 ++++++++----------- .../quantifiers/sygus/sygus_grammar_cons.h | 14 ++-- .../quantifiers/sygus/sygus_interpol.cpp | 1 + .../quantifiers/sygus/sygus_unif_rl.cpp | 24 ++++--- src/theory/quantifiers/sygus/sygus_unif_rl.h | 10 ++- src/theory/quantifiers/sygus_inst.cpp | 3 +- 9 files changed, 88 insertions(+), 64 deletions(-) diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index 93e29f8b3..ed8c7589f 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -125,7 +125,8 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) d_secd.get(), &d_stats, false, - options().quantifiers.sygusRepairConst); + options().quantifiers.sygusRepairConst, + options().quantifiers.sygusEnumFastNumConsts); } } Trace("sygus-active-gen") diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index bc9146dfd..53b8e4ada 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -38,13 +38,15 @@ SygusEnumerator::SygusEnumerator(Env& env, SygusEnumeratorCallback* sec, SygusStatistics* s, bool enumShapes, - bool enumAnyConstHoles) + bool enumAnyConstHoles, + size_t numConstants) : EnumValGenerator(env), d_tds(tds), d_sec(sec), d_stats(s), d_enumShapes(enumShapes), d_enumAnyConstHoles(enumAnyConstHoles), + d_enumNumConsts(numConstants), d_tlEnum(nullptr), d_abortSize(-1) { @@ -598,7 +600,7 @@ SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) } initializeTermCache(tn); // create the master enumerator - d_masterEnumInt[tn].reset(new TermEnumMasterInterp(tn)); + d_masterEnumInt[tn].reset(new TermEnumMasterInterp(tn, d_enumNumConsts)); // initialize the master enumerator TermEnumMasterInterp* temi = d_masterEnumInt[tn].get(); bool ret = temi->initialize(this, tn); @@ -1147,8 +1149,13 @@ Node SygusEnumerator::TermEnumMaster::convertShape( return visited[n]; } -SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn) - : TermEnum(), d_te(tn), d_currNumConsts(0), d_nextIndexEnd(0) +SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn, + size_t numConstants) + : TermEnum(), + d_te(tn), + d_currNumConsts(0), + d_nextIndexEnd(0), + d_enumNumConsts(numConstants) { } @@ -1177,7 +1184,7 @@ bool SygusEnumerator::TermEnumMasterInterp::increment() { tc.pushEnumSizeIndex(); d_currSize++; - d_currNumConsts = d_currNumConsts * options::sygusEnumFastNumConsts(); + d_currNumConsts = d_currNumConsts * d_enumNumConsts; d_nextIndexEnd = d_nextIndexEnd + d_currNumConsts; } ++d_te; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 441c57618..2626aca5a 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -70,13 +70,16 @@ class SygusEnumerator : public EnumValGenerator * number of free variables * @param enumAnyConstHoles If true, this enumerator will generate terms where * free variables are the arguments to any-constant constructors. + * @param numConstants The number of interpreted constants to consider for + * each size */ SygusEnumerator(Env& env, TermDbSygus* tds = nullptr, SygusEnumeratorCallback* sec = nullptr, SygusStatistics* s = nullptr, bool enumShapes = false, - bool enumAnyConstHoles = false); + bool enumAnyConstHoles = false, + size_t numConstants = 5); ~SygusEnumerator() {} /** initialize this class with enumerator e */ void initialize(Node e) override; @@ -103,6 +106,8 @@ class SygusEnumerator : public EnumValGenerator /** Whether we are enumerating free variables as arguments to any-constant * constructors */ bool d_enumAnyConstHoles; + /** The number of interpreted constants to consider for each size */ + size_t d_enumNumConsts; /** Term cache * * This stores a list of terms for a given sygus type. The key features of @@ -456,7 +461,7 @@ class SygusEnumerator : public EnumValGenerator class TermEnumMasterInterp : public TermEnum { public: - TermEnumMasterInterp(TypeNode tn); + TermEnumMasterInterp(TypeNode tn, size_t numConstants); /** initialize this enumerator */ bool initialize(SygusEnumerator* se, TypeNode tn); /** get the current term of the enumerator */ @@ -471,6 +476,8 @@ class SygusEnumerator : public EnumValGenerator unsigned d_currNumConsts; /** the next end threshold */ unsigned d_nextIndexEnd; + /** The number of interpreted constants to consider for each size */ + size_t d_enumNumConsts; }; /** a free variable enumerator * diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 9d3e9d7fa..2081ed86d 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -22,7 +22,6 @@ #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/base_options.h" -#include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" @@ -169,7 +168,8 @@ Node CegGrammarConstructor::process(Node q, } // make the default grammar - tn = mkSygusDefaultType(preGrammarType, + tn = mkSygusDefaultType(options(), + preGrammarType, sfvl, ss.str(), extra_cons, @@ -392,13 +392,9 @@ Node CegGrammarConstructor::convertToEmbedding(Node n) return visited[n]; } -TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, - std::set& unres) +TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name) { - TypeNode unresolved = - NodeManager::currentNM()->mkUnresolvedDatatypeSort(name); - unres.insert(unresolved); - return unresolved; + return NodeManager::currentNM()->mkUnresolvedDatatypeSort(name); } void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, @@ -576,7 +572,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( const std::map>& include_cons, std::unordered_set& term_irrelevant, std::vector& sdts, - std::set& unres) + options::SygusGrammarConsMode sgcm) { NodeManager* nm = NodeManager::currentNM(); Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " @@ -615,14 +611,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // create placeholder for boolean type (kept apart since not collected) + // make Boolean type + TypeNode bool_type = nm->booleanType(); + // the index of Bool in types + size_t boolIndex = types.size(); + types.push_back(bool_type); + // create placeholders for collected types std::vector unres_types; std::map type_to_unres; std::map>::const_iterator itc; // maps types to the index of its "any term" grammar construction std::map> typeToGAnyTerm; - options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode(); - for (unsigned i = 0, size = types.size(); i < size; ++i) + for (size_t i = 0, size = types.size(); i < size; ++i) { std::stringstream ss; ss << fun << "_" << types[i]; @@ -639,23 +640,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdts.back().d_include_cons = itc->second; } //make unresolved type - TypeNode unres_t = mkUnresolvedType(dname, unres); + TypeNode unres_t = mkUnresolvedType(dname); unres_types.push_back(unres_t); type_to_unres[types[i]] = unres_t; sygus_to_builtin[unres_t] = types[i]; } - // make Boolean type - std::stringstream ssb; - ssb << fun << "_Bool"; - std::string dbname = ssb.str(); - sdts.push_back(SygusDatatypeGenerator(dbname)); - unsigned boolIndex = types.size(); - TypeNode bool_type = nm->booleanType(); - TypeNode unres_bt = mkUnresolvedType(ssb.str(), unres); - types.push_back(bool_type); - unres_types.push_back(unres_bt); - type_to_unres[bool_type] = unres_bt; - sygus_to_builtin[unres_bt] = bool_type; + TypeNode unres_bt = type_to_unres[bool_type]; // We ensure an ordering on types such that parametric types are processed // before their consitituents. Since parametric types were added before their @@ -687,7 +677,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::stringstream ssat; ssat << sdts[i].d_sdt.getName() << "_any_term"; sdts.push_back(SygusDatatypeGenerator(ssat.str())); - TypeNode unresAnyTerm = mkUnresolvedType(ssat.str(), unres); + TypeNode unresAnyTerm = mkUnresolvedType(ssat.str()); unres_types.push_back(unresAnyTerm); // set tracking information for later addition at boolean type. std::pair p(sdts.size() - 1, false); @@ -789,7 +779,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( ss << fun << "_PosIReal"; std::string posIRealName = ss.str(); // make unresolved type - TypeNode unresPosIReal = mkUnresolvedType(posIRealName, unres); + TypeNode unresPosIReal = mkUnresolvedType(posIRealName); unres_types.push_back(unresPosIReal); // make data type for positive constant integral reals sdts.push_back(SygusDatatypeGenerator(posIRealName)); @@ -1117,7 +1107,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::stringstream ss; ss << fun << "_AnyConst"; // Make sygus datatype for any constant. - TypeNode unresAnyConst = mkUnresolvedType(ss.str(), unres); + TypeNode unresAnyConst = mkUnresolvedType(ss.str()); unres_types.push_back(unresAnyConst); sdts.push_back(SygusDatatypeGenerator(ss.str())); sdts.back().d_sdt.addAnyConstantConstructor(types[i]); @@ -1460,13 +1450,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( for (unsigned i = 0; i < 4; i++) { Kind k = i == 0 ? NOT : (i == 1 ? AND : (i == 2 ? OR : ITE)); - // 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::sygusUnifPi() == options::SygusUnifPiMode::NONE) - { - continue; - } Trace("sygus-grammar-def") << "...add for " << k << std::endl; std::vector cargs; cargs.push_back(unres_bt); @@ -1498,6 +1481,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } TypeNode CegGrammarConstructor::mkSygusDefaultType( + const Options& opts, TypeNode range, Node bvl, const std::string& fun, @@ -1506,6 +1490,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( std::map>& include_cons, std::unordered_set& term_irrelevant) { + NodeManager* nm = NodeManager::currentNM(); Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl; for (std::map>::iterator it = extra_cons.begin(); @@ -1514,7 +1499,15 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( { Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl; } - std::set unres; + // 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 (opts.quantifiers.sygusUnifPi == options::SygusUnifPiMode::NONE) + { + TypeNode btype = nm->booleanType(); + exclude_cons[btype].insert(nm->operatorOf(ITE)); + Trace("sygus-grammar-def") << "...exclude Boolean ITE" << std::endl; + } std::vector sdts; mkSygusDefaultGrammar(range, bvl, @@ -1524,7 +1517,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( include_cons, term_irrelevant, sdts, - unres); + opts.quantifiers.sygusGrammarConsMode); // extract the datatypes from the sygus datatype generator objects std::vector datatypes; for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) @@ -1533,8 +1526,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( } Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; Assert(!datatypes.empty()); - std::vector types = - NodeManager::currentNM()->mkMutualDatatypeTypes(datatypes); + std::vector types = nm->mkMutualDatatypeTypes(datatypes); Trace("sygus-grammar-def") << "...finished" << std::endl; Assert(types.size() == datatypes.size()); return types[0]; @@ -1547,7 +1539,6 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a return templ_arg_sygus_type; }else{ tcount++; - std::set unres; std::vector sdts; std::stringstream ssd; ssd << fun << "_templ_" << tcount; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 4d01ad866..7b9e5a700 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -25,6 +25,7 @@ #include "expr/attribute.h" #include "expr/node.h" #include "expr/sygus_datatype.h" +#include "options/quantifiers_options.h" #include "smt/env_obj.h" namespace cvc5::internal { @@ -109,6 +110,7 @@ public: * will be included. */ static TypeNode mkSygusDefaultType( + const Options& opts, TypeNode range, Node bvl, const std::string& fun, @@ -120,7 +122,8 @@ public: /** * Make the default sygus datatype type corresponding to builtin type range. */ - static TypeNode mkSygusDefaultType(TypeNode range, + static TypeNode mkSygusDefaultType(const Options& opts, + TypeNode range, Node bvl, const std::string& fun) { @@ -128,7 +131,8 @@ public: std::map> exclude_cons; std::map> include_cons; std::unordered_set term_irrelevant; - return mkSygusDefaultType(range, + return mkSygusDefaultType(opts, + range, bvl, fun, extra_cons, @@ -220,15 +224,13 @@ public: }; // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) - static TypeNode mkUnresolvedType(const std::string& name, - std::set& unres); + static TypeNode mkUnresolvedType(const std::string& name); // collect the list of types that depend on type range static void collectSygusGrammarTypesFor(TypeNode range, std::vector& types); /** helper function for function mkSygusDefaultType * Collects a set of mutually recursive datatypes "datatypes" corresponding to * encoding type "range" to SyGuS. - * unres is used for the resulting call to mkMutualDatatypeTypes */ static void mkSygusDefaultGrammar( TypeNode range, @@ -239,7 +241,7 @@ public: const std::map>& include_cons, std::unordered_set& term_irrelevant, std::vector& sdts, - std::set& unres); + options::SygusGrammarConsMode sgcm); // helper function for mkSygusTemplateType static TypeNode mkSygusTemplateTypeRec(Node templ, diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 7230e0ce6..df6b237b6 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -192,6 +192,7 @@ TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType, getIncludeCons(axioms, conj, include_cons); std::unordered_set terms_irrelevant; itpGTypeS = CegGrammarConstructor::mkSygusDefaultType( + options(), NodeManager::currentNM()->booleanType(), d_ibvlShared, "interpolation_grammar", diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 8bc1e5a96..827e0e360 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -361,7 +361,11 @@ Node SygusUnifRl::constructSol( return d_parent->getModelValue(e); } EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()]; - Node sol = itd->second.buildSol(etis->d_cons, lemmas); + Node sol = + itd->second.buildSol(etis->d_cons, + lemmas, + options().quantifiers.sygusUnifShuffleCond, + options().quantifiers.sygusUnifCondIndNoRepeatSol); Assert(d_useCondPool || !sol.isNull() || !lemmas.empty()); return sol; } @@ -558,7 +562,9 @@ unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const } Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, - std::vector& lemmas) + std::vector& lemmas, + bool shuffleCond, + bool condIndNoRepeatSol) { if (!d_template.first.isNull()) { @@ -570,12 +576,15 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, << " conditions..." << std::endl; // reset the trie d_pt_sep.d_trie.clear(); - return d_unif->usingConditionPool() ? buildSolAllCond(cons, lemmas) - : buildSolMinCond(cons, lemmas); + return d_unif->usingConditionPool() + ? buildSolAllCond(cons, lemmas, shuffleCond, condIndNoRepeatSol) + : buildSolMinCond(cons, lemmas); } Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons, - std::vector& lemmas) + std::vector& lemmas, + bool shuffleCond, + bool condIndNoRepeatSol) { // model values for evaluation heads std::map hd_mv; @@ -589,7 +598,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons, // bigger, or have no impact) and which conditions will be present in the DT, // which influences the "quality" of the solution for cases not covered in the // current data points - if (options::sygusUnifShuffleCond()) + if (shuffleCond) { std::shuffle(d_conds.begin(), d_conds.end(), Random::getRandom()); } @@ -624,8 +633,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons, Trace("sygus-unif-sol") << "...ready to build solution from DT\n"; Node sol = extractSol(cons, hd_mv); // repeated solution - if (options::sygusUnifCondIndNoRepeatSol() - && d_sols.find(sol) != d_sols.end()) + if (condIndNoRepeatSol && d_sols.find(sol) != d_sols.end()) { return Node::null(); } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index e99ec3118..f6655438c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -224,9 +224,15 @@ class SygusUnifRl : public SygusUnif * A solution is possible when all different valued heads can be separated, * i.e. the current set of conditions separates them in a decision tree */ - Node buildSol(Node cons, std::vector& lemmas); + Node buildSol(Node cons, + std::vector& lemmas, + bool shuffleCond, + bool condIndNoRepeatSol); /** bulids a solution by considering all condition values ever enumerated */ - Node buildSolAllCond(Node cons, std::vector& lemmas); + Node buildSolAllCond(Node cons, + std::vector& lemmas, + bool shuffleCond, + bool condIndNoRepeatSol); /** builds a solution by incrementally adding points and conditions to DT * * Differently from the above method, here a condition is only added to the diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index a5f88dc37..938c5e848 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -446,7 +446,8 @@ void SygusInst::registerQuantifier(Node q) for (const Node& var : q[0]) { addSpecialValues(var.getType(), extra_cons); - TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(), + TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(options(), + var.getType(), Node(), var.toString(), extra_cons, -- 2.30.2