Searched refs:sk_vars (Results 1 – 3 of 3) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | sygus_repair_const.cpp | 174 std::vector<Node> sk_vars; in repairSolution() local
203 if (sk_vars.empty()) in repairSolution()
231 sk_vars, in repairSolution()
273 for (const Node& v : sk_vars) in repairSolution()
299 sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end()); in repairSolution()
390 sk_vars.push_back(sk_var); in getSkeleton()
480 for (const Node& v : sk_vars) in getFoQuery()
513 if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end()) in getFoQuery()
588 std::find(sk_vars.begin(), sk_vars.end(), exc_var); in fitToLogic()
589 Assert(it != sk_vars.end()); in fitToLogic()
[all …]
|
| H A D | sygus_repair_const.h | 142 std::vector<Node>& sk_vars,
155 const std::vector<Node>& sk_vars);
178 std::vector<Node>& sk_vars,
|
| H A D | synth_conjecture.cpp | 639 std::vector<Node> sk_vars; in doRefine() local
663 sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end()); in doRefine()
685 Assert(sk_vars.size() == sk_subs.size()); in doRefine()
689 sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end()); in doRefine()
694 d_master->registerRefinementLemma(sk_vars, base_lem, lems); in doRefine()
|