From: Andrew Reynolds Date: Sat, 8 Feb 2020 02:54:05 +0000 (-0600) Subject: Interface for example evaluation cache utilities (#3726) X-Git-Tag: cvc5-1.0.0~3670 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=585e2876429dc93945cdaac202d5555468671861;p=cvc5.git Interface for example evaluation cache utilities (#3726) This adds interfaces in synth_conjecture for getting an ExampleEvalCache, per enumerator. It also adds a specialization `checkRefinementEvalLemmas` of `getRefinementEvalLemmas` in the cegis module, which does evaluation on CEGIS refinement lemmas without structural generalization. This function will be used as an alternative to `getRefinementEvalLemmas` for fast enumerators. The next PR will update all utilities to use ExampleEvalCache instead of SygusPbe for evaluating examples. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 26cc5bbcc..f0aee982c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -562,6 +562,12 @@ libcvc4_add_sources( theory/quantifiers/sygus/cegis_core_connective.h theory/quantifiers/sygus/cegis_unif.cpp theory/quantifiers/sygus/cegis_unif.h + theory/quantifiers/sygus/example_eval_cache.cpp + theory/quantifiers/sygus/example_eval_cache.h + theory/quantifiers/sygus/example_infer.cpp + theory/quantifiers/sygus/example_infer.h + theory/quantifiers/sygus/example_min_eval.cpp + theory/quantifiers/sygus/example_min_eval.h theory/quantifiers/sygus/enum_stream_substitution.cpp theory/quantifiers/sygus/enum_stream_substitution.h theory/quantifiers/sygus/example_infer.cpp diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 2d27878fd..f7d0e7b7e 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -426,6 +426,7 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, d_rl_eval_hds.push_back(term); d_rl_vals.push_back(val); d_refinement_lemma_unit.insert(lem); + // apply to waiting lemmas beyond this one for (unsigned i = wcounter + 1, size = waiting.size(); i < size; i++) { @@ -573,6 +574,54 @@ bool Cegis::getRefinementEvalLemmas(const std::vector& vs, return ret; } +bool Cegis::checkRefinementEvalLemmas(const std::vector& vs, + const std::vector& ms) +{ + // Maybe we already evaluated some terms in refinement lemmas. + // In particular, the example eval cache for f may have some evaluations + // cached, which we add to evalVisited and pass to the evaluator below. + std::unordered_map evalVisited; + ExampleInfer* ei = d_parent->getExampleInfer(); + for (unsigned i = 0, vsize = vs.size(); i < vsize; i++) + { + Node f = vs[i]; + ExampleEvalCache* eec = d_parent->getExampleEvalCache(f); + if (eec != nullptr) + { + // get the results we obtained through the example evaluation utility + std::vector vsProc; + std::vector msProc; + Node bmsi = d_tds->sygusToBuiltin(ms[i]); + ei->getExampleTerms(f, vsProc); + eec->evaluateVec(bmsi, msProc); + Assert(vsProc.size() == msProc.size()); + for (unsigned j = 0, psize = vsProc.size(); j < psize; j++) + { + evalVisited[vsProc[j]] = msProc[j]; + Assert(vsProc[j].getType() == msProc[j].getType()); + } + } + } + + Evaluator* eval = d_tds->getEvaluator(); + for (unsigned r = 0; r < 2; r++) + { + std::unordered_set& rlemmas = + r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj; + for (const Node& lem : rlemmas) + { + // We may have computed the evaluation of some function applications + // via example-based symmetry breaking, stored in evalVisited. + Node lemcsu = eval->eval(lem, vs, ms, evalVisited); + if (lemcsu.isConst() && !lemcsu.getConst()) + { + return true; + } + } + } + return false; +} + bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, const std::vector& vals, std::vector& lems) diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index adaecc7f6..2c21257b9 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -114,6 +114,7 @@ class Cegis : public SygusModule std::vector d_rl_vals; /** all variables appearing in refinement lemmas */ std::unordered_set d_refinement_lemma_vars; + /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); /** add refinement lemma conjunct @@ -175,7 +176,7 @@ class Cegis : public SygusModule /** Get refinement evaluation lemmas * * This method performs "refinement evaluation", that is, it tests - * whether the current solution, given by { candidates -> candidate_values }, + * whether the current solution, given by { vs -> ms }, * 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. @@ -191,6 +192,17 @@ class Cegis : public SygusModule const std::vector& ms, std::vector& lems, bool doGen); + /** Check refinement evaluation lemmas + * + * This method is similar to above, but does not perform any generalization + * techniques. It is used when we are using only fast enumerators for + * all functions-to-synthesize. + * + * Returns true if a refinement lemma is false for the solution + * { vs -> ms }. + */ + bool checkRefinementEvalLemmas(const std::vector& vs, + const std::vector& ms); /** sampler object for the option cegisSample() * * This samples points of the type of the inner variables of the synthesis diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index b7c3851af..fe0e99a4d 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -55,10 +55,11 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), d_sygus_rconst(new SygusRepairConst(qe)), - d_sygus_ccore(new CegisCoreConnective(qe, this)), + d_exampleInfer(new ExampleInfer(d_tds)), d_ceg_pbe(new SygusPbe(qe, this)), d_ceg_cegis(new Cegis(qe, this)), d_ceg_cegisUnif(new CegisUnif(qe, this)), + d_sygus_ccore(new CegisCoreConnective(qe, this)), d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), @@ -191,6 +192,15 @@ void SynthConjecture::assign(Node q) } } } + // initialize the example inference utility + if (!d_exampleInfer->initialize(d_base_inst, d_candidates)) + { + // there is a contradictory example pair, the conjecture is infeasible. + Node infLem = d_feasible_guard.negate(); + d_qe->getOutputChannel().lemma(infLem); + // we don't need to continue initialization in this case + return; + } // register this term with sygus database and other utilities that impact // the enumerative sygus search @@ -442,6 +452,16 @@ bool SynthConjecture::doCheck(std::vector& lems) Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( terms, enum_values, d_candidates, candidate_values, lems); + // now clear the evaluation caches + for (std::pair >& ecp : + d_exampleEvalCache) + { + ExampleEvalCache* eec = ecp.second.get(); + if (eec != nullptr) + { + eec->clearEvaluationAll(); + } + } } NodeManager* nm = NodeManager::currentNM(); @@ -1320,6 +1340,25 @@ Node SynthConjecture::getSymmetryBreakingPredicate( } } +ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e) +{ + std::map >::iterator it = + d_exampleEvalCache.find(e); + if (it != d_exampleEvalCache.end()) + { + return it->second.get(); + } + Node f = d_tds->getSynthFunForEnumerator(e); + // if f does not have examples, we don't construct the utility + if (!d_exampleInfer->hasExamples(f) || d_exampleInfer->getNumExamples(f) == 0) + { + d_exampleEvalCache[e].reset(nullptr); + return nullptr; + } + d_exampleEvalCache[e].reset(new ExampleEvalCache(d_tds, this, f, e)); + return d_exampleEvalCache[e].get(); +} + } // namespace quantifiers } // namespace theory } /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index a001572c2..a4f4af2e8 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -26,6 +26,8 @@ #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/cegis_core_connective.h" #include "theory/quantifiers/sygus/cegis_unif.h" +#include "theory/quantifiers/sygus/example_eval_cache.h" +#include "theory/quantifiers/sygus/example_infer.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" @@ -37,6 +39,7 @@ namespace theory { namespace quantifiers { class SynthEngine; +class SygusStatistics; /** * A base class for generating values for actively-generated enumerators. @@ -155,6 +158,10 @@ class SynthConjecture SynthConjectureProcess* getProcess() { return d_ceg_proc.get(); } /** get constant repair utility */ SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); } + /** get example inference utility */ + ExampleInfer* getExampleInfer() { return d_exampleInfer.get(); } + /** get the example evaluation cache utility for enumerator e */ + ExampleEvalCache* getExampleEvalCache(Node e); /** get program by examples module */ SygusPbe* getPbe() { return d_ceg_pbe.get(); } /** get the symmetry breaking predicate for type */ @@ -196,8 +203,10 @@ class SynthConjecture std::unique_ptr d_ceg_gc; /** repair constant utility */ std::unique_ptr d_sygus_rconst; - /** connective core utility */ - std::unique_ptr d_sygus_ccore; + /** example inference utility */ + std::unique_ptr d_exampleInfer; + /** example evaluation cache utility for each enumerator */ + std::map > d_exampleEvalCache; //------------------------modules /** program by examples module */ @@ -206,6 +215,8 @@ class SynthConjecture std::unique_ptr d_ceg_cegis; /** CEGIS UNIF module */ std::unique_ptr d_ceg_cegisUnif; + /** connective core utility */ + std::unique_ptr d_sygus_ccore; /** the set of active modules (subset of the above list) */ std::vector d_modules; /** master module