Searched refs:d_candidates (Results 1 – 5 of 5) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_conjecture.cpp | 140 Assert(d_candidates.empty()); in assign()
147 d_candidates.push_back(e); in assign()
153 d_embed_quant, vars, d_candidates)); in assign()
157 vars.begin(), vars.end(), d_candidates.begin(), d_candidates.end()); in assign()
182 d_ceg_proc->initialize(d_base_inst, d_candidates); in assign()
319 d_master->getTermList(d_candidates, terms); in doCheck()
321 Assert(!d_candidates.empty()); in doCheck()
339 for (const Node& cprog : d_candidates) in doCheck()
448 inst = d_base_inst.substitute(d_candidates.begin(), in doCheck()
449 d_candidates.end(), in doCheck()
[all …]
|
| H A D | synth_conjecture.h | 254 std::vector<Node> d_candidates; variable
309 Node getCandidate(unsigned int i) { return d_candidates[i]; } in getCandidate()
313 Assert(vs.size() == d_candidates.size()); in recordInstantiation()
316 d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]); in recordInstantiation()
|
| H A D | sygus_unif.h | 105 std::vector<Node> d_candidates; variable
|
| H A D | sygus_unif.cpp | 43 d_candidates.push_back(f); in initializeCandidate()
|
| H A D | sygus_unif_rl.cpp | 92 Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0]) in purifyLemma()
93 != d_candidates.end()); in purifyLemma()
296 for (const Node& c : d_candidates) in constructSolution()
|