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.
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
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++)
{
return ret;
}
+bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs,
+ const std::vector<Node>& 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<Node, Node, NodeHashFunction> 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<Node> vsProc;
+ std::vector<Node> 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<Node, NodeHashFunction>& 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<bool>())
+ {
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
const std::vector<Node>& vals,
std::vector<Node>& lems)
std::vector<Node> d_rl_vals;
/** all variables appearing in refinement lemmas */
std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_vars;
+
/** adds lem as a refinement lemma */
void addRefinementLemma(Node lem);
/** add refinement lemma conjunct
/** 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.
const std::vector<Node>& ms,
std::vector<Node>& 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<Node>& vs,
+ const std::vector<Node>& ms);
/** sampler object for the option cegisSample()
*
* This samples points of the type of the inner variables of the synthesis
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),
}
}
}
+ // 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
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<const Node, std::unique_ptr<ExampleEvalCache> >& ecp :
+ d_exampleEvalCache)
+ {
+ ExampleEvalCache* eec = ecp.second.get();
+ if (eec != nullptr)
+ {
+ eec->clearEvaluationAll();
+ }
+ }
}
NodeManager* nm = NodeManager::currentNM();
}
}
+ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e)
+{
+ std::map<Node, std::unique_ptr<ExampleEvalCache> >::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 */
#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"
namespace quantifiers {
class SynthEngine;
+class SygusStatistics;
/**
* A base class for generating values for actively-generated enumerators.
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 */
std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
/** repair constant utility */
std::unique_ptr<SygusRepairConst> d_sygus_rconst;
- /** connective core utility */
- std::unique_ptr<CegisCoreConnective> d_sygus_ccore;
+ /** example inference utility */
+ std::unique_ptr<ExampleInfer> d_exampleInfer;
+ /** example evaluation cache utility for each enumerator */
+ std::map<Node, std::unique_ptr<ExampleEvalCache> > d_exampleEvalCache;
//------------------------modules
/** program by examples module */
std::unique_ptr<Cegis> d_ceg_cegis;
/** CEGIS UNIF module */
std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
+ /** connective core utility */
+ std::unique_ptr<CegisCoreConnective> d_sygus_ccore;
/** the set of active modules (subset of the above list) */
std::vector<SygusModule*> d_modules;
/** master module
projects / cvc5.git / commitdiff