From: Andrew Reynolds Date: Tue, 11 Feb 2020 04:41:18 +0000 (-0600) Subject: Use example evaluation cache instead of sygus PBE (#3733) X-Git-Tag: cvc5-1.0.0~3661 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d5fae3f69a2ab8b07bb89e94a368a73bd281c203;p=cvc5.git Use example evaluation cache instead of sygus PBE (#3733) --- diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 890b8b2b9..1e593a664 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1054,16 +1054,16 @@ Node SygusExtension::registerSearchValue(Node a, Node bad_val_bvr; bool by_examples = false; if( itsv==d_cache[a].d_search_val[tn].end() ){ - // TODO (github #1210) conjecture-specific symmetry breaking - // this should be generalized and encapsulated within the - // SynthConjecture class. // Is it equivalent under examples? Node bvr_equiv; if (options::sygusSymBreakPbe()) { - if (aconj->getPbe()->hasExamples(a)) + // If the enumerator has examples, see if it is equivalent up to its + // examples with a previous term. + quantifiers::ExampleEvalCache* eec = aconj->getExampleEvalCache(a); + if (eec != nullptr) { - bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr); + bvr_equiv = eec->addSearchVal(bvr); } } if( !bvr_equiv.isNull() ){ diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index f7d0e7b7e..3ef3a3edc 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -17,6 +17,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "theory/quantifiers/sygus/example_min_eval.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers_engine.h" @@ -143,30 +144,36 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, : "") << "..." << std::endl; // see if any refinement lemma is refuted by evaluation - std::vector cre_lems; - bool ret = - getRefinementEvalLemmas(candidates, candidate_values, cre_lems, doGen); - if (ret && !doGen) + if (doGen) { - Trace("cegqi-engine") << "...(actively enumerated) candidate failed " - "refinement lemma evaluation." - << std::endl; - return true; - } - if (!cre_lems.empty()) - { - lems.insert(lems.end(), cre_lems.begin(), cre_lems.end()); - addedEvalLemmas = true; - if (Trace.isOn("cegqi-lemma")) + std::vector cre_lems; + getRefinementEvalLemmas(candidates, candidate_values, cre_lems); + 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")) { - Trace("cegqi-lemma") - << "Cegqi::Lemma : ref evaluation : " << lem << std::endl; + for (const Node& lem : cre_lems) + { + Trace("cegqi-lemma") + << "Cegqi::Lemma : ref evaluation : " << lem << std::endl; + } } + /* we could, but do not return here. experimentally, it is better to + add the lemmas below as well, in parallel. */ + } + } + else + { + // just check whether the refinement lemmas are satisfied, fail if not + if (checkRefinementEvalLemmas(candidates, candidate_values)) + { + Trace("cegqi-engine") << "...(actively enumerated) candidate failed " + "refinement lemma evaluation." + << std::endl; + return true; } - /* we could, but do not return here. experimentally, it is better to - add the lemmas below as well, in parallel. */ } } // we only do evaluation unfolding for passive enumerators @@ -481,8 +488,7 @@ void Cegis::registerRefinementLemma(const std::vector& vars, bool Cegis::usingRepairConst() { return true; } bool Cegis::getRefinementEvalLemmas(const std::vector& vs, const std::vector& ms, - std::vector& lems, - bool doGen) + std::vector& lems) { Trace("sygus-cref-eval") << "Cref eval : conjecture has " << d_refinement_lemma_unit.size() << " unit and " @@ -496,6 +502,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector& vs, Node nfalse = nm->mkConst(false); Node neg_guard = d_parent->getGuard().negate(); bool ret = false; + for (unsigned r = 0; r < 2; r++) { std::unordered_set& rlemmas = @@ -519,11 +526,6 @@ bool Cegis::getRefinementEvalLemmas(const std::vector& vs, << "...after unfolding is : " << lemcsu << std::endl; if (lemcsu.isConst() && !lemcsu.getConst()) { - if (!doGen) - { - // we are not generating the lemmas, instead just return - return true; - } ret = true; std::vector msu; std::vector mexp; diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 2c21257b9..bebb91fa3 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -185,13 +185,11 @@ class Cegis : public SygusModule * to lems based on evaluating the conjecture, instantiated for ms, on lemmas * for previous refinements (d_refinement_lemmas). * - * Returns true if any such lemma exists. If doGen is false, then the - * lemmas are not generated or added to lems. + * Returns true if any such lemma exists. */ bool getRefinementEvalLemmas(const std::vector& vs, const std::vector& ms, - std::vector& lems, - bool doGen); + std::vector& lems); /** Check refinement evaluation lemmas * * This method is similar to above, but does not perform any generalization diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp index a7dd59900..2a43335d7 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.cpp +++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp @@ -51,17 +51,17 @@ Node ExampleEvalCache::addSearchVal(Node bv) return Node::null(); } std::vector vals; - evaluateVec(bv, vals, false); + evaluateVec(bv, vals, true); Trace("sygus-pbe-debug") << "Add to trie..." << std::endl; Node ret = d_trie.addOrGetTerm(bv, vals); Trace("sygus-pbe-debug") << "...got " << ret << std::endl; // Only save the cache data if necessary: if the enumerated term // is redundant, its cached data will not be used later and thus should - // be discarded. - if (ret == bv) + // be discarded. This applies also to the case where the evaluation + // was cached prior to this call. + if (ret != bv) { - std::vector& eocv = d_exOutCache[bv]; - eocv.insert(eocv.end(), vals.begin(), vals.end()); + clearEvaluationCache(bv); } Assert(ret.getType().isComparableTo(bv.getType())); return ret; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 99f8eee2c..63a61b818 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -17,6 +17,7 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/quantifiers/sygus/synth_engine.h" using namespace CVC4::kind; @@ -143,7 +144,7 @@ Node SygusEnumerator::getCurrent() SygusEnumerator::TermCache::TermCache() : d_tds(nullptr), - d_pbe(nullptr), + d_eec(nullptr), d_isSygusType(false), d_numConClasses(0), d_sizeEnum(0), @@ -151,15 +152,19 @@ SygusEnumerator::TermCache::TermCache() d_sampleRrVInit(false) { } -void SygusEnumerator::TermCache::initialize( - SygusStatistics* s, Node e, TypeNode tn, TermDbSygus* tds, SygusPbe* pbe) + +void SygusEnumerator::TermCache::initialize(SygusStatistics* s, + Node e, + TypeNode tn, + TermDbSygus* tds, + ExampleEvalCache* eec) { Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl; d_stats = s; d_enum = e; d_tn = tn; d_tds = tds; - d_pbe = pbe; + d_eec = eec; d_sizeStartIndex[0] = 0; d_isSygusType = false; @@ -334,11 +339,11 @@ bool SygusEnumerator::TermCache::addTerm(Node n) return false; } // if we are doing PBE symmetry breaking - if (d_pbe != nullptr) + if (d_eec != nullptr) { ++(d_stats->d_enumTermsExampleEval); // Is it equivalent under examples? - Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr); + Node bne = d_eec->addSearchVal(bnr); if (!bne.isNull()) { if (bnr != bne) @@ -533,17 +538,13 @@ void SygusEnumerator::TermEnumSlave::validateIndexNextEnd() void SygusEnumerator::initializeTermCache(TypeNode tn) { // initialize the term cache - // see if we use sygus PBE for symmetry breaking - SygusPbe* pbe = nullptr; + // see if we use an example evaluation cache for symmetry breaking + ExampleEvalCache* eec = nullptr; if (options::sygusSymBreakPbe()) { - pbe = d_parent->getPbe(); - if (!pbe->hasExamples(d_enum)) - { - pbe = nullptr; - } + eec = d_parent->getExampleEvalCache(d_enum); } - d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, pbe); + d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, eec); } SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 7e5add299..9803cd962 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -103,7 +103,7 @@ class SygusEnumerator : public EnumValGenerator Node e, TypeNode tn, TermDbSygus* tds, - SygusPbe* pbe = nullptr); + ExampleEvalCache* ece = nullptr); /** get last constructor class index for weight * * This returns a minimal index n such that all constructor classes at @@ -152,8 +152,11 @@ class SygusEnumerator : public EnumValGenerator TypeNode d_tn; /** pointer to term database sygus */ TermDbSygus* d_tds; - /** pointer to the PBE utility (used for symmetry breaking) */ - SygusPbe* d_pbe; + /** + * Pointer to the example evaluation cache utility (used for symmetry + * breaking). + */ + ExampleEvalCache* d_eec; //-------------------------static information about type /** is d_tn a sygus type? */ bool d_isSygusType; diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index b494e085e..9d20e1c3c 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -91,15 +91,14 @@ void EquivSygusInvarianceTest::init( { // compute the current examples d_bvr = bvr; - if (aconj->getPbe()->hasExamples(e)) + Assert(tds != nullptr); + ExampleEvalCache* eec = aconj->getExampleEvalCache(e); + if (eec != nullptr) { + // get the result of evaluating bvr on the examples of enumerator e. + eec->evaluateVec(bvr, d_exo, false); d_conj = aconj; d_enum = e; - unsigned nex = aconj->getPbe()->getNumExamples(e); - for (unsigned i = 0; i < nex; i++) - { - d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i)); - } } } @@ -149,9 +148,11 @@ bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) if (!d_enum.isNull()) { bool ex_equiv = true; - for (unsigned j = 0; j < d_exo.size(); j++) + ExampleEvalCache* eec = d_conj->getExampleEvalCache(d_enum); + Assert(eec != nullptr); + for (unsigned j = 0, esize = d_exo.size(); j < esize; j++) { - Node nbvr_ex = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, j); + Node nbvr_ex = eec->evaluate(nbvr, j); if (nbvr_ex != d_exo[j]) { ex_equiv = false; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index ae019e50f..dc290d4ba 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -16,6 +16,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/sygus/example_infer.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -38,114 +39,6 @@ SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p) SygusPbe::~SygusPbe() {} -//--------------------------------- collecting finite input/output domain information - -bool SygusPbe::collectExamples(Node n, - std::map& visited, - bool hasPol, - bool pol) -{ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - Node neval; - Node n_output; - bool neval_is_evalapp = false; - if (n.getKind() == DT_SYGUS_EVAL) - { - neval = n; - if( hasPol ){ - n_output = pol ? d_true : d_false; - } - neval_is_evalapp = true; - } - else if (n.getKind() == EQUAL && hasPol && pol) - { - for( unsigned r=0; r<2; r++ ){ - if (n[r].getKind() == DT_SYGUS_EVAL) - { - neval = n[r]; - if( n[1-r].isConst() ){ - n_output = n[1-r]; - } - neval_is_evalapp = true; - } - } - } - // is it an evaluation function? - if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end()) - { - Trace("sygus-pbe-debug") - << "Process head: " << n << " == " << n_output << std::endl; - // If n_output is null, then neval does not have a constant value - // If n_output is non-null, then neval is constrained to always be - // that value. - if (!n_output.isNull()) - { - std::map::iterator itet = d_exampleTermMap.find(neval); - if (itet == d_exampleTermMap.end()) - { - d_exampleTermMap[neval] = n_output; - } - else if (itet->second != n_output) - { - // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2, - // the conjecture is infeasible. - return false; - } - } - // get the evaluation head - Node eh = neval[0]; - std::map::iterator itx = d_examples_invalid.find(eh); - if (itx == d_examples_invalid.end()) - { - // collect example - bool success = true; - std::vector ex; - for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++) - { - if (!neval[j].isConst()) - { - success = false; - break; - } - ex.push_back(neval[j]); - } - if (success) - { - d_examples[eh].push_back(ex); - d_examples_out[eh].push_back(n_output); - d_examples_term[eh].push_back(neval); - if (n_output.isNull()) - { - d_examples_out_invalid[eh] = true; - } - else - { - Assert(n_output.isConst()); - // finished processing this node if it was an I/O pair - return true; - } - } - else - { - d_examples_invalid[eh] = true; - d_examples_out_invalid[eh] = true; - } - } - } - for( unsigned i=0; i& candidates, @@ -154,51 +47,6 @@ bool SygusPbe::initialize(Node conj, Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); - for (unsigned i = 0; i < candidates.size(); i++) - { - Node v = candidates[i]; - d_examples[v].clear(); - d_examples_out[v].clear(); - d_examples_term[v].clear(); - } - - std::map visited; - // n is negated conjecture - if (!collectExamples(n, visited, true, false)) - { - Trace("sygus-pbe") << "...conflicting examples" << std::endl; - Node infeasible = d_parent->getGuard().negate(); - lemmas.push_back(infeasible); - return false; - } - - for (unsigned i = 0; i < candidates.size(); i++) - { - Node v = candidates[i]; - Trace("sygus-pbe") << " examples for " << v << " : "; - if (d_examples_invalid.find(v) != d_examples_invalid.end()) - { - Trace("sygus-pbe") << "INVALID" << std::endl; - } - else - { - Trace("sygus-pbe") << std::endl; - for (unsigned j = 0; j < d_examples[v].size(); j++) - { - Trace("sygus-pbe") << " "; - for (unsigned k = 0; k < d_examples[v][j].size(); k++) - { - Trace("sygus-pbe") << d_examples[v][j][k] << " "; - } - if (!d_examples_out[v][j].isNull()) - { - Trace("sygus-pbe") << " -> " << d_examples_out[v][j]; - } - Trace("sygus-pbe") << std::endl; - } - } - } - if (!options::sygusUnifPbe()) { // we are not doing unification @@ -206,11 +54,12 @@ bool SygusPbe::initialize(Node conj, } // check if all candidates are valid examples + ExampleInfer* ei = d_parent->getExampleInfer(); d_is_pbe = true; for (const Node& c : candidates) { - if (d_examples[c].empty() - || d_examples_out_invalid.find(c) != d_examples_out_invalid.end()) + // if it has no examples or the output of the examples is invalid + if (ei->getNumExamples(c) == 0 || !ei->hasExamplesOut(c)) { d_is_pbe = false; return false; @@ -218,11 +67,12 @@ bool SygusPbe::initialize(Node conj, } for (const Node& c : candidates) { - Assert(d_examples.find(c) != d_examples.end()); + Assert(ei->hasExamples(c)); + d_sygus_unif[c].reset(new SygusUnifIo(d_parent)); Trace("sygus-pbe") << "Initialize unif utility for " << c << "..." << std::endl; std::map> strategy_lemmas; - d_sygus_unif[c].initializeCandidate( + d_sygus_unif[c]->initializeCandidate( d_qe, c, d_candidate_to_enum[c], strategy_lemmas); Assert(!d_candidate_to_enum[c].empty()); Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size() @@ -288,163 +138,10 @@ bool SygusPbe::initialize(Node conj, d_tds->registerSymBreakLemma(e, lem, etn, 0, false); } } - Trace("sygus-pbe") << "Initialize " << d_examples[c].size() - << " example points for " << c << "..." << std::endl; - // initialize the examples - for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++) - { - d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]); - } } return true; } -Node SygusPbe::PbeTrie::addTerm(Node b, const std::vector& exOut) -{ - PbeTrie* curr = this; - for (const Node& eo : exOut) - { - curr = &(curr->d_children[eo]); - } - if (!curr->d_children.empty()) - { - return curr->d_children.begin()->first; - } - curr->d_children.insert(std::pair(b, PbeTrie())); - return b; -} - -bool SygusPbe::hasExamples(Node e) -{ - e = d_tds->getSynthFunForEnumerator(e); - if (e.isNull()) - { - // enumerator is not associated with synthesis function? - return false; - } - std::map::iterator itx = d_examples_invalid.find(e); - if (itx == d_examples_invalid.end()) - { - return d_examples.find(e) != d_examples.end(); - } - return false; -} - -unsigned SygusPbe::getNumExamples(Node e) -{ - e = d_tds->getSynthFunForEnumerator(e); - Assert(!e.isNull()); - std::map > >::iterator it = - d_examples.find(e); - if (it != d_examples.end()) { - return it->second.size(); - } else { - return 0; - } -} - -void SygusPbe::getExample(Node e, unsigned i, std::vector& ex) -{ - e = d_tds->getSynthFunForEnumerator(e); - Assert(!e.isNull()); - std::map > >::iterator it = - d_examples.find(e); - if (it != d_examples.end()) { - Assert(i < it->second.size()); - ex.insert(ex.end(), it->second[i].begin(), it->second[i].end()); - } else { - Assert(false); - } -} - -Node SygusPbe::getExampleOut(Node e, unsigned i) -{ - e = d_tds->getSynthFunForEnumerator(e); - Assert(!e.isNull()); - std::map >::iterator it = d_examples_out.find(e); - if (it != d_examples_out.end()) { - Assert(i < it->second.size()); - return it->second[i]; - } else { - Assert(false); - return Node::null(); - } -} - -Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) -{ - Assert(!e.isNull()); - if (d_tds->isVariableAgnosticEnumerator(e)) - { - // we cannot apply conjecture-specific symmetry breaking on variable - // agnostic enumerators - return Node::null(); - } - Node ee = d_tds->getSynthFunForEnumerator(e); - Assert(!e.isNull()); - std::map::iterator itx = d_examples_invalid.find(ee); - if (itx == d_examples_invalid.end()) { - std::vector vals; - Trace("sygus-pbe-debug") - << "Compute examples " << bvr << "..." << std::endl; - if (d_is_pbe) - { - // Compute example values with the I/O utility, which ensures they are - // not later recomputed when the enumerated term is given the I/O utility. - d_sygus_unif[ee].computeExamples(e, bvr, vals); - } - else - { - // If the I/O utility is not enabled (if the conjecture is not PBE), - // compute them separately. This handles the case when all applications - // of a function-to-synthesize are applied to constant arguments but - // the conjecture is not PBE. - TypeNode etn = e.getType(); - std::vector>& exs = d_examples[ee]; - for (size_t i = 0, esize = exs.size(); i < esize; i++) - { - Node res = d_tds->evaluateBuiltin(etn, bvr, exs[i]); - vals.push_back(res); - } - } - Assert(vals.size() == d_examples[ee].size()); - Trace("sygus-pbe-debug") << "...got " << vals << std::endl; - Trace("sygus-pbe-debug") << "Add to trie..." << std::endl; - Node ret = d_pbe_trie[e][tn].addTerm(bvr, vals); - Trace("sygus-pbe-debug") << "...got " << ret << std::endl; - if (d_is_pbe) - { - // Clean up the cache data if necessary: if the enumerated term - // is redundant, its cached data will not be used later and thus should - // be cleared now. - if (ret != bvr) - { - Trace("sygus-pbe-debug") << "...clear example cache" << std::endl; - d_sygus_unif[ee].clearExampleCache(e, bvr); - } - } - Assert(ret.getType().isComparableTo(bvr.getType())); - return ret; - } - return Node::null(); -} - -Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) -{ - e = d_tds->getSynthFunForEnumerator(e); - Assert(!e.isNull()); - std::map::iterator itx = d_examples_invalid.find(e); - if (itx == d_examples_invalid.end()) { - std::map > >::iterator it = - d_examples.find(e); - if (it != d_examples.end()) { - Assert(i < it->second.size()); - return d_tds->evaluateBuiltin(tn, bn, it->second[i]); - } - } - return Rewriter::rewrite(bn); -} - // ------------------------------------------- solution construction from enumeration void SygusPbe::getTermList(const std::vector& candidates, @@ -526,7 +223,7 @@ bool SygusPbe::constructCandidates(const std::vector& enums, Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end()); Node c = d_enum_to_candidate[e]; std::vector enum_lems; - d_sygus_unif[c].notifyEnumeration(e, v, enum_lems); + d_sygus_unif[c]->notifyEnumeration(e, v, enum_lems); if (!enum_lems.empty()) { // the lemmas must be guarded by the active guard of the enumerator @@ -544,7 +241,7 @@ bool SygusPbe::constructCandidates(const std::vector& enums, Node c = candidates[i]; //build decision tree for candidate std::vector sol; - if (d_sygus_unif[c].constructSolution(sol, lems)) + if (d_sygus_unif[c]->constructSolution(sol, lems)) { Assert(sol.size() == 1); candidate_values.push_back(sol[0]); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 2e6ca2659..3aa668e0d 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -34,13 +34,14 @@ class SynthConjecture; * * [EX#1] An example of a synthesis conjecture in PBE form is : * exists f. forall x. - * ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 ) + * ( f( 0 ) = 2 ) ^ ( f( 5 ) = 7 ) ^ ( f( 6 ) = 8 ) * * We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8. * * Internally, this class does the following for SyGuS inputs: * - * (1) Infers whether the input conjecture is in PBE form or not. + * (1) Infers whether the input conjecture is in PBE form or not, which + * is based on looking up information in the ExampleInfer utility. * (2) Based on this information and on the syntactic restrictions, it * devises a strategy for enumerating terms and construction solutions, * which is inspired by Alur et al. "Scaling Enumerative Program Synthesis @@ -68,22 +69,11 @@ class SynthConjecture; * syntactic restrictions for it. The search may continue unless all enumerators * become inactive. * - * (4) During search, the extension of quantifier-free datatypes procedure for - * SyGuS datatypes may ask this class whether current candidates can be - * discarded based on inferring when two candidate solutions are equivalent - * up to examples. For example, the candidate solutions: - * f = \x ite( x < 0, x+1, x ) and f = \x x - * are equivalent up to examples on the above conjecture, since they have - * the same value on the points x = 0,5,6. Hence, we need only consider one of - * them. The interface for querying this is - * SygusPbe::addSearchVal(...). - * For details, see Reynolds et al. SYNT 2017. - * - * (5) When the extension of quantifier-free datatypes procedure for SyGuS + * (4) When the extension of quantifier-free datatypes procedure for SyGuS * datatypes terminates with a model, the parent of this class calls * SygusPbe::getCandidateList(...), where this class returns the list * of active enumerators. - * (6) The parent class subsequently calls + * (5) The parent class subsequently calls * SygusPbe::constructValues(...), which informs this class that new * values have been enumerated for active enumerators, as indicated by the * current model. This call also requests that based on these @@ -153,67 +143,6 @@ class SygusPbe : public SygusModule std::vector& lems) override; /** is PBE enabled for any enumerator? */ bool isPbe() { return d_is_pbe; } - /** - * Is the enumerator e associated with examples? This is true if the - * function-to-synthesize associated with e is only applied to concrete - * arguments. Notice that the conjecture need not be in PBE form for this - * to be the case. For example, f has examples in: - * exists f. f( 1 ) = 3 ^ f( 2 ) = 4 - * exists f. f( 45 ) > 0 ^ f( 99 ) > 0 - * exists f. forall x. ( x > 5 => f( 4 ) < x ) - * It does not have examples in: - * exists f. forall x. f( x ) > 5 - * exists f. f( f( 4 ) ) = 5 - * This class implements techniques for functions-to-synthesize that - * have examples. In particular, the method addSearchVal below can be - * called. - */ - bool hasExamples(Node e); - /** get number of examples for enumerator e */ - unsigned getNumExamples(Node e); - /** - * Get the input arguments for i^th example for e, which is added to the - * vector ex - */ - void getExample(Node e, unsigned i, std::vector& ex); - /** - * Get the output value of the i^th example for enumerator e, or null if - * it does not exist (an example does not have an associate output if it is - * not a top-level equality). - */ - Node getExampleOut(Node e, unsigned i); - - /** add the search val - * This function is called by the extension of quantifier-free datatypes - * procedure for SyGuS datatypes or the SyGuS fast enumerator when we are - * considering a value of enumerator e of sygus type tn whose analog in the - * signature of builtin theory is bvr. - * - * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) - * and tn is a sygus datatype that encodes a subsignature of the integers. - * - * This returns either: - * - A SyGuS term whose analog is equivalent to bvr up to examples - * In the above example, - * it may return a term t of the form Plus( One(), x() ), such that this - * function was previously called with t as input. - * - e, indicating that no previous terms are equivalent to e up to examples. - * - * This method should only be called if hasExamples(e) returns true. - */ - Node addSearchVal(TypeNode tn, Node e, Node bvr); - /** evaluate builtin - * This returns the evaluation of bn on the i^th example for the - * function-to-synthesis - * associated with enumerator e. If there are not at least i examples, it - * returns the rewritten form of bn. - * For example, if bn = x+5, e is an enumerator for f in the above example - * [EX#1], then - * evaluateBuiltin( tn, bn, e, 0 ) = 7 - * evaluateBuiltin( tn, bn, e, 1 ) = 9 - * evaluateBuiltin( tn, bn, e, 2 ) = 10 - */ - Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i); private: /** true and false nodes */ @@ -221,31 +150,12 @@ class SygusPbe : public SygusModule Node d_false; /** is this a PBE conjecture for any function? */ bool d_is_pbe; - /** for each candidate variable f (a function-to-synthesize), whether the - * conjecture is purely PBE for that variable - * In other words, all occurrences of f are guarded by equalities that - * constraint its arguments to constants. - */ - std::map d_examples_invalid; - /** for each candidate variable (function-to-synthesize), whether the - * conjecture is purely PBE for that variable. - * An example of a conjecture for which d_examples_invalid is false but - * d_examples_out_invalid is true is: - * exists f. forall x. ( x = 0 => f( x ) > 2 ) - * another example is: - * exists f. forall x. ( ( x = 0 => f( x ) = 2 ) V ( x = 3 => f( x ) = 3 ) ) - * since the formula is not a conjunction (the example values are not - * entailed). - * However, the domain of f in both cases is finite, which can be used for - * search space pruning. - */ - std::map d_examples_out_invalid; /** * Map from candidates to sygus unif utility. This class implements * the core algorithm (e.g. decision tree learning) that this module relies * upon. */ - std::map d_sygus_unif; + std::map > d_sygus_unif; /** * map from candidates to the list of enumerators that are being used to * build solutions for that candidate by the above utility. @@ -253,63 +163,6 @@ class SygusPbe : public SygusModule std::map > d_candidate_to_enum; /** reverse map of above */ std::map d_enum_to_candidate; - /** for each candidate variable (function-to-synthesize), input of I/O - * examples */ - std::map > > d_examples; - /** for each candidate variable (function-to-synthesize), output of I/O - * examples */ - std::map > d_examples_out; - /** the list of example terms - * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 ) - */ - std::map > d_examples_term; - /** - * Map from example input terms to their output, for example [EX#1] above, - * this is { f( 0 ) -> 2, f( 5 ) -> 7, f( 6 ) -> 8 }. - */ - std::map d_exampleTermMap; - /** collect the PBE examples in n - * This is called on the input conjecture, and will populate the above - * vectors, where hasPol/pol denote the polarity of n in the conjecture. This - * function returns false if it finds two examples that are contradictory. - */ - bool collectExamples(Node n, - std::map& visited, - bool hasPol, - bool pol); - - //--------------------------------- PBE search values - /** - * This class is an index of candidate solutions for PBE synthesis and their - * (concrete) evaluation on the set of input examples. For example, if the - * set of input examples for (x,y) is (0,1), (1,3), then: - * term x is indexed by 0,1 - * term x+y is indexed by 1,4 - * term 0 is indexed by 0,0. - */ - class PbeTrie - { - public: - PbeTrie() {} - ~PbeTrie() {} - /** the children for this node in the trie */ - std::map d_children; - /** clear this trie */ - void clear() { d_children.clear(); } - /** - * Add term b whose value on examples is exOut to the trie. Return - * the first term registered to this trie whose evaluation was exOut. - */ - Node addTerm(Node b, const std::vector& exOut); - }; - /** trie of candidate solutions tried - * This stores information for each (enumerator, type), - * where type is a type in the grammar of the space of solutions for a subterm - * of e. This is used for symmetry breaking in quantifier-free reasoning - * about SyGuS datatypes. - */ - std::map > d_pbe_trie; - //--------------------------------- end PBE search values }; } /* namespace CVC4::theory::quantifiers */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index d423b1777..e3e94ba44 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -16,8 +16,11 @@ #include "options/quantifiers_options.h" #include "theory/evaluator.h" +#include "theory/quantifiers/sygus/example_infer.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "util/random.h" #include @@ -495,8 +498,9 @@ void SubsumeTrie::getLeaves(const std::vector& vals, getLeavesInternal(vals, pol, v, 0, -2); } -SygusUnifIo::SygusUnifIo() - : d_check_sol(false), +SygusUnifIo::SygusUnifIo(SynthConjecture* p) + : d_parent(p), + d_check_sol(false), d_cond_count(0), d_sol_term_size(0), d_sol_cons_nondet(false), @@ -507,53 +511,36 @@ SygusUnifIo::SygusUnifIo() } SygusUnifIo::~SygusUnifIo() {} + void SygusUnifIo::initializeCandidate( QuantifiersEngine* qe, Node f, std::vector& enums, std::map>& strategy_lemmas) { + d_candidate = f; + // copy the examples from the parent + ExampleInfer* ei = d_parent->getExampleInfer(); d_examples.clear(); d_examples_out.clear(); + // copy the examples + if (ei->hasExamples(f)) + { + for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++) + { + std::vector input; + ei->getExample(f, i, input); + Node output = ei->getExampleOut(f, i); + d_examples.push_back(input); + d_examples_out.push_back(output); + } + } d_ecache.clear(); - d_candidate = f; SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas); // learn redundant operators based on the strategy d_strategy[f].staticLearnRedundantOps(strategy_lemmas); } -void SygusUnifIo::addExample(const std::vector& input, Node output) -{ - d_examples.push_back(input); - d_examples_out.push_back(output); -} - -void SygusUnifIo::computeExamples(Node e, Node bv, std::vector& exOut) -{ - std::map>& eoc = d_exOutCache[e]; - std::map>::iterator it = eoc.find(bv); - if (it != eoc.end()) - { - exOut.insert(exOut.end(), it->second.begin(), it->second.end()); - return; - } - TypeNode xtn = e.getType(); - std::vector& eocv = eoc[bv]; - for (size_t j = 0, size = d_examples.size(); j < size; j++) - { - Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]); - exOut.push_back(res); - eocv.push_back(res); - } -} - -void SygusUnifIo::clearExampleCache(Node e, Node bv) -{ - std::map>& eoc = d_exOutCache[e]; - Assert(eoc.find(bv) != eoc.end()); - eoc.erase(bv); -} - void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) { Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v @@ -573,9 +560,13 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) bv = d_tds->getExtRewriter()->extendedRewrite(bv); Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv << std::endl; // compte the results (should be cached) - computeExamples(e, bv, base_results); - // don't need it after this - clearExampleCache(e, bv); + ExampleEvalCache* eec = d_parent->getExampleEvalCache(e); + Assert(eec != nullptr); + // Evaluate, which should be cached (assuming we have performed example-based + // symmetry breaking on bv). Moreover don't cache the result in the case it + // is not there already, since we won't need this evaluation anywhere outside + // of this class. + eec->evaluateVec(bv, base_results); // get the results for each slave enumerator std::map> srmap; Evaluator* ev = d_tds->getEvaluator(); diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 7e9c5abd2..da08044bf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -243,19 +243,19 @@ class SubsumeTrie int status); }; +class SynthConjecture; + /** Sygus unification I/O utility * * This class implement synthesis-by-unification, where the specification is - * I/O examples. With respect to SygusUnif, it's main interface function is - * addExample, which adds an I/O example to the specification. + * I/O examples. * * Since I/O specifications for multiple functions can be fully separated, we * assume that this class is used only for a single function to synthesize. * * In addition to the base class which maintains a strategy tree, this class * maintains: - * (1) A set of input/output examples that are the specification for f. This - * can be updated via calls to resetExmaples/addExamples, + * (1) A set of input/output examples that are the specification for f. * (2) A set of terms that have been enumerated for enumerators (d_ecache). This * can be updated via calls to notifyEnumeration. */ @@ -264,10 +264,13 @@ class SygusUnifIo : public SygusUnif friend class UnifContextIo; public: - SygusUnifIo(); + SygusUnifIo(SynthConjecture* p); ~SygusUnifIo(); /** initialize + * + * This initializes this class for solving PBE conjectures for + * function-to-synthesize f. * * We only initialize for one function f, since I/O specifications across * multiple functions can be separated. @@ -283,29 +286,10 @@ class SygusUnifIo : public SygusUnif /** Construct solution */ bool constructSolution(std::vector& sols, std::vector& lemmas) override; - - /** add example - * - * This adds input -> output to the specification for f. The arity of - * input should be equal to the number of arguments in the sygus variable - * list of the grammar of f. That is, if we are searching for solutions for f - * of the form (lambda v1...vn. t), then the arity of input should be n. - */ - void addExample(const std::vector& input, Node output); - - /** compute examples - * - * This adds the result of evaluating bv on the set of input examples managed - * by this class. Term bv is the builtin version of a term generated for - * enumerator e. It stores the resulting output for each example in exOut. - */ - void computeExamples(Node e, Node bv, std::vector& exOut); - - /** clear example cache */ - void clearExampleCache(Node e, Node bv); - protected: - /** the candidate */ + /** The synthesis conjecture */ + SynthConjecture* d_parent; + /** the function-to-synthesize */ Node d_candidate; /** * Whether we will try to construct solution on the next call to @@ -363,9 +347,6 @@ class SygusUnifIo : public SygusUnif /** output of I/O examples */ std::vector d_examples_out; - /** cache for computeExamples */ - std::map>> d_exOutCache; - /** * This class stores information regarding an enumerator, including: * a database of values that have been enumerated for this enumerator.