From aecb70fd1ab7c8928d8a440278a8cf2a9a828984 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 3 Oct 2018 15:28:34 -0500 Subject: [PATCH] Add actively generated sygus enumerators (#2552) --- src/options/quantifiers_options.toml | 8 + src/theory/datatypes/datatypes_sygus.cpp | 189 ++++++++----- src/theory/datatypes/datatypes_sygus.h | 26 +- src/theory/datatypes/theory_datatypes.cpp | 2 + src/theory/quantifiers/sygus/cegis.cpp | 43 ++- src/theory/quantifiers/sygus/cegis.h | 31 ++- src/theory/quantifiers/sygus/cegis_unif.cpp | 12 +- .../sygus/enum_stream_substitution.cpp | 3 + .../sygus/enum_stream_substitution.h | 20 ++ src/theory/quantifiers/sygus/sygus_pbe.cpp | 9 +- .../quantifiers/sygus/synth_conjecture.cpp | 256 +++++++++++++----- .../quantifiers/sygus/synth_conjecture.h | 81 +++++- .../quantifiers/sygus/term_database_sygus.cpp | 19 ++ 13 files changed, 538 insertions(+), 161 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 7b58f955a..e8d8fbe3d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1031,6 +1031,14 @@ header = "options/quantifiers_options.h" type = "unsigned long" help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions" +[[option]] + name = "sygusEnumVarAgnostic" + category = "regular" + long = "sygus-var-agnostic" + type = "bool" + default = "false" + help = "when possible, use variable-agnostic enumerators" + [[option]] name = "sygusMinGrammar" category = "regular" diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 227bd6170..0db05d93c 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -556,22 +556,40 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, << "Simple symmetry breaking for " << dt.getName() << ", constructor " << dt[tindex].getName() << ", at depth " << depth << std::endl; - // if we are the "any constant" constructor, we do no symmetry breaking - // only do simple symmetry breaking up to depth 2 + // get the sygus operator Node sop = Node::fromExpr(dt[tindex].getSygusOp()); - if (sop.getAttribute(SygusAnyConstAttribute()) || depth > 2) - { - d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = Node::null(); - return Node::null(); - } + // get the kind of the constructor operator + Kind nk = d_tds->getConsNumKind(tn, tindex); + // is this the any-constant constructor? + bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute()); + // conjunctive conclusion of lemma std::vector sbp_conj; + // the number of (sygus) arguments + // Notice if this is an any-constant constructor, its child is not a + // sygus child, hence we set to 0 here. + unsigned dt_index_nargs = isAnyConstant ? 0 : dt[tindex].getNumArgs(); + + // builtin type + TypeNode tnb = TypeNode::fromType(dt.getSygusType()); + // get children + std::vector children; + for (unsigned j = 0; j < dt_index_nargs; j++) + { + Node sel = nm->mkNode( + APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)), + n); + Assert(sel.getType().isDatatype()); + children.push_back(sel); + } + if (depth == 0) { Trace("sygus-sb-simple-debug") << " Size..." << std::endl; // fairness - if (options::sygusFair() == SYGUS_FAIR_DT_SIZE) + if (options::sygusFair() == SYGUS_FAIR_DT_SIZE && !isAnyConstant) { Node szl = nm->mkNode(DT_SIZE, n); Node szr = @@ -579,48 +597,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, szr = Rewriter::rewrite(szr); sbp_conj.push_back(szl.eqNode(szr)); } - } - - // symmetry breaking - Kind nk = d_tds->getConsNumKind(tn, tindex); - if (options::sygusSymBreak()) - { - // the number of (sygus) arguments - unsigned dt_index_nargs = dt[tindex].getNumArgs(); - - // builtin type - TypeNode tnb = TypeNode::fromType(dt.getSygusType()); - // get children - std::vector children; - for (unsigned j = 0; j < dt_index_nargs; j++) - { - Node sel = nm->mkNode( - APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)), - n); - Assert(sel.getType().isDatatype()); - children.push_back(sel); - } - - // direct solving for children - // for instance, we may want to insist that the LHS of MINUS is 0 - Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl; - std::map children_solved; - for (unsigned j = 0; j < dt_index_nargs; j++) - { - int i = d_ssb.solveForArgument(tn, tindex, j); - if (i >= 0) - { - children_solved[j] = i; - TypeNode ctn = children[j].getType(); - const Datatype& cdt = - static_cast(ctn.toType()).getDatatype(); - Assert(i < static_cast(cdt.getNumConstructors())); - sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt)); - } - } - - if (isVarAgnostic && depth == 0) + if (isVarAgnostic) { // Enforce symmetry breaking lemma template for each x_i: // template z. @@ -695,6 +672,36 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, sbp_conj.push_back(finish.eqNode(prev)); } } + } + + // if we are the "any constant" constructor, we do no symmetry breaking + // only do simple symmetry breaking up to depth 2 + bool doSymBreak = options::sygusSymBreak(); + if (isAnyConstant || depth > 2) + { + doSymBreak = false; + } + // symmetry breaking + if (doSymBreak) + { + // direct solving for children + // for instance, we may want to insist that the LHS of MINUS is 0 + Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl; + std::map children_solved; + for (unsigned j = 0; j < dt_index_nargs; j++) + { + int i = d_ssb.solveForArgument(tn, tindex, j); + if (i >= 0) + { + children_solved[j] = i; + TypeNode ctn = children[j].getType(); + const Datatype& cdt = + static_cast(ctn.toType()).getDatatype(); + Assert(i < static_cast(cdt.getNumConstructors())); + sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt)); + } + } + // depth 1 symmetry breaking : talks about direct children if (depth == 1) { @@ -947,8 +954,13 @@ void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool } } -Node SygusSymBreakNew::registerSearchValue( - Node a, Node n, Node nv, unsigned d, std::vector& lemmas) +Node SygusSymBreakNew::registerSearchValue(Node a, + Node n, + Node nv, + unsigned d, + std::vector& lemmas, + bool isVarAgnostic, + bool doSym) { Assert(n.getType().isComparableTo(nv.getType())); TypeNode tn = n.getType(); @@ -979,7 +991,13 @@ Node SygusSymBreakNew::registerSearchValue( APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)), n); - Node nvc = registerSearchValue(a, sel, nv[i], d + 1, lemmas); + Node nvc = registerSearchValue(a, + sel, + nv[i], + d + 1, + lemmas, + isVarAgnostic, + doSym && (!isVarAgnostic || i == 0)); if (nvc.isNull()) { return Node::null(); @@ -993,6 +1011,10 @@ Node SygusSymBreakNew::registerSearchValue( nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children); } } + if (!doSym) + { + return nv; + } Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl; std::map var_count; Node cnv = d_tds->canonizeBuiltin(nv, var_count); @@ -1127,11 +1149,22 @@ Node SygusSymBreakNew::registerSearchValue( Node bad_val_o = d_cache[a].d_search_val[tn][bad_val_bvr]; Assert( d_cache[a].d_search_val_sz[tn].find( bad_val_bvr )!=d_cache[a].d_search_val_sz[tn].end() ); unsigned prev_sz = d_cache[a].d_search_val_sz[tn][bad_val_bvr]; - if( prev_sz>sz ){ + bool doFlip = (prev_sz > sz); + if (doFlip) + { //swap : the excluded value is the previous d_cache[a].d_search_val_sz[tn][bad_val_bvr] = sz; bad_val = d_cache[a].d_search_val[tn][bad_val_bvr]; bad_val_o = nv; + if (Trace.isOn("sygus-sb-exc")) + { + Trace("sygus-sb-exc") << "Flip : exclude "; + quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val); + Trace("sygus-sb-exc") << " instead of "; + quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val_o); + Trace("sygus-sb-exc") << ", since its size is " << sz << " < " + << prev_sz << std::endl; + } sz = prev_sz; } if( Trace.isOn("sygus-sb-exc") ){ @@ -1154,7 +1187,14 @@ Node SygusSymBreakNew::registerSearchValue( a, bad_val, eset, bad_val_o, var_count, lemmas); // other generalization criteria go here - return Node::null(); + + // If the exclusion was flipped, we are excluding a previous value + // instead of the current one. Hence, the current value is a legal + // value that we will consider. + if (!doFlip) + { + return Node::null(); + } } } } @@ -1538,8 +1578,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { Trace("dt-sygus") << ss.str() << std::endl; } // first check that the value progv for prog is what we expected + bool isExc = true; if (checkValue(prog, progv, 0, lemmas)) { + isExc = false; //debugging : ensure fairness was properly handled if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog ); @@ -1552,20 +1594,23 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { Node szlem = NodeManager::currentNM()->mkNode( kind::OR, prog.eqNode( progv ).negate(), prog_sz.eqNode( progv_sz ) ); Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem << std::endl; - lemmas.push_back( szlem ); - return; + lemmas.push_back(szlem); + isExc = true; } } - - // register the search value ( prog -> progv ), this may invoke symmetry breaking - if( options::sygusSymBreakDynamic() ){ + + // register the search value ( prog -> progv ), this may invoke symmetry + // breaking + if (!isExc && options::sygusSymBreakDynamic()) + { + bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog); // check that it is unique up to theory-specific rewriting and // conjecture-specific symmetry breaking. - Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas); - SygusSymBreakExcAttribute ssbea; - prog.setAttribute(ssbea, rsv.isNull()); + Node rsv = registerSearchValue( + prog, prog, progv, 0, lemmas, isVarAgnostic, true); if (rsv.isNull()) { + isExc = true; Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl; } else @@ -1574,6 +1619,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } } } + SygusSymBreakExcAttribute ssbea; + prog.setAttribute(ssbea, isExc); } } //register any measured terms that we haven't encountered yet (should only be invoked on first call to check @@ -1584,9 +1631,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { registerSizeTerm( mts[i], lemmas ); } Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl; - - if( Trace.isOn("cegqi-engine") ){ - if (lemmas.empty() && !d_szinfo.empty()) + + if (Trace.isOn("cegqi-engine") && !d_szinfo.empty()) + { + if (lemmas.empty()) { Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : "; for (std::pair>& @@ -1597,6 +1645,15 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } Trace("cegqi-engine") << std::endl; } + else + { + Trace("cegqi-engine") + << "*** Sygus : produced symmetry breaking lemmas" << std::endl; + for (const Node& lem : lemmas) + { + Trace("cegqi-engine-debug") << " " << lem << std::endl; + } + } } } diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index a38e7c5b8..6cf1d7d37 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -370,9 +370,29 @@ private: * not "some constant". Thus, we should consider the subterm * C_{any_constant}( 5 ) above to be an unconstrained variable (as represented * by a selector chain), instead of the concrete value 5. - */ - Node registerSearchValue( - Node a, Node n, Node nv, unsigned d, std::vector& lemmas); + * + * The flag isVarAgnostic is whether "a" is a variable agnostic enumerator. If + * this is the case, we restrict symmetry breaking to subterms of n on its + * leftmost subchain. For example, consider the grammar: + * A -> B=B + * B -> B+B | x | y | 0 + * Say we are registering the search value x = y+x. Notice that this value is + * ordered. If a were a variable-agnostic enumerator of type A in this + * case, we would only register x = y+x and x, and not y+x or y, since the + * latter two terms are not leftmost subterms in this value. If we did on the + * other hand register y+x, we would be prevented from solutions like x+y = 0 + * later, since x+y is equivalent to (the already registered value) y+x. + * + * If doSym is false, we are not performing symmetry breaking on n. This flag + * is set to false on branches of n that are not leftmost. + */ + Node registerSearchValue(Node a, + Node n, + Node nv, + unsigned d, + std::vector& lemmas, + bool isVarAgnostic, + bool doSym); /** Register symmetry breaking lemma * * This function adds the symmetry breaking lemma template lem for terms of diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 10328c653..6aed1514c 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -453,6 +453,8 @@ bool TheoryDatatypes::doSendLemma( Node lem ) { d_addedLemma = true; return true; }else{ + Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : duplicate : " + << lem << std::endl; return false; } } diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index db9af10b4..9706e3732 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -68,8 +68,19 @@ bool Cegis::processInitialize(Node n, std::vector& lemmas) { 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 isVarAgnostic = options::sygusEnumVarAgnostic() && csize == 1; // initialize an enumerator for each candidate - for (unsigned i = 0; i < candidates.size(); i++) + for (unsigned i = 0; i < csize; i++) { Trace("cegis") << "...register enumerator " << candidates[i]; bool do_repair_const = false; @@ -86,8 +97,13 @@ bool Cegis::processInitialize(Node n, } } Trace("cegis") << std::endl; - d_tds->registerEnumerator( - candidates[i], candidates[i], d_parent, false, do_repair_const); + // variable agnostic enumerators require an active guard + d_tds->registerEnumerator(candidates[i], + candidates[i], + d_parent, + isVarAgnostic, + do_repair_const, + isVarAgnostic); } return true; } @@ -99,7 +115,8 @@ void Cegis::getTermList(const std::vector& candidates, } bool Cegis::addEvalLemmas(const std::vector& candidates, - const std::vector& candidate_values) + const std::vector& candidate_values, + std::vector& lems) { // First, decide if this call will apply "conjecture-specific refinement". // In other words, in some settings, the following method will identify and @@ -144,13 +161,14 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, } if (!cre_lems.empty()) { - for (const Node& lem : cre_lems) + lems.insert(lems.end(), cre_lems.begin(), cre_lems.end()); + addedEvalLemmas = true; + if (Trace.isOn("cegqi-lemma")) { - if (d_qe->addLemma(lem)) + for (const Node& lem : cre_lems) { Trace("cegqi-lemma") << "Cegqi::Lemma : ref evaluation : " << lem << std::endl; - addedEvalLemmas = true; } } /* we could, but do not return here. experimentally, it is better to @@ -178,12 +196,9 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, { Node lem = nm->mkNode( OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i])); - if (d_qe->addLemma(lem)) - { - Trace("cegqi-lemma") - << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl; - addedEvalLemmas = true; - } + lems.push_back(lem); + Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem + << std::endl; } } return addedEvalLemmas; @@ -258,7 +273,7 @@ bool Cegis::constructCandidates(const std::vector& enums, } // evaluate on refinement lemmas - bool addedEvalLemmas = addEvalLemmas(enums, enum_values); + bool addedEvalLemmas = addEvalLemmas(enums, enum_values, lems); // try to construct candidates if (!processConstructCandidates(enums, diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 7387bd468..849a39639 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -137,17 +137,38 @@ class Cegis : public SygusModule /** evaluates candidate values on current refinement lemmas * - * Returns true if refinement lemmas are added after evaluation, false - * otherwise. + * This method performs techniques that ensure that + * { candidates -> candidate_values } is a candidate solution that should + * be checked by the solution verifier of the CEGIS loop. This method + * invokes two sub-methods which may reject the current solution. + * The first is "refinement evaluation", described above the method + * getRefinementEvalLemmas below. The second is "evaluation unfolding", + * which eagerly unfolds applications of evaluation functions (see + * sygus_eval_unfold.h for details). * - * Also eagerly unfolds evaluation functions in a heuristic manner, which is - * useful e.g. for boolean connectives + * If this method returns true, then { candidates -> candidate_values } + * is not ready to be tried as a candidate solution. In this case, it may add + * lemmas to lems. + * + * Notice that this method may return true without adding any lemmas to + * lems, in the case that terms from candidates are "actively-generated + * enumerators", since the model values of such terms are managed + * explicitly within getEnumeratedValue. In this case, the owner of the + * actively-generated enumerators (e.g. SynthConjecture) is responsible for + * blocking the current value of candidates. */ bool addEvalLemmas(const std::vector& candidates, - const std::vector& candidate_values); + const std::vector& candidate_values, + std::vector& lems); //-----------------------------------end refinement lemmas /** Get refinement evaluation lemmas + * + * This method performs "refinement evaluation", that is, it tests + * whether the current solution, given by { candidates -> candidate_values }, + * satisfies all current refinement lemmas. If it does not, it may add + * blocking lemmas L to lems which exclude (a generalization of) the current + * solution. * * Given a candidate solution ms for candidates vs, this function adds lemmas * to lems based on evaluating the conjecture, instantiated for ms, on lemmas diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index d71139eef..fc26d72f6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -600,10 +600,20 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, } // register the enumerator si.d_enums[index].push_back(e); + bool mkActiveGuard = false; + bool isVarAgnostic = 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(); + } Trace("cegis-unif-enum") << "* Registering new enumerator " << e << " to strategy point " << si.d_pt << "\n"; d_tds->registerEnumerator( - e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1); + e, si.d_pt, d_parent, mkActiveGuard, false, isVarAgnostic); } void CegisUnifEnumDecisionStrategy::registerEvalPts( diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index b307876ed..bf939e0fe 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -597,6 +597,9 @@ bool EnumStreamSubstitution::CombinationState::getNextCombination() return new_comb; } +void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); } +void EnumStreamConcrete::addValue(Node v) { d_ess.resetValue(v); } +Node EnumStreamConcrete::getNext() { return d_ess.getNext(); } } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 5d3daa538..38fa0627b 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -274,6 +274,26 @@ class EnumStreamSubstitution unsigned d_curr_ind; }; +/** + * An enumerated value generator based on the above class. This is + * SynthConjecture's interface to using the above utility. + */ +class EnumStreamConcrete : public EnumValGenerator +{ + public: + EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {} + /** initialize this class with enumerator e */ + void initialize(Node e) override; + /** get that value v was enumerated */ + void addValue(Node v) override; + /** get the next value enumerated by this class */ + Node getNext() override; + + private: + /** stream substitution utility */ + EnumStreamSubstitution d_ess; +}; + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index b7e6e0c65..889f4d9c9 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -179,6 +179,7 @@ bool SygusPbe::initialize(Node n, return false; } } + bool isVarAgnostic = options::sygusEnumVarAgnostic(); for (const Node& c : candidates) { Assert(d_examples.find(c) != d_examples.end()); @@ -202,7 +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); + d_tds->registerEnumerator(e, c, d_parent, true, false, isVarAgnostic); Node g = d_tds->getActiveGuardForEnumerator(e); d_enum_to_active_guard[e] = g; d_enum_to_candidate[e] = c; @@ -357,6 +358,12 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Assert(isPbe()); Assert(!e.isNull()); + if (!d_tds->isPassiveEnumerator(e)) + { + // we cannot apply conjecture-specific symmetry breaking on enumerators that + // are not passive + return Node::null(); + } e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map::iterator itx = d_examples_invalid.find(e); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 99f1131fe..4dfe33b58 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -27,6 +27,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/enum_stream_substitution.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -290,7 +291,21 @@ void SynthConjecture::doCheck(std::vector& lems) return; } } + 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); @@ -318,16 +333,16 @@ void SynthConjecture::doCheck(std::vector& lems) Assert(d_repair_index < d_cinfo[cprog].d_inst.size()); fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]); } - if (Trace.isOn("cegqi-check")) + if (Trace.isOn("cegqi-engine")) { - Trace("cegqi-check") << "CegConjuncture : repair previous solution "; + Trace("cegqi-engine") << "CegConjuncture : repair previous solution "; for (const Node& fc : fail_cvs) { std::stringstream ss; Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc); - Trace("cegqi-check") << ss.str() << " "; + Trace("cegqi-engine") << ss.str() << " "; } - Trace("cegqi-check") << std::endl; + Trace("cegqi-engine") << std::endl; } d_repair_index++; if (d_sygus_rconst->repairSolution( @@ -338,19 +353,62 @@ void SynthConjecture::doCheck(std::vector& lems) } } - // get the model value of the relevant terms from the master module - std::vector enum_values; - bool fullModel = getEnumeratedValues(terms, enum_values); - - // if the master requires a full model and the model is partial, we fail - if (!d_master->allowPartialModel() && !fullModel) - { - Trace("cegqi-check") << "...partial model, fail." << std::endl; - return; - } - if (!constructed_cand) { + // get the model value of the relevant terms from the master module + std::vector enum_values; + bool fullModel = getEnumeratedValues(terms, enum_values); + + // if the master requires a full model and the model is partial, we fail + if (!d_master->allowPartialModel() && !fullModel) + { + // we retain the values in d_ev_active_gen_waiting + Trace("cegqi-engine") << "...partial model, fail." << std::endl; + return false; + } + // the waiting values are passed to the module below, clear + d_ev_active_gen_waiting.clear(); + + // debug print + Assert(terms.size() == enum_values.size()); + bool emptyModel = true; + Trace("cegqi-engine") << " * Value is : "; + for (unsigned i = 0, size = terms.size(); i < size; i++) + { + Node nv = enum_values[i]; + if (!nv.isNull()) + { + emptyModel = false; + } + if (Trace.isOn("cegqi-engine")) + { + Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv; + TypeNode tn = onv.getType(); + std::stringstream ss; + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv); + Trace("cegqi-engine") << terms[i] << " -> "; + if (nv.isNull()) + { + Trace("cegqi-engine") << "[EXC: " << ss.str() << "] "; + } + else + { + Trace("cegqi-engine") << ss.str() << " "; + if (Trace.isOn("cegqi-engine-rr")) + { + Node bv = d_tds->sygusToBuiltin(nv, tn); + bv = Rewriter::rewrite(bv); + Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + } + } + } + } + Trace("cegqi-engine") << std::endl; + if (emptyModel) + { + Trace("cegqi-engine") << "...empty model, fail." << std::endl; + return false; + } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( terms, enum_values, d_candidates, candidate_values, lems); @@ -396,7 +454,7 @@ void SynthConjecture::doCheck(std::vector& lems) lem = getStreamGuardedLemma(lem); lems.push_back(lem); recordInstantiation(candidate_values); - return; + return true; } Assert(!d_set_ce_sk_vars); } @@ -404,7 +462,7 @@ void SynthConjecture::doCheck(std::vector& lems) { if (!constructed_cand) { - return; + return true; } } @@ -444,7 +502,7 @@ void SynthConjecture::doCheck(std::vector& lems) if (lem.isNull()) { // no lemma to check - return; + return true; } lem = Rewriter::rewrite(lem); @@ -499,7 +557,7 @@ void SynthConjecture::doCheck(std::vector& lems) Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; Assert(squery.isConst() && squery.getConst()); #endif - return; + return true; } else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { @@ -519,10 +577,11 @@ void SynthConjecture::doCheck(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; + return true; } lem = getStreamGuardedLemma(lem); lems.push_back(lem); + return true; } void SynthConjecture::doRefine(std::vector& lems) @@ -604,36 +663,12 @@ bool SynthConjecture::getEnumeratedValues(std::vector& n, std::vector& v) { bool ret = true; - Trace("cegqi-engine") << " * Value is : "; for (unsigned i = 0; i < n.size(); i++) { Node nv = getEnumeratedValue(n[i]); v.push_back(nv); ret = ret && !nv.isNull(); - if (Trace.isOn("cegqi-engine")) - { - Node onv = nv.isNull() ? d_qe->getModel()->getValue(n[i]) : nv; - TypeNode tn = onv.getType(); - std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv); - Trace("cegqi-engine") << n[i] << " -> "; - if (nv.isNull()) - { - Trace("cegqi-engine") << "[EXC: " << ss.str() << "] "; - } - else - { - Trace("cegqi-engine") << ss.str() << " "; - if (Trace.isOn("cegqi-engine-rr")) - { - Node bv = d_tds->sygusToBuiltin(nv, tn); - bv = Rewriter::rewrite(bv); - Trace("cegqi-engine-rr") << " -> " << bv << std::endl; - } - } - } } - Trace("cegqi-engine") << std::endl; return ret; } @@ -646,13 +681,105 @@ Node SynthConjecture::getEnumeratedValue(Node e) // return null. return Node::null(); } - if (d_tds->isPassiveEnumerator(e)) + + if (!d_tds->isEnumerator(e) || d_tds->isPassiveEnumerator(e)) { return getModelValue(e); } - Assert(false); // management of actively generated enumerators goes here - return getModelValue(e); + + // initialize the enumerated value generator for e + std::map >::iterator iteg = + d_evg.find(e); + if (iteg == d_evg.end()) + { + d_evg[e].reset(new EnumStreamConcrete(d_tds)); + Trace("sygus-active-gen") + << "Active-gen: initialize for " << e << std::endl; + d_evg[e]->initialize(e); + d_ev_curr_active_gen[e] = Node::null(); + iteg = d_evg.find(e); + Trace("sygus-active-gen-debug") << "...finish" << std::endl; + } + // if we have a waiting value, return it + std::map::iterator itw = d_ev_active_gen_waiting.find(e); + if (itw != d_ev_active_gen_waiting.end()) + { + Trace("sygus-active-gen-debug") + << "Active-gen: return waiting " << itw->second << std::endl; + return itw->second; + } + // Check if there is an (abstract) value absE we were actively generating + // values based on. + Node absE = d_ev_curr_active_gen[e]; + if (absE.isNull()) + { + // None currently exist. The next abstract value is the model value for e. + absE = getModelValue(e); + if (Trace.isOn("sygus-active-gen")) + { + Trace("sygus-active-gen") << "Active-gen: new abstract value : "; + TermDbSygus::toStreamSygus("sygus-active-gen", e); + Trace("sygus-active-gen") << " -> "; + TermDbSygus::toStreamSygus("sygus-active-gen", absE); + Trace("sygus-active-gen") << std::endl; + } + d_ev_curr_active_gen[e] = absE; + iteg->second->addValue(absE); + } + Node v = iteg->second->getNext(); + if (v.isNull()) + { + // No more concrete values generated from absE. + NodeManager* nm = NodeManager::currentNM(); + d_ev_curr_active_gen[e] = Node::null(); + // We must block e = absE. + std::vector exp; + d_tds->getExplain()->getExplanationForEquality(e, absE, exp); + for (unsigned i = 0, size = exp.size(); i < size; i++) + { + exp[i] = exp[i].negate(); + } + Node g = d_tds->getActiveGuardForEnumerator(e); + if (!g.isNull()) + { + if (d_ev_active_gen_first_val.find(e) == d_ev_active_gen_first_val.end()) + { + exp.push_back(g.negate()); + d_ev_active_gen_first_val[e] = absE; + } + } + else + { + Assert(false); + } + Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp); + Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator " + "exclude current solution : " + << lem << std::endl; + if (Trace.isOn("sygus-active-gen-debug")) + { + Trace("sygus-active-gen-debug") << "Active-gen: block "; + TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE); + Trace("sygus-active-gen-debug") << std::endl; + } + d_qe->getOutputChannel().lemma(lem); + } + else + { + // We are waiting to send e -> v to the module that requested it. + d_ev_active_gen_waiting[e] = v; + if (Trace.isOn("sygus-active-gen")) + { + Trace("sygus-active-gen") << "Active-gen : " << e << " : "; + TermDbSygus::toStreamSygus("sygus-active-gen", absE); + Trace("sygus-active-gen") << " -> "; + TermDbSygus::toStreamSygus("sygus-active-gen", v); + Trace("sygus-active-gen") << std::endl; + } + } + + return v; } Node SynthConjecture::getModelValue(Node n) @@ -724,28 +851,35 @@ void SynthConjecture::printAndContinueStream() d_ce_sk_vars.clear(); d_ce_sk_var_mvs.clear(); // However, we need to exclude the current solution using an explicit - // blocking clause, so that we proceed to the next solution. + // blocking clause, so that we proceed to the next solution. We do this only + // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator). std::vector terms; d_master->getTermList(d_candidates, terms); std::vector exp; for (const Node& cprog : terms) { - Node sol = cprog; - if (!d_cinfo[cprog].d_inst.empty()) + Assert(d_tds->isEnumerator(cprog)); + if (d_tds->isPassiveEnumerator(cprog)) { - sol = d_cinfo[cprog].d_inst.back(); - // add to explanation of exclusion - d_tds->getExplain()->getExplanationForEquality(cprog, sol, exp); + Node sol = cprog; + if (!d_cinfo[cprog].d_inst.empty()) + { + sol = d_cinfo[cprog].d_inst.back(); + // add to explanation of exclusion + d_tds->getExplain()->getExplanationForEquality(cprog, sol, exp); + } } } - Assert(!exp.empty()); - Node exc_lem = exp.size() == 1 - ? exp[0] - : NodeManager::currentNM()->mkNode(kind::AND, exp); - exc_lem = exc_lem.negate(); - Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " - << exc_lem << std::endl; - d_qe->getOutputChannel().lemma(exc_lem); + if (!exp.empty()) + { + Node exc_lem = exp.size() == 1 + ? exp[0] + : NodeManager::currentNM()->mkNode(kind::AND, exp); + exc_lem = exc_lem.negate(); + Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " + << exc_lem << std::endl; + d_qe->getOutputChannel().lemma(exc_lem); + } } void SynthConjecture::printSynthSolution(std::ostream& out, diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 694e4a0cb..4c18205af 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -35,6 +35,24 @@ namespace CVC4 { namespace theory { namespace quantifiers { +/** + * A base class for generating values for actively-generated enumerators. + * At a high level, the job of this class is to accept a stream of "abstract + * values" a1, ..., an, ..., and generate a (possibly larger) stream of + * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, .... + */ +class EnumValGenerator +{ + public: + virtual ~EnumValGenerator() {} + /** initialize this class with enumerator e */ + virtual void initialize(Node e) = 0; + /** Inform this generator that abstract value v was enumerated. */ + virtual void addValue(Node v) = 0; + /** Get the next concrete value generated by this class. */ + virtual Node getNext() = 0; +}; + /** a synthesis conjecture * This class implements approaches for a synthesis conecjture, given by data * member d_quant. @@ -112,16 +130,6 @@ class SynthConjecture void assign(Node q); /** has a conjecture been assigned to this class */ bool isAssigned() { return !d_embed_quant.isNull(); } - /** - * 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. - */ - bool getEnumeratedValues(std::vector& n, std::vector& v); - /** - * Get model value for term n. If n has a value that was excluded by - * datatypes sygus symmetry breaking, this method returns null. - */ - Node getEnumeratedValue(Node n); /** * Get model value for term n. */ @@ -174,6 +182,47 @@ class SynthConjecture SygusModule* d_master; //------------------------end modules + //------------------------enumerators + /** + * 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. + */ + bool getEnumeratedValues(std::vector& n, std::vector& v); + /** + * Get model value for term n. If n has a value that was excluded by + * datatypes sygus symmetry breaking, this method returns null. + */ + Node getEnumeratedValue(Node n); + /** enumerator generators for each actively-generated enumerator */ + std::map > d_evg; + /** + * Map from enumerators to whether they are currently being + * "actively-generated". That is, we are in a state where we have called + * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet + * returned null. The range of this map stores the abstract value that + * we are currently generating values from. + */ + std::map d_ev_curr_active_gen; + /** the current waiting value of each actively-generated enumerator, if any + * + * This caches values that are actively generated and that we have not yet + * passed to a call to SygusModule::constructCandidates. An example of when + * this may occur is when there are two actively-generated enumerators e1 and + * e2. Say on some iteration we actively-generate v1 for e1, the value + * of e2 was excluded by symmetry breaking, and say the current master sygus + * module does not handle partial models. Hence, we abort the current check. + * We remember that the value of e1 was v1 by storing it here, so that on + * a future check when v2 has a proper value, it is returned. + */ + std::map d_ev_active_gen_waiting; + /** the first value enumerated for each actively-generated enumerator + * + * This is to implement an optimization that only guards the blocking lemma + * for the first value of an actively-generated enumerator. + */ + std::map d_ev_active_gen_first_val; + //------------------------end enumerators + /** list of constants for quantified formula * The outer Skolems for the negation of d_embed_quant. */ @@ -237,6 +286,18 @@ 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 diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 23b35cfed..1a8c81bcc 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -589,6 +589,25 @@ void TermDbSygus::registerEnumerator(Node e, d_var_subclass_list[et][sc].push_back(v); } } + // If no subclass has more than one variable, do not use variable agnostic + // enumeration + bool useVarAgnostic = false; + for (std::pair >& p : + d_var_subclass_list[et]) + { + if (p.second.size() > 1) + { + useVarAgnostic = true; + } + } + if (!useVarAgnostic) + { + Trace("sygus-db") + << "...disabling variable agnostic for " << e + << " since it has no subclass with more than one variable." + << std::endl; + d_enum_var_agnostic[e] = false; + } } } -- 2.30.2