From: Andrew Reynolds Date: Tue, 9 Oct 2018 21:54:58 +0000 (-0500) Subject: Support for basic actively-generated enumerators (#2606) X-Git-Tag: cvc5-1.0.0~4442 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9168f325706e61bb12fec71cd375647e2102f8d3;p=cvc5.git Support for basic actively-generated enumerators (#2606) --- diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 22d944e4c..6eed732e2 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -525,6 +525,21 @@ post \n\ \n\ "; +const std::string OptionsHandler::s_sygusActiveGenHelp = + "\ +Modes for actively-generated sygus enumerators, supported by --sygus-active-gen:\n\ +\n\ +none \n\ ++ Do not use actively-generated sygus enumerators.\n\ +\n\ +basic \n\ ++ Use basic type enumerator as sygus enumerator.\n\ +\n\ +var-agnostic \n\ ++ Use sygus solver to enumerate terms that are agnostic to variables. \n\ +\n\ +"; + const std::string OptionsHandler::s_macrosQuantHelp = "\ Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ \n\ @@ -952,6 +967,34 @@ OptionsHandler::stringToSygusInvTemplMode(std::string option, } } +theory::quantifiers::SygusActiveGenMode +OptionsHandler::stringToSygusActiveGenMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_NONE; + } + else if (optarg == "basic") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_BASIC; + } + else if (optarg == "var-agnostic") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC; + } + else if (optarg == "help") + { + puts(s_sygusActiveGenHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + + optarg + "'. Try --sygus-inv-templ 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 1869dc6a0..0205b0b73 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -114,6 +114,8 @@ public: std::string option, std::string optarg); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( std::string option, std::string optarg); + theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode( + std::string option, std::string optarg); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode( std::string option, std::string optarg); theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode( @@ -245,6 +247,7 @@ public: static const std::string s_cegqiSingleInvRconsHelp; static const std::string s_cegisSampleHelp; static const std::string s_sygusInvTemplHelp; + static const std::string s_sygusActiveGenHelp; static const std::string s_termDbModeHelp; static const std::string s_theoryOfModeHelp; static const std::string s_triggerSelModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 1fd29340d..42ab7bc06 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -262,6 +262,16 @@ enum SygusInvTemplMode { SYGUS_INV_TEMPL_MODE_POST, }; +enum SygusActiveGenMode +{ + /** do not use actively-generated enumerators */ + SYGUS_ACTIVE_GEN_NONE, + /** use basic actively-generated enumerators */ + SYGUS_ACTIVE_GEN_BASIC, + /** use variable-agnostic enumerators */ + SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, +}; + enum MacrosQuantMode { /** infer all definitions */ MACROS_QUANT_MODE_ALL, diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index eb32beef5..cbc380f43 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1032,12 +1032,15 @@ header = "options/quantifiers_options.h" help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions" [[option]] - name = "sygusEnumVarAgnostic" + name = "sygusActiveGenMode" category = "regular" - long = "sygus-var-agnostic" - type = "bool" - default = "false" - help = "when possible, use variable-agnostic enumerators" + long = "sygus-active-gen=MODE" + type = "CVC4::theory::quantifiers::SygusActiveGenMode" + default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE" + handler = "stringToSygusActiveGenMode" + includes = ["options/quantifiers_modes.h"] + read_only = true + help = "mode for actively-generated sygus enumerators" [[option]] name = "sygusMinGrammar" diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 05f1a9960..2eeecbb0e 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -40,15 +40,16 @@ struct SygusAnyConstAttributeId typedef expr::Attribute SygusAnyConstAttribute; /** - * Attribute true for enumerators whose current model values have been excluded - * by sygus symmetry breaking. This is set by the datatypes sygus solver during - * LAST_CALL effort checks for each active sygus enumerator. + * Attribute true for enumerators whose current model values were registered by + * the datatypes sygus solver, and were not excluded by sygus symmetry breaking. + * This is set by the datatypes sygus solver during LAST_CALL effort checks for + * each active sygus enumerator. */ -struct SygusSymBreakExcAttributeId +struct SygusSymBreakOkAttributeId { }; -typedef expr::Attribute - SygusSymBreakExcAttribute; +typedef expr::Attribute + SygusSymBreakOkAttribute; namespace datatypes { diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 7d3947bf4..17ef4f968 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1619,8 +1619,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } } } - SygusSymBreakExcAttribute ssbea; - prog.setAttribute(ssbea, isExc); + SygusSymBreakOkAttribute ssbo; + prog.setAttribute(ssbo, !isExc); } } //register any measured terms that we haven't encountered yet (should only be invoked on first call to check diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index b698422a7..d4735b3d8 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -661,8 +661,6 @@ Node CegSingleInv::reconstructToSyntax(Node s, } } -bool CegSingleInv::needsCheck() { return true; } - void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; } bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index cfd7cd23b..0de7b4290 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -275,8 +275,6 @@ class CegSingleInv bool rconsSygus = true ); // is single invocation bool isSingleInvocation() const { return !d_single_inv.isNull(); } - //needs check - bool needsCheck(); /** preregister conjecture */ void preregisterConjecture( Node q ); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index ad45fb9b7..2e7f0cc02 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -78,7 +78,8 @@ bool Cegis::processInitialize(Node n, // 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 isVarAgnostic = options::sygusEnumVarAgnostic() && csize == 1; + bool isActiveGen = + options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1; // initialize an enumerator for each candidate for (unsigned i = 0; i < csize; i++) { @@ -101,9 +102,9 @@ bool Cegis::processInitialize(Node n, d_tds->registerEnumerator(candidates[i], candidates[i], d_parent, - isVarAgnostic, + isActiveGen, do_repair_const, - isVarAgnostic); + isActiveGen); } return true; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 9367444ac..dbde79aae 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -86,7 +86,6 @@ void CegisUnif::getTermList(const std::vector& candidates, // Non-unif candidate are themselves the enumerators enums.insert( enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end()); - Valuation& valuation = d_qe->getValuation(); for (const Node& c : d_unif_candidates) { // Collect heads of candidates @@ -104,19 +103,6 @@ void CegisUnif::getTermList(const std::vector& candidates, std::vector uenums; // get the current unification enumerators d_u_enum_manager.getEnumeratorsForStrategyPt(e, uenums, index); - if (index == 1 && options::sygusUnifCondIndependent()) - { - Assert(uenums.size() == 1); - Node eu = uenums[0]; - Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); - // If active guard for this enumerator is not true, there are no more - // values for it, and hence we ignore it - Node gstatus = valuation.getSatValue(g); - if (gstatus.isNull() || !gstatus.getConst()) - { - continue; - } - } // get the model value of each enumerator enums.insert(enums.end(), uenums.begin(), uenums.end()); } @@ -264,7 +250,7 @@ void CegisUnif::setConditions( Assert(!itv->second.empty()); if (d_tds->isPassiveEnumerator(eu)) { - Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); + Node g = d_tds->getActiveGuardForEnumerator(eu); Node exp_exc = d_tds->getExplain() ->getExplanationForEquality(eu, itv->second[0]) .negate(); @@ -563,7 +549,6 @@ void CegisUnifEnumDecisionStrategy::initialize( { Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type); setUpEnumerator(ceu, ci.second, 1); - d_enum_to_active_guard[ceu] = d_tds->getActiveGuardForEnumerator(ceu); } } } @@ -592,12 +577,6 @@ void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt( } } -Node CegisUnifEnumDecisionStrategy::getActiveGuardForEnumerator(Node e) -{ - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - return d_enum_to_active_guard[e]; -} - void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index) @@ -628,19 +607,19 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, // register the enumerator si.d_enums[index].push_back(e); bool mkActiveGuard = false; - bool isVarAgnostic = false; + bool isActiveGen = false; // 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; - isVarAgnostic = options::sygusEnumVarAgnostic(); + isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; } 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, isVarAgnostic); + e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen); } void CegisUnifEnumDecisionStrategy::registerEvalPts( diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 02cf1cdf2..fef24e9bb 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -84,10 +84,14 @@ class SygusModule /** construct candidate * * This function takes as input: - * terms : the terms returned by a call to getTermList, + * terms : (a subset of) the terms returned by a call to getTermList, * term_values : the current model values of terms, * candidates : the list of candidates. * + * In particular, notice that terms do not include inactive enumerators, + * thus if inactive enumerators were added to getTermList, then the terms + * list passed to this call will be a (strict) subset of that list. + * * If this function returns true, it adds to candidate_values a list of terms * of the same length and type as candidates that are candidate solutions * to the synthesis conjecture in question. This candidate { v } will then be diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 8050e97f8..ac8b56ee4 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -179,7 +179,7 @@ bool SygusPbe::initialize(Node n, return false; } } - bool isVarAgnostic = options::sygusEnumVarAgnostic(); + bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; for (const Node& c : candidates) { Assert(d_examples.find(c) != d_examples.end()); @@ -203,9 +203,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, isVarAgnostic); - Node g = d_tds->getActiveGuardForEnumerator(e); - d_enum_to_active_guard[e] = g; + d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen); d_enum_to_candidate[e] = c; TNode te = e; // initialize static symmetry breaking lemmas for it @@ -397,27 +395,13 @@ Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) void SygusPbe::getTermList(const std::vector& candidates, std::vector& terms) { - Valuation& valuation = d_qe->getValuation(); for( unsigned i=0; i >::iterator it = d_candidate_to_enum.find(v); if (it != d_candidate_to_enum.end()) { - for (unsigned j = 0; j < it->second.size(); j++) - { - Node e = it->second[j]; - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; - // Get whether the active guard for this enumerator is true, - // if so, then there may exist more values for it, and hence we add it - // to terms. - Node gstatus = valuation.getSatValue(g); - if (!gstatus.isNull() && gstatus.getConst()) - { - terms.push_back(e); - } - } + terms.insert(terms.end(), it->second.begin(), it->second.end()); } } } @@ -491,8 +475,8 @@ bool SygusPbe::constructCandidates(const std::vector& enums, if (!enum_lems.empty()) { // the lemmas must be guarded by the active guard of the enumerator - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; + Node g = d_tds->getActiveGuardForEnumerator(e); + Assert(!g.isNull()); for (unsigned j = 0, size = enum_lems.size(); j < size; j++) { enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index b2ad5f63a..e21c9263f 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -230,8 +230,6 @@ class SygusPbe : public SygusModule std::map > d_candidate_to_enum; /** reverse map of above */ std::map d_enum_to_candidate; - /** map from enumerators to active guards */ - std::map d_enum_to_active_guard; /** for each candidate variable (function-to-synthesize), input of I/O * examples */ std::map > > d_examples; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 469775a46..7955d59a8 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -53,7 +53,8 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe) d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), - d_refine_count(0) + d_refine_count(0), + d_guarded_stream_exc(false) { if (options::sygusSymBreakPbe() || options::sygusUnifPbe()) { @@ -240,10 +241,6 @@ bool SynthConjecture::isSingleInvocation() const bool SynthConjecture::needsCheck() { - if (isSingleInvocation() && !d_ceg_si->needsCheck()) - { - return false; - } bool value; Assert(!d_feasible_guard.isNull()); // non or fully single invocation : look at guard only @@ -254,6 +251,11 @@ bool SynthConjecture::needsCheck() Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; return false; } + else + { + Trace("cegqi-engine-debug") << "Feasible guard " << d_feasible_guard + << " assigned true." << std::endl; + } } else { @@ -273,7 +275,7 @@ void SynthConjecture::doSingleInvCheck(std::vector& lems) } bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; } -void SynthConjecture::doCheck(std::vector& lems) +bool SynthConjecture::doCheck(std::vector& lems) { Assert(d_master != nullptr); @@ -288,24 +290,10 @@ void SynthConjecture::doCheck(std::vector& lems) // we have a new guard, print and continue the stream printAndContinueStream(); d_current_stream_guard = currGuard; - return; + return true; } } - bool checkSuccess = false; - do - { - Trace("cegqi-check-debug") << "doCheckNext..." << std::endl; - checkSuccess = doCheckNext(lems); - Trace("cegqi-check-debug") - << "...finished " << lems.empty() << " " << !needsRefinement() << " " - << !d_qe->getTheoryEngine()->needCheck() << " " << checkSuccess - << std::endl; - } while (lems.empty() && !needsRefinement() - && !d_qe->getTheoryEngine()->needCheck() && checkSuccess); -} -bool SynthConjecture::doCheckNext(std::vector& lems) -{ // get the list of terms that the master strategy is interested in std::vector terms; d_master->getTermList(d_candidates, terms); @@ -364,7 +352,7 @@ bool SynthConjecture::doCheckNext(std::vector& lems) { // we retain the values in d_ev_active_gen_waiting Trace("cegqi-engine") << "...partial model, fail." << std::endl; - return false; + return true; } // the waiting values are passed to the module below, clear d_ev_active_gen_waiting.clear(); @@ -407,7 +395,7 @@ bool SynthConjecture::doCheckNext(std::vector& lems) if (emptyModel) { Trace("cegqi-engine") << "...empty model, fail." << std::endl; - return false; + return true; } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( @@ -462,7 +450,7 @@ bool SynthConjecture::doCheckNext(std::vector& lems) { if (!constructed_cand) { - return true; + return false; } } @@ -502,7 +490,7 @@ bool SynthConjecture::doCheckNext(std::vector& lems) if (lem.isNull()) { // no lemma to check - return true; + return false; } lem = Rewriter::rewrite(lem); @@ -557,7 +545,7 @@ bool SynthConjecture::doCheckNext(std::vector& lems) Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; Assert(squery.isConst() && squery.getConst()); #endif - return true; + return false; } else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { @@ -577,7 +565,7 @@ bool SynthConjecture::doCheckNext(std::vector& lems) // if we were successful, we immediately print the current solution. // this saves us from introducing a verification lemma and a new guard. printAndContinueStream(); - return true; + return false; } lem = getStreamGuardedLemma(lem); lems.push_back(lem); @@ -662,30 +650,101 @@ void SynthConjecture::preregisterConjecture(Node q) bool SynthConjecture::getEnumeratedValues(std::vector& n, std::vector& v) { + std::vector ncheck = n; + n.clear(); bool ret = true; - for (unsigned i = 0; i < n.size(); i++) + for (unsigned i = 0, size = ncheck.size(); i < size; i++) { - Node nv = getEnumeratedValue(n[i]); + Node e = ncheck[i]; + // if it is not active, we return null + Node g = d_tds->getActiveGuardForEnumerator(e); + if (!g.isNull()) + { + Node gstatus = d_qe->getValuation().getSatValue(g); + if (gstatus.isNull() || !gstatus.getConst()) + { + Trace("cegqi-engine-debug") + << "Enumerator " << e << " is inactive." << std::endl; + continue; + } + } + Node nv = getEnumeratedValue(e); + n.push_back(e); v.push_back(nv); ret = ret && !nv.isNull(); } return ret; } +/** A basic sygus value generator + * + * This class is a "naive" term generator for sygus conjectures, which invokes + * the type enumerator to generate a stream of (all) sygus terms of a given + * type. + */ +class EnumValGeneratorBasic : public EnumValGenerator +{ + public: + EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_te(tn) {} + ~EnumValGeneratorBasic() {} + /** initialize (do nothing) */ + void initialize(Node e) override {} + /** initialize (do nothing) */ + void addValue(Node v) override {} + /** + * Get next returns the next (T-rewriter-unique) value based on the type + * enumerator. + */ + Node getNext() override + { + if (d_te.isFinished()) + { + return Node::null(); + } + Node next = *d_te; + ++d_te; + Node nextb = d_tds->sygusToBuiltin(next); + if (options::sygusSymBreakDynamic()) + { + nextb = d_tds->getExtRewriter()->extendedRewrite(nextb); + } + if (d_cache.find(nextb) == d_cache.end()) + { + d_cache.insert(nextb); + return next; + } + return getNext(); + } + + private: + /** pointer to term database sygus */ + TermDbSygus* d_tds; + /** the type enumerator */ + TypeEnumerator d_te; + /** cache of (enumerated) builtin values we have enumerated so far */ + std::unordered_set d_cache; +}; + Node SynthConjecture::getEnumeratedValue(Node e) { - if (e.getAttribute(SygusSymBreakExcAttribute())) + bool isEnum = d_tds->isEnumerator(e); + + if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute())) { - // if the current model value of e was excluded by symmetry breaking, then - // it does not have a proper model value that we should consider, thus we - // return null. + // if the current model value of e was not registered by the datatypes + // sygus solver, or was excluded by symmetry breaking, then it does not + // have a proper model value that we should consider, thus we return null. + Trace("cegqi-engine-debug") + << "Enumerator " << e << " does not have proper model value." + << std::endl; return Node::null(); } - if (!d_tds->isEnumerator(e) || d_tds->isPassiveEnumerator(e)) + if (!isEnum || d_tds->isPassiveEnumerator(e)) { return getModelValue(e); } + // management of actively generated enumerators goes here // initialize the enumerated value generator for e @@ -693,7 +752,14 @@ Node SynthConjecture::getEnumeratedValue(Node e) d_evg.find(e); if (iteg == d_evg.end()) { - d_evg[e].reset(new EnumStreamConcrete(d_tds)); + if (d_tds->isVariableAgnosticEnumerator(e)) + { + d_evg[e].reset(new EnumStreamConcrete(d_tds)); + } + else + { + d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); + } Trace("sygus-active-gen") << "Active-gen: initialize for " << e << std::endl; d_evg[e]->initialize(e); @@ -872,6 +938,11 @@ void SynthConjecture::printAndContinueStream() } if (!exp.empty()) { + if (!d_guarded_stream_exc) + { + d_guarded_stream_exc = true; + exp.push_back(d_feasible_guard); + } Node exc_lem = exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(kind::AND, exp); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index d5ace4dfe..ef1b4459f 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -83,9 +83,19 @@ class SynthConjecture */ void doSingleInvCheck(std::vector& lems); /** do syntax-guided enumerative check + * * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. + * + * The method returns true if this conjecture is finished trying solutions + * for the given call to SynthEngine::check. + * + * Notice that we make multiple calls to doCheck on one call to + * SynthEngine::check. For example, if we are using an actively-generated + * enumerator, one enumerated (abstract) term may correspond to multiple + * concrete terms t1, ..., tn to check, where we make up to n calls to doCheck + * when each of t1, ..., tn fails to satisfy the current refinement lemmas. */ - void doCheck(std::vector& lems); + bool doCheck(std::vector& lems); /** do refinement * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. */ @@ -94,7 +104,7 @@ class SynthConjecture /** * Prints the synthesis solution to output stream out. This invokes solution * reconstruction if the conjecture is single invocation. Otherwise, it - * returns the enumer + * returns the solution found by sygus enumeration. */ void printSynthSolution(std::ostream& out); /** get synth solutions @@ -182,6 +192,9 @@ class SynthConjecture /** * Get model values for terms n, store in vector v. This method returns true * if and only if all values added to v are non-null. + * + * It removes terms from n that correspond to "inactive" enumerators, that + * is, enumerators whose values have been exhausted. */ bool getEnumeratedValues(std::vector& n, std::vector& v); /** @@ -282,18 +295,6 @@ class SynthConjecture d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]); } } - /** - * This performs the next check of the syntax-guided enumerative check - * (see doCheck above). The method returns true if a new solution was - * considered. - * - * Notice that one call to doCheck may correspond to multiple calls to - * doCheckNext. For example, if we are using an actively-generated enumerator, - * one enumerated (abstract) term may correspond to multiple concrete - * terms t1, ..., tn to check, where we make up to n calls to doCheckNext when - * each of t1, ..., tn fail to satisfy the current refinement lemmas. - */ - bool doCheckNext(std::vector& lems); /** get synth solutions internal * * This function constructs the body of solutions for all @@ -343,9 +344,15 @@ class SynthConjecture /** * Prints the current synthesis solution to the output stream indicated by * the Options object, send a lemma blocking the current solution to the - * output channel. + * output channel, which we refer to as a "stream exclusion lemma". */ void printAndContinueStream(); + /** + * Whether we have guarded a stream exclusion lemma when using sygusStream. + * This is an optimization that allows us to guard only the first stream + * exclusion lemma. + */ + bool d_guarded_stream_exc; //-------------------------------- end sygus stream /** expression miner managers for each function-to-synthesize * diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 7ff16d82b..ba227bc8f 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -80,6 +80,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) << std::endl; Trace("cegqi-engine-debug") << std::endl; Valuation& valuation = d_quantEngine->getValuation(); + std::vector activeCheckConj; for (unsigned i = 0, size = d_conjs.size(); i < size; i++) { SynthConjecture* sc = d_conjs[i].get(); @@ -98,9 +99,30 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) << "Current conjecture status : active : " << active << std::endl; if (active && sc->needsCheck()) { - checkConjecture(sc); + activeCheckConj.push_back(sc); } } + std::vector acnext; + do + { + Trace("cegqi-engine-debug") << "Checking " << activeCheckConj.size() + << " active conjectures..." << std::endl; + for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++) + { + SynthConjecture* sc = activeCheckConj[i]; + if (!checkConjecture(sc)) + { + if (!sc->needsRefinement()) + { + acnext.push_back(sc); + } + } + } + activeCheckConj.clear(); + activeCheckConj = acnext; + acnext.clear(); + } while (!activeCheckConj.empty() + && !d_quantEngine->getTheoryEngine()->needCheck()); Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; } @@ -258,7 +280,7 @@ void SynthEngine::registerQuantifier(Node q) } } -void SynthEngine::checkConjecture(SynthConjecture* conj) +bool SynthEngine::checkConjecture(SynthConjecture* conj) { Node q = conj->getEmbeddedConjecture(); Node aq = conj->getConjecture(); @@ -296,12 +318,12 @@ void SynthEngine::checkConjecture(SynthConjecture* conj) << " ...FAILED to add cbqi instantiation for single invocation!" << std::endl; } - return; + return true; } Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; std::vector cclems; - conj->doCheck(cclems); + bool ret = conj->doCheck(cclems); bool addedLemma = false; for (const Node& lem : cclems) { @@ -322,16 +344,17 @@ void SynthEngine::checkConjecture(SynthConjecture* conj) if (addedLemma) { Trace("cegqi-engine") << " ...check for counterexample." << std::endl; + return true; } else { if (conj->needsRefinement()) { // immediately go to refine candidate - checkConjecture(conj); - return; + return checkConjecture(conj); } } + return ret; } else { @@ -361,6 +384,7 @@ void SynthEngine::checkConjecture(SynthConjecture* conj) Trace("cegqi-engine") << " ...refine candidate." << std::endl; } } + return true; } void SynthEngine::printSynthSolution(std::ostream& out) diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 2a8994c25..8f0eea58f 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -50,8 +50,12 @@ class SynthEngine : public QuantifiersModule * this is the quantifier elimination step option::sygusQePreproc(). */ void assignConjecture(Node q); - /** check conjecture */ - void checkConjecture(SynthConjecture* conj); + /** check conjecture + * + * This method returns true if the conjecture is finished processing solutions + * for this call to SynthEngine::check(). + */ + bool checkConjecture(SynthConjecture* conj); public: SynthEngine(QuantifiersEngine* qe, context::Context* c); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 1a8c81bcc..d5b7bc51c 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -371,7 +371,9 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { Trace("sygus-db") << ", kind = " << sk; d_kinds[tn][sk] = i; d_arg_kind[tn][i] = sk; - }else if( sop.isConst() ){ + } + else if (sop.isConst() && dt[i].getNumArgs() == 0) + { Trace("sygus-db") << ", constant"; d_consts[tn][n] = i; d_arg_const[tn][i] = n; @@ -466,7 +468,7 @@ void TermDbSygus::registerEnumerator(Node e, SynthConjecture* conj, bool mkActiveGuard, bool useSymbolicCons, - bool isVarAgnostic) + bool isActiveGen) { if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) { @@ -564,6 +566,10 @@ void TermDbSygus::registerEnumerator(Node e, } Trace("sygus-db") << " ...finished" << std::endl; + d_enum_active_gen[e] = isActiveGen; + bool isVarAgnostic = + isActiveGen + && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC; d_enum_var_agnostic[e] = isVarAgnostic; if (isVarAgnostic) { @@ -667,11 +673,11 @@ bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const bool TermDbSygus::isPassiveEnumerator(Node e) const { - if (isVariableAgnosticEnumerator(e)) + std::map::const_iterator itus = d_enum_active_gen.find(e); + if (itus != d_enum_active_gen.end()) { - return false; + return !itus->second; } - // other criteria go here return true; } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 785e8731c..56ed68e76 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -69,8 +69,10 @@ class TermDbSygus { * (see d_enum_to_active_guard), * useSymbolicCons : whether we want model values for e to include symbolic * constructors like the "any constant" variable. - * isVarAgnostic : if this flag is true, the enumerator will only generate - * values whose variables are in canonical order (for example, only x1-x2 + * isActiveGen : if this flag is true, the enumerator will be + * actively-generated based on the mode specified by --sygus-active-gen. + * 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). * @@ -83,7 +85,7 @@ class TermDbSygus { SynthConjecture* conj, bool mkActiveGuard = false, bool useSymbolicCons = false, - bool isVarAgnostic = false); + bool isActiveGen = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ @@ -298,6 +300,8 @@ class TermDbSygus { std::map d_sb_lemma_to_type; /** mapping from symmetry breaking lemmas to size */ std::map d_sb_lemma_to_size; + /** enumerators to whether they are actively-generated */ + std::map d_enum_active_gen; /** enumerators to whether they are variable agnostic */ std::map d_enum_var_agnostic; //------------------------------end enumerators diff --git a/test/regress/regress1/sygus/trivial-stream.sy b/test/regress/regress1/sygus/trivial-stream.sy index b8b08d03b..33abb6ee8 100644 --- a/test/regress/regress1/sygus/trivial-stream.sy +++ b/test/regress/regress1/sygus/trivial-stream.sy @@ -3,7 +3,7 @@ ; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded.") ; EXIT: 1 -; COMMAND-LINE: --sygus-stream --sygus-abort-size=0 +; COMMAND-LINE: --sygus-stream --sygus-abort-size=0 --sygus-active-gen=var-agnostic (set-logic LIA)