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 D | cegis_unif.cpp | 32 : 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 D | sygus_pbe.cpp | 222 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 D | sygus_pbe.h | 225 std::map<Node, SygusUnifIo> d_sygus_unif; variable
|
H A D | cegis_unif.h | 300 SygusUnifRl d_sygus_unif; variable
|