Home
last modified time | relevance | path

Searched refs:d_sygus_unif (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dcegis_unif.cpp32 : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p) in CegisUnif()
56 d_sygus_unif.initializeCandidate( in processInitialize()
58 if (!d_sygus_unif.usingUnif(f)) in processInitialize()
75 Node cond = d_sygus_unif.getConditionForEvaluationPoint(e); in processInitialize()
97 for (const Node& hd : d_sygus_unif.getEvalPointHeads(c)) in getTermList()
247 d_sygus_unif.setConditions(e, cost_lit, itc->second, itv->second); in setConditions()
288 for (const Node& hd : d_sygus_unif.getEvalPointHeads(c)) in processConstructCandidates()
337 if (d_sygus_unif.constructSolution(sols, lemmas)) in processConstructCandidates()
371 Node plem = d_sygus_unif.addRefLemma(lem, eval_pts); in registerRefinementLemma()
H A Dsygus_pbe.cpp222 d_sygus_unif[c].initializeCandidate( in initialize()
293 d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]); in initialize()
386 d_sygus_unif[ee].computeExamples(e, bvr, vals); in addSearchVal()
395 d_sygus_unif[ee].clearExampleCache(e, bvr); in addSearchVal()
500 d_sygus_unif[c].notifyEnumeration(e, v, enum_lems); in constructCandidates()
518 if (d_sygus_unif[c].constructSolution(sol, lems)) in constructCandidates()
H A Dsygus_pbe.h225 std::map<Node, SygusUnifIo> d_sygus_unif; variable
H A Dcegis_unif.h300 SygusUnifRl d_sygus_unif; variable